Theorem sqrecii

Description: The square of a reciprocal is the reciprocal of the square. (Contributed by NM, 17-Sep-1999)

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

Proof

Step	Hyp	Ref	Expression
1		sqval.1	$$⊢A\in ℂ$$
2		sqreci.1	$$⊢A\ne 0$$
3		ax-1cn	$$⊢1\in ℂ$$
4	3 1 3 1 2 2	divmuldivi	$$⊢\left(\frac{1}{A}\right)\left(\frac{1}{A}\right)=\frac{1\cdot 1}{AA}$$
5		1t1e1	$$⊢1\cdot 1=1$$
6	5	oveq1i	$$⊢\frac{1\cdot 1}{AA}=\frac{1}{AA}$$
7	4 6	eqtri	$$⊢\left(\frac{1}{A}\right)\left(\frac{1}{A}\right)=\frac{1}{AA}$$
8	1 2	reccli	$$⊢\frac{1}{A}\in ℂ$$
9	8	sqvali	$$⊢{\left(\frac{1}{A}\right)}^2=\left(\frac{1}{A}\right)\left(\frac{1}{A}\right)$$
10	1	sqvali	$$⊢A^2=AA$$
11	10	oveq2i	$$⊢\frac{1}{A^2}=\frac{1}{AA}$$
12	7 9 11	3eqtr4i	$$⊢{\left(\frac{1}{A}\right)}^2=\frac{1}{A^2}$$