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 10610
Description: 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by theorem ax1rid 10586. Weakened from the original axiom in the form of statement in mulid1 10642, 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 10539 . . 3 class
31, 2wcel 2113 . 2 wff 𝐴 ∈ ℝ
4 c1 10541 . . . 4 class 1
5 cmul 10545 . . . 4 class ·
61, 4, 5co 7159 . . 3 class (𝐴 · 1)
76, 1wceq 1536 . 2 wff (𝐴 · 1) = 𝐴
83, 7wi 4 1 wff (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)
Colors of variables: wff setvar class
This axiom is referenced by:  mulid1  10642  mulgt1  11502  ltmulgt11  11503  lemulge11  11505  nnmulcl  11664  addltmul  11876  xmulid1  12675  2submod  13303  cshw1  14187  bezoutlem1  15890  cshwshashnsame  16440  numclwlk1lem1  28151  numclwwlk6  28172  nmopub2tALT  29689  nmfnleub2  29706  unitdivcld  31148  zrhre  31264  sgnmulrp2  31805  knoppcnlem4  33839  1t1e1ALT  39161  remulcan2d  39162  sn-1ne2  39164  nnadddir  39169  nnmul1com  39170  sn-00idlem1  39234  sn-00idlem3  39236  remul02  39241  remul01  39243  sn-0lt1  39252  remulinvcom  39254  remulid2  39255  3cubeslem1  39287  relexpmulnn  40060  relogbmulbexp  44628  line2xlem  44747  line2x  44748
  Copyright terms: Public domain W3C validator