Proof of Theorem unbdqndv2lem1
Step | Hyp | Ref
| Expression |
1 | | unbdqndv2lem1.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℂ) |
2 | | unbdqndv2lem1.b |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ ℂ) |
3 | 1, 2 | subcld 11442 |
. . . . 5
⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℂ) |
4 | | unbdqndv2lem1.d |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ ℂ) |
5 | | unbdqndv2lem1.1 |
. . . . 5
⊢ (𝜑 → 𝐷 ≠ 0) |
6 | 3, 4, 5 | absdivd 15271 |
. . . 4
⊢ (𝜑 → (abs‘((𝐴 − 𝐵) / 𝐷)) = ((abs‘(𝐴 − 𝐵)) / (abs‘𝐷))) |
7 | 6 | adantr 482 |
. . 3
⊢ ((𝜑 ∧ ¬ ((𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐴 − 𝐶)) ∨ (𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐵 − 𝐶)))) → (abs‘((𝐴 − 𝐵) / 𝐷)) = ((abs‘(𝐴 − 𝐵)) / (abs‘𝐷))) |
8 | 3 | abscld 15252 |
. . . . . 6
⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) ∈ ℝ) |
9 | 8 | adantr 482 |
. . . . 5
⊢ ((𝜑 ∧ ¬ ((𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐴 − 𝐶)) ∨ (𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐵 − 𝐶)))) → (abs‘(𝐴 − 𝐵)) ∈ ℝ) |
10 | | unbdqndv2lem1.c |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ ℂ) |
11 | 1, 10 | subcld 11442 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 − 𝐶) ∈ ℂ) |
12 | 11 | abscld 15252 |
. . . . . . 7
⊢ (𝜑 → (abs‘(𝐴 − 𝐶)) ∈ ℝ) |
13 | 2, 10 | subcld 11442 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 − 𝐶) ∈ ℂ) |
14 | 13 | abscld 15252 |
. . . . . . 7
⊢ (𝜑 → (abs‘(𝐵 − 𝐶)) ∈ ℝ) |
15 | 12, 14 | readdcld 11114 |
. . . . . 6
⊢ (𝜑 → ((abs‘(𝐴 − 𝐶)) + (abs‘(𝐵 − 𝐶))) ∈ ℝ) |
16 | 15 | adantr 482 |
. . . . 5
⊢ ((𝜑 ∧ ¬ ((𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐴 − 𝐶)) ∨ (𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐵 − 𝐶)))) → ((abs‘(𝐴 − 𝐶)) + (abs‘(𝐵 − 𝐶))) ∈ ℝ) |
17 | | 2re 12157 |
. . . . . . . . 9
⊢ 2 ∈
ℝ |
18 | 17 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 2 ∈
ℝ) |
19 | | unbdqndv2lem1.e |
. . . . . . . . 9
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
20 | 19 | rpred 12882 |
. . . . . . . 8
⊢ (𝜑 → 𝐸 ∈ ℝ) |
21 | 18, 20 | remulcld 11115 |
. . . . . . 7
⊢ (𝜑 → (2 · 𝐸) ∈
ℝ) |
22 | 4 | abscld 15252 |
. . . . . . 7
⊢ (𝜑 → (abs‘𝐷) ∈
ℝ) |
23 | 21, 22 | remulcld 11115 |
. . . . . 6
⊢ (𝜑 → ((2 · 𝐸) · (abs‘𝐷)) ∈
ℝ) |
24 | 23 | adantr 482 |
. . . . 5
⊢ ((𝜑 ∧ ¬ ((𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐴 − 𝐶)) ∨ (𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐵 − 𝐶)))) → ((2 · 𝐸) · (abs‘𝐷)) ∈ ℝ) |
25 | 1, 2, 10 | abs3difd 15276 |
. . . . . . 7
⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) ≤ ((abs‘(𝐴 − 𝐶)) + (abs‘(𝐶 − 𝐵)))) |
26 | 10, 2 | abssubd 15269 |
. . . . . . . 8
⊢ (𝜑 → (abs‘(𝐶 − 𝐵)) = (abs‘(𝐵 − 𝐶))) |
27 | 26 | oveq2d 7362 |
. . . . . . 7
⊢ (𝜑 → ((abs‘(𝐴 − 𝐶)) + (abs‘(𝐶 − 𝐵))) = ((abs‘(𝐴 − 𝐶)) + (abs‘(𝐵 − 𝐶)))) |
28 | 25, 27 | breqtrd 5126 |
. . . . . 6
⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) ≤ ((abs‘(𝐴 − 𝐶)) + (abs‘(𝐵 − 𝐶)))) |
29 | 28 | adantr 482 |
. . . . 5
⊢ ((𝜑 ∧ ¬ ((𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐴 − 𝐶)) ∨ (𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐵 − 𝐶)))) → (abs‘(𝐴 − 𝐵)) ≤ ((abs‘(𝐴 − 𝐶)) + (abs‘(𝐵 − 𝐶)))) |
30 | 12 | adantr 482 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ ((𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐴 − 𝐶)) ∨ (𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐵 − 𝐶)))) → (abs‘(𝐴 − 𝐶)) ∈ ℝ) |
31 | 14 | adantr 482 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ ((𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐴 − 𝐶)) ∨ (𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐵 − 𝐶)))) → (abs‘(𝐵 − 𝐶)) ∈ ℝ) |
32 | 20, 22 | remulcld 11115 |
. . . . . . . 8
⊢ (𝜑 → (𝐸 · (abs‘𝐷)) ∈ ℝ) |
33 | 32 | adantr 482 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ ((𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐴 − 𝐶)) ∨ (𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐵 − 𝐶)))) → (𝐸 · (abs‘𝐷)) ∈ ℝ) |
34 | | pm2.45 880 |
. . . . . . . . 9
⊢ (¬
((𝐸 ·
(abs‘𝐷)) ≤
(abs‘(𝐴 − 𝐶)) ∨ (𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐵 − 𝐶))) → ¬ (𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐴 − 𝐶))) |
35 | 34 | adantl 483 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ ((𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐴 − 𝐶)) ∨ (𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐵 − 𝐶)))) → ¬ (𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐴 − 𝐶))) |
36 | 12, 32 | ltnled 11232 |
. . . . . . . . 9
⊢ (𝜑 → ((abs‘(𝐴 − 𝐶)) < (𝐸 · (abs‘𝐷)) ↔ ¬ (𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐴 − 𝐶)))) |
37 | 36 | adantr 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ ((𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐴 − 𝐶)) ∨ (𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐵 − 𝐶)))) → ((abs‘(𝐴 − 𝐶)) < (𝐸 · (abs‘𝐷)) ↔ ¬ (𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐴 − 𝐶)))) |
38 | 35, 37 | mpbird 257 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ ((𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐴 − 𝐶)) ∨ (𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐵 − 𝐶)))) → (abs‘(𝐴 − 𝐶)) < (𝐸 · (abs‘𝐷))) |
39 | | pm2.46 881 |
. . . . . . . . 9
⊢ (¬
((𝐸 ·
(abs‘𝐷)) ≤
(abs‘(𝐴 − 𝐶)) ∨ (𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐵 − 𝐶))) → ¬ (𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐵 − 𝐶))) |
40 | 39 | adantl 483 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ ((𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐴 − 𝐶)) ∨ (𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐵 − 𝐶)))) → ¬ (𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐵 − 𝐶))) |
41 | 14, 32 | ltnled 11232 |
. . . . . . . . 9
⊢ (𝜑 → ((abs‘(𝐵 − 𝐶)) < (𝐸 · (abs‘𝐷)) ↔ ¬ (𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐵 − 𝐶)))) |
42 | 41 | adantr 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ ((𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐴 − 𝐶)) ∨ (𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐵 − 𝐶)))) → ((abs‘(𝐵 − 𝐶)) < (𝐸 · (abs‘𝐷)) ↔ ¬ (𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐵 − 𝐶)))) |
43 | 40, 42 | mpbird 257 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ ((𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐴 − 𝐶)) ∨ (𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐵 − 𝐶)))) → (abs‘(𝐵 − 𝐶)) < (𝐸 · (abs‘𝐷))) |
44 | 30, 31, 33, 33, 38, 43 | lt2addd 11708 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ ((𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐴 − 𝐶)) ∨ (𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐵 − 𝐶)))) → ((abs‘(𝐴 − 𝐶)) + (abs‘(𝐵 − 𝐶))) < ((𝐸 · (abs‘𝐷)) + (𝐸 · (abs‘𝐷)))) |
45 | 32 | recnd 11113 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐸 · (abs‘𝐷)) ∈ ℂ) |
46 | 45 | 2timesd 12326 |
. . . . . . . . 9
⊢ (𝜑 → (2 · (𝐸 · (abs‘𝐷))) = ((𝐸 · (abs‘𝐷)) + (𝐸 · (abs‘𝐷)))) |
47 | 46 | eqcomd 2743 |
. . . . . . . 8
⊢ (𝜑 → ((𝐸 · (abs‘𝐷)) + (𝐸 · (abs‘𝐷))) = (2 · (𝐸 · (abs‘𝐷)))) |
48 | 18 | recnd 11113 |
. . . . . . . . . 10
⊢ (𝜑 → 2 ∈
ℂ) |
49 | 20 | recnd 11113 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐸 ∈ ℂ) |
50 | 22 | recnd 11113 |
. . . . . . . . . 10
⊢ (𝜑 → (abs‘𝐷) ∈
ℂ) |
51 | 48, 49, 50 | mulassd 11108 |
. . . . . . . . 9
⊢ (𝜑 → ((2 · 𝐸) · (abs‘𝐷)) = (2 · (𝐸 · (abs‘𝐷)))) |
52 | 51 | eqcomd 2743 |
. . . . . . . 8
⊢ (𝜑 → (2 · (𝐸 · (abs‘𝐷))) = ((2 · 𝐸) · (abs‘𝐷))) |
53 | 47, 52 | eqtrd 2777 |
. . . . . . 7
⊢ (𝜑 → ((𝐸 · (abs‘𝐷)) + (𝐸 · (abs‘𝐷))) = ((2 · 𝐸) · (abs‘𝐷))) |
54 | 53 | adantr 482 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ ((𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐴 − 𝐶)) ∨ (𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐵 − 𝐶)))) → ((𝐸 · (abs‘𝐷)) + (𝐸 · (abs‘𝐷))) = ((2 · 𝐸) · (abs‘𝐷))) |
55 | 44, 54 | breqtrd 5126 |
. . . . 5
⊢ ((𝜑 ∧ ¬ ((𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐴 − 𝐶)) ∨ (𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐵 − 𝐶)))) → ((abs‘(𝐴 − 𝐶)) + (abs‘(𝐵 − 𝐶))) < ((2 · 𝐸) · (abs‘𝐷))) |
56 | 9, 16, 24, 29, 55 | lelttrd 11243 |
. . . 4
⊢ ((𝜑 ∧ ¬ ((𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐴 − 𝐶)) ∨ (𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐵 − 𝐶)))) → (abs‘(𝐴 − 𝐵)) < ((2 · 𝐸) · (abs‘𝐷))) |
57 | | absgt0 15140 |
. . . . . . . . . 10
⊢ (𝐷 ∈ ℂ → (𝐷 ≠ 0 ↔ 0 <
(abs‘𝐷))) |
58 | 4, 57 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐷 ≠ 0 ↔ 0 < (abs‘𝐷))) |
59 | 5, 58 | mpbid 231 |
. . . . . . . 8
⊢ (𝜑 → 0 < (abs‘𝐷)) |
60 | 22, 59 | jca 513 |
. . . . . . 7
⊢ (𝜑 → ((abs‘𝐷) ∈ ℝ ∧ 0 <
(abs‘𝐷))) |
61 | 8, 21, 60 | 3jca 1128 |
. . . . . 6
⊢ (𝜑 → ((abs‘(𝐴 − 𝐵)) ∈ ℝ ∧ (2 · 𝐸) ∈ ℝ ∧
((abs‘𝐷) ∈
ℝ ∧ 0 < (abs‘𝐷)))) |
62 | | ltdivmul2 11962 |
. . . . . 6
⊢
(((abs‘(𝐴
− 𝐵)) ∈ ℝ
∧ (2 · 𝐸) ∈
ℝ ∧ ((abs‘𝐷) ∈ ℝ ∧ 0 <
(abs‘𝐷))) →
(((abs‘(𝐴 −
𝐵)) / (abs‘𝐷)) < (2 · 𝐸) ↔ (abs‘(𝐴 − 𝐵)) < ((2 · 𝐸) · (abs‘𝐷)))) |
63 | 61, 62 | syl 17 |
. . . . 5
⊢ (𝜑 → (((abs‘(𝐴 − 𝐵)) / (abs‘𝐷)) < (2 · 𝐸) ↔ (abs‘(𝐴 − 𝐵)) < ((2 · 𝐸) · (abs‘𝐷)))) |
64 | 63 | adantr 482 |
. . . 4
⊢ ((𝜑 ∧ ¬ ((𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐴 − 𝐶)) ∨ (𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐵 − 𝐶)))) → (((abs‘(𝐴 − 𝐵)) / (abs‘𝐷)) < (2 · 𝐸) ↔ (abs‘(𝐴 − 𝐵)) < ((2 · 𝐸) · (abs‘𝐷)))) |
65 | 56, 64 | mpbird 257 |
. . 3
⊢ ((𝜑 ∧ ¬ ((𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐴 − 𝐶)) ∨ (𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐵 − 𝐶)))) → ((abs‘(𝐴 − 𝐵)) / (abs‘𝐷)) < (2 · 𝐸)) |
66 | 7, 65 | eqbrtrd 5122 |
. 2
⊢ ((𝜑 ∧ ¬ ((𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐴 − 𝐶)) ∨ (𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐵 − 𝐶)))) → (abs‘((𝐴 − 𝐵) / 𝐷)) < (2 · 𝐸)) |
67 | | unbdqndv2lem1.2 |
. . . 4
⊢ (𝜑 → (2 · 𝐸) ≤ (abs‘((𝐴 − 𝐵) / 𝐷))) |
68 | 3, 4, 5 | divcld 11861 |
. . . . . 6
⊢ (𝜑 → ((𝐴 − 𝐵) / 𝐷) ∈ ℂ) |
69 | 68 | abscld 15252 |
. . . . 5
⊢ (𝜑 → (abs‘((𝐴 − 𝐵) / 𝐷)) ∈ ℝ) |
70 | 21, 69 | lenltd 11231 |
. . . 4
⊢ (𝜑 → ((2 · 𝐸) ≤ (abs‘((𝐴 − 𝐵) / 𝐷)) ↔ ¬ (abs‘((𝐴 − 𝐵) / 𝐷)) < (2 · 𝐸))) |
71 | 67, 70 | mpbid 231 |
. . 3
⊢ (𝜑 → ¬ (abs‘((𝐴 − 𝐵) / 𝐷)) < (2 · 𝐸)) |
72 | 71 | adantr 482 |
. 2
⊢ ((𝜑 ∧ ¬ ((𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐴 − 𝐶)) ∨ (𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐵 − 𝐶)))) → ¬ (abs‘((𝐴 − 𝐵) / 𝐷)) < (2 · 𝐸)) |
73 | 66, 72 | condan 816 |
1
⊢ (𝜑 → ((𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐴 − 𝐶)) ∨ (𝐸 · (abs‘𝐷)) ≤ (abs‘(𝐵 − 𝐶)))) |