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

Metamath Proof Explorer

Theorem sqcl

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

		Ref	Expression
	Assertion	sqcl	$⊢ A \in ℂ \to A^{2} \in ℂ$

Step	Hyp	Ref	Expression
1		sqval	$⊢ A \in ℂ \to A^{2} = A A$
2		mulcl	$⊢ (A \in ℂ \land A \in ℂ) \to A A \in ℂ$
3	2	anidms	$⊢ A \in ℂ \to A A \in ℂ$
4	1 3	eqeltrd	$⊢ A \in ℂ \to A^{2} \in ℂ$