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

Axiom ax-1rid 9583
Description: is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by theorem ax1rid 9559. Weakened from the original axiom in the form of statement in mulid1 9614, 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 9512 . . 3
31, 2wcel 1818 . 2
4 c1 9514 . . . 4
5 cmul 9518 . . . 4
61, 4, 5co 6296 . . 3
76, 1wceq 1395 . 2
83, 7wi 4 1
Colors of variables: wff setvar class
This axiom is referenced by:  mulid1  9614  mulgt1  10426  ltmulgt11  10427  lemulge11  10429  addltmul  10799  xmulid1  11500  2submod  12048  cshw1  12790  bezoutlem1  14176  cshwshashnsame  14588  frghash2spot  25063  usgreghash2spotv  25066  numclwwlk6  25113  nmopub2tALT  26828  nmfnleub2  26845  unitdivcld  27883  zrhre  27997  sgnmulrp2  28482
  Copyright terms: Public domain W3C validator