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 | ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 = 0 ↔ - 𝐴 = 0 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | neg0 | ⊢ - 0 = 0 | |
2 | 1 | eqeq2i | ⊢ ( - 𝐴 = - 0 ↔ - 𝐴 = 0 ) |
3 | 0cn | ⊢ 0 ∈ ℂ | |
4 | neg11 | ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ∈ ℂ ) → ( - 𝐴 = - 0 ↔ 𝐴 = 0 ) ) | |
5 | 3 4 | mpan2 | ⊢ ( 𝐴 ∈ ℂ → ( - 𝐴 = - 0 ↔ 𝐴 = 0 ) ) |
6 | 2 5 | syl5rbbr | ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 = 0 ↔ - 𝐴 = 0 ) ) |