| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ax-1rid | Structured version Visualization version GIF version | ||
| Description: 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by Theorem ax1rid 11201. Weakened from the original axiom in the form of statement in mulrid 11259, based on ideas by Eric Schmidt. (Contributed by NM, 29-Jan-1995.) |
| Ref | Expression |
|---|---|
| ax-1rid | ⊢ (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cA | . . 3 class 𝐴 | |
| 2 | cr 11154 | . . 3 class ℝ | |
| 3 | 1, 2 | wcel 2108 | . 2 wff 𝐴 ∈ ℝ |
| 4 | c1 11156 | . . . 4 class 1 | |
| 5 | cmul 11160 | . . . 4 class · | |
| 6 | 1, 4, 5 | co 7431 | . . 3 class (𝐴 · 1) |
| 7 | 6, 1 | wceq 1540 | . 2 wff (𝐴 · 1) = 𝐴 |
| 8 | 3, 7 | wi 4 | 1 wff (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴) |
| Colors of variables: wff setvar class |
| This axiom is referenced by: mulrid 11259 mulgt1OLD 12126 ltmulgt11 12127 lemulge11 12130 nnmulcl 12290 addltmul 12502 xmulrid 13321 2submod 13973 cshw1 14860 bezoutlem1 16576 cshwshashnsame 17141 numclwlk1lem1 30388 numclwwlk6 30409 nmopub2tALT 31928 nmfnleub2 31945 1fldgenq 33324 unitdivcld 33900 zrhre 34020 sgnmulrp2 34546 knoppcnlem4 36497 1t1e1ALT 42296 remulcan2d 42298 sn-1ne2 42300 nnadddir 42305 nnmul1com 42306 sn-00idlem1 42428 sn-00idlem3 42430 remul02 42435 remul01 42437 rei4 42453 remulinvcom 42462 remullid 42463 sn-0tie0 42469 renegmulnnass 42483 mulgt0b2d 42490 sn-ltmulgt11d 42492 sn-0lt1 42493 3cubeslem1 42695 relexpmulnn 43722 relogbmulbexp 48482 line2xlem 48674 line2x 48675 |
| Copyright terms: Public domain | W3C validator |