This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ 𝐴 ∈ ℂ
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 ) )