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 le0neg1 ⊢ B ∈ ℝ → B ≤ 0 ↔ 0 ≤ − B
11 9 10 syl ⊢ φ ∧ B ≤ 0 → B ≤ 0 ↔ 0 ≤ − B
12 8 11 mpbid ⊢ φ ∧ B ≤ 0 → 0 ≤ − B
13 7 12 jca ⊢ φ ∧ B ≤ 0 → − B ∈ ℝ ∧ 0 ≤ − B
14 1 renegcld ⊢ φ → − A ∈ ℝ
15 14 adantr ⊢ φ ∧ B ≤ 0 → − A ∈ ℝ
16 1 2 jca ⊢ φ → A ∈ ℝ ∧ B ∈ ℝ
17 ltneg ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ↔ − B < − A
18 16 17 syl ⊢ φ → A < B ↔ − B < − A
19 4 18 mpbid ⊢ φ → − B < − A
20 19 adantr ⊢ φ ∧ B ≤ 0 → − B < − A
21 13 15 20 3jca ⊢ φ ∧ B ≤ 0 → − B ∈ ℝ ∧ 0 ≤ − B ∧ − A ∈ ℝ ∧ − B < − A
22 lt2msq1 ⊢ − B ∈ ℝ ∧ 0 ≤ − B ∧ − A ∈ ℝ ∧ − B < − A → − B ⁢ − B < − A ⁢ − A
23 21 22 syl ⊢ φ ∧ B ≤ 0 → − B ⁢ − B < − A ⁢ − A
24 recn ⊢ B ∈ ℝ → B ∈ ℂ
25 mul2neg ⊢ B ∈ ℂ ∧ B ∈ ℂ → − B ⁢ − B = B ⁢ B
26 24 24 25 syl2anc ⊢ B ∈ ℝ → − B ⁢ − B = B ⁢ B
27 2 26 syl ⊢ φ → − B ⁢ − B = B ⁢ B
28 recn ⊢ A ∈ ℝ → A ∈ ℂ
29 mul2neg ⊢ A ∈ ℂ ∧ A ∈ ℂ → − A ⁢ − A = A ⁢ A
30 28 28 29 syl2anc ⊢ A ∈ ℝ → − A ⁢ − A = A ⁢ A
31 1 30 syl ⊢ φ → − A ⁢ − A = A ⁢ A
32 27 31 breq12d ⊢ φ → − B ⁢ − B < − A ⁢ − A ↔ B ⁢ B < A ⁢ A
33 32 adantr ⊢ φ ∧ B ≤ 0 → − B ⁢ − B < − A ⁢ − A ↔ B ⁢ B < A ⁢ A
34 23 33 mpbid ⊢ φ ∧ B ≤ 0 → B ⁢ B < A ⁢ A
35 34 orcd ⊢ φ ∧ B ≤ 0 → B ⁢ B < A ⁢ A ∨ B ⁢ B < C ⁢ C
36 2 anim1i ⊢ φ ∧ 0 ≤ B → B ∈ ℝ ∧ 0 ≤ B
37 3 adantr ⊢ φ ∧ 0 ≤ B → C ∈ ℝ
38 5 adantr ⊢ φ ∧ 0 ≤ B → B < C
39 36 37 38 3jca ⊢ φ ∧ 0 ≤ B → B ∈ ℝ ∧ 0 ≤ B ∧ C ∈ ℝ ∧ B < C
40 lt2msq1 ⊢ B ∈ ℝ ∧ 0 ≤ B ∧ C ∈ ℝ ∧ B < C → B ⁢ B < C ⁢ C
41 39 40 syl ⊢ φ ∧ 0 ≤ B → B ⁢ B < C ⁢ C
42 41 olcd ⊢ φ ∧ 0 ≤ B → B ⁢ B < A ⁢ A ∨ B ⁢ B < C ⁢ C
43 0re ⊢ 0 ∈ ℝ
44 43 jctr ⊢ B ∈ ℝ → B ∈ ℝ ∧ 0 ∈ ℝ
45 letric ⊢ B ∈ ℝ ∧ 0 ∈ ℝ → B ≤ 0 ∨ 0 ≤ B
46 2 44 45 3syl ⊢ φ → B ≤ 0 ∨ 0 ≤ B
47 35 42 46 mpjaodan ⊢ φ → B ⁢ B < A ⁢ A ∨ B ⁢ B < C ⁢ C