Metamath Proof Explorer


Theorem sqcli

Description: Closure of square. (Contributed by NM, 2-Aug-1999)

Ref Expression
Hypothesis sqval.1 𝐴 ∈ ℂ
Assertion sqcli ( 𝐴 ↑ 2 ) ∈ ℂ

Proof

Step Hyp Ref Expression
1 sqval.1 𝐴 ∈ ℂ
2 sqcl ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 2 ) ∈ ℂ )
3 1 2 ax-mp ( 𝐴 ↑ 2 ) ∈ ℂ