Step | Hyp | Ref
| Expression |
1 | | dvfsum.s |
. . . 4
⊢ 𝑆 = (𝑇(,)+∞) |
2 | | ioossre 12996 |
. . . 4
⊢ (𝑇(,)+∞) ⊆
ℝ |
3 | 1, 2 | eqsstri 3935 |
. . 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 24922 |
. . 3
⊢ (𝜑 → 𝐺:𝑆⟶ℝ) |
17 | | ax-resscn 10786 |
. . 3
⊢ ℝ
⊆ ℂ |
18 | | fss 6562 |
. . 3
⊢ ((𝐺:𝑆⟶ℝ ∧ ℝ ⊆
ℂ) → 𝐺:𝑆⟶ℂ) |
19 | 16, 17, 18 | sylancl 589 |
. 2
⊢ (𝜑 → 𝐺:𝑆⟶ℂ) |
20 | 1 | supeq1i 9063 |
. . 3
⊢ sup(𝑆, ℝ*, < ) =
sup((𝑇(,)+∞),
ℝ*, < ) |
21 | | ressxr 10877 |
. . . . 5
⊢ ℝ
⊆ ℝ* |
22 | 21, 9 | sseldi 3899 |
. . . 4
⊢ (𝜑 → 𝑇 ∈
ℝ*) |
23 | 9 | renepnfd 10884 |
. . . 4
⊢ (𝜑 → 𝑇 ≠ +∞) |
24 | | ioopnfsup 13437 |
. . . 4
⊢ ((𝑇 ∈ ℝ*
∧ 𝑇 ≠ +∞)
→ sup((𝑇(,)+∞),
ℝ*, < ) = +∞) |
25 | 22, 23, 24 | syl2anc 587 |
. . 3
⊢ (𝜑 → sup((𝑇(,)+∞), ℝ*, < ) =
+∞) |
26 | 20, 25 | syl5eq 2790 |
. 2
⊢ (𝜑 → sup(𝑆, ℝ*, < ) =
+∞) |
27 | | dvfsumrlim.k |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ 𝐵) ⇝𝑟
0) |
28 | 11, 27 | rlimmptrcl 15169 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ ℂ) |
29 | 28 | ralrimiva 3105 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝑆 𝐵 ∈ ℂ) |
30 | 29, 4 | rlim0 15069 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ 𝐵) ⇝𝑟 0 ↔
∀𝑒 ∈
ℝ+ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒))) |
31 | 27, 30 | mpbid 235 |
. . 3
⊢ (𝜑 → ∀𝑒 ∈ ℝ+ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒)) |
32 | 3 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → 𝑆 ⊆
ℝ) |
33 | | peano2re 11005 |
. . . . . . . . 9
⊢ (𝑇 ∈ ℝ → (𝑇 + 1) ∈
ℝ) |
34 | 9, 33 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑇 + 1) ∈ ℝ) |
35 | 34, 7 | ifcld 4485 |
. . . . . . 7
⊢ (𝜑 → if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷) ∈ ℝ) |
36 | 35 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷) ∈ ℝ) |
37 | | rexico 14917 |
. . . . . 6
⊢ ((𝑆 ⊆ ℝ ∧ if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷) ∈ ℝ) → (∃𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒) ↔ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒))) |
38 | 32, 36, 37 | syl2anc 587 |
. . . . 5
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) →
(∃𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒) ↔ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒))) |
39 | | elicopnf 13033 |
. . . . . . . . . . . . . 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 502 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → 𝑐 ∈ ℝ) |
42 | 9 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → 𝑇 ∈ ℝ) |
43 | 42, 33 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → (𝑇 + 1) ∈ ℝ) |
44 | 42 | ltp1d 11762 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → 𝑇 < (𝑇 + 1)) |
45 | 40 | simplbda 503 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷) ≤ 𝑐) |
46 | 7 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → 𝐷 ∈ ℝ) |
47 | | maxle 12781 |
. . . . . . . . . . . . . . . 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 235 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → (𝐷 ≤ 𝑐 ∧ (𝑇 + 1) ≤ 𝑐)) |
50 | 49 | simprd 499 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → (𝑇 + 1) ≤ 𝑐) |
51 | 42, 43, 41, 44, 50 | ltletrd 10992 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → 𝑇 < 𝑐) |
52 | 22 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → 𝑇 ∈
ℝ*) |
53 | | elioopnf 13031 |
. . . . . . . . . . . . 13
⊢ (𝑇 ∈ ℝ*
→ (𝑐 ∈ (𝑇(,)+∞) ↔ (𝑐 ∈ ℝ ∧ 𝑇 < 𝑐))) |
54 | 52, 53 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → (𝑐 ∈ (𝑇(,)+∞) ↔ (𝑐 ∈ ℝ ∧ 𝑇 < 𝑐))) |
55 | 41, 51, 54 | mpbir2and 713 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → 𝑐 ∈ (𝑇(,)+∞)) |
56 | 55, 1 | eleqtrrdi 2849 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → 𝑐 ∈ 𝑆) |
57 | 49 | simpld 498 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → 𝐷 ≤ 𝑐) |
58 | 56, 57 | jca 515 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) |
59 | 58 | adantlr 715 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) |
60 | | simprrl 781 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐))) → 𝑐 ∈ 𝑆) |
61 | 60 | adantrr 717 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → 𝑐 ∈ 𝑆) |
62 | 3, 61 | sseldi 3899 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → 𝑐 ∈ ℝ) |
63 | 62 | leidd 11398 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → 𝑐 ≤ 𝑐) |
64 | | nfv 1922 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥 𝑐 ≤ 𝑐 |
65 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑥abs |
66 | | nfcsb1v 3836 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑥⦋𝑐 / 𝑥⦌𝐵 |
67 | 65, 66 | nffv 6727 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥(abs‘⦋𝑐 / 𝑥⦌𝐵) |
68 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥
< |
69 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥𝑒 |
70 | 67, 68, 69 | nfbr 5100 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥(abs‘⦋𝑐 / 𝑥⦌𝐵) < 𝑒 |
71 | 64, 70 | nfim 1904 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥(𝑐 ≤ 𝑐 → (abs‘⦋𝑐 / 𝑥⦌𝐵) < 𝑒) |
72 | | breq2 5057 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑐 → (𝑐 ≤ 𝑥 ↔ 𝑐 ≤ 𝑐)) |
73 | | csbeq1a 3825 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑐 → 𝐵 = ⦋𝑐 / 𝑥⦌𝐵) |
74 | 73 | fveq2d 6721 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑐 → (abs‘𝐵) = (abs‘⦋𝑐 / 𝑥⦌𝐵)) |
75 | 74 | breq1d 5063 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑐 → ((abs‘𝐵) < 𝑒 ↔ (abs‘⦋𝑐 / 𝑥⦌𝐵) < 𝑒)) |
76 | 72, 75 | imbi12d 348 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑐 → ((𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒) ↔ (𝑐 ≤ 𝑐 → (abs‘⦋𝑐 / 𝑥⦌𝐵) < 𝑒))) |
77 | 71, 76 | rspc 3525 |
. . . . . . . . . . . . . . . . 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 24921 |
. . . . . . . . . . . . . . . . . . . . . . . . 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 24927 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) → 0 ≤ 𝐵) |
84 | | elrege0 13042 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐵 ∈ (0[,)+∞) ↔
(𝐵 ∈ ℝ ∧ 0
≤ 𝐵)) |
85 | 81, 83, 84 | sylanbrc 586 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) → 𝐵 ∈ (0[,)+∞)) |
86 | 85 | expr 460 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐷 ≤ 𝑥 → 𝐵 ∈ (0[,)+∞))) |
87 | 86 | ralrimiva 3105 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ∀𝑥 ∈ 𝑆 (𝐷 ≤ 𝑥 → 𝐵 ∈ (0[,)+∞))) |
88 | 87 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → ∀𝑥 ∈ 𝑆 (𝐷 ≤ 𝑥 → 𝐵 ∈ (0[,)+∞))) |
89 | | simprrr 782 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐))) → 𝐷 ≤ 𝑐) |
90 | 89 | adantrr 717 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → 𝐷 ≤ 𝑐) |
91 | | nfv 1922 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑥 𝐷 ≤ 𝑐 |
92 | 66 | nfel1 2920 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑥⦋𝑐 / 𝑥⦌𝐵 ∈ (0[,)+∞) |
93 | 91, 92 | nfim 1904 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑥(𝐷 ≤ 𝑐 → ⦋𝑐 / 𝑥⦌𝐵 ∈ (0[,)+∞)) |
94 | | breq2 5057 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑐 → (𝐷 ≤ 𝑥 ↔ 𝐷 ≤ 𝑐)) |
95 | 73 | eleq1d 2822 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑐 → (𝐵 ∈ (0[,)+∞) ↔
⦋𝑐 / 𝑥⦌𝐵 ∈ (0[,)+∞))) |
96 | 94, 95 | imbi12d 348 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑐 → ((𝐷 ≤ 𝑥 → 𝐵 ∈ (0[,)+∞)) ↔ (𝐷 ≤ 𝑐 → ⦋𝑐 / 𝑥⦌𝐵 ∈ (0[,)+∞)))) |
97 | 93, 96 | rspc 3525 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑐 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 (𝐷 ≤ 𝑥 → 𝐵 ∈ (0[,)+∞)) → (𝐷 ≤ 𝑐 → ⦋𝑐 / 𝑥⦌𝐵 ∈ (0[,)+∞)))) |
98 | 61, 88, 90, 97 | syl3c 66 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → ⦋𝑐 / 𝑥⦌𝐵 ∈ (0[,)+∞)) |
99 | | elrege0 13042 |
. . . . . . . . . . . . . . . . . . 19
⊢
(⦋𝑐 /
𝑥⦌𝐵 ∈ (0[,)+∞) ↔
(⦋𝑐 / 𝑥⦌𝐵 ∈ ℝ ∧ 0 ≤
⦋𝑐 / 𝑥⦌𝐵)) |
100 | 98, 99 | sylib 221 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → (⦋𝑐 / 𝑥⦌𝐵 ∈ ℝ ∧ 0 ≤
⦋𝑐 / 𝑥⦌𝐵)) |
101 | | absid 14860 |
. . . . . . . . . . . . . . . . . 18
⊢
((⦋𝑐 /
𝑥⦌𝐵 ∈ ℝ ∧ 0 ≤
⦋𝑐 / 𝑥⦌𝐵) → (abs‘⦋𝑐 / 𝑥⦌𝐵) = ⦋𝑐 / 𝑥⦌𝐵) |
102 | 100, 101 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → (abs‘⦋𝑐 / 𝑥⦌𝐵) = ⦋𝑐 / 𝑥⦌𝐵) |
103 | 102 | breq1d 5063 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → ((abs‘⦋𝑐 / 𝑥⦌𝐵) < 𝑒 ↔ ⦋𝑐 / 𝑥⦌𝐵 < 𝑒)) |
104 | 6 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → 𝑀 ∈ ℤ) |
105 | 7 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → 𝐷 ∈ ℝ) |
106 | 8 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → 𝑀 ≤ (𝐷 + 1)) |
107 | 9 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → 𝑇 ∈ ℝ) |
108 | 10 | adantlr 715 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ) |
109 | 11 | adantlr 715 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉) |
110 | 12 | adantlr 715 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ) |
111 | 13 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵)) |
112 | | pnfxr 10887 |
. . . . . . . . . . . . . . . . . . 19
⊢ +∞
∈ ℝ* |
113 | 112 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → +∞ ∈
ℝ*) |
114 | | 3simpa 1150 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ +∞) → (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘)) |
115 | 114, 82 | syl3an3 1167 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ +∞)) → 𝐶 ≤ 𝐵) |
116 | 115 | 3adant1r 1179 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ +∞)) → 𝐶 ≤ 𝐵) |
117 | 83 | 3adantr3 1173 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ +∞)) → 0 ≤ 𝐵) |
118 | 117 | adantlr 715 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ +∞)) → 0 ≤ 𝐵) |
119 | | simprrl 781 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → 𝑦 ∈ 𝑆) |
120 | | simprrr 782 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → 𝑐 ≤ 𝑦) |
121 | 3, 21 | sstri 3910 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑆 ⊆
ℝ* |
122 | 121, 119 | sseldi 3899 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → 𝑦 ∈ ℝ*) |
123 | | pnfge 12722 |
. . . . . . . . . . . . . . . . . . 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 24926 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) ≤ ⦋𝑐 / 𝑥⦌𝐵) |
126 | 19 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → 𝐺:𝑆⟶ℂ) |
127 | 126, 119 | ffvelrnd 6905 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → (𝐺‘𝑦) ∈ ℂ) |
128 | 126, 61 | ffvelrnd 6905 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → (𝐺‘𝑐) ∈ ℂ) |
129 | 127, 128 | subcld 11189 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → ((𝐺‘𝑦) − (𝐺‘𝑐)) ∈ ℂ) |
130 | 129 | abscld 15000 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) ∈ ℝ) |
131 | 100 | simpld 498 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → ⦋𝑐 / 𝑥⦌𝐵 ∈ ℝ) |
132 | | simprll 779 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → 𝑒 ∈ ℝ+) |
133 | 132 | rpred 12628 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → 𝑒 ∈ ℝ) |
134 | | lelttr 10923 |
. . . . . . . . . . . . . . . . . 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 243 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → ((abs‘⦋𝑐 / 𝑥⦌𝐵) < 𝑒 → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) < 𝑒)) |
138 | 79, 137 | syld 47 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → (∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒) → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) < 𝑒)) |
139 | 138 | anassrs 471 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐))) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦)) → (∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒) → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) < 𝑒)) |
140 | 139 | expr 460 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐))) ∧ 𝑦 ∈ 𝑆) → (𝑐 ≤ 𝑦 → (∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒) → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) < 𝑒))) |
141 | 140 | com23 86 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐))) ∧ 𝑦 ∈ 𝑆) → (∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒) → (𝑐 ≤ 𝑦 → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) < 𝑒))) |
142 | 141 | ralrimdva 3110 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐))) → (∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒) → ∀𝑦 ∈ 𝑆 (𝑐 ≤ 𝑦 → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) < 𝑒))) |
143 | 142, 60 | jctild 529 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐))) → (∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒) → (𝑐 ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 (𝑐 ≤ 𝑦 → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) < 𝑒)))) |
144 | 143 | anassrs 471 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) → (∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒) → (𝑐 ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 (𝑐 ≤ 𝑦 → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) < 𝑒)))) |
145 | 59, 144 | syldan 594 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → (∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒) → (𝑐 ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 (𝑐 ≤ 𝑦 → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) < 𝑒)))) |
146 | 145 | expimpd 457 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → ((𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞) ∧ ∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒)) → (𝑐 ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 (𝑐 ≤ 𝑦 → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) < 𝑒)))) |
147 | 146 | reximdv2 3190 |
. . . . 5
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) →
(∃𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒) → ∃𝑐 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑐 ≤ 𝑦 → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) < 𝑒))) |
148 | 38, 147 | sylbird 263 |
. . . 4
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) →
(∃𝑐 ∈ ℝ
∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒) → ∃𝑐 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑐 ≤ 𝑦 → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) < 𝑒))) |
149 | 148 | ralimdva 3100 |
. . 3
⊢ (𝜑 → (∀𝑒 ∈ ℝ+
∃𝑐 ∈ ℝ
∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒) → ∀𝑒 ∈ ℝ+ ∃𝑐 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑐 ≤ 𝑦 → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) < 𝑒))) |
150 | 31, 149 | mpd 15 |
. 2
⊢ (𝜑 → ∀𝑒 ∈ ℝ+ ∃𝑐 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑐 ≤ 𝑦 → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) < 𝑒)) |
151 | 4, 19, 26, 150 | caucvgr 15239 |
1
⊢ (𝜑 → 𝐺 ∈ dom ⇝𝑟
) |