Database
REAL AND COMPLEX NUMBERS
Integer sets
Some properties of specific numbers
1e2m1
Next ⟩
3m1e2
Metamath Proof Explorer
Ascii
Unicode
Theorem
1e2m1
Description:
1 = 2 - 1.
(Contributed by
David A. Wheeler
, 8-Dec-2018)
Ref
Expression
Assertion
1e2m1
⊢
1
=
2
−
1
Proof
Step
Hyp
Ref
Expression
1
2m1e1
⊢
2
−
1
=
1
2
1
eqcomi
⊢
1
=
2
−
1