Theorem sqrecii

Description: Square of reciprocal. (Contributed by NM, 17-Sep-1999)

	Ref	Expression
Hypotheses	sqval.1	⊢ 𝐴 ∈ ℂ
	sqreci.1	⊢ 𝐴 ≠ 0
Assertion	sqrecii	⊢ ( ( 1 / 𝐴 ) ↑ 2 ) = ( 1 / ( 𝐴 ↑ 2 ) )

Proof

Step	Hyp	Ref	Expression
1		sqval.1	⊢ 𝐴 ∈ ℂ
2		sqreci.1	⊢ 𝐴 ≠ 0
3		ax-1cn	⊢ 1 ∈ ℂ
4	3 1 3 1 2 2	divmuldivi	⊢ ( ( 1 / 𝐴 ) · ( 1 / 𝐴 ) ) = ( ( 1 · 1 ) / ( 𝐴 · 𝐴 ) )
5		1t1e1	⊢ ( 1 · 1 ) = 1
6	5	oveq1i	⊢ ( ( 1 · 1 ) / ( 𝐴 · 𝐴 ) ) = ( 1 / ( 𝐴 · 𝐴 ) )
7	4 6	eqtri	⊢ ( ( 1 / 𝐴 ) · ( 1 / 𝐴 ) ) = ( 1 / ( 𝐴 · 𝐴 ) )
8	1 2	reccli	⊢ ( 1 / 𝐴 ) ∈ ℂ
9	8	sqvali	⊢ ( ( 1 / 𝐴 ) ↑ 2 ) = ( ( 1 / 𝐴 ) · ( 1 / 𝐴 ) )
10	1	sqvali	⊢ ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 )
11	10	oveq2i	⊢ ( 1 / ( 𝐴 ↑ 2 ) ) = ( 1 / ( 𝐴 · 𝐴 ) )
12	7 9 11	3eqtr4i	⊢ ( ( 1 / 𝐴 ) ↑ 2 ) = ( 1 / ( 𝐴 ↑ 2 ) )