| Step | Hyp | Ref
| Expression |
| 1 | | dvbdfbdioolem2.f |
. . . . . . . 8
⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℝ) |
| 2 | 1 | ffvelcdmda 7104 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑥) ∈ ℝ) |
| 3 | 2 | recnd 11289 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑥) ∈ ℂ) |
| 4 | 3 | abscld 15475 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (abs‘(𝐹‘𝑥)) ∈ ℝ) |
| 5 | | dvbdfbdioolem2.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℝ) |
| 6 | 5 | rexrd 11311 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
| 7 | | dvbdfbdioolem2.b |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℝ) |
| 8 | 7 | rexrd 11311 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
| 9 | 5, 7 | readdcld 11290 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℝ) |
| 10 | 9 | rehalfcld 12513 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴 + 𝐵) / 2) ∈ ℝ) |
| 11 | | dvbdfbdioolem2.altb |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 < 𝐵) |
| 12 | | avglt1 12504 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 𝐴 < ((𝐴 + 𝐵) / 2))) |
| 13 | 5, 7, 12 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 < 𝐵 ↔ 𝐴 < ((𝐴 + 𝐵) / 2))) |
| 14 | 11, 13 | mpbid 232 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 < ((𝐴 + 𝐵) / 2)) |
| 15 | | avglt2 12505 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ((𝐴 + 𝐵) / 2) < 𝐵)) |
| 16 | 5, 7, 15 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 < 𝐵 ↔ ((𝐴 + 𝐵) / 2) < 𝐵)) |
| 17 | 11, 16 | mpbid 232 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴 + 𝐵) / 2) < 𝐵) |
| 18 | 6, 8, 10, 14, 17 | eliood 45511 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵)) |
| 19 | 1, 18 | ffvelcdmd 7105 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘((𝐴 + 𝐵) / 2)) ∈ ℝ) |
| 20 | 19 | recnd 11289 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘((𝐴 + 𝐵) / 2)) ∈ ℂ) |
| 21 | 20 | abscld 15475 |
. . . . . 6
⊢ (𝜑 → (abs‘(𝐹‘((𝐴 + 𝐵) / 2))) ∈ ℝ) |
| 22 | 21 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (abs‘(𝐹‘((𝐴 + 𝐵) / 2))) ∈ ℝ) |
| 23 | 4, 22 | resubcld 11691 |
. . . 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 11691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐵 − 𝐴) ∈ ℝ) |
| 29 | 25, 28 | remulcld 11291 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐾 · (𝐵 − 𝐴)) ∈ ℝ) |
| 30 | 20 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐹‘((𝐴 + 𝐵) / 2)) ∈ ℂ) |
| 31 | 3, 30 | subcld 11620 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((𝐹‘𝑥) − (𝐹‘((𝐴 + 𝐵) / 2))) ∈ ℂ) |
| 32 | 31 | abscld 15475 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (abs‘((𝐹‘𝑥) − (𝐹‘((𝐴 + 𝐵) / 2)))) ∈ ℝ) |
| 33 | 3, 30 | abs2difd 15496 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((abs‘(𝐹‘𝑥)) − (abs‘(𝐹‘((𝐴 + 𝐵) / 2)))) ≤ (abs‘((𝐹‘𝑥) − (𝐹‘((𝐴 + 𝐵) / 2))))) |
| 34 | | simpll 767 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ ((𝐴 + 𝐵) / 2) < 𝑥) → 𝜑) |
| 35 | 10 | rexrd 11311 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴 + 𝐵) / 2) ∈
ℝ*) |
| 36 | 35 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ ((𝐴 + 𝐵) / 2) < 𝑥) → ((𝐴 + 𝐵) / 2) ∈
ℝ*) |
| 37 | 8 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ ((𝐴 + 𝐵) / 2) < 𝑥) → 𝐵 ∈
ℝ*) |
| 38 | | elioore 13417 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 ∈ ℝ) |
| 39 | 38 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ ℝ) |
| 40 | 39 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ ((𝐴 + 𝐵) / 2) < 𝑥) → 𝑥 ∈ ℝ) |
| 41 | | simpr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ ((𝐴 + 𝐵) / 2) < 𝑥) → ((𝐴 + 𝐵) / 2) < 𝑥) |
| 42 | 6 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝐴 ∈
ℝ*) |
| 43 | 8 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝐵 ∈
ℝ*) |
| 44 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ (𝐴(,)𝐵)) |
| 45 | | iooltub 45523 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑥
∈ (𝐴(,)𝐵)) → 𝑥 < 𝐵) |
| 46 | 42, 43, 44, 45 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 < 𝐵) |
| 47 | 46 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ ((𝐴 + 𝐵) / 2) < 𝑥) → 𝑥 < 𝐵) |
| 48 | 36, 37, 40, 41, 47 | eliood 45511 |
. . . . . . 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 | | 2fveq3 6911 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (abs‘((ℝ D 𝐹)‘𝑥)) = (abs‘((ℝ D 𝐹)‘𝑦))) |
| 57 | 56 | breq1d 5153 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → ((abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝐾 ↔ (abs‘((ℝ D 𝐹)‘𝑦)) ≤ 𝐾)) |
| 58 | 57 | cbvralvw 3237 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
(𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝐾 ↔ ∀𝑦 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑦)) ≤ 𝐾) |
| 59 | 55, 58 | sylib 218 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑦 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑦)) ≤ 𝐾) |
| 60 | 59 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (((𝐴 + 𝐵) / 2)(,)𝐵)) → ∀𝑦 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑦)) ≤ 𝐾) |
| 61 | 18 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (((𝐴 + 𝐵) / 2)(,)𝐵)) → ((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵)) |
| 62 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (((𝐴 + 𝐵) / 2)(,)𝐵)) → 𝑥 ∈ (((𝐴 + 𝐵) / 2)(,)𝐵)) |
| 63 | 49, 50, 51, 53, 54, 60, 61, 62 | dvbdfbdioolem1 45943 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (((𝐴 + 𝐵) / 2)(,)𝐵)) → ((abs‘((𝐹‘𝑥) − (𝐹‘((𝐴 + 𝐵) / 2)))) ≤ (𝐾 · (𝑥 − ((𝐴 + 𝐵) / 2))) ∧ (abs‘((𝐹‘𝑥) − (𝐹‘((𝐴 + 𝐵) / 2)))) ≤ (𝐾 · (𝐵 − 𝐴)))) |
| 64 | 63 | simprd 495 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (((𝐴 + 𝐵) / 2)(,)𝐵)) → (abs‘((𝐹‘𝑥) − (𝐹‘((𝐴 + 𝐵) / 2)))) ≤ (𝐾 · (𝐵 − 𝐴))) |
| 65 | 34, 48, 64 | syl2anc 584 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ ((𝐴 + 𝐵) / 2) < 𝑥) → (abs‘((𝐹‘𝑥) − (𝐹‘((𝐴 + 𝐵) / 2)))) ≤ (𝐾 · (𝐵 − 𝐴))) |
| 66 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 + 𝐵) / 2) = 𝑥 → (𝐹‘((𝐴 + 𝐵) / 2)) = (𝐹‘𝑥)) |
| 67 | 66 | eqcomd 2743 |
. . . . . . . . . . . . 13
⊢ (((𝐴 + 𝐵) / 2) = 𝑥 → (𝐹‘𝑥) = (𝐹‘((𝐴 + 𝐵) / 2))) |
| 68 | 67 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝐴 + 𝐵) / 2) = 𝑥) → (𝐹‘𝑥) = (𝐹‘((𝐴 + 𝐵) / 2))) |
| 69 | 20 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝐴 + 𝐵) / 2) = 𝑥) → (𝐹‘((𝐴 + 𝐵) / 2)) ∈ ℂ) |
| 70 | 68, 69 | eqeltrd 2841 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝐴 + 𝐵) / 2) = 𝑥) → (𝐹‘𝑥) ∈ ℂ) |
| 71 | 70, 68 | subeq0bd 11689 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝐴 + 𝐵) / 2) = 𝑥) → ((𝐹‘𝑥) − (𝐹‘((𝐴 + 𝐵) / 2))) = 0) |
| 72 | 71 | abs00bd 15330 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝐴 + 𝐵) / 2) = 𝑥) → (abs‘((𝐹‘𝑥) − (𝐹‘((𝐴 + 𝐵) / 2)))) = 0) |
| 73 | 24 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝐴 + 𝐵) / 2) = 𝑥) → 𝐾 ∈ ℝ) |
| 74 | 7 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝐴 + 𝐵) / 2) = 𝑥) → 𝐵 ∈ ℝ) |
| 75 | 5 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝐴 + 𝐵) / 2) = 𝑥) → 𝐴 ∈ ℝ) |
| 76 | 74, 75 | resubcld 11691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝐴 + 𝐵) / 2) = 𝑥) → (𝐵 − 𝐴) ∈ ℝ) |
| 77 | | 0red 11264 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ∈
ℝ) |
| 78 | | ioossre 13448 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴(,)𝐵) ⊆ ℝ |
| 79 | | dvfre 25989 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:(𝐴(,)𝐵)⟶ℝ ∧ (𝐴(,)𝐵) ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) |
| 80 | 1, 78, 79 | sylancl 586 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) |
| 81 | 18, 52 | eleqtrrd 2844 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐴 + 𝐵) / 2) ∈ dom (ℝ D 𝐹)) |
| 82 | 80, 81 | ffvelcdmd 7105 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2)) ∈ ℝ) |
| 83 | 82 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2)) ∈ ℂ) |
| 84 | 83 | abscld 15475 |
. . . . . . . . . . . 12
⊢ (𝜑 → (abs‘((ℝ D
𝐹)‘((𝐴 + 𝐵) / 2))) ∈ ℝ) |
| 85 | 83 | absge0d 15483 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ≤
(abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2)))) |
| 86 | | 2fveq3 6911 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = ((𝐴 + 𝐵) / 2) → (abs‘((ℝ D 𝐹)‘𝑥)) = (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2)))) |
| 87 | 86 | breq1d 5153 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = ((𝐴 + 𝐵) / 2) → ((abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝐾 ↔ (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝐾)) |
| 88 | 87 | rspccva 3621 |
. . . . . . . . . . . . 13
⊢
((∀𝑥 ∈
(𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝐾 ∧ ((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵)) → (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝐾) |
| 89 | 55, 18, 88 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → (abs‘((ℝ D
𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝐾) |
| 90 | 77, 84, 24, 85, 89 | letrd 11418 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≤ 𝐾) |
| 91 | 90 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝐴 + 𝐵) / 2) = 𝑥) → 0 ≤ 𝐾) |
| 92 | 7, 5 | resubcld 11691 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ) |
| 93 | 5, 7 | posdifd 11850 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴))) |
| 94 | 11, 93 | mpbid 232 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 < (𝐵 − 𝐴)) |
| 95 | 77, 92, 94 | ltled 11409 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≤ (𝐵 − 𝐴)) |
| 96 | 95 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝐴 + 𝐵) / 2) = 𝑥) → 0 ≤ (𝐵 − 𝐴)) |
| 97 | 73, 76, 91, 96 | mulge0d 11840 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝐴 + 𝐵) / 2) = 𝑥) → 0 ≤ (𝐾 · (𝐵 − 𝐴))) |
| 98 | 72, 97 | eqbrtrd 5165 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝐴 + 𝐵) / 2) = 𝑥) → (abs‘((𝐹‘𝑥) − (𝐹‘((𝐴 + 𝐵) / 2)))) ≤ (𝐾 · (𝐵 − 𝐴))) |
| 99 | 98 | ad4ant14 752 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ ¬ ((𝐴 + 𝐵) / 2) < 𝑥) ∧ ((𝐴 + 𝐵) / 2) = 𝑥) → (abs‘((𝐹‘𝑥) − (𝐹‘((𝐴 + 𝐵) / 2)))) ≤ (𝐾 · (𝐵 − 𝐴))) |
| 100 | | simpll 767 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ ¬ ((𝐴 + 𝐵) / 2) < 𝑥) ∧ ¬ ((𝐴 + 𝐵) / 2) = 𝑥) → (𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵))) |
| 101 | 39 | ad2antrr 726 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ ¬ ((𝐴 + 𝐵) / 2) < 𝑥) ∧ ¬ ((𝐴 + 𝐵) / 2) = 𝑥) → 𝑥 ∈ ℝ) |
| 102 | 10 | ad3antrrr 730 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ ¬ ((𝐴 + 𝐵) / 2) < 𝑥) ∧ ¬ ((𝐴 + 𝐵) / 2) = 𝑥) → ((𝐴 + 𝐵) / 2) ∈ ℝ) |
| 103 | 39 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ ¬ ((𝐴 + 𝐵) / 2) < 𝑥) → 𝑥 ∈ ℝ) |
| 104 | 10 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ ¬ ((𝐴 + 𝐵) / 2) < 𝑥) → ((𝐴 + 𝐵) / 2) ∈ ℝ) |
| 105 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ ¬ ((𝐴 + 𝐵) / 2) < 𝑥) → ¬ ((𝐴 + 𝐵) / 2) < 𝑥) |
| 106 | 103, 104,
105 | nltled 11411 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ ¬ ((𝐴 + 𝐵) / 2) < 𝑥) → 𝑥 ≤ ((𝐴 + 𝐵) / 2)) |
| 107 | 106 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ ¬ ((𝐴 + 𝐵) / 2) < 𝑥) ∧ ¬ ((𝐴 + 𝐵) / 2) = 𝑥) → 𝑥 ≤ ((𝐴 + 𝐵) / 2)) |
| 108 | | neqne 2948 |
. . . . . . . . . 10
⊢ (¬
((𝐴 + 𝐵) / 2) = 𝑥 → ((𝐴 + 𝐵) / 2) ≠ 𝑥) |
| 109 | 108 | adantl 481 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ ¬ ((𝐴 + 𝐵) / 2) < 𝑥) ∧ ¬ ((𝐴 + 𝐵) / 2) = 𝑥) → ((𝐴 + 𝐵) / 2) ≠ 𝑥) |
| 110 | 101, 102,
107, 109 | leneltd 11415 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ ¬ ((𝐴 + 𝐵) / 2) < 𝑥) ∧ ¬ ((𝐴 + 𝐵) / 2) = 𝑥) → 𝑥 < ((𝐴 + 𝐵) / 2)) |
| 111 | 3, 30 | abssubd 15492 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (abs‘((𝐹‘𝑥) − (𝐹‘((𝐴 + 𝐵) / 2)))) = (abs‘((𝐹‘((𝐴 + 𝐵) / 2)) − (𝐹‘𝑥)))) |
| 112 | 111 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑥 < ((𝐴 + 𝐵) / 2)) → (abs‘((𝐹‘𝑥) − (𝐹‘((𝐴 + 𝐵) / 2)))) = (abs‘((𝐹‘((𝐴 + 𝐵) / 2)) − (𝐹‘𝑥)))) |
| 113 | 5 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑥 < ((𝐴 + 𝐵) / 2)) → 𝐴 ∈ ℝ) |
| 114 | 7 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑥 < ((𝐴 + 𝐵) / 2)) → 𝐵 ∈ ℝ) |
| 115 | 1 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑥 < ((𝐴 + 𝐵) / 2)) → 𝐹:(𝐴(,)𝐵)⟶ℝ) |
| 116 | 52 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑥 < ((𝐴 + 𝐵) / 2)) → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) |
| 117 | 24 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑥 < ((𝐴 + 𝐵) / 2)) → 𝐾 ∈ ℝ) |
| 118 | 59 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑥 < ((𝐴 + 𝐵) / 2)) → ∀𝑦 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑦)) ≤ 𝐾) |
| 119 | 44 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑥 < ((𝐴 + 𝐵) / 2)) → 𝑥 ∈ (𝐴(,)𝐵)) |
| 120 | 38 | rexrd 11311 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 ∈ ℝ*) |
| 121 | 120 | ad2antlr 727 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑥 < ((𝐴 + 𝐵) / 2)) → 𝑥 ∈ ℝ*) |
| 122 | 8 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑥 < ((𝐴 + 𝐵) / 2)) → 𝐵 ∈
ℝ*) |
| 123 | 10 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑥 < ((𝐴 + 𝐵) / 2)) → ((𝐴 + 𝐵) / 2) ∈ ℝ) |
| 124 | | simpr 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑥 < ((𝐴 + 𝐵) / 2)) → 𝑥 < ((𝐴 + 𝐵) / 2)) |
| 125 | 17 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑥 < ((𝐴 + 𝐵) / 2)) → ((𝐴 + 𝐵) / 2) < 𝐵) |
| 126 | 121, 122,
123, 124, 125 | eliood 45511 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑥 < ((𝐴 + 𝐵) / 2)) → ((𝐴 + 𝐵) / 2) ∈ (𝑥(,)𝐵)) |
| 127 | 113, 114,
115, 116, 117, 118, 119, 126 | dvbdfbdioolem1 45943 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑥 < ((𝐴 + 𝐵) / 2)) → ((abs‘((𝐹‘((𝐴 + 𝐵) / 2)) − (𝐹‘𝑥))) ≤ (𝐾 · (((𝐴 + 𝐵) / 2) − 𝑥)) ∧ (abs‘((𝐹‘((𝐴 + 𝐵) / 2)) − (𝐹‘𝑥))) ≤ (𝐾 · (𝐵 − 𝐴)))) |
| 128 | 127 | simprd 495 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑥 < ((𝐴 + 𝐵) / 2)) → (abs‘((𝐹‘((𝐴 + 𝐵) / 2)) − (𝐹‘𝑥))) ≤ (𝐾 · (𝐵 − 𝐴))) |
| 129 | 112, 128 | eqbrtrd 5165 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑥 < ((𝐴 + 𝐵) / 2)) → (abs‘((𝐹‘𝑥) − (𝐹‘((𝐴 + 𝐵) / 2)))) ≤ (𝐾 · (𝐵 − 𝐴))) |
| 130 | 100, 110,
129 | syl2anc 584 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ ¬ ((𝐴 + 𝐵) / 2) < 𝑥) ∧ ¬ ((𝐴 + 𝐵) / 2) = 𝑥) → (abs‘((𝐹‘𝑥) − (𝐹‘((𝐴 + 𝐵) / 2)))) ≤ (𝐾 · (𝐵 − 𝐴))) |
| 131 | 99, 130 | pm2.61dan 813 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ ¬ ((𝐴 + 𝐵) / 2) < 𝑥) → (abs‘((𝐹‘𝑥) − (𝐹‘((𝐴 + 𝐵) / 2)))) ≤ (𝐾 · (𝐵 − 𝐴))) |
| 132 | 65, 131 | pm2.61dan 813 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (abs‘((𝐹‘𝑥) − (𝐹‘((𝐴 + 𝐵) / 2)))) ≤ (𝐾 · (𝐵 − 𝐴))) |
| 133 | 23, 32, 29, 33, 132 | letrd 11418 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((abs‘(𝐹‘𝑥)) − (abs‘(𝐹‘((𝐴 + 𝐵) / 2)))) ≤ (𝐾 · (𝐵 − 𝐴))) |
| 134 | 23, 29, 22, 133 | leadd1dd 11877 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((abs‘(𝐹‘𝑥)) − (abs‘(𝐹‘((𝐴 + 𝐵) / 2)))) + (abs‘(𝐹‘((𝐴 + 𝐵) / 2)))) ≤ ((𝐾 · (𝐵 − 𝐴)) + (abs‘(𝐹‘((𝐴 + 𝐵) / 2))))) |
| 135 | 4 | recnd 11289 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (abs‘(𝐹‘𝑥)) ∈ ℂ) |
| 136 | 22 | recnd 11289 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (abs‘(𝐹‘((𝐴 + 𝐵) / 2))) ∈ ℂ) |
| 137 | 135, 136 | npcand 11624 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((abs‘(𝐹‘𝑥)) − (abs‘(𝐹‘((𝐴 + 𝐵) / 2)))) + (abs‘(𝐹‘((𝐴 + 𝐵) / 2)))) = (abs‘(𝐹‘𝑥))) |
| 138 | 137 | eqcomd 2743 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (abs‘(𝐹‘𝑥)) = (((abs‘(𝐹‘𝑥)) − (abs‘(𝐹‘((𝐴 + 𝐵) / 2)))) + (abs‘(𝐹‘((𝐴 + 𝐵) / 2))))) |
| 139 | | dvbdfbdioolem2.m |
. . . . 5
⊢ 𝑀 = ((abs‘(𝐹‘((𝐴 + 𝐵) / 2))) + (𝐾 · (𝐵 − 𝐴))) |
| 140 | 21 | recnd 11289 |
. . . . . 6
⊢ (𝜑 → (abs‘(𝐹‘((𝐴 + 𝐵) / 2))) ∈ ℂ) |
| 141 | 24 | recnd 11289 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ ℂ) |
| 142 | 7 | recnd 11289 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℂ) |
| 143 | 5 | recnd 11289 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℂ) |
| 144 | 142, 143 | subcld 11620 |
. . . . . . 7
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℂ) |
| 145 | 141, 144 | mulcld 11281 |
. . . . . 6
⊢ (𝜑 → (𝐾 · (𝐵 − 𝐴)) ∈ ℂ) |
| 146 | 140, 145 | addcomd 11463 |
. . . . 5
⊢ (𝜑 → ((abs‘(𝐹‘((𝐴 + 𝐵) / 2))) + (𝐾 · (𝐵 − 𝐴))) = ((𝐾 · (𝐵 − 𝐴)) + (abs‘(𝐹‘((𝐴 + 𝐵) / 2))))) |
| 147 | 139, 146 | eqtrid 2789 |
. . . 4
⊢ (𝜑 → 𝑀 = ((𝐾 · (𝐵 − 𝐴)) + (abs‘(𝐹‘((𝐴 + 𝐵) / 2))))) |
| 148 | 147 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑀 = ((𝐾 · (𝐵 − 𝐴)) + (abs‘(𝐹‘((𝐴 + 𝐵) / 2))))) |
| 149 | 134, 138,
148 | 3brtr4d 5175 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (abs‘(𝐹‘𝑥)) ≤ 𝑀) |
| 150 | 149 | ralrimiva 3146 |
1
⊢ (𝜑 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑀) |