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 ( 𝐴 ∈ ℂ → ( 𝐴 = - 𝐴 ↔ 𝐴 = 0 ) )

Proof

Step Hyp Ref Expression
1 1p1times ⊢ ( 𝐴 ∈ ℂ → ( ( 1 + 1 ) · 𝐴 ) = ( 𝐴 + 𝐴 ) )
2 ax-1cn ⊢ 1 ∈ ℂ
3 2 2 addcli ⊢ ( 1 + 1 ) ∈ ℂ
4 3 mul01i ⊢ ( ( 1 + 1 ) · 0 ) = 0
5 negid ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 + - 𝐴 ) = 0 )
6 4 5 eqtr4id ⊢ ( 𝐴 ∈ ℂ → ( ( 1 + 1 ) · 0 ) = ( 𝐴 + - 𝐴 ) )
7 1 6 eqeq12d ⊢ ( 𝐴 ∈ ℂ → ( ( ( 1 + 1 ) · 𝐴 ) = ( ( 1 + 1 ) · 0 ) ↔ ( 𝐴 + 𝐴 ) = ( 𝐴 + - 𝐴 ) ) )
8 id ⊢ ( 𝐴 ∈ ℂ → 𝐴 ∈ ℂ )
9 0cnd ⊢ ( 𝐴 ∈ ℂ → 0 ∈ ℂ )
10 3 a1i ⊢ ( 𝐴 ∈ ℂ → ( 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 ⊢ ( 𝐴 ∈ ℂ → ( 1 + 1 ) ≠ 0 )
17 8 9 10 16 mulcand ⊢ ( 𝐴 ∈ ℂ → ( ( ( 1 + 1 ) · 𝐴 ) = ( ( 1 + 1 ) · 0 ) ↔ 𝐴 = 0 ) )
18 negcl ⊢ ( 𝐴 ∈ ℂ → - 𝐴 ∈ ℂ )
19 8 8 18 addcand ⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 + 𝐴 ) = ( 𝐴 + - 𝐴 ) ↔ 𝐴 = - 𝐴 ) )
20 7 17 19 3bitr3rd ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 = - 𝐴 ↔ 𝐴 = 0 ) )