Metamath Proof Explorer

Theorem abs2sqlt

Description: The absolute values of two numbers compare as their squares. (Contributed by Paul Chapman, 7-Sep-2007)

Ref Expression
Assertion abs2sqlt 
|- ( ( A e. CC /\ B e. CC ) -> ( ( abs ` A ) < ( abs ` B ) <-> ( ( abs ` A ) ^ 2 ) < ( ( abs ` B ) ^ 2 ) ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( A = if ( A e. CC , A , 0 ) -> ( abs ` A ) = ( abs ` if ( A e. CC , A , 0 ) ) )
2 1 breq1d 
 |-  ( A = if ( A e. CC , A , 0 ) -> ( ( abs ` A ) < ( abs ` B ) <-> ( abs ` if ( A e. CC , A , 0 ) ) < ( abs ` B ) ) )
3 1 oveq1d 
 |-  ( A = if ( A e. CC , A , 0 ) -> ( ( abs ` A ) ^ 2 ) = ( ( abs ` if ( A e. CC , A , 0 ) ) ^ 2 ) )
4 3 breq1d 
 |-  ( A = if ( A e. CC , A , 0 ) -> ( ( ( abs ` A ) ^ 2 ) < ( ( abs ` B ) ^ 2 ) <-> ( ( abs ` if ( A e. CC , A , 0 ) ) ^ 2 ) < ( ( abs ` B ) ^ 2 ) ) )
5 2 4 bibi12d 
 |-  ( A = if ( A e. CC , A , 0 ) -> ( ( ( abs ` A ) < ( abs ` B ) <-> ( ( abs ` A ) ^ 2 ) < ( ( abs ` B ) ^ 2 ) ) <-> ( ( abs ` if ( A e. CC , A , 0 ) ) < ( abs ` B ) <-> ( ( abs ` if ( A e. CC , A , 0 ) ) ^ 2 ) < ( ( abs ` B ) ^ 2 ) ) ) )
6 fveq2 
 |-  ( B = if ( B e. CC , B , 0 ) -> ( abs ` B ) = ( abs ` if ( B e. CC , B , 0 ) ) )
7 6 breq2d 
 |-  ( B = if ( B e. CC , B , 0 ) -> ( ( abs ` if ( A e. CC , A , 0 ) ) < ( abs ` B ) <-> ( abs ` if ( A e. CC , A , 0 ) ) < ( abs ` if ( B e. CC , B , 0 ) ) ) )
8 oveq1 
 |-  ( ( abs ` B ) = ( abs ` if ( B e. CC , B , 0 ) ) -> ( ( abs ` B ) ^ 2 ) = ( ( abs ` if ( B e. CC , B , 0 ) ) ^ 2 ) )
9 8 breq2d 
 |-  ( ( abs ` B ) = ( abs ` if ( B e. CC , B , 0 ) ) -> ( ( ( abs ` if ( A e. CC , A , 0 ) ) ^ 2 ) < ( ( abs ` B ) ^ 2 ) <-> ( ( abs ` if ( A e. CC , A , 0 ) ) ^ 2 ) < ( ( abs ` if ( B e. CC , B , 0 ) ) ^ 2 ) ) )
10 6 9 syl 
 |-  ( B = if ( B e. CC , B , 0 ) -> ( ( ( abs ` if ( A e. CC , A , 0 ) ) ^ 2 ) < ( ( abs ` B ) ^ 2 ) <-> ( ( abs ` if ( A e. CC , A , 0 ) ) ^ 2 ) < ( ( abs ` if ( B e. CC , B , 0 ) ) ^ 2 ) ) )
11 7 10 bibi12d 
 |-  ( B = if ( B e. CC , B , 0 ) -> ( ( ( abs ` if ( A e. CC , A , 0 ) ) < ( abs ` B ) <-> ( ( abs ` if ( A e. CC , A , 0 ) ) ^ 2 ) < ( ( abs ` B ) ^ 2 ) ) <-> ( ( abs ` if ( A e. CC , A , 0 ) ) < ( abs ` if ( B e. CC , B , 0 ) ) <-> ( ( abs ` if ( A e. CC , A , 0 ) ) ^ 2 ) < ( ( abs ` if ( B e. CC , B , 0 ) ) ^ 2 ) ) ) )
12 0cn 
 |-  0 e. CC
13 12 elimel 
 |-  if ( A e. CC , A , 0 ) e. CC
14 12 elimel 
 |-  if ( B e. CC , B , 0 ) e. CC
15 13 14 abs2sqlti 
 |-  ( ( abs ` if ( A e. CC , A , 0 ) ) < ( abs ` if ( B e. CC , B , 0 ) ) <-> ( ( abs ` if ( A e. CC , A , 0 ) ) ^ 2 ) < ( ( abs ` if ( B e. CC , B , 0 ) ) ^ 2 ) )
16 5 11 15 dedth2h 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( abs ` A ) < ( abs ` B ) <-> ( ( abs ` A ) ^ 2 ) < ( ( abs ` B ) ^ 2 ) ) )