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

Axiom ax-1rid 9231
Description: is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by theorem ax1rid 9207. Weakened from the original axiom in the form of statement in mulid1 9262, 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 9160 . . 3
31, 2wcel 1732 . 2
4 c1 9162 . . . 4
5 cmul 9166 . . . 4
61, 4, 5co 6103 . . 3
76, 1wceq 1670 . 2
83, 7wi 4 1
Colors of variables: wff set class
This axiom is referenced by:  mulid1  9262  mulgt1  10057  ltmulgt11  10058  lemulge11  10060  addltmul  10426  xmulid1  11106  2submod  11609  cshw1  12303  bezoutlem1  13569  cshwshashnsame  13977  nmopub2tALT  24435  nmfnleub2  24452  unitdivcld  25510  zrhre  25625  sgnmulrp2  26076  frghash2spot  29837  usgreghash2spotv  29840  numclwwlk6  29887  frgraregord013  29892
  Copyright terms: Public domain W3C validator