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

Metamath Proof Explorer

Theorem abssq

Description: Square can be moved in and out of absolute value. (Contributed by Scott Fenton, 18-Apr-2014) (Proof shortened by Mario Carneiro, 29-May-2016)

		Ref	Expression
	Assertion	abssq	$⊢ A \in ℂ \to {\|A\|}^{2} = \|A^{2}\|$

Proof

Step	Hyp	Ref	Expression
1		2nn0	$⊢ 2 \in ℕ_{0}$
2		absexp	$⊢ (A \in ℂ \land 2 \in ℕ_{0}) \to \|A^{2}\| = {\|A\|}^{2}$
3	1 2	mpan2	$⊢ A \in ℂ \to \|A^{2}\| = {\|A\|}^{2}$
4	3	eqcomd	$⊢ A \in ℂ \to {\|A\|}^{2} = \|A^{2}\|$