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 ) )