Metamath Proof Explorer


Theorem half0

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

Proof

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