Metamath Proof Explorer

Theorem sqdiv

Description: Distribution of square over division. (Contributed by Scott Fenton, 7-Jun-2013) (Proof shortened by Mario Carneiro, 9-Jul-2013)

Ref Expression
Assertion sqdiv 
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( A / B ) ^ 2 ) = ( ( A ^ 2 ) / ( B ^ 2 ) ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> A e. CC )
2 3simpc 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( B e. CC /\ B =/= 0 ) )
3 divmuldiv 
 |-  ( ( ( A e. CC /\ A e. CC ) /\ ( ( B e. CC /\ B =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) ) -> ( ( A / B ) x. ( A / B ) ) = ( ( A x. A ) / ( B x. B ) ) )
4 1 1 2 2 3 syl22anc 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( A / B ) x. ( A / B ) ) = ( ( A x. A ) / ( B x. B ) ) )
5 divcl 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A / B ) e. CC )
6 sqval 
 |-  ( ( A / B ) e. CC -> ( ( A / B ) ^ 2 ) = ( ( A / B ) x. ( A / B ) ) )
7 5 6 syl 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( A / B ) ^ 2 ) = ( ( A / B ) x. ( A / B ) ) )
8 sqval 
 |-  ( A e. CC -> ( A ^ 2 ) = ( A x. A ) )
9 sqval 
 |-  ( B e. CC -> ( B ^ 2 ) = ( B x. B ) )
10 8 9 oveqan12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A ^ 2 ) / ( B ^ 2 ) ) = ( ( A x. A ) / ( B x. B ) ) )
11 10 3adant3 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( A ^ 2 ) / ( B ^ 2 ) ) = ( ( A x. A ) / ( B x. B ) ) )
12 4 7 11 3eqtr4d 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( A / B ) ^ 2 ) = ( ( A ^ 2 ) / ( B ^ 2 ) ) )