sqrecii

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

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

Metamath Proof Explorer