Theorem sqdivi

Description: Distribution of square over division. (Contributed by NM, 20-Aug-2001)

	Ref	Expression
Hypotheses	sqval.1	|- A e. CC
	sqmul.2	|- B e. CC
	sqdiv.3	|- B =/= 0
Assertion	sqdivi	|- ( ( A / B ) ^ 2 ) = ( ( A ^ 2 ) / ( B ^ 2 ) )

Proof

Step	Hyp	Ref	Expression
1		sqval.1	|- A e. CC
2		sqmul.2	|- B e. CC
3		sqdiv.3	|- B =/= 0
4	1 2 1 2 3 3	divmuldivi	|- ( ( A / B ) x. ( A / B ) ) = ( ( A x. A ) / ( B x. B ) )
5	1 2 3	divcli	|- ( A / B ) e. CC
6	5	sqvali	|- ( ( A / B ) ^ 2 ) = ( ( A / B ) x. ( A / B ) )
7	1	sqvali	|- ( A ^ 2 ) = ( A x. A )
8	2	sqvali	|- ( B ^ 2 ) = ( B x. B )
9	7 8	oveq12i	|- ( ( A ^ 2 ) / ( B ^ 2 ) ) = ( ( A x. A ) / ( B x. B ) )
10	4 6 9	3eqtr4i	|- ( ( A / B ) ^ 2 ) = ( ( A ^ 2 ) / ( B ^ 2 ) )