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 ) )