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 le0neg1 
 |-  ( B e. RR -> ( B <_ 0 <-> 0 <_ -u B ) )
11 9 10 syl 
 |-  ( ( ph /\ B <_ 0 ) -> ( B <_ 0 <-> 0 <_ -u B ) )
12 8 11 mpbid 
 |-  ( ( ph /\ B <_ 0 ) -> 0 <_ -u B )
13 7 12 jca 
 |-  ( ( ph /\ B <_ 0 ) -> ( -u B e. RR /\ 0 <_ -u B ) )
14 1 renegcld 
 |-  ( ph -> -u A e. RR )
15 14 adantr 
 |-  ( ( ph /\ B <_ 0 ) -> -u A e. RR )
16 1 2 jca 
 |-  ( ph -> ( A e. RR /\ B e. RR ) )
17 ltneg 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < B <-> -u B < -u A ) )
18 16 17 syl 
 |-  ( ph -> ( A < B <-> -u B < -u A ) )
19 4 18 mpbid 
 |-  ( ph -> -u B < -u A )
20 19 adantr 
 |-  ( ( ph /\ B <_ 0 ) -> -u B < -u A )
21 13 15 20 3jca 
 |-  ( ( ph /\ B <_ 0 ) -> ( ( -u B e. RR /\ 0 <_ -u B ) /\ -u A e. RR /\ -u B < -u A ) )
22 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 ) )
23 21 22 syl 
 |-  ( ( ph /\ B <_ 0 ) -> ( -u B x. -u B ) < ( -u A x. -u A ) )
24 recn 
 |-  ( B e. RR -> B e. CC )
25 mul2neg 
 |-  ( ( B e. CC /\ B e. CC ) -> ( -u B x. -u B ) = ( B x. B ) )
26 24 24 25 syl2anc 
 |-  ( B e. RR -> ( -u B x. -u B ) = ( B x. B ) )
27 2 26 syl 
 |-  ( ph -> ( -u B x. -u B ) = ( B x. B ) )
28 recn 
 |-  ( A e. RR -> A e. CC )
29 mul2neg 
 |-  ( ( A e. CC /\ A e. CC ) -> ( -u A x. -u A ) = ( A x. A ) )
30 28 28 29 syl2anc 
 |-  ( A e. RR -> ( -u A x. -u A ) = ( A x. A ) )
31 1 30 syl 
 |-  ( ph -> ( -u A x. -u A ) = ( A x. A ) )
32 27 31 breq12d 
 |-  ( ph -> ( ( -u B x. -u B ) < ( -u A x. -u A ) <-> ( B x. B ) < ( A x. A ) ) )
33 32 adantr 
 |-  ( ( ph /\ B <_ 0 ) -> ( ( -u B x. -u B ) < ( -u A x. -u A ) <-> ( B x. B ) < ( A x. A ) ) )
34 23 33 mpbid 
 |-  ( ( ph /\ B <_ 0 ) -> ( B x. B ) < ( A x. A ) )
35 34 orcd 
 |-  ( ( ph /\ B <_ 0 ) -> ( ( B x. B ) < ( A x. A ) \/ ( B x. B ) < ( C x. C ) ) )
36 2 anim1i 
 |-  ( ( ph /\ 0 <_ B ) -> ( B e. RR /\ 0 <_ B ) )
37 3 adantr 
 |-  ( ( ph /\ 0 <_ B ) -> C e. RR )
38 5 adantr 
 |-  ( ( ph /\ 0 <_ B ) -> B < C )
39 36 37 38 3jca 
 |-  ( ( ph /\ 0 <_ B ) -> ( ( B e. RR /\ 0 <_ B ) /\ C e. RR /\ B < C ) )
40 lt2msq1 
 |-  ( ( ( B e. RR /\ 0 <_ B ) /\ C e. RR /\ B < C ) -> ( B x. B ) < ( C x. C ) )
41 39 40 syl 
 |-  ( ( ph /\ 0 <_ B ) -> ( B x. B ) < ( C x. C ) )
42 41 olcd 
 |-  ( ( ph /\ 0 <_ B ) -> ( ( B x. B ) < ( A x. A ) \/ ( B x. B ) < ( C x. C ) ) )
43 0re 
 |-  0 e. RR
44 43 jctr 
 |-  ( B e. RR -> ( B e. RR /\ 0 e. RR ) )
45 letric 
 |-  ( ( B e. RR /\ 0 e. RR ) -> ( B <_ 0 \/ 0 <_ B ) )
46 2 44 45 3syl 
 |-  ( ph -> ( B <_ 0 \/ 0 <_ B ) )
47 35 42 46 mpjaodan 
 |-  ( ph -> ( ( B x. B ) < ( A x. A ) \/ ( B x. B ) < ( C x. C ) ) )