This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem abslt2sqd

Description: Comparison of the square of two numbers. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses abslt2sqd.a 
|- ( ph -> A e. RR )
abslt2sqd.b 
|- ( ph -> B e. RR )
abslt2sqd.l 
|- ( ph -> ( abs ` A ) < ( abs ` B ) )
Assertion abslt2sqd 
|- ( ph -> ( A ^ 2 ) < ( B ^ 2 ) )

Proof

Step Hyp Ref Expression
1 abslt2sqd.a 
 |-  ( ph -> A e. RR )
2 abslt2sqd.b 
 |-  ( ph -> B e. RR )
3 abslt2sqd.l 
 |-  ( ph -> ( abs ` A ) < ( abs ` B ) )
4 1 recnd 
 |-  ( ph -> A e. CC )
5 4 abscld 
 |-  ( ph -> ( abs ` A ) e. RR )
6 4 absge0d 
 |-  ( ph -> 0 <_ ( abs ` A ) )
7 2 recnd 
 |-  ( ph -> B e. CC )
8 7 abscld 
 |-  ( ph -> ( abs ` B ) e. RR )
9 7 absge0d 
 |-  ( ph -> 0 <_ ( abs ` B ) )
10 lt2sq 
 |-  ( ( ( ( abs ` A ) e. RR /\ 0 <_ ( abs ` A ) ) /\ ( ( abs ` B ) e. RR /\ 0 <_ ( abs ` B ) ) ) -> ( ( abs ` A ) < ( abs ` B ) <-> ( ( abs ` A ) ^ 2 ) < ( ( abs ` B ) ^ 2 ) ) )
11 5 6 8 9 10 syl22anc 
 |-  ( ph -> ( ( abs ` A ) < ( abs ` B ) <-> ( ( abs ` A ) ^ 2 ) < ( ( abs ` B ) ^ 2 ) ) )
12 3 11 mpbid 
 |-  ( ph -> ( ( abs ` A ) ^ 2 ) < ( ( abs ` B ) ^ 2 ) )
13 absresq 
 |-  ( A e. RR -> ( ( abs ` A ) ^ 2 ) = ( A ^ 2 ) )
14 1 13 syl 
 |-  ( ph -> ( ( abs ` A ) ^ 2 ) = ( A ^ 2 ) )
15 absresq 
 |-  ( B e. RR -> ( ( abs ` B ) ^ 2 ) = ( B ^ 2 ) )
16 2 15 syl 
 |-  ( ph -> ( ( abs ` B ) ^ 2 ) = ( B ^ 2 ) )
17 14 16 breq12d 
 |-  ( ph -> ( ( ( abs ` A ) ^ 2 ) < ( ( abs ` B ) ^ 2 ) <-> ( A ^ 2 ) < ( B ^ 2 ) ) )
18 12 17 mpbid 
 |-  ( ph -> ( A ^ 2 ) < ( B ^ 2 ) )