Metamath Proof Explorer

Theorem sqdivzi

Description: Distribution of square over division. (Contributed by Scott Fenton, 7-Jun-2013)

Ref Expression
Hypotheses sqdivzi.1 
|- A e. CC
sqdivzi.2 
|- B e. CC
Assertion sqdivzi 
|- ( B =/= 0 -> ( ( A / B ) ^ 2 ) = ( ( A ^ 2 ) / ( B ^ 2 ) ) )

Proof

Step Hyp Ref Expression
1 sqdivzi.1 
 |-  A e. CC
2 sqdivzi.2 
 |-  B e. CC
3 oveq2 
 |-  ( B = if ( B =/= 0 , B , 1 ) -> ( A / B ) = ( A / if ( B =/= 0 , B , 1 ) ) )
4 3 oveq1d 
 |-  ( B = if ( B =/= 0 , B , 1 ) -> ( ( A / B ) ^ 2 ) = ( ( A / if ( B =/= 0 , B , 1 ) ) ^ 2 ) )
5 oveq1 
 |-  ( B = if ( B =/= 0 , B , 1 ) -> ( B ^ 2 ) = ( if ( B =/= 0 , B , 1 ) ^ 2 ) )
6 5 oveq2d 
 |-  ( B = if ( B =/= 0 , B , 1 ) -> ( ( A ^ 2 ) / ( B ^ 2 ) ) = ( ( A ^ 2 ) / ( if ( B =/= 0 , B , 1 ) ^ 2 ) ) )
7 4 6 eqeq12d 
 |-  ( B = if ( B =/= 0 , B , 1 ) -> ( ( ( A / B ) ^ 2 ) = ( ( A ^ 2 ) / ( B ^ 2 ) ) <-> ( ( A / if ( B =/= 0 , B , 1 ) ) ^ 2 ) = ( ( A ^ 2 ) / ( if ( B =/= 0 , B , 1 ) ^ 2 ) ) ) )
8 ax-1cn 
 |-  1 e. CC
9 2 8 ifcli 
 |-  if ( B =/= 0 , B , 1 ) e. CC
10 elimne0 
 |-  if ( B =/= 0 , B , 1 ) =/= 0
11 1 9 10 sqdivi 
 |-  ( ( A / if ( B =/= 0 , B , 1 ) ) ^ 2 ) = ( ( A ^ 2 ) / ( if ( B =/= 0 , B , 1 ) ^ 2 ) )
12 7 11 dedth 
 |-  ( B =/= 0 -> ( ( A / B ) ^ 2 ) = ( ( A ^ 2 ) / ( B ^ 2 ) ) )