Metamath Proof Explorer

Theorem unbdqndv2lem1

Description: Lemma for unbdqndv2 . (Contributed by Asger C. Ipsen, 12-May-2021)

Ref Expression
Hypotheses unbdqndv2lem1.a ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
unbdqndv2lem1.b ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
unbdqndv2lem1.c ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
unbdqndv2lem1.d ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
unbdqndv2lem1.e ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
unbdqndv2lem1.1 ⊢ ( 𝜑 → 𝐷 ≠ 0 )
unbdqndv2lem1.2 ⊢ ( 𝜑 → ( 2 · 𝐸 ) ≤ ( abs ‘ ( ( 𝐴 − 𝐵 ) / 𝐷 ) ) )
Assertion unbdqndv2lem1 ( 𝜑 → ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) )

Proof

Step Hyp Ref Expression
1 unbdqndv2lem1.a ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2 unbdqndv2lem1.b ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3 unbdqndv2lem1.c ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
4 unbdqndv2lem1.d ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
5 unbdqndv2lem1.e ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
6 unbdqndv2lem1.1 ⊢ ( 𝜑 → 𝐷 ≠ 0 )
7 unbdqndv2lem1.2 ⊢ ( 𝜑 → ( 2 · 𝐸 ) ≤ ( abs ‘ ( ( 𝐴 − 𝐵 ) / 𝐷 ) ) )
8 1 2 subcld ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ∈ ℂ )
9 8 4 6 absdivd ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 − 𝐵 ) / 𝐷 ) ) = ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / ( abs ‘ 𝐷 ) ) )
10 9 adantr ⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ) → ( abs ‘ ( ( 𝐴 − 𝐵 ) / 𝐷 ) ) = ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / ( abs ‘ 𝐷 ) ) )
11 8 abscld ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ℝ )
12 11 adantr ⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ) → ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ℝ )
13 1 3 subcld ⊢ ( 𝜑 → ( 𝐴 − 𝐶 ) ∈ ℂ )
14 13 abscld ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 − 𝐶 ) ) ∈ ℝ )
15 2 3 subcld ⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) ∈ ℂ )
16 15 abscld ⊢ ( 𝜑 → ( abs ‘ ( 𝐵 − 𝐶 ) ) ∈ ℝ )
17 14 16 readdcld ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐴 − 𝐶 ) ) + ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ∈ ℝ )
18 17 adantr ⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ) → ( ( abs ‘ ( 𝐴 − 𝐶 ) ) + ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ∈ ℝ )
19 2re ⊢ 2 ∈ ℝ
20 19 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
21 5 rpred ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
22 20 21 remulcld ⊢ ( 𝜑 → ( 2 · 𝐸 ) ∈ ℝ )
23 4 abscld ⊢ ( 𝜑 → ( abs ‘ 𝐷 ) ∈ ℝ )
24 22 23 remulcld ⊢ ( 𝜑 → ( ( 2 · 𝐸 ) · ( abs ‘ 𝐷 ) ) ∈ ℝ )
25 24 adantr ⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ) → ( ( 2 · 𝐸 ) · ( abs ‘ 𝐷 ) ) ∈ ℝ )
26 1 2 3 abs3difd ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 − 𝐵 ) ) ≤ ( ( abs ‘ ( 𝐴 − 𝐶 ) ) + ( abs ‘ ( 𝐶 − 𝐵 ) ) ) )
27 3 2 abssubd ⊢ ( 𝜑 → ( abs ‘ ( 𝐶 − 𝐵 ) ) = ( abs ‘ ( 𝐵 − 𝐶 ) ) )
28 27 oveq2d ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐴 − 𝐶 ) ) + ( abs ‘ ( 𝐶 − 𝐵 ) ) ) = ( ( abs ‘ ( 𝐴 − 𝐶 ) ) + ( abs ‘ ( 𝐵 − 𝐶 ) ) ) )
29 26 28 breqtrd ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 − 𝐵 ) ) ≤ ( ( abs ‘ ( 𝐴 − 𝐶 ) ) + ( abs ‘ ( 𝐵 − 𝐶 ) ) ) )
30 29 adantr ⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ) → ( abs ‘ ( 𝐴 − 𝐵 ) ) ≤ ( ( abs ‘ ( 𝐴 − 𝐶 ) ) + ( abs ‘ ( 𝐵 − 𝐶 ) ) ) )
31 14 adantr ⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ) → ( abs ‘ ( 𝐴 − 𝐶 ) ) ∈ ℝ )
32 16 adantr ⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ) → ( abs ‘ ( 𝐵 − 𝐶 ) ) ∈ ℝ )
33 21 23 remulcld ⊢ ( 𝜑 → ( 𝐸 · ( abs ‘ 𝐷 ) ) ∈ ℝ )
34 33 adantr ⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ) → ( 𝐸 · ( abs ‘ 𝐷 ) ) ∈ ℝ )
35 pm2.45 ⊢ ( ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) → ¬ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) )
36 35 adantl ⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ) → ¬ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) )
37 14 33 ltnled ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐴 − 𝐶 ) ) < ( 𝐸 · ( abs ‘ 𝐷 ) ) ↔ ¬ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ) )
38 37 adantr ⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ) → ( ( abs ‘ ( 𝐴 − 𝐶 ) ) < ( 𝐸 · ( abs ‘ 𝐷 ) ) ↔ ¬ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ) )
39 36 38 mpbird ⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ) → ( abs ‘ ( 𝐴 − 𝐶 ) ) < ( 𝐸 · ( abs ‘ 𝐷 ) ) )
40 pm2.46 ⊢ ( ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) → ¬ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) )
41 40 adantl ⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ) → ¬ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) )
42 16 33 ltnled ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐵 − 𝐶 ) ) < ( 𝐸 · ( abs ‘ 𝐷 ) ) ↔ ¬ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) )
43 42 adantr ⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ) → ( ( abs ‘ ( 𝐵 − 𝐶 ) ) < ( 𝐸 · ( abs ‘ 𝐷 ) ) ↔ ¬ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) )
44 41 43 mpbird ⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ) → ( abs ‘ ( 𝐵 − 𝐶 ) ) < ( 𝐸 · ( abs ‘ 𝐷 ) ) )
45 31 32 34 34 39 44 lt2addd ⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ) → ( ( abs ‘ ( 𝐴 − 𝐶 ) ) + ( abs ‘ ( 𝐵 − 𝐶 ) ) ) < ( ( 𝐸 · ( abs ‘ 𝐷 ) ) + ( 𝐸 · ( abs ‘ 𝐷 ) ) ) )
46 33 recnd ⊢ ( 𝜑 → ( 𝐸 · ( abs ‘ 𝐷 ) ) ∈ ℂ )
47 46 2timesd ⊢ ( 𝜑 → ( 2 · ( 𝐸 · ( abs ‘ 𝐷 ) ) ) = ( ( 𝐸 · ( abs ‘ 𝐷 ) ) + ( 𝐸 · ( abs ‘ 𝐷 ) ) ) )
48 47 eqcomd ⊢ ( 𝜑 → ( ( 𝐸 · ( abs ‘ 𝐷 ) ) + ( 𝐸 · ( abs ‘ 𝐷 ) ) ) = ( 2 · ( 𝐸 · ( abs ‘ 𝐷 ) ) ) )
49 20 recnd ⊢ ( 𝜑 → 2 ∈ ℂ )
50 21 recnd ⊢ ( 𝜑 → 𝐸 ∈ ℂ )
51 23 recnd ⊢ ( 𝜑 → ( abs ‘ 𝐷 ) ∈ ℂ )
52 49 50 51 mulassd ⊢ ( 𝜑 → ( ( 2 · 𝐸 ) · ( abs ‘ 𝐷 ) ) = ( 2 · ( 𝐸 · ( abs ‘ 𝐷 ) ) ) )
53 52 eqcomd ⊢ ( 𝜑 → ( 2 · ( 𝐸 · ( abs ‘ 𝐷 ) ) ) = ( ( 2 · 𝐸 ) · ( abs ‘ 𝐷 ) ) )
54 48 53 eqtrd ⊢ ( 𝜑 → ( ( 𝐸 · ( abs ‘ 𝐷 ) ) + ( 𝐸 · ( abs ‘ 𝐷 ) ) ) = ( ( 2 · 𝐸 ) · ( abs ‘ 𝐷 ) ) )
55 54 adantr ⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ) → ( ( 𝐸 · ( abs ‘ 𝐷 ) ) + ( 𝐸 · ( abs ‘ 𝐷 ) ) ) = ( ( 2 · 𝐸 ) · ( abs ‘ 𝐷 ) ) )
56 45 55 breqtrd ⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ) → ( ( abs ‘ ( 𝐴 − 𝐶 ) ) + ( abs ‘ ( 𝐵 − 𝐶 ) ) ) < ( ( 2 · 𝐸 ) · ( abs ‘ 𝐷 ) ) )
57 12 18 25 30 56 lelttrd ⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ) → ( abs ‘ ( 𝐴 − 𝐵 ) ) < ( ( 2 · 𝐸 ) · ( abs ‘ 𝐷 ) ) )
58 absgt0 ⊢ ( 𝐷 ∈ ℂ → ( 𝐷 ≠ 0 ↔ 0 < ( abs ‘ 𝐷 ) ) )
59 4 58 syl ⊢ ( 𝜑 → ( 𝐷 ≠ 0 ↔ 0 < ( abs ‘ 𝐷 ) ) )
60 6 59 mpbid ⊢ ( 𝜑 → 0 < ( abs ‘ 𝐷 ) )
61 23 60 jca ⊢ ( 𝜑 → ( ( abs ‘ 𝐷 ) ∈ ℝ ∧ 0 < ( abs ‘ 𝐷 ) ) )
62 11 22 61 3jca ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ℝ ∧ ( 2 · 𝐸 ) ∈ ℝ ∧ ( ( abs ‘ 𝐷 ) ∈ ℝ ∧ 0 < ( abs ‘ 𝐷 ) ) ) )
63 ltdivmul2 ⊢ ( ( ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ℝ ∧ ( 2 · 𝐸 ) ∈ ℝ ∧ ( ( abs ‘ 𝐷 ) ∈ ℝ ∧ 0 < ( abs ‘ 𝐷 ) ) ) → ( ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / ( abs ‘ 𝐷 ) ) < ( 2 · 𝐸 ) ↔ ( abs ‘ ( 𝐴 − 𝐵 ) ) < ( ( 2 · 𝐸 ) · ( abs ‘ 𝐷 ) ) ) )
64 62 63 syl ⊢ ( 𝜑 → ( ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / ( abs ‘ 𝐷 ) ) < ( 2 · 𝐸 ) ↔ ( abs ‘ ( 𝐴 − 𝐵 ) ) < ( ( 2 · 𝐸 ) · ( abs ‘ 𝐷 ) ) ) )
65 64 adantr ⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ) → ( ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / ( abs ‘ 𝐷 ) ) < ( 2 · 𝐸 ) ↔ ( abs ‘ ( 𝐴 − 𝐵 ) ) < ( ( 2 · 𝐸 ) · ( abs ‘ 𝐷 ) ) ) )
66 57 65 mpbird ⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ) → ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / ( abs ‘ 𝐷 ) ) < ( 2 · 𝐸 ) )
67 10 66 eqbrtrd ⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ) → ( abs ‘ ( ( 𝐴 − 𝐵 ) / 𝐷 ) ) < ( 2 · 𝐸 ) )
68 8 4 6 divcld ⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) / 𝐷 ) ∈ ℂ )
69 68 abscld ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 − 𝐵 ) / 𝐷 ) ) ∈ ℝ )
70 22 69 lenltd ⊢ ( 𝜑 → ( ( 2 · 𝐸 ) ≤ ( abs ‘ ( ( 𝐴 − 𝐵 ) / 𝐷 ) ) ↔ ¬ ( abs ‘ ( ( 𝐴 − 𝐵 ) / 𝐷 ) ) < ( 2 · 𝐸 ) ) )
71 7 70 mpbid ⊢ ( 𝜑 → ¬ ( abs ‘ ( ( 𝐴 − 𝐵 ) / 𝐷 ) ) < ( 2 · 𝐸 ) )
72 71 adantr ⊢ ( ( 𝜑 ∧ ¬ ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) ) → ¬ ( abs ‘ ( ( 𝐴 − 𝐵 ) / 𝐷 ) ) < ( 2 · 𝐸 ) )
73 67 72 condan ⊢ ( 𝜑 → ( ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) ∨ ( 𝐸 · ( abs ‘ 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) ) )