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 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
squeezedltsq.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
squeezedltsq.3 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
squeezedltsq.4 ⊢ ( 𝜑 → 𝐴 < 𝐵 )
squeezedltsq.5 ⊢ ( 𝜑 → 𝐵 < 𝐶 )
Assertion squeezedltsq ( 𝜑 → ( ( 𝐵 · 𝐵 ) < ( 𝐴 · 𝐴 ) ∨ ( 𝐵 · 𝐵 ) < ( 𝐶 · 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 squeezedltsq.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 squeezedltsq.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 squeezedltsq.3 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
4 squeezedltsq.4 ⊢ ( 𝜑 → 𝐴 < 𝐵 )
5 squeezedltsq.5 ⊢ ( 𝜑 → 𝐵 < 𝐶 )
6 2 renegcld ⊢ ( 𝜑 → - 𝐵 ∈ ℝ )
7 6 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 0 ) → - 𝐵 ∈ ℝ )
8 simpr ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 0 ) → 𝐵 ≤ 0 )
9 2 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 0 ) → 𝐵 ∈ ℝ )
10 le0neg1 ⊢ ( 𝐵 ∈ ℝ → ( 𝐵 ≤ 0 ↔ 0 ≤ - 𝐵 ) )
11 9 10 syl ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 0 ) → ( 𝐵 ≤ 0 ↔ 0 ≤ - 𝐵 ) )
12 8 11 mpbid ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 0 ) → 0 ≤ - 𝐵 )
13 7 12 jca ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 0 ) → ( - 𝐵 ∈ ℝ ∧ 0 ≤ - 𝐵 ) )
14 1 renegcld ⊢ ( 𝜑 → - 𝐴 ∈ ℝ )
15 14 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 0 ) → - 𝐴 ∈ ℝ )
16 1 2 jca ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
17 ltneg ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ - 𝐵 < - 𝐴 ) )
18 16 17 syl ⊢ ( 𝜑 → ( 𝐴 < 𝐵 ↔ - 𝐵 < - 𝐴 ) )
19 4 18 mpbid ⊢ ( 𝜑 → - 𝐵 < - 𝐴 )
20 19 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 0 ) → - 𝐵 < - 𝐴 )
21 13 15 20 3jca ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 0 ) → ( ( - 𝐵 ∈ ℝ ∧ 0 ≤ - 𝐵 ) ∧ - 𝐴 ∈ ℝ ∧ - 𝐵 < - 𝐴 ) )
22 lt2msq1 ⊢ ( ( ( - 𝐵 ∈ ℝ ∧ 0 ≤ - 𝐵 ) ∧ - 𝐴 ∈ ℝ ∧ - 𝐵 < - 𝐴 ) → ( - 𝐵 · - 𝐵 ) < ( - 𝐴 · - 𝐴 ) )
23 21 22 syl ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 0 ) → ( - 𝐵 · - 𝐵 ) < ( - 𝐴 · - 𝐴 ) )
24 recn ⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
25 mul2neg ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( - 𝐵 · - 𝐵 ) = ( 𝐵 · 𝐵 ) )
26 24 24 25 syl2anc ⊢ ( 𝐵 ∈ ℝ → ( - 𝐵 · - 𝐵 ) = ( 𝐵 · 𝐵 ) )
27 2 26 syl ⊢ ( 𝜑 → ( - 𝐵 · - 𝐵 ) = ( 𝐵 · 𝐵 ) )
28 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
29 mul2neg ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( - 𝐴 · - 𝐴 ) = ( 𝐴 · 𝐴 ) )
30 28 28 29 syl2anc ⊢ ( 𝐴 ∈ ℝ → ( - 𝐴 · - 𝐴 ) = ( 𝐴 · 𝐴 ) )
31 1 30 syl ⊢ ( 𝜑 → ( - 𝐴 · - 𝐴 ) = ( 𝐴 · 𝐴 ) )
32 27 31 breq12d ⊢ ( 𝜑 → ( ( - 𝐵 · - 𝐵 ) < ( - 𝐴 · - 𝐴 ) ↔ ( 𝐵 · 𝐵 ) < ( 𝐴 · 𝐴 ) ) )
33 32 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 0 ) → ( ( - 𝐵 · - 𝐵 ) < ( - 𝐴 · - 𝐴 ) ↔ ( 𝐵 · 𝐵 ) < ( 𝐴 · 𝐴 ) ) )
34 23 33 mpbid ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 0 ) → ( 𝐵 · 𝐵 ) < ( 𝐴 · 𝐴 ) )
35 34 orcd ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 0 ) → ( ( 𝐵 · 𝐵 ) < ( 𝐴 · 𝐴 ) ∨ ( 𝐵 · 𝐵 ) < ( 𝐶 · 𝐶 ) ) )
36 2 anim1i ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐵 ) → ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) )
37 3 adantr ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐵 ) → 𝐶 ∈ ℝ )
38 5 adantr ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐵 ) → 𝐵 < 𝐶 )
39 36 37 38 3jca ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐵 ) → ( ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ ∧ 𝐵 < 𝐶 ) )
40 lt2msq1 ⊢ ( ( ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ ∧ 𝐵 < 𝐶 ) → ( 𝐵 · 𝐵 ) < ( 𝐶 · 𝐶 ) )
41 39 40 syl ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐵 ) → ( 𝐵 · 𝐵 ) < ( 𝐶 · 𝐶 ) )
42 41 olcd ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐵 ) → ( ( 𝐵 · 𝐵 ) < ( 𝐴 · 𝐴 ) ∨ ( 𝐵 · 𝐵 ) < ( 𝐶 · 𝐶 ) ) )
43 0re ⊢ 0 ∈ ℝ
44 43 jctr ⊢ ( 𝐵 ∈ ℝ → ( 𝐵 ∈ ℝ ∧ 0 ∈ ℝ ) )
45 letric ⊢ ( ( 𝐵 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 𝐵 ≤ 0 ∨ 0 ≤ 𝐵 ) )
46 2 44 45 3syl ⊢ ( 𝜑 → ( 𝐵 ≤ 0 ∨ 0 ≤ 𝐵 ) )
47 35 42 46 mpjaodan ⊢ ( 𝜑 → ( ( 𝐵 · 𝐵 ) < ( 𝐴 · 𝐴 ) ∨ ( 𝐵 · 𝐵 ) < ( 𝐶 · 𝐶 ) ) )