This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Description: Alternate proof of 1t1e1 using a different set of axioms (add
ax-mulrcl , ax-i2m1 , ax-1ne0 , ax-rrecex and remove ax-resscn ,
ax-mulcom , ax-mulass , ax-distr ). (Contributed by Steven Nguyen, 20-Sep-2022) (Proof modification is discouraged.)
(New usage is discouraged.)
|
|
Ref |
Expression |
|
Assertion |
1t1e1ALT |
⊢ ( 1 · 1 ) = 1 |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
1re |
⊢ 1 ∈ ℝ |
| 2 |
|
ax-1rid |
⊢ ( 1 ∈ ℝ → ( 1 · 1 ) = 1 ) |
| 3 |
1 2
|
ax-mp |
⊢ ( 1 · 1 ) = 1 |