Database
REAL AND COMPLEX NUMBERS
Integer sets
Some properties of specific numbers
1m0e1
Next ⟩
0p1e1
Metamath Proof Explorer
Ascii
Unicode
Theorem
1m0e1
Description:
1 - 0 = 1.
(Contributed by
David A. Wheeler
, 8-Dec-2018)
Ref
Expression
Assertion
1m0e1
⊢
1
−
0
=
1
Proof
Step
Hyp
Ref
Expression
1
ax-1cn
⊢
1
∈
ℂ
2
1
subid1i
⊢
1
−
0
=
1