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 
|- ( A e. CC -> ( ( A / 2 ) = 0 <-> A = 0 ) )

Proof

Step Hyp Ref Expression
1 2cn 
 |-  2 e. CC
2 2ne0 
 |-  2 =/= 0
3 diveq0 
 |-  ( ( A e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( ( A / 2 ) = 0 <-> A = 0 ) )
4 1 2 3 mp3an23 
 |-  ( A e. CC -> ( ( A / 2 ) = 0 <-> A = 0 ) )