Metamath Proof Explorer

Theorem squeezedltsq

Description: If a real value is squeezed between two others, its square is less than square of at least one of them. Deduction form. (Contributed by Ender Ting, 31-Oct-2025)

Ref Expression
Hypotheses squeezedltsq.1 
|- ( ph -> A e. RR )
squeezedltsq.2 
|- ( ph -> B e. RR )
squeezedltsq.3 
|- ( ph -> C e. RR )
squeezedltsq.4 
|- ( ph -> A < B )
squeezedltsq.5 
|- ( ph -> B < C )
Assertion squeezedltsq 
|- ( ph -> ( ( B x. B ) < ( A x. A ) \/ ( B x. B ) < ( C x. C ) ) )

Proof

Step Hyp Ref Expression
1 squeezedltsq.1 
 |-  ( ph -> A e. RR )
2 squeezedltsq.2 
 |-  ( ph -> B e. RR )
3 squeezedltsq.3 
 |-  ( ph -> C e. RR )
4 squeezedltsq.4 
 |-  ( ph -> A < B )
5 squeezedltsq.5 
 |-  ( ph -> B < C )
6 2 renegcld 
 |-  ( ph -> -u B e. RR )
7 6 adantr 
 |-  ( ( ph /\ B <_ 0 ) -> -u B e. RR )
8 simpr 
 |-  ( ( ph /\ B <_ 0 ) -> B <_ 0 )
9 2 adantr 
 |-  ( ( ph /\ B <_ 0 ) -> B e. RR )
10 9 le0neg1d 
 |-  ( ( ph /\ B <_ 0 ) -> ( B <_ 0 <-> 0 <_ -u B ) )
11 8 10 mpbid 
 |-  ( ( ph /\ B <_ 0 ) -> 0 <_ -u B )
12 1 renegcld 
 |-  ( ph -> -u A e. RR )
13 12 adantr 
 |-  ( ( ph /\ B <_ 0 ) -> -u A e. RR )
14 1 2 ltnegd 
 |-  ( ph -> ( A < B <-> -u B < -u A ) )
15 4 14 mpbid 
 |-  ( ph -> -u B < -u A )
16 15 adantr 
 |-  ( ( ph /\ B <_ 0 ) -> -u B < -u A )
17 lt2msq1 
 |-  ( ( ( -u B e. RR /\ 0 <_ -u B ) /\ -u A e. RR /\ -u B < -u A ) -> ( -u B x. -u B ) < ( -u A x. -u A ) )
18 7 11 13 16 17 syl211anc 
 |-  ( ( ph /\ B <_ 0 ) -> ( -u B x. -u B ) < ( -u A x. -u A ) )
19 recn 
 |-  ( B e. RR -> B e. CC )
20 19 19 mul2negd 
 |-  ( B e. RR -> ( -u B x. -u B ) = ( B x. B ) )
21 2 20 syl 
 |-  ( ph -> ( -u B x. -u B ) = ( B x. B ) )
22 recn 
 |-  ( A e. RR -> A e. CC )
23 22 22 mul2negd 
 |-  ( A e. RR -> ( -u A x. -u A ) = ( A x. A ) )
24 1 23 syl 
 |-  ( ph -> ( -u A x. -u A ) = ( A x. A ) )
25 21 24 breq12d 
 |-  ( ph -> ( ( -u B x. -u B ) < ( -u A x. -u A ) <-> ( B x. B ) < ( A x. A ) ) )
26 25 adantr 
 |-  ( ( ph /\ B <_ 0 ) -> ( ( -u B x. -u B ) < ( -u A x. -u A ) <-> ( B x. B ) < ( A x. A ) ) )
27 18 26 mpbid 
 |-  ( ( ph /\ B <_ 0 ) -> ( B x. B ) < ( A x. A ) )
28 2 anim1i 
 |-  ( ( ph /\ 0 <_ B ) -> ( B e. RR /\ 0 <_ B ) )
29 3 adantr 
 |-  ( ( ph /\ 0 <_ B ) -> C e. RR )
30 5 adantr 
 |-  ( ( ph /\ 0 <_ B ) -> B < C )
31 lt2msq1 
 |-  ( ( ( B e. RR /\ 0 <_ B ) /\ C e. RR /\ B < C ) -> ( B x. B ) < ( C x. C ) )
32 28 29 30 31 syl3anc 
 |-  ( ( ph /\ 0 <_ B ) -> ( B x. B ) < ( C x. C ) )
33 0re 
 |-  0 e. RR
34 letric 
 |-  ( ( B e. RR /\ 0 e. RR ) -> ( B <_ 0 \/ 0 <_ B ) )
35 2 33 34 sylancl 
 |-  ( ph -> ( B <_ 0 \/ 0 <_ B ) )
36 27 32 35 orim12da 
 |-  ( ph -> ( ( B x. B ) < ( A x. A ) \/ ( B x. B ) < ( C x. C ) ) )