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 9 le0neg1d ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 0 ) → ( 𝐵 ≤ 0 ↔ 0 ≤ - 𝐵 ) )
11 8 10 mpbid ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 0 ) → 0 ≤ - 𝐵 )
12 1 renegcld ⊢ ( 𝜑 → - 𝐴 ∈ ℝ )
13 12 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 0 ) → - 𝐴 ∈ ℝ )
14 1 2 ltnegd ⊢ ( 𝜑 → ( 𝐴 < 𝐵 ↔ - 𝐵 < - 𝐴 ) )
15 4 14 mpbid ⊢ ( 𝜑 → - 𝐵 < - 𝐴 )
16 15 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 0 ) → - 𝐵 < - 𝐴 )
17 lt2msq1 ⊢ ( ( ( - 𝐵 ∈ ℝ ∧ 0 ≤ - 𝐵 ) ∧ - 𝐴 ∈ ℝ ∧ - 𝐵 < - 𝐴 ) → ( - 𝐵 · - 𝐵 ) < ( - 𝐴 · - 𝐴 ) )
18 7 11 13 16 17 syl211anc ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 0 ) → ( - 𝐵 · - 𝐵 ) < ( - 𝐴 · - 𝐴 ) )
19 recn ⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
20 19 19 mul2negd ⊢ ( 𝐵 ∈ ℝ → ( - 𝐵 · - 𝐵 ) = ( 𝐵 · 𝐵 ) )
21 2 20 syl ⊢ ( 𝜑 → ( - 𝐵 · - 𝐵 ) = ( 𝐵 · 𝐵 ) )
22 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
23 22 22 mul2negd ⊢ ( 𝐴 ∈ ℝ → ( - 𝐴 · - 𝐴 ) = ( 𝐴 · 𝐴 ) )
24 1 23 syl ⊢ ( 𝜑 → ( - 𝐴 · - 𝐴 ) = ( 𝐴 · 𝐴 ) )
25 21 24 breq12d ⊢ ( 𝜑 → ( ( - 𝐵 · - 𝐵 ) < ( - 𝐴 · - 𝐴 ) ↔ ( 𝐵 · 𝐵 ) < ( 𝐴 · 𝐴 ) ) )
26 25 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 0 ) → ( ( - 𝐵 · - 𝐵 ) < ( - 𝐴 · - 𝐴 ) ↔ ( 𝐵 · 𝐵 ) < ( 𝐴 · 𝐴 ) ) )
27 18 26 mpbid ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 0 ) → ( 𝐵 · 𝐵 ) < ( 𝐴 · 𝐴 ) )
28 2 anim1i ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐵 ) → ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) )
29 3 adantr ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐵 ) → 𝐶 ∈ ℝ )
30 5 adantr ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐵 ) → 𝐵 < 𝐶 )
31 lt2msq1 ⊢ ( ( ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ ∧ 𝐵 < 𝐶 ) → ( 𝐵 · 𝐵 ) < ( 𝐶 · 𝐶 ) )
32 28 29 30 31 syl3anc ⊢ ( ( 𝜑 ∧ 0 ≤ 𝐵 ) → ( 𝐵 · 𝐵 ) < ( 𝐶 · 𝐶 ) )
33 0re ⊢ 0 ∈ ℝ
34 letric ⊢ ( ( 𝐵 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 𝐵 ≤ 0 ∨ 0 ≤ 𝐵 ) )
35 2 33 34 sylancl ⊢ ( 𝜑 → ( 𝐵 ≤ 0 ∨ 0 ≤ 𝐵 ) )
36 27 32 35 orim12da ⊢ ( 𝜑 → ( ( 𝐵 · 𝐵 ) < ( 𝐴 · 𝐴 ) ∨ ( 𝐵 · 𝐵 ) < ( 𝐶 · 𝐶 ) ) )