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

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

Detailed syntax breakdown of Axiom ax-1rid
StepHypRef Expression
1 cA . . 3
2 cr 9281 . . 3
31, 2wcel 1756 . 2
4 c1 9283 . . . 4
5 cmul 9287 . . . 4
61, 4, 5co 6091 . . 3
76, 1wceq 1369 . 2
83, 7wi 4 1
Colors of variables: wff setvar class
This axiom is referenced by:  mulid1  9383  mulgt1  10188  ltmulgt11  10189  lemulge11  10191  addltmul  10560  xmulid1  11242  2submod  11760  cshw1  12456  bezoutlem1  13722  cshwshashnsame  14130  nmopub2tALT  25313  nmfnleub2  25330  unitdivcld  26331  zrhre  26445  sgnmulrp2  26926  frghash2spot  30656  usgreghash2spotv  30659  numclwwlk6  30706
  Copyright terms: Public domain W3C validator