Database
REAL AND COMPLEX NUMBERS
Integer sets
Some properties of specific numbers
1pneg1e0
Next ⟩
0m0e0
Metamath Proof Explorer
Ascii
Unicode
Theorem
1pneg1e0
Description:
1 + -u 1
is 0.
(Contributed by
David A. Wheeler
, 8-Dec-2018)
Ref
Expression
Assertion
1pneg1e0
$${\u22a2}1+-1=0$$
Proof
Step
Hyp
Ref
Expression
1
ax-1cn
$${\u22a2}1\in \u2102$$
2
1
negidi
$${\u22a2}1+-1=0$$