Theorem resqcl

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

	Ref	Expression
Assertion	resqcl	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 ↑ 2 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		2nn0	⊢ 2 ∈ ℕ0
2		reexpcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ∈ ℕ0 ) → ( 𝐴 ↑ 2 ) ∈ ℝ )
3	1 2	mpan2	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 ↑ 2 ) ∈ ℝ )