Theorem rehalfcl

Description: Real closure of half. (Contributed by NM, 1-Jan-2006)

	Ref	Expression
Assertion	rehalfcl	|- ( A e. RR -> ( A / 2 ) e. RR )

Proof

Step	Hyp	Ref	Expression
1		2re	|- 2 e. RR
2		2ne0	|- 2 =/= 0
3		redivcl	|- ( ( A e. RR /\ 2 e. RR /\ 2 =/= 0 ) -> ( A / 2 ) e. RR )
4	1 2 3	mp3an23	|- ( A e. RR -> ( A / 2 ) e. RR )