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

Axiom ax-1rid 9174
Description: is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by theorem ax1rid 9150. Weakened from the original axiom in the form of statement in mulid1 9205, 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 9103 . . 3
31, 2wcel 1724 . 2
4 c1 9105 . . . 4
5 cmul 9109 . . . 4
61, 4, 5co 6067 . . 3
76, 1wceq 1662 . 2
83, 7wi 4 1
Colors of variables: wff set class
This axiom is referenced by:  mulid1  9205  mulgt1  10000  ltmulgt11  10001  lemulge11  10003  addltmul  10369  xmulid1  11049  2submod  11552  cshw1  12242  bezoutlem1  13508  cshwshashnsame  13916  nmopub2tALT  23923  nmfnleub2  23940  unitdivcld  25001  zrhre  25116  sgnmulrp2  25567  frghash2spot  29515  usgreghash2spotv  29518  numclwwlk6  29565  frgraregord013  29570
  Copyright terms: Public domain W3C validator