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 10211
Description: 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by theorem ax1rid 10187. Weakened from the original axiom in the form of statement in mulid1 10242, 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 10140 . . 3 class
31, 2wcel 2145 . 2 wff 𝐴 ∈ ℝ
4 c1 10142 . . . 4 class 1
5 cmul 10146 . . . 4 class ·
61, 4, 5co 6795 . . 3 class (𝐴 · 1)
76, 1wceq 1631 . 2 wff (𝐴 · 1) = 𝐴
83, 7wi 4 1 wff (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)
Colors of variables: wff setvar class
This axiom is referenced by:  mulid1  10242  mulgt1  11087  ltmulgt11  11088  lemulge11  11090  addltmul  11474  xmulid1  12313  2submod  12938  cshw1  13776  bezoutlem1  15463  cshwshashnsame  16016  numclwlk1lem1  27559  numclwwlk6  27588  nmopub2tALT  29107  nmfnleub2  29124  unitdivcld  30286  zrhre  30402  sgnmulrp2  30944  knoppcnlem4  32822  relexpmulnn  38527  relogbmulbexp  42880
  Copyright terms: Public domain W3C validator