Theorem sqdivi

Description: Distribution of square over division. (Contributed by NM, 20-Aug-2001)

	Ref	Expression
Hypotheses	sqval.1	$$⊢A\in ℂ$$
	sqmul.2	$$⊢B\in ℂ$$
	sqdiv.3	$$⊢B\ne 0$$
Assertion	sqdivi	$$⊢{\left(\frac{A}{B}\right)}^2=\frac{A^2}{B^2}$$

Proof

Step	Hyp	Ref	Expression
1		sqval.1	$$⊢A\in ℂ$$
2		sqmul.2	$$⊢B\in ℂ$$
3		sqdiv.3	$$⊢B\ne 0$$
4	1 2 1 2 3 3	divmuldivi	$$⊢\left(\frac{A}{B}\right)\left(\frac{A}{B}\right)=\frac{AA}{BB}$$
5	1 2 3	divcli	$$⊢\frac{A}{B}\in ℂ$$
6	5	sqvali	$$⊢{\left(\frac{A}{B}\right)}^2=\left(\frac{A}{B}\right)\left(\frac{A}{B}\right)$$
7	1	sqvali	$$⊢A^2=AA$$
8	2	sqvali	$$⊢B^2=BB$$
9	7 8	oveq12i	$$⊢\frac{A^2}{B^2}=\frac{AA}{BB}$$
10	4 6 9	3eqtr4i	$$⊢{\left(\frac{A}{B}\right)}^2=\frac{A^2}{B^2}$$