Step | Hyp | Ref
| Expression |
1 | | dvbdfbdioolem2.f |
. . . . . . . 8
⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℝ) |
2 | 1 | ffvelrnda 6267 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑥) ∈ ℝ) |
3 | 2 | recnd 9947 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑥) ∈ ℂ) |
4 | 3 | abscld 14023 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (abs‘(𝐹‘𝑥)) ∈ ℝ) |
5 | | dvbdfbdioolem2.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℝ) |
6 | 5 | rexrd 9968 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
7 | | dvbdfbdioolem2.b |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℝ) |
8 | 7 | rexrd 9968 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
9 | 5, 7 | readdcld 9948 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℝ) |
10 | 9 | rehalfcld 11156 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴 + 𝐵) / 2) ∈ ℝ) |
11 | | dvbdfbdioolem2.altb |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 < 𝐵) |
12 | | avglt1 11147 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 𝐴 < ((𝐴 + 𝐵) / 2))) |
13 | 5, 7, 12 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 < 𝐵 ↔ 𝐴 < ((𝐴 + 𝐵) / 2))) |
14 | 11, 13 | mpbid 221 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 < ((𝐴 + 𝐵) / 2)) |
15 | | avglt2 11148 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ((𝐴 + 𝐵) / 2) < 𝐵)) |
16 | 5, 7, 15 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 < 𝐵 ↔ ((𝐴 + 𝐵) / 2) < 𝐵)) |
17 | 11, 16 | mpbid 221 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴 + 𝐵) / 2) < 𝐵) |
18 | 6, 8, 10, 14, 17 | eliood 38567 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵)) |
19 | 1, 18 | ffvelrnd 6268 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘((𝐴 + 𝐵) / 2)) ∈ ℝ) |
20 | 19 | recnd 9947 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘((𝐴 + 𝐵) / 2)) ∈ ℂ) |
21 | 20 | abscld 14023 |
. . . . . 6
⊢ (𝜑 → (abs‘(𝐹‘((𝐴 + 𝐵) / 2))) ∈ ℝ) |
22 | 21 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (abs‘(𝐹‘((𝐴 + 𝐵) / 2))) ∈ ℝ) |
23 | 4, 22 | resubcld 10337 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((abs‘(𝐹‘𝑥)) − (abs‘(𝐹‘((𝐴 + 𝐵) / 2)))) ∈ ℝ) |
24 | | dvbdfbdioolem2.k |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ ℝ) |
25 | 24 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝐾 ∈ ℝ) |
26 | 7 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝐵 ∈ ℝ) |
27 | 5 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝐴 ∈ ℝ) |
28 | 26, 27 | resubcld 10337 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐵 − 𝐴) ∈ ℝ) |
29 | 25, 28 | remulcld 9949 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐾 · (𝐵 − 𝐴)) ∈ ℝ) |
30 | 20 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐹‘((𝐴 + 𝐵) / 2)) ∈ ℂ) |
31 | 3, 30 | subcld 10271 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((𝐹‘𝑥) − (𝐹‘((𝐴 + 𝐵) / 2))) ∈ ℂ) |
32 | 31 | abscld 14023 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (abs‘((𝐹‘𝑥) − (𝐹‘((𝐴 + 𝐵) / 2)))) ∈ ℝ) |
33 | 3, 30 | abs2difd 14044 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((abs‘(𝐹‘𝑥)) − (abs‘(𝐹‘((𝐴 + 𝐵) / 2)))) ≤ (abs‘((𝐹‘𝑥) − (𝐹‘((𝐴 + 𝐵) / 2))))) |
34 | | simpll 786 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ ((𝐴 + 𝐵) / 2) < 𝑥) → 𝜑) |
35 | 10 | rexrd 9968 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴 + 𝐵) / 2) ∈
ℝ*) |
36 | 35 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ ((𝐴 + 𝐵) / 2) < 𝑥) → ((𝐴 + 𝐵) / 2) ∈
ℝ*) |
37 | 8 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ ((𝐴 + 𝐵) / 2) < 𝑥) → 𝐵 ∈
ℝ*) |
38 | | elioore 12076 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 ∈ ℝ) |
39 | 38 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ ℝ) |
40 | 39 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ ((𝐴 + 𝐵) / 2) < 𝑥) → 𝑥 ∈ ℝ) |
41 | | simpr 476 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ ((𝐴 + 𝐵) / 2) < 𝑥) → ((𝐴 + 𝐵) / 2) < 𝑥) |
42 | 6 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝐴 ∈
ℝ*) |
43 | 8 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝐵 ∈
ℝ*) |
44 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ (𝐴(,)𝐵)) |
45 | | iooltub 38582 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑥
∈ (𝐴(,)𝐵)) → 𝑥 < 𝐵) |
46 | 42, 43, 44, 45 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 < 𝐵) |
47 | 46 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ ((𝐴 + 𝐵) / 2) < 𝑥) → 𝑥 < 𝐵) |
48 | 36, 37, 40, 41, 47 | eliood 38567 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ ((𝐴 + 𝐵) / 2) < 𝑥) → 𝑥 ∈ (((𝐴 + 𝐵) / 2)(,)𝐵)) |
49 | 5 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (((𝐴 + 𝐵) / 2)(,)𝐵)) → 𝐴 ∈ ℝ) |
50 | 7 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (((𝐴 + 𝐵) / 2)(,)𝐵)) → 𝐵 ∈ ℝ) |
51 | 1 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (((𝐴 + 𝐵) / 2)(,)𝐵)) → 𝐹:(𝐴(,)𝐵)⟶ℝ) |
52 | | dvbdfbdioolem2.dmdv |
. . . . . . . . . 10
⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) |
53 | 52 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (((𝐴 + 𝐵) / 2)(,)𝐵)) → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) |
54 | 24 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (((𝐴 + 𝐵) / 2)(,)𝐵)) → 𝐾 ∈ ℝ) |
55 | | dvbdfbdioolem2.dvbd |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝐾) |
56 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → ((ℝ D 𝐹)‘𝑥) = ((ℝ D 𝐹)‘𝑦)) |
57 | 56 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (abs‘((ℝ D 𝐹)‘𝑥)) = (abs‘((ℝ D 𝐹)‘𝑦))) |
58 | 57 | breq1d 4593 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → ((abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝐾 ↔ (abs‘((ℝ D 𝐹)‘𝑦)) ≤ 𝐾)) |
59 | 58 | cbvralv 3147 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
(𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝐾 ↔ ∀𝑦 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑦)) ≤ 𝐾) |
60 | 55, 59 | sylib 207 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑦 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑦)) ≤ 𝐾) |
61 | 60 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (((𝐴 + 𝐵) / 2)(,)𝐵)) → ∀𝑦 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑦)) ≤ 𝐾) |
62 | 18 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (((𝐴 + 𝐵) / 2)(,)𝐵)) → ((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵)) |
63 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (((𝐴 + 𝐵) / 2)(,)𝐵)) → 𝑥 ∈ (((𝐴 + 𝐵) / 2)(,)𝐵)) |
64 | 49, 50, 51, 53, 54, 61, 62, 63 | dvbdfbdioolem1 38818 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (((𝐴 + 𝐵) / 2)(,)𝐵)) → ((abs‘((𝐹‘𝑥) − (𝐹‘((𝐴 + 𝐵) / 2)))) ≤ (𝐾 · (𝑥 − ((𝐴 + 𝐵) / 2))) ∧ (abs‘((𝐹‘𝑥) − (𝐹‘((𝐴 + 𝐵) / 2)))) ≤ (𝐾 · (𝐵 − 𝐴)))) |
65 | 64 | simprd 478 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (((𝐴 + 𝐵) / 2)(,)𝐵)) → (abs‘((𝐹‘𝑥) − (𝐹‘((𝐴 + 𝐵) / 2)))) ≤ (𝐾 · (𝐵 − 𝐴))) |
66 | 34, 48, 65 | syl2anc 691 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ ((𝐴 + 𝐵) / 2) < 𝑥) → (abs‘((𝐹‘𝑥) − (𝐹‘((𝐴 + 𝐵) / 2)))) ≤ (𝐾 · (𝐵 − 𝐴))) |
67 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 + 𝐵) / 2) = 𝑥 → (𝐹‘((𝐴 + 𝐵) / 2)) = (𝐹‘𝑥)) |
68 | 67 | eqcomd 2616 |
. . . . . . . . . . . . 13
⊢ (((𝐴 + 𝐵) / 2) = 𝑥 → (𝐹‘𝑥) = (𝐹‘((𝐴 + 𝐵) / 2))) |
69 | 68 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝐴 + 𝐵) / 2) = 𝑥) → (𝐹‘𝑥) = (𝐹‘((𝐴 + 𝐵) / 2))) |
70 | 20 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝐴 + 𝐵) / 2) = 𝑥) → (𝐹‘((𝐴 + 𝐵) / 2)) ∈ ℂ) |
71 | 69, 70 | eqeltrd 2688 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝐴 + 𝐵) / 2) = 𝑥) → (𝐹‘𝑥) ∈ ℂ) |
72 | 71, 69 | subeq0bd 10335 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝐴 + 𝐵) / 2) = 𝑥) → ((𝐹‘𝑥) − (𝐹‘((𝐴 + 𝐵) / 2))) = 0) |
73 | 72 | abs00bd 13879 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝐴 + 𝐵) / 2) = 𝑥) → (abs‘((𝐹‘𝑥) − (𝐹‘((𝐴 + 𝐵) / 2)))) = 0) |
74 | 24 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝐴 + 𝐵) / 2) = 𝑥) → 𝐾 ∈ ℝ) |
75 | 7 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝐴 + 𝐵) / 2) = 𝑥) → 𝐵 ∈ ℝ) |
76 | 5 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝐴 + 𝐵) / 2) = 𝑥) → 𝐴 ∈ ℝ) |
77 | 75, 76 | resubcld 10337 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝐴 + 𝐵) / 2) = 𝑥) → (𝐵 − 𝐴) ∈ ℝ) |
78 | | 0red 9920 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ∈
ℝ) |
79 | | ioossre 12106 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴(,)𝐵) ⊆ ℝ |
80 | | dvfre 23520 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:(𝐴(,)𝐵)⟶ℝ ∧ (𝐴(,)𝐵) ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) |
81 | 1, 79, 80 | sylancl 693 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) |
82 | 18, 52 | eleqtrrd 2691 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐴 + 𝐵) / 2) ∈ dom (ℝ D 𝐹)) |
83 | 81, 82 | ffvelrnd 6268 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2)) ∈ ℝ) |
84 | 83 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2)) ∈ ℂ) |
85 | 84 | abscld 14023 |
. . . . . . . . . . . 12
⊢ (𝜑 → (abs‘((ℝ D
𝐹)‘((𝐴 + 𝐵) / 2))) ∈ ℝ) |
86 | 84 | absge0d 14031 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ≤
(abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2)))) |
87 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = ((𝐴 + 𝐵) / 2) → ((ℝ D 𝐹)‘𝑥) = ((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) |
88 | 87 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = ((𝐴 + 𝐵) / 2) → (abs‘((ℝ D 𝐹)‘𝑥)) = (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2)))) |
89 | 88 | breq1d 4593 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = ((𝐴 + 𝐵) / 2) → ((abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝐾 ↔ (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝐾)) |
90 | 89 | rspccva 3281 |
. . . . . . . . . . . . 13
⊢
((∀𝑥 ∈
(𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝐾 ∧ ((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵)) → (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝐾) |
91 | 55, 18, 90 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝜑 → (abs‘((ℝ D
𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝐾) |
92 | 78, 85, 24, 86, 91 | letrd 10073 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≤ 𝐾) |
93 | 92 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝐴 + 𝐵) / 2) = 𝑥) → 0 ≤ 𝐾) |
94 | 7, 5 | resubcld 10337 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ) |
95 | 5, 7 | posdifd 10493 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴))) |
96 | 11, 95 | mpbid 221 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 < (𝐵 − 𝐴)) |
97 | 78, 94, 96 | ltled 10064 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≤ (𝐵 − 𝐴)) |
98 | 97 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝐴 + 𝐵) / 2) = 𝑥) → 0 ≤ (𝐵 − 𝐴)) |
99 | 74, 77, 93, 98 | mulge0d 10483 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝐴 + 𝐵) / 2) = 𝑥) → 0 ≤ (𝐾 · (𝐵 − 𝐴))) |
100 | 73, 99 | eqbrtrd 4605 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝐴 + 𝐵) / 2) = 𝑥) → (abs‘((𝐹‘𝑥) − (𝐹‘((𝐴 + 𝐵) / 2)))) ≤ (𝐾 · (𝐵 − 𝐴))) |
101 | 100 | ad4ant14 1285 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ ¬ ((𝐴 + 𝐵) / 2) < 𝑥) ∧ ((𝐴 + 𝐵) / 2) = 𝑥) → (abs‘((𝐹‘𝑥) − (𝐹‘((𝐴 + 𝐵) / 2)))) ≤ (𝐾 · (𝐵 − 𝐴))) |
102 | | simpll 786 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ ¬ ((𝐴 + 𝐵) / 2) < 𝑥) ∧ ¬ ((𝐴 + 𝐵) / 2) = 𝑥) → (𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵))) |
103 | 39 | ad2antrr 758 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ ¬ ((𝐴 + 𝐵) / 2) < 𝑥) ∧ ¬ ((𝐴 + 𝐵) / 2) = 𝑥) → 𝑥 ∈ ℝ) |
104 | 10 | ad3antrrr 762 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ ¬ ((𝐴 + 𝐵) / 2) < 𝑥) ∧ ¬ ((𝐴 + 𝐵) / 2) = 𝑥) → ((𝐴 + 𝐵) / 2) ∈ ℝ) |
105 | 39 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ ¬ ((𝐴 + 𝐵) / 2) < 𝑥) → 𝑥 ∈ ℝ) |
106 | 10 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ ¬ ((𝐴 + 𝐵) / 2) < 𝑥) → ((𝐴 + 𝐵) / 2) ∈ ℝ) |
107 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ ¬ ((𝐴 + 𝐵) / 2) < 𝑥) → ¬ ((𝐴 + 𝐵) / 2) < 𝑥) |
108 | 105, 106,
107 | nltled 10066 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ ¬ ((𝐴 + 𝐵) / 2) < 𝑥) → 𝑥 ≤ ((𝐴 + 𝐵) / 2)) |
109 | 108 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ ¬ ((𝐴 + 𝐵) / 2) < 𝑥) ∧ ¬ ((𝐴 + 𝐵) / 2) = 𝑥) → 𝑥 ≤ ((𝐴 + 𝐵) / 2)) |
110 | | neqne 2790 |
. . . . . . . . . 10
⊢ (¬
((𝐴 + 𝐵) / 2) = 𝑥 → ((𝐴 + 𝐵) / 2) ≠ 𝑥) |
111 | 110 | adantl 481 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ ¬ ((𝐴 + 𝐵) / 2) < 𝑥) ∧ ¬ ((𝐴 + 𝐵) / 2) = 𝑥) → ((𝐴 + 𝐵) / 2) ≠ 𝑥) |
112 | 103, 104,
109, 111 | leneltd 10070 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ ¬ ((𝐴 + 𝐵) / 2) < 𝑥) ∧ ¬ ((𝐴 + 𝐵) / 2) = 𝑥) → 𝑥 < ((𝐴 + 𝐵) / 2)) |
113 | 3, 30 | abssubd 14040 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (abs‘((𝐹‘𝑥) − (𝐹‘((𝐴 + 𝐵) / 2)))) = (abs‘((𝐹‘((𝐴 + 𝐵) / 2)) − (𝐹‘𝑥)))) |
114 | 113 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑥 < ((𝐴 + 𝐵) / 2)) → (abs‘((𝐹‘𝑥) − (𝐹‘((𝐴 + 𝐵) / 2)))) = (abs‘((𝐹‘((𝐴 + 𝐵) / 2)) − (𝐹‘𝑥)))) |
115 | 5 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑥 < ((𝐴 + 𝐵) / 2)) → 𝐴 ∈ ℝ) |
116 | 7 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑥 < ((𝐴 + 𝐵) / 2)) → 𝐵 ∈ ℝ) |
117 | 1 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑥 < ((𝐴 + 𝐵) / 2)) → 𝐹:(𝐴(,)𝐵)⟶ℝ) |
118 | 52 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑥 < ((𝐴 + 𝐵) / 2)) → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) |
119 | 24 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑥 < ((𝐴 + 𝐵) / 2)) → 𝐾 ∈ ℝ) |
120 | 60 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑥 < ((𝐴 + 𝐵) / 2)) → ∀𝑦 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑦)) ≤ 𝐾) |
121 | 44 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑥 < ((𝐴 + 𝐵) / 2)) → 𝑥 ∈ (𝐴(,)𝐵)) |
122 | 38 | rexrd 9968 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 ∈ ℝ*) |
123 | 122 | ad2antlr 759 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑥 < ((𝐴 + 𝐵) / 2)) → 𝑥 ∈ ℝ*) |
124 | 8 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑥 < ((𝐴 + 𝐵) / 2)) → 𝐵 ∈
ℝ*) |
125 | 10 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑥 < ((𝐴 + 𝐵) / 2)) → ((𝐴 + 𝐵) / 2) ∈ ℝ) |
126 | | simpr 476 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑥 < ((𝐴 + 𝐵) / 2)) → 𝑥 < ((𝐴 + 𝐵) / 2)) |
127 | 17 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑥 < ((𝐴 + 𝐵) / 2)) → ((𝐴 + 𝐵) / 2) < 𝐵) |
128 | 123, 124,
125, 126, 127 | eliood 38567 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑥 < ((𝐴 + 𝐵) / 2)) → ((𝐴 + 𝐵) / 2) ∈ (𝑥(,)𝐵)) |
129 | 115, 116,
117, 118, 119, 120, 121, 128 | dvbdfbdioolem1 38818 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑥 < ((𝐴 + 𝐵) / 2)) → ((abs‘((𝐹‘((𝐴 + 𝐵) / 2)) − (𝐹‘𝑥))) ≤ (𝐾 · (((𝐴 + 𝐵) / 2) − 𝑥)) ∧ (abs‘((𝐹‘((𝐴 + 𝐵) / 2)) − (𝐹‘𝑥))) ≤ (𝐾 · (𝐵 − 𝐴)))) |
130 | 129 | simprd 478 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑥 < ((𝐴 + 𝐵) / 2)) → (abs‘((𝐹‘((𝐴 + 𝐵) / 2)) − (𝐹‘𝑥))) ≤ (𝐾 · (𝐵 − 𝐴))) |
131 | 114, 130 | eqbrtrd 4605 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑥 < ((𝐴 + 𝐵) / 2)) → (abs‘((𝐹‘𝑥) − (𝐹‘((𝐴 + 𝐵) / 2)))) ≤ (𝐾 · (𝐵 − 𝐴))) |
132 | 102, 112,
131 | syl2anc 691 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ ¬ ((𝐴 + 𝐵) / 2) < 𝑥) ∧ ¬ ((𝐴 + 𝐵) / 2) = 𝑥) → (abs‘((𝐹‘𝑥) − (𝐹‘((𝐴 + 𝐵) / 2)))) ≤ (𝐾 · (𝐵 − 𝐴))) |
133 | 101, 132 | pm2.61dan 828 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ ¬ ((𝐴 + 𝐵) / 2) < 𝑥) → (abs‘((𝐹‘𝑥) − (𝐹‘((𝐴 + 𝐵) / 2)))) ≤ (𝐾 · (𝐵 − 𝐴))) |
134 | 66, 133 | pm2.61dan 828 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (abs‘((𝐹‘𝑥) − (𝐹‘((𝐴 + 𝐵) / 2)))) ≤ (𝐾 · (𝐵 − 𝐴))) |
135 | 23, 32, 29, 33, 134 | letrd 10073 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((abs‘(𝐹‘𝑥)) − (abs‘(𝐹‘((𝐴 + 𝐵) / 2)))) ≤ (𝐾 · (𝐵 − 𝐴))) |
136 | 23, 29, 22, 135 | leadd1dd 10520 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((abs‘(𝐹‘𝑥)) − (abs‘(𝐹‘((𝐴 + 𝐵) / 2)))) + (abs‘(𝐹‘((𝐴 + 𝐵) / 2)))) ≤ ((𝐾 · (𝐵 − 𝐴)) + (abs‘(𝐹‘((𝐴 + 𝐵) / 2))))) |
137 | 4 | recnd 9947 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (abs‘(𝐹‘𝑥)) ∈ ℂ) |
138 | 22 | recnd 9947 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (abs‘(𝐹‘((𝐴 + 𝐵) / 2))) ∈ ℂ) |
139 | 137, 138 | npcand 10275 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((abs‘(𝐹‘𝑥)) − (abs‘(𝐹‘((𝐴 + 𝐵) / 2)))) + (abs‘(𝐹‘((𝐴 + 𝐵) / 2)))) = (abs‘(𝐹‘𝑥))) |
140 | 139 | eqcomd 2616 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (abs‘(𝐹‘𝑥)) = (((abs‘(𝐹‘𝑥)) − (abs‘(𝐹‘((𝐴 + 𝐵) / 2)))) + (abs‘(𝐹‘((𝐴 + 𝐵) / 2))))) |
141 | | dvbdfbdioolem2.m |
. . . . 5
⊢ 𝑀 = ((abs‘(𝐹‘((𝐴 + 𝐵) / 2))) + (𝐾 · (𝐵 − 𝐴))) |
142 | 21 | recnd 9947 |
. . . . . 6
⊢ (𝜑 → (abs‘(𝐹‘((𝐴 + 𝐵) / 2))) ∈ ℂ) |
143 | 24 | recnd 9947 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ ℂ) |
144 | 7 | recnd 9947 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℂ) |
145 | 5 | recnd 9947 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℂ) |
146 | 144, 145 | subcld 10271 |
. . . . . . 7
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℂ) |
147 | 143, 146 | mulcld 9939 |
. . . . . 6
⊢ (𝜑 → (𝐾 · (𝐵 − 𝐴)) ∈ ℂ) |
148 | 142, 147 | addcomd 10117 |
. . . . 5
⊢ (𝜑 → ((abs‘(𝐹‘((𝐴 + 𝐵) / 2))) + (𝐾 · (𝐵 − 𝐴))) = ((𝐾 · (𝐵 − 𝐴)) + (abs‘(𝐹‘((𝐴 + 𝐵) / 2))))) |
149 | 141, 148 | syl5eq 2656 |
. . . 4
⊢ (𝜑 → 𝑀 = ((𝐾 · (𝐵 − 𝐴)) + (abs‘(𝐹‘((𝐴 + 𝐵) / 2))))) |
150 | 149 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑀 = ((𝐾 · (𝐵 − 𝐴)) + (abs‘(𝐹‘((𝐴 + 𝐵) / 2))))) |
151 | 136, 140,
150 | 3brtr4d 4615 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (abs‘(𝐹‘𝑥)) ≤ 𝑀) |
152 | 151 | ralrimiva 2949 |
1
⊢ (𝜑 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑀) |