Database
REAL AND COMPLEX NUMBERS
Integer sets
Some properties of specific numbers
negneg1e1
Next ⟩
1pneg1e0
Metamath Proof Explorer
Ascii
Structured
Theorem
negneg1e1
Description:
-u -u 1
is 1.
(Contributed by
David A. Wheeler
, 8-Dec-2018)
Ref
Expression
Assertion
negneg1e1
⊢
- - 1 = 1
Proof
Step
Hyp
Ref
Expression
1
ax-1cn
⊢
1 ∈ ℂ
2
1
negnegi
⊢
- - 1 = 1