MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-1rid Structured version   Visualization version   GIF version

Axiom ax-1rid 10169
Description: 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by theorem ax1rid 10145. Weakened from the original axiom in the form of statement in mulid1 10200, based on ideas by Eric Schmidt. (Contributed by NM, 29-Jan-1995.)
Assertion
Ref Expression
ax-1rid (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)

Detailed syntax breakdown of Axiom ax-1rid
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cr 10098 . . 3 class
31, 2wcel 2127 . 2 wff 𝐴 ∈ ℝ
4 c1 10100 . . . 4 class 1
5 cmul 10104 . . . 4 class ·
61, 4, 5co 6801 . . 3 class (𝐴 · 1)
76, 1wceq 1620 . 2 wff (𝐴 · 1) = 𝐴
83, 7wi 4 1 wff (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)
Colors of variables: wff setvar class
This axiom is referenced by:  mulid1  10200  mulgt1  11045  ltmulgt11  11046  lemulge11  11048  addltmul  11431  xmulid1  12273  2submod  12896  cshw1  13739  bezoutlem1  15429  cshwshashnsame  15983  numclwlk1lem1  27501  numclwwlk6  27529  nmopub2tALT  29048  nmfnleub2  29065  unitdivcld  30227  zrhre  30343  sgnmulrp2  30885  knoppcnlem4  32763  relexpmulnn  38472  relogbmulbexp  42834
  Copyright terms: Public domain W3C validator