Description: Half of a number is zero iff the number is zero. (Contributed by NM, 20-Apr-2006)
Ref | Expression | ||
---|---|---|---|
Assertion | half0 | ⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 / 2 ) = 0 ↔ 𝐴 = 0 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2cn | ⊢ 2 ∈ ℂ | |
2 | 2ne0 | ⊢ 2 ≠ 0 | |
3 | diveq0 | ⊢ ( ( 𝐴 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( ( 𝐴 / 2 ) = 0 ↔ 𝐴 = 0 ) ) | |
4 | 1 2 3 | mp3an23 | ⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 / 2 ) = 0 ↔ 𝐴 = 0 ) ) |