Theorem sqdivzi

Description: Distribution of square over division. (Contributed by Scott Fenton, 7-Jun-2013)

	Ref	Expression
Hypotheses	sqdivzi.1	$$⊢A\in ℂ$$
	sqdivzi.2	$$⊢B\in ℂ$$
Assertion	sqdivzi	$$⊢B\ne 0\to {\left(\frac{A}{B}\right)}^2=\frac{A^2}{B^2}$$

Proof

Step	Hyp	Ref	Expression
1		sqdivzi.1	$$⊢A\in ℂ$$
2		sqdivzi.2	$$⊢B\in ℂ$$
3		oveq2	$$⊢B=if\left(B\ne 0,B,1\right)\to \frac{A}{B}=\frac{A}{if\left(B\ne 0,B,1\right)}$$
4	3	oveq1d	$$⊢B=if\left(B\ne 0,B,1\right)\to {\left(\frac{A}{B}\right)}^2={\left(\frac{A}{if\left(B\ne 0,B,1\right)}\right)}^2$$
5		oveq1	$$⊢B=if\left(B\ne 0,B,1\right)\to B^2={if\left(B\ne 0,B,1\right)}^2$$
6	5	oveq2d	$$⊢B=if\left(B\ne 0,B,1\right)\to \frac{A^2}{B^2}=\frac{A^2}{{if\left(B\ne 0,B,1\right)}^2}$$
7	4 6	eqeq12d	$$⊢B=if\left(B\ne 0,B,1\right)\to \left({\left(\frac{A}{B}\right)}^2=\frac{A^2}{B^2}\leftrightarrow {\left(\frac{A}{if\left(B\ne 0,B,1\right)}\right)}^2=\frac{A^2}{{if\left(B\ne 0,B,1\right)}^2}\right)$$
8		ax-1cn	$$⊢1\in ℂ$$
9	2 8	ifcli	$$⊢if\left(B\ne 0,B,1\right)\in ℂ$$
10		elimne0	$$⊢if\left(B\ne 0,B,1\right)\ne 0$$
11	1 9 10	sqdivi	$$⊢{\left(\frac{A}{if\left(B\ne 0,B,1\right)}\right)}^2=\frac{A^2}{{if\left(B\ne 0,B,1\right)}^2}$$
12	7 11	dedth	$$⊢B\ne 0\to {\left(\frac{A}{B}\right)}^2=\frac{A^2}{B^2}$$