Theorem sqcl

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

	Ref	Expression
Assertion	sqcl	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 2 ) ∈ ℂ )

Proof

Step	Hyp	Ref	Expression
1		sqval	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 ) )
2		mulcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 𝐴 · 𝐴 ) ∈ ℂ )
3	2	anidms	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · 𝐴 ) ∈ ℂ )
4	1 3	eqeltrd	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 2 ) ∈ ℂ )