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 
|- A e. CC
sqreci.1 
|- A =/= 0
Assertion sqrecii 
|- ( ( 1 / A ) ^ 2 ) = ( 1 / ( A ^ 2 ) )

Proof

Step Hyp Ref Expression
1 sqval.1 
 |-  A e. CC
2 sqreci.1 
 |-  A =/= 0
3 ax-1cn 
 |-  1 e. CC
4 3 1 3 1 2 2 divmuldivi 
 |-  ( ( 1 / A ) x. ( 1 / A ) ) = ( ( 1 x. 1 ) / ( A x. A ) )
5 1t1e1 
 |-  ( 1 x. 1 ) = 1
6 5 oveq1i 
 |-  ( ( 1 x. 1 ) / ( A x. A ) ) = ( 1 / ( A x. A ) )
7 4 6 eqtri 
 |-  ( ( 1 / A ) x. ( 1 / A ) ) = ( 1 / ( A x. A ) )
8 1 2 reccli 
 |-  ( 1 / A ) e. CC
9 8 sqvali 
 |-  ( ( 1 / A ) ^ 2 ) = ( ( 1 / A ) x. ( 1 / A ) )
10 1 sqvali 
 |-  ( A ^ 2 ) = ( A x. A )
11 10 oveq2i 
 |-  ( 1 / ( A ^ 2 ) ) = ( 1 / ( A x. A ) )
12 7 9 11 3eqtr4i 
 |-  ( ( 1 / A ) ^ 2 ) = ( 1 / ( A ^ 2 ) )