This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem negneg

Description: A number is equal to the negative of its negative. Theorem I.4 of Apostol p. 18. (Contributed by NM, 12-Jan-2002) (Revised by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion negneg ⊢ A ∈ ℂ → − − A = A

Proof

Step Hyp Ref Expression
1 df-neg ⊢ − − A = 0 − − A
2 0cn ⊢ 0 ∈ ℂ
3 subneg ⊢ 0 ∈ ℂ ∧ A ∈ ℂ → 0 − − A = 0 + A
4 2 3 mpan ⊢ A ∈ ℂ → 0 − − A = 0 + A
5 1 4 eqtrid ⊢ A ∈ ℂ → − − A = 0 + A
6 addlid ⊢ A ∈ ℂ → 0 + A = A
7 5 6 eqtrd ⊢ A ∈ ℂ → − − A = A