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 10572. Weakened from the original axiom in the form of statement in mulid1 10628, 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 10525 | . . 3 class ℝ | |
3 | 1, 2 | wcel 2105 | . 2 wff 𝐴 ∈ ℝ |
4 | c1 10527 | . . . 4 class 1 | |
5 | cmul 10531 | . . . 4 class · | |
6 | 1, 4, 5 | co 7145 | . . 3 class (𝐴 · 1) |
7 | 6, 1 | wceq 1528 | . 2 wff (𝐴 · 1) = 𝐴 |
8 | 3, 7 | wi 4 | 1 wff (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴) |
Colors of variables: wff setvar class |
This axiom is referenced by: mulid1 10628 mulgt1 11488 ltmulgt11 11489 lemulge11 11491 nnmulcl 11650 addltmul 11862 xmulid1 12662 2submod 13290 cshw1 14174 bezoutlem1 15877 cshwshashnsame 16427 numclwlk1lem1 28076 numclwwlk6 28097 nmopub2tALT 29614 nmfnleub2 29631 unitdivcld 31044 zrhre 31160 sgnmulrp2 31701 knoppcnlem4 33733 1t1e1ALT 39035 remulcan2d 39036 sn-1ne2 39038 nnadddir 39043 nnmul1com 39044 sn-00idlem1 39108 sn-00idlem3 39110 remul02 39115 remul01 39117 sn-0lt1 39126 remulinvcom 39128 remulid2 39129 3cubeslem1 39161 relexpmulnn 39934 relogbmulbexp 44519 line2xlem 44638 line2x 44639 |
Copyright terms: Public domain | W3C validator |