![]() |
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 10145. Weakened from the original axiom in the form of statement in mulid1 10200, 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 10098 | . . 3 class ℝ | |
3 | 1, 2 | wcel 2127 | . 2 wff 𝐴 ∈ ℝ |
4 | c1 10100 | . . . 4 class 1 | |
5 | cmul 10104 | . . . 4 class · | |
6 | 1, 4, 5 | co 6801 | . . 3 class (𝐴 · 1) |
7 | 6, 1 | wceq 1620 | . 2 wff (𝐴 · 1) = 𝐴 |
8 | 3, 7 | wi 4 | 1 wff (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴) |
Colors of variables: wff setvar class |
This axiom is referenced by: mulid1 10200 mulgt1 11045 ltmulgt11 11046 lemulge11 11048 addltmul 11431 xmulid1 12273 2submod 12896 cshw1 13739 bezoutlem1 15429 cshwshashnsame 15983 numclwlk1lem1 27501 numclwwlk6 27529 nmopub2tALT 29048 nmfnleub2 29065 unitdivcld 30227 zrhre 30343 sgnmulrp2 30885 knoppcnlem4 32763 relexpmulnn 38472 relogbmulbexp 42834 |
Copyright terms: Public domain | W3C validator |