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 ) )