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 {\left|A\right|}^2=\left|A^2\right|$$

Proof

Step	Hyp	Ref	Expression
1		2nn0	$$⊢2\in {\mathbb{N}}_0$$
2		absexp	$$⊢\left(A\in ℂ\wedge 2\in {\mathbb{N}}_0\right)\to \left|A^2\right|={\left|A\right|}^2$$
3	1 2	mpan2	$$⊢A\in ℂ\to \left|A^2\right|={\left|A\right|}^2$$
4	3	eqcomd	$$⊢A\in ℂ\to {\left|A\right|}^2=\left|A^2\right|$$