Theorem sqmul

Description: Distribution of squaring over multiplication. (Contributed by NM, 21-Mar-2008)

	Ref	Expression
Assertion	sqmul	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to {AB}^2=A^2{B}^2$$

Proof

Step	Hyp	Ref	Expression
1		2nn0	$$⊢2\in {\mathbb{N}}_0$$
2		mulexp	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge 2\in {\mathbb{N}}_0\right)\to {AB}^2=A^2{B}^2$$
3	1 2	mp3an3	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to {AB}^2=A^2{B}^2$$