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

Metamath Proof Explorer

Theorem negeq0

Description: A number is zero iff its negative is zero. (Contributed by NM, 12-Jul-2005) (Revised by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion negeq0 ⊢ A ∈ ℂ → A = 0 ↔ − A = 0

Proof

Step Hyp Ref Expression
1 0cn ⊢ 0 ∈ ℂ
2 neg11 ⊢ A ∈ ℂ ∧ 0 ∈ ℂ → − A = − 0 ↔ A = 0
3 1 2 mpan2 ⊢ A ∈ ℂ → − A = − 0 ↔ A = 0
4 neg0 ⊢ − 0 = 0
5 4 eqeq2i ⊢ − A = − 0 ↔ − A = 0
6 3 5 bitr3di ⊢ A ∈ ℂ → A = 0 ↔ − A = 0