Theorem sqdiv

Description: Distribution of square over division. (Contributed by Scott Fenton, 7-Jun-2013) (Proof shortened by Mario Carneiro, 9-Jul-2013)

	Ref	Expression
Assertion	sqdiv	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\to {\left(\frac{A}{B}\right)}^2=\frac{A^2}{B^2}$$

Proof

Step	Hyp	Ref	Expression
1		simp1	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\to A\in ℂ$$
2		3simpc	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\to \left(B\in ℂ\wedge B\ne 0\right)$$
3		divmuldiv	$$⊢\left(\left(A\in ℂ\wedge A\in ℂ\right)\wedge \left(\left(B\in ℂ\wedge B\ne 0\right)\wedge \left(B\in ℂ\wedge B\ne 0\right)\right)\right)\to \left(\frac{A}{B}\right)\left(\frac{A}{B}\right)=\frac{AA}{BB}$$
4	1 1 2 2 3	syl22anc	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\to \left(\frac{A}{B}\right)\left(\frac{A}{B}\right)=\frac{AA}{BB}$$
5		divcl	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\to \frac{A}{B}\in ℂ$$
6		sqval	$$⊢\frac{A}{B}\in ℂ\to {\left(\frac{A}{B}\right)}^2=\left(\frac{A}{B}\right)\left(\frac{A}{B}\right)$$
7	5 6	syl	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\to {\left(\frac{A}{B}\right)}^2=\left(\frac{A}{B}\right)\left(\frac{A}{B}\right)$$
8		sqval	$$⊢A\in ℂ\to A^2=AA$$
9		sqval	$$⊢B\in ℂ\to B^2=BB$$
10	8 9	oveqan12d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \frac{A^2}{B^2}=\frac{AA}{BB}$$
11	10	3adant3	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\to \frac{A^2}{B^2}=\frac{AA}{BB}$$
12	4 7 11	3eqtr4d	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\to {\left(\frac{A}{B}\right)}^2=\frac{A^2}{B^2}$$