Theorem resqcl

Description: Closure of squaring in reals. (Contributed by NM, 18-Oct-1999)

	Ref	Expression
Assertion	resqcl	|- ( A e. RR -> ( A ^ 2 ) e. RR )

Proof

Step	Hyp	Ref	Expression
1		2nn0	|- 2 e. NN0
2		reexpcl	|- ( ( A e. RR /\ 2 e. NN0 ) -> ( A ^ 2 ) e. RR )
3	1 2	mpan2	|- ( A e. RR -> ( A ^ 2 ) e. RR )