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

Metamath Proof Explorer

Theorem eqneg

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

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

Proof

Step Hyp Ref Expression
1 1p1times ⊢ A ∈ ℂ → 1 + 1 ⁢ A = A + A
2 ax-1cn ⊢ 1 ∈ ℂ
3 2 2 addcli ⊢ 1 + 1 ∈ ℂ
4 3 mul01i ⊢ 1 + 1 ⋅ 0 = 0
5 negid ⊢ A ∈ ℂ → A + − A = 0
6 4 5 eqtr4id ⊢ A ∈ ℂ → 1 + 1 ⋅ 0 = A + − A
7 1 6 eqeq12d ⊢ A ∈ ℂ → 1 + 1 ⁢ A = 1 + 1 ⋅ 0 ↔ A + A = A + − A
8 id ⊢ A ∈ ℂ → A ∈ ℂ
9 0cnd ⊢ A ∈ ℂ → 0 ∈ ℂ
10 3 a1i ⊢ A ∈ ℂ → 1 + 1 ∈ ℂ
11 1re ⊢ 1 ∈ ℝ
12 11 11 readdcli ⊢ 1 + 1 ∈ ℝ
13 0lt1 ⊢ 0 < 1
14 11 11 13 13 addgt0ii ⊢ 0 < 1 + 1
15 12 14 gt0ne0ii ⊢ 1 + 1 ≠ 0
16 15 a1i ⊢ A ∈ ℂ → 1 + 1 ≠ 0
17 8 9 10 16 mulcand ⊢ A ∈ ℂ → 1 + 1 ⁢ A = 1 + 1 ⋅ 0 ↔ A = 0
18 negcl ⊢ A ∈ ℂ → − A ∈ ℂ
19 8 8 18 addcand ⊢ A ∈ ℂ → A + A = A + − A ↔ A = − A
20 7 17 19 3bitr3rd ⊢ A ∈ ℂ → A = − A ↔ A = 0