This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ∈ ℝ )