| Step | Hyp | Ref
| Expression |
| 1 | | dvfsum.s |
. . . 4
⊢ 𝑆 = (𝑇(,)+∞) |
| 2 | | ioossre 13448 |
. . . 4
⊢ (𝑇(,)+∞) ⊆
ℝ |
| 3 | 1, 2 | eqsstri 4030 |
. . 3
⊢ 𝑆 ⊆
ℝ |
| 4 | 3 | a1i 11 |
. 2
⊢ (𝜑 → 𝑆 ⊆ ℝ) |
| 5 | | dvfsum.z |
. . . 4
⊢ 𝑍 =
(ℤ≥‘𝑀) |
| 6 | | dvfsum.m |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 7 | | dvfsum.d |
. . . 4
⊢ (𝜑 → 𝐷 ∈ ℝ) |
| 8 | | dvfsum.md |
. . . 4
⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1)) |
| 9 | | dvfsum.t |
. . . 4
⊢ (𝜑 → 𝑇 ∈ ℝ) |
| 10 | | dvfsum.a |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ) |
| 11 | | dvfsum.b1 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉) |
| 12 | | dvfsum.b2 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ) |
| 13 | | dvfsum.b3 |
. . . 4
⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵)) |
| 14 | | dvfsum.c |
. . . 4
⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶) |
| 15 | | dvfsumrlim.g |
. . . 4
⊢ 𝐺 = (𝑥 ∈ 𝑆 ↦ (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴)) |
| 16 | 1, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15 | dvfsumrlimf 26065 |
. . 3
⊢ (𝜑 → 𝐺:𝑆⟶ℝ) |
| 17 | | ax-resscn 11212 |
. . 3
⊢ ℝ
⊆ ℂ |
| 18 | | fss 6752 |
. . 3
⊢ ((𝐺:𝑆⟶ℝ ∧ ℝ ⊆
ℂ) → 𝐺:𝑆⟶ℂ) |
| 19 | 16, 17, 18 | sylancl 586 |
. 2
⊢ (𝜑 → 𝐺:𝑆⟶ℂ) |
| 20 | 1 | supeq1i 9487 |
. . 3
⊢ sup(𝑆, ℝ*, < ) =
sup((𝑇(,)+∞),
ℝ*, < ) |
| 21 | | ressxr 11305 |
. . . . 5
⊢ ℝ
⊆ ℝ* |
| 22 | 21, 9 | sselid 3981 |
. . . 4
⊢ (𝜑 → 𝑇 ∈
ℝ*) |
| 23 | 9 | renepnfd 11312 |
. . . 4
⊢ (𝜑 → 𝑇 ≠ +∞) |
| 24 | | ioopnfsup 13904 |
. . . 4
⊢ ((𝑇 ∈ ℝ*
∧ 𝑇 ≠ +∞)
→ sup((𝑇(,)+∞),
ℝ*, < ) = +∞) |
| 25 | 22, 23, 24 | syl2anc 584 |
. . 3
⊢ (𝜑 → sup((𝑇(,)+∞), ℝ*, < ) =
+∞) |
| 26 | 20, 25 | eqtrid 2789 |
. 2
⊢ (𝜑 → sup(𝑆, ℝ*, < ) =
+∞) |
| 27 | | dvfsumrlim.k |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ 𝐵) ⇝𝑟
0) |
| 28 | 11, 27 | rlimmptrcl 15644 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ ℂ) |
| 29 | 28 | ralrimiva 3146 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝑆 𝐵 ∈ ℂ) |
| 30 | 29, 4 | rlim0 15544 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ 𝐵) ⇝𝑟 0 ↔
∀𝑒 ∈
ℝ+ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒))) |
| 31 | 27, 30 | mpbid 232 |
. . 3
⊢ (𝜑 → ∀𝑒 ∈ ℝ+ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒)) |
| 32 | 3 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → 𝑆 ⊆
ℝ) |
| 33 | | peano2re 11434 |
. . . . . . . . 9
⊢ (𝑇 ∈ ℝ → (𝑇 + 1) ∈
ℝ) |
| 34 | 9, 33 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑇 + 1) ∈ ℝ) |
| 35 | 34, 7 | ifcld 4572 |
. . . . . . 7
⊢ (𝜑 → if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷) ∈ ℝ) |
| 36 | 35 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷) ∈ ℝ) |
| 37 | | rexico 15392 |
. . . . . 6
⊢ ((𝑆 ⊆ ℝ ∧ if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷) ∈ ℝ) → (∃𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒) ↔ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒))) |
| 38 | 32, 36, 37 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) →
(∃𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒) ↔ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒))) |
| 39 | | elicopnf 13485 |
. . . . . . . . . . . . . 14
⊢ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷) ∈ ℝ → (𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞) ↔ (𝑐 ∈ ℝ ∧ if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷) ≤ 𝑐))) |
| 40 | 35, 39 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞) ↔ (𝑐 ∈ ℝ ∧ if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷) ≤ 𝑐))) |
| 41 | 40 | simprbda 498 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → 𝑐 ∈ ℝ) |
| 42 | 9 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → 𝑇 ∈ ℝ) |
| 43 | 42, 33 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → (𝑇 + 1) ∈ ℝ) |
| 44 | 42 | ltp1d 12198 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → 𝑇 < (𝑇 + 1)) |
| 45 | 40 | simplbda 499 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷) ≤ 𝑐) |
| 46 | 7 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → 𝐷 ∈ ℝ) |
| 47 | | maxle 13233 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ ℝ ∧ (𝑇 + 1) ∈ ℝ ∧ 𝑐 ∈ ℝ) →
(if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷) ≤ 𝑐 ↔ (𝐷 ≤ 𝑐 ∧ (𝑇 + 1) ≤ 𝑐))) |
| 48 | 46, 43, 41, 47 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷) ≤ 𝑐 ↔ (𝐷 ≤ 𝑐 ∧ (𝑇 + 1) ≤ 𝑐))) |
| 49 | 45, 48 | mpbid 232 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → (𝐷 ≤ 𝑐 ∧ (𝑇 + 1) ≤ 𝑐)) |
| 50 | 49 | simprd 495 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → (𝑇 + 1) ≤ 𝑐) |
| 51 | 42, 43, 41, 44, 50 | ltletrd 11421 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → 𝑇 < 𝑐) |
| 52 | 22 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → 𝑇 ∈
ℝ*) |
| 53 | | elioopnf 13483 |
. . . . . . . . . . . . 13
⊢ (𝑇 ∈ ℝ*
→ (𝑐 ∈ (𝑇(,)+∞) ↔ (𝑐 ∈ ℝ ∧ 𝑇 < 𝑐))) |
| 54 | 52, 53 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → (𝑐 ∈ (𝑇(,)+∞) ↔ (𝑐 ∈ ℝ ∧ 𝑇 < 𝑐))) |
| 55 | 41, 51, 54 | mpbir2and 713 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → 𝑐 ∈ (𝑇(,)+∞)) |
| 56 | 55, 1 | eleqtrrdi 2852 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → 𝑐 ∈ 𝑆) |
| 57 | 49 | simpld 494 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → 𝐷 ≤ 𝑐) |
| 58 | 56, 57 | jca 511 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) |
| 59 | 58 | adantlr 715 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) |
| 60 | | simprrl 781 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐))) → 𝑐 ∈ 𝑆) |
| 61 | 60 | adantrr 717 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → 𝑐 ∈ 𝑆) |
| 62 | 3, 61 | sselid 3981 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → 𝑐 ∈ ℝ) |
| 63 | 62 | leidd 11829 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → 𝑐 ≤ 𝑐) |
| 64 | | nfv 1914 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥 𝑐 ≤ 𝑐 |
| 65 | | nfcv 2905 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑥abs |
| 66 | | nfcsb1v 3923 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑥⦋𝑐 / 𝑥⦌𝐵 |
| 67 | 65, 66 | nffv 6916 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥(abs‘⦋𝑐 / 𝑥⦌𝐵) |
| 68 | | nfcv 2905 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥
< |
| 69 | | nfcv 2905 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥𝑒 |
| 70 | 67, 68, 69 | nfbr 5190 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥(abs‘⦋𝑐 / 𝑥⦌𝐵) < 𝑒 |
| 71 | 64, 70 | nfim 1896 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥(𝑐 ≤ 𝑐 → (abs‘⦋𝑐 / 𝑥⦌𝐵) < 𝑒) |
| 72 | | breq2 5147 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑐 → (𝑐 ≤ 𝑥 ↔ 𝑐 ≤ 𝑐)) |
| 73 | | csbeq1a 3913 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑐 → 𝐵 = ⦋𝑐 / 𝑥⦌𝐵) |
| 74 | 73 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑐 → (abs‘𝐵) = (abs‘⦋𝑐 / 𝑥⦌𝐵)) |
| 75 | 74 | breq1d 5153 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑐 → ((abs‘𝐵) < 𝑒 ↔ (abs‘⦋𝑐 / 𝑥⦌𝐵) < 𝑒)) |
| 76 | 72, 75 | imbi12d 344 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑐 → ((𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒) ↔ (𝑐 ≤ 𝑐 → (abs‘⦋𝑐 / 𝑥⦌𝐵) < 𝑒))) |
| 77 | 71, 76 | rspc 3610 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒) → (𝑐 ≤ 𝑐 → (abs‘⦋𝑐 / 𝑥⦌𝐵) < 𝑒))) |
| 78 | 61, 77 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → (∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒) → (𝑐 ≤ 𝑐 → (abs‘⦋𝑐 / 𝑥⦌𝐵) < 𝑒))) |
| 79 | 63, 78 | mpid 44 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → (∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒) → (abs‘⦋𝑐 / 𝑥⦌𝐵) < 𝑒)) |
| 80 | 4, 10, 11, 13 | dvmptrecl 26064 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ ℝ) |
| 81 | 80 | adantrr 717 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) → 𝐵 ∈ ℝ) |
| 82 | | dvfsumrlim.l |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘)) → 𝐶 ≤ 𝐵) |
| 83 | 1, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 82, 15, 27 | dvfsumrlimge0 26071 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) → 0 ≤ 𝐵) |
| 84 | | elrege0 13494 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐵 ∈ (0[,)+∞) ↔
(𝐵 ∈ ℝ ∧ 0
≤ 𝐵)) |
| 85 | 81, 83, 84 | sylanbrc 583 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) → 𝐵 ∈ (0[,)+∞)) |
| 86 | 85 | expr 456 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐷 ≤ 𝑥 → 𝐵 ∈ (0[,)+∞))) |
| 87 | 86 | ralrimiva 3146 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ∀𝑥 ∈ 𝑆 (𝐷 ≤ 𝑥 → 𝐵 ∈ (0[,)+∞))) |
| 88 | 87 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → ∀𝑥 ∈ 𝑆 (𝐷 ≤ 𝑥 → 𝐵 ∈ (0[,)+∞))) |
| 89 | | simprrr 782 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐))) → 𝐷 ≤ 𝑐) |
| 90 | 89 | adantrr 717 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → 𝐷 ≤ 𝑐) |
| 91 | | nfv 1914 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑥 𝐷 ≤ 𝑐 |
| 92 | 66 | nfel1 2922 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑥⦋𝑐 / 𝑥⦌𝐵 ∈ (0[,)+∞) |
| 93 | 91, 92 | nfim 1896 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑥(𝐷 ≤ 𝑐 → ⦋𝑐 / 𝑥⦌𝐵 ∈ (0[,)+∞)) |
| 94 | | breq2 5147 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑐 → (𝐷 ≤ 𝑥 ↔ 𝐷 ≤ 𝑐)) |
| 95 | 73 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑐 → (𝐵 ∈ (0[,)+∞) ↔
⦋𝑐 / 𝑥⦌𝐵 ∈ (0[,)+∞))) |
| 96 | 94, 95 | imbi12d 344 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑐 → ((𝐷 ≤ 𝑥 → 𝐵 ∈ (0[,)+∞)) ↔ (𝐷 ≤ 𝑐 → ⦋𝑐 / 𝑥⦌𝐵 ∈ (0[,)+∞)))) |
| 97 | 93, 96 | rspc 3610 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑐 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 (𝐷 ≤ 𝑥 → 𝐵 ∈ (0[,)+∞)) → (𝐷 ≤ 𝑐 → ⦋𝑐 / 𝑥⦌𝐵 ∈ (0[,)+∞)))) |
| 98 | 61, 88, 90, 97 | syl3c 66 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → ⦋𝑐 / 𝑥⦌𝐵 ∈ (0[,)+∞)) |
| 99 | | elrege0 13494 |
. . . . . . . . . . . . . . . . . . 19
⊢
(⦋𝑐 /
𝑥⦌𝐵 ∈ (0[,)+∞) ↔
(⦋𝑐 / 𝑥⦌𝐵 ∈ ℝ ∧ 0 ≤
⦋𝑐 / 𝑥⦌𝐵)) |
| 100 | 98, 99 | sylib 218 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → (⦋𝑐 / 𝑥⦌𝐵 ∈ ℝ ∧ 0 ≤
⦋𝑐 / 𝑥⦌𝐵)) |
| 101 | | absid 15335 |
. . . . . . . . . . . . . . . . . 18
⊢
((⦋𝑐 /
𝑥⦌𝐵 ∈ ℝ ∧ 0 ≤
⦋𝑐 / 𝑥⦌𝐵) → (abs‘⦋𝑐 / 𝑥⦌𝐵) = ⦋𝑐 / 𝑥⦌𝐵) |
| 102 | 100, 101 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → (abs‘⦋𝑐 / 𝑥⦌𝐵) = ⦋𝑐 / 𝑥⦌𝐵) |
| 103 | 102 | breq1d 5153 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → ((abs‘⦋𝑐 / 𝑥⦌𝐵) < 𝑒 ↔ ⦋𝑐 / 𝑥⦌𝐵 < 𝑒)) |
| 104 | 6 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → 𝑀 ∈ ℤ) |
| 105 | 7 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → 𝐷 ∈ ℝ) |
| 106 | 8 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → 𝑀 ≤ (𝐷 + 1)) |
| 107 | 9 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → 𝑇 ∈ ℝ) |
| 108 | 10 | adantlr 715 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ) |
| 109 | 11 | adantlr 715 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉) |
| 110 | 12 | adantlr 715 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ) |
| 111 | 13 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵)) |
| 112 | | pnfxr 11315 |
. . . . . . . . . . . . . . . . . . 19
⊢ +∞
∈ ℝ* |
| 113 | 112 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → +∞ ∈
ℝ*) |
| 114 | | 3simpa 1149 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ +∞) → (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘)) |
| 115 | 114, 82 | syl3an3 1166 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ +∞)) → 𝐶 ≤ 𝐵) |
| 116 | 115 | 3adant1r 1178 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ +∞)) → 𝐶 ≤ 𝐵) |
| 117 | 83 | 3adantr3 1172 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ +∞)) → 0 ≤ 𝐵) |
| 118 | 117 | adantlr 715 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ +∞)) → 0 ≤ 𝐵) |
| 119 | | simprrl 781 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → 𝑦 ∈ 𝑆) |
| 120 | | simprrr 782 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → 𝑐 ≤ 𝑦) |
| 121 | 3, 21 | sstri 3993 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑆 ⊆
ℝ* |
| 122 | 121, 119 | sselid 3981 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → 𝑦 ∈ ℝ*) |
| 123 | | pnfge 13172 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ℝ*
→ 𝑦 ≤
+∞) |
| 124 | 122, 123 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → 𝑦 ≤ +∞) |
| 125 | 1, 5, 104, 105, 106, 107, 108, 109, 110, 111, 14, 113, 116, 15, 118, 61, 119, 90, 120, 124 | dvfsumlem4 26070 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) ≤ ⦋𝑐 / 𝑥⦌𝐵) |
| 126 | 19 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → 𝐺:𝑆⟶ℂ) |
| 127 | 126, 119 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → (𝐺‘𝑦) ∈ ℂ) |
| 128 | 126, 61 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → (𝐺‘𝑐) ∈ ℂ) |
| 129 | 127, 128 | subcld 11620 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → ((𝐺‘𝑦) − (𝐺‘𝑐)) ∈ ℂ) |
| 130 | 129 | abscld 15475 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) ∈ ℝ) |
| 131 | 100 | simpld 494 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → ⦋𝑐 / 𝑥⦌𝐵 ∈ ℝ) |
| 132 | | simprll 779 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → 𝑒 ∈ ℝ+) |
| 133 | 132 | rpred 13077 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → 𝑒 ∈ ℝ) |
| 134 | | lelttr 11351 |
. . . . . . . . . . . . . . . . . 18
⊢
(((abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) ∈ ℝ ∧ ⦋𝑐 / 𝑥⦌𝐵 ∈ ℝ ∧ 𝑒 ∈ ℝ) → (((abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) ≤ ⦋𝑐 / 𝑥⦌𝐵 ∧ ⦋𝑐 / 𝑥⦌𝐵 < 𝑒) → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) < 𝑒)) |
| 135 | 130, 131,
133, 134 | syl3anc 1373 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → (((abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) ≤ ⦋𝑐 / 𝑥⦌𝐵 ∧ ⦋𝑐 / 𝑥⦌𝐵 < 𝑒) → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) < 𝑒)) |
| 136 | 125, 135 | mpand 695 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → (⦋𝑐 / 𝑥⦌𝐵 < 𝑒 → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) < 𝑒)) |
| 137 | 103, 136 | sylbid 240 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → ((abs‘⦋𝑐 / 𝑥⦌𝐵) < 𝑒 → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) < 𝑒)) |
| 138 | 79, 137 | syld 47 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → (∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒) → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) < 𝑒)) |
| 139 | 138 | anassrs 467 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐))) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦)) → (∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒) → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) < 𝑒)) |
| 140 | 139 | expr 456 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐))) ∧ 𝑦 ∈ 𝑆) → (𝑐 ≤ 𝑦 → (∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒) → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) < 𝑒))) |
| 141 | 140 | com23 86 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐))) ∧ 𝑦 ∈ 𝑆) → (∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒) → (𝑐 ≤ 𝑦 → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) < 𝑒))) |
| 142 | 141 | ralrimdva 3154 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐))) → (∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒) → ∀𝑦 ∈ 𝑆 (𝑐 ≤ 𝑦 → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) < 𝑒))) |
| 143 | 142, 60 | jctild 525 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐))) → (∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒) → (𝑐 ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 (𝑐 ≤ 𝑦 → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) < 𝑒)))) |
| 144 | 143 | anassrs 467 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) → (∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒) → (𝑐 ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 (𝑐 ≤ 𝑦 → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) < 𝑒)))) |
| 145 | 59, 144 | syldan 591 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → (∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒) → (𝑐 ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 (𝑐 ≤ 𝑦 → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) < 𝑒)))) |
| 146 | 145 | expimpd 453 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → ((𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞) ∧ ∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒)) → (𝑐 ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 (𝑐 ≤ 𝑦 → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) < 𝑒)))) |
| 147 | 146 | reximdv2 3164 |
. . . . 5
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) →
(∃𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒) → ∃𝑐 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑐 ≤ 𝑦 → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) < 𝑒))) |
| 148 | 38, 147 | sylbird 260 |
. . . 4
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) →
(∃𝑐 ∈ ℝ
∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒) → ∃𝑐 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑐 ≤ 𝑦 → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) < 𝑒))) |
| 149 | 148 | ralimdva 3167 |
. . 3
⊢ (𝜑 → (∀𝑒 ∈ ℝ+
∃𝑐 ∈ ℝ
∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒) → ∀𝑒 ∈ ℝ+ ∃𝑐 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑐 ≤ 𝑦 → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) < 𝑒))) |
| 150 | 31, 149 | mpd 15 |
. 2
⊢ (𝜑 → ∀𝑒 ∈ ℝ+ ∃𝑐 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑐 ≤ 𝑦 → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) < 𝑒)) |
| 151 | 4, 19, 26, 150 | caucvgr 15712 |
1
⊢ (𝜑 → 𝐺 ∈ dom ⇝𝑟
) |