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

Axiom ax-1rid 9111
Description: is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by theorem ax1rid 9087. Weakened from the original axiom in the form of statement in mulid1 9139, 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 9040 . . 3
31, 2wcel 1728 . 2
4 c1 9042 . . . 4
5 cmul 9046 . . . 4
61, 4, 5co 6129 . . 3
76, 1wceq 1654 . 2
83, 7wi 4 1
Colors of variables: wff set class
This axiom is referenced by:  mulid1  9139  mulgt1  9920  ltmulgt11  9921  lemulge11  9923  addltmul  10254  xmulid1  10909  sqrlem7  12105  bezoutlem1  13089  nmopub2tALT  23463  nmfnleub2  23480  unitdivcld  24348  zrhre  24434  2submod  28339  cshw1  28473  cshwssizensame  28487  frghash2spot  28690  usgreghash2spotv  28693
  Copyright terms: Public domain W3C validator