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 10596
Description: 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by theorem ax1rid 10572. Weakened from the original axiom in the form of statement in mulid1 10628, 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 10525 . . 3 class
31, 2wcel 2105 . 2 wff 𝐴 ∈ ℝ
4 c1 10527 . . . 4 class 1
5 cmul 10531 . . . 4 class ·
61, 4, 5co 7145 . . 3 class (𝐴 · 1)
76, 1wceq 1528 . 2 wff (𝐴 · 1) = 𝐴
83, 7wi 4 1 wff (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)
Colors of variables: wff setvar class
This axiom is referenced by:  mulid1  10628  mulgt1  11488  ltmulgt11  11489  lemulge11  11491  nnmulcl  11650  addltmul  11862  xmulid1  12662  2submod  13290  cshw1  14174  bezoutlem1  15877  cshwshashnsame  16427  numclwlk1lem1  28076  numclwwlk6  28097  nmopub2tALT  29614  nmfnleub2  29631  unitdivcld  31044  zrhre  31160  sgnmulrp2  31701  knoppcnlem4  33733  1t1e1ALT  39035  remulcan2d  39036  sn-1ne2  39038  nnadddir  39043  nnmul1com  39044  sn-00idlem1  39108  sn-00idlem3  39110  remul02  39115  remul01  39117  sn-0lt1  39126  remulinvcom  39128  remulid2  39129  3cubeslem1  39161  relexpmulnn  39934  relogbmulbexp  44519  line2xlem  44638  line2x  44639
  Copyright terms: Public domain W3C validator