Theorem halfcl

Description: Closure of half of a number. (Contributed by NM, 1-Jan-2006)

	Ref	Expression
Assertion	halfcl	|- ( A e. CC -> ( A / 2 ) e. CC )

Proof

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