Metamath Proof Explorer


Theorem sqcli

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

Ref Expression
Hypothesis sqval.1 ⊢ A ∈ ℂ
Assertion sqcli ⊢ A 2 ∈ ℂ

Proof

Step Hyp Ref Expression
1 sqval.1 ⊢ A ∈ ℂ
2 sqcl ⊢ A ∈ ℂ → A 2 ∈ ℂ
3 1 2 ax-mp ⊢ A 2 ∈ ℂ