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 ⊢ φ → A ∈ ℝ
squeezedltsq.2 ⊢ φ → B ∈ ℝ
squeezedltsq.3 ⊢ φ → C ∈ ℝ
squeezedltsq.4 ⊢ φ → A < B
squeezedltsq.5 ⊢ φ → B < C
Assertion squeezedltsq ⊢ φ → B ⁢ B < A ⁢ A ∨ B ⁢ B < C ⁢ C

Proof

Step Hyp Ref Expression
1 squeezedltsq.1 ⊢ φ → A ∈ ℝ
2 squeezedltsq.2 ⊢ φ → B ∈ ℝ
3 squeezedltsq.3 ⊢ φ → C ∈ ℝ
4 squeezedltsq.4 ⊢ φ → A < B
5 squeezedltsq.5 ⊢ φ → B < C
6 2 renegcld ⊢ φ → − B ∈ ℝ
7 6 adantr ⊢ φ ∧ B ≤ 0 → − B ∈ ℝ
8 simpr ⊢ φ ∧ B ≤ 0 → B ≤ 0
9 2 adantr ⊢ φ ∧ B ≤ 0 → B ∈ ℝ
10 9 le0neg1d ⊢ φ ∧ B ≤ 0 → B ≤ 0 ↔ 0 ≤ − B
11 8 10 mpbid ⊢ φ ∧ B ≤ 0 → 0 ≤ − B
12 1 renegcld ⊢ φ → − A ∈ ℝ
13 12 adantr ⊢ φ ∧ B ≤ 0 → − A ∈ ℝ
14 1 2 ltnegd ⊢ φ → A < B ↔ − B < − A
15 4 14 mpbid ⊢ φ → − B < − A
16 15 adantr ⊢ φ ∧ B ≤ 0 → − B < − A
17 lt2msq1 ⊢ − B ∈ ℝ ∧ 0 ≤ − B ∧ − A ∈ ℝ ∧ − B < − A → − B ⁢ − B < − A ⁢ − A
18 7 11 13 16 17 syl211anc ⊢ φ ∧ B ≤ 0 → − B ⁢ − B < − A ⁢ − A
19 recn ⊢ B ∈ ℝ → B ∈ ℂ
20 19 19 mul2negd ⊢ B ∈ ℝ → − B ⁢ − B = B ⁢ B
21 2 20 syl ⊢ φ → − B ⁢ − B = B ⁢ B
22 recn ⊢ A ∈ ℝ → A ∈ ℂ
23 22 22 mul2negd ⊢ A ∈ ℝ → − A ⁢ − A = A ⁢ A
24 1 23 syl ⊢ φ → − A ⁢ − A = A ⁢ A
25 21 24 breq12d ⊢ φ → − B ⁢ − B < − A ⁢ − A ↔ B ⁢ B < A ⁢ A
26 25 adantr ⊢ φ ∧ B ≤ 0 → − B ⁢ − B < − A ⁢ − A ↔ B ⁢ B < A ⁢ A
27 18 26 mpbid ⊢ φ ∧ B ≤ 0 → B ⁢ B < A ⁢ A
28 2 anim1i ⊢ φ ∧ 0 ≤ B → B ∈ ℝ ∧ 0 ≤ B
29 3 adantr ⊢ φ ∧ 0 ≤ B → C ∈ ℝ
30 5 adantr ⊢ φ ∧ 0 ≤ B → B < C
31 lt2msq1 ⊢ B ∈ ℝ ∧ 0 ≤ B ∧ C ∈ ℝ ∧ B < C → B ⁢ B < C ⁢ C
32 28 29 30 31 syl3anc ⊢ φ ∧ 0 ≤ B → B ⁢ B < C ⁢ C
33 0re ⊢ 0 ∈ ℝ
34 letric ⊢ B ∈ ℝ ∧ 0 ∈ ℝ → B ≤ 0 ∨ 0 ≤ B
35 2 33 34 sylancl ⊢ φ → B ≤ 0 ∨ 0 ≤ B
36 27 32 35 orim12da ⊢ φ → B ⁢ B < A ⁢ A ∨ B ⁢ B < C ⁢ C