MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dvfsumrlim Structured version   Visualization version   GIF version

Theorem dvfsumrlim 25258
Description: Compare a finite sum to an integral (the integral here is given as a function with a known derivative). The statement here says that if 𝑥𝑆𝐵 is a decreasing function with antiderivative 𝐴 converging to zero, then the difference between Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐵(𝑘) and 𝐴(𝑥) = ∫𝑢 ∈ (𝑀[,]𝑥)𝐵(𝑢) d𝑢 converges to a constant limit value, with the remainder term bounded by 𝐵(𝑥). (Contributed by Mario Carneiro, 18-May-2016.)
Hypotheses
Ref Expression
dvfsum.s 𝑆 = (𝑇(,)+∞)
dvfsum.z 𝑍 = (ℤ𝑀)
dvfsum.m (𝜑𝑀 ∈ ℤ)
dvfsum.d (𝜑𝐷 ∈ ℝ)
dvfsum.md (𝜑𝑀 ≤ (𝐷 + 1))
dvfsum.t (𝜑𝑇 ∈ ℝ)
dvfsum.a ((𝜑𝑥𝑆) → 𝐴 ∈ ℝ)
dvfsum.b1 ((𝜑𝑥𝑆) → 𝐵𝑉)
dvfsum.b2 ((𝜑𝑥𝑍) → 𝐵 ∈ ℝ)
dvfsum.b3 (𝜑 → (ℝ D (𝑥𝑆𝐴)) = (𝑥𝑆𝐵))
dvfsum.c (𝑥 = 𝑘𝐵 = 𝐶)
dvfsumrlim.l ((𝜑 ∧ (𝑥𝑆𝑘𝑆) ∧ (𝐷𝑥𝑥𝑘)) → 𝐶𝐵)
dvfsumrlim.g 𝐺 = (𝑥𝑆 ↦ (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶𝐴))
dvfsumrlim.k (𝜑 → (𝑥𝑆𝐵) ⇝𝑟 0)
Assertion
Ref Expression
dvfsumrlim (𝜑𝐺 ∈ dom ⇝𝑟 )
Distinct variable groups:   𝐵,𝑘   𝑥,𝐶   𝑥,𝑘,𝐷   𝜑,𝑘,𝑥   𝑆,𝑘,𝑥   𝑘,𝑀,𝑥   𝑥,𝑇   𝑥,𝑍
Allowed substitution hints:   𝐴(𝑥,𝑘)   𝐵(𝑥)   𝐶(𝑘)   𝑇(𝑘)   𝐺(𝑥,𝑘)   𝑉(𝑥,𝑘)   𝑍(𝑘)

Proof of Theorem dvfsumrlim
Dummy variables 𝑦 𝑒 𝑐 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dvfsum.s . . . 4 𝑆 = (𝑇(,)+∞)
2 ioossre 13200 . . . 4 (𝑇(,)+∞) ⊆ ℝ
31, 2eqsstri 3959 . . 3 𝑆 ⊆ ℝ
43a1i 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 𝐺 = (𝑥𝑆 ↦ (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶𝐴))
161, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15dvfsumrlimf 25252 . . 3 (𝜑𝐺:𝑆⟶ℝ)
17 ax-resscn 10988 . . 3 ℝ ⊆ ℂ
18 fss 6647 . . 3 ((𝐺:𝑆⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐺:𝑆⟶ℂ)
1916, 17, 18sylancl 586 . 2 (𝜑𝐺:𝑆⟶ℂ)
201supeq1i 9264 . . 3 sup(𝑆, ℝ*, < ) = sup((𝑇(,)+∞), ℝ*, < )
21 ressxr 11079 . . . . 5 ℝ ⊆ ℝ*
2221, 9sselid 3923 . . . 4 (𝜑𝑇 ∈ ℝ*)
239renepnfd 11086 . . . 4 (𝜑𝑇 ≠ +∞)
24 ioopnfsup 13644 . . . 4 ((𝑇 ∈ ℝ*𝑇 ≠ +∞) → sup((𝑇(,)+∞), ℝ*, < ) = +∞)
2522, 23, 24syl2anc 584 . . 3 (𝜑 → sup((𝑇(,)+∞), ℝ*, < ) = +∞)
2620, 25eqtrid 2787 . 2 (𝜑 → sup(𝑆, ℝ*, < ) = +∞)
27 dvfsumrlim.k . . . 4 (𝜑 → (𝑥𝑆𝐵) ⇝𝑟 0)
2811, 27rlimmptrcl 15376 . . . . . 6 ((𝜑𝑥𝑆) → 𝐵 ∈ ℂ)
2928ralrimiva 3138 . . . . 5 (𝜑 → ∀𝑥𝑆 𝐵 ∈ ℂ)
3029, 4rlim0 15276 . . . 4 (𝜑 → ((𝑥𝑆𝐵) ⇝𝑟 0 ↔ ∀𝑒 ∈ ℝ+𝑐 ∈ ℝ ∀𝑥𝑆 (𝑐𝑥 → (abs‘𝐵) < 𝑒)))
3127, 30mpbid 231 . . 3 (𝜑 → ∀𝑒 ∈ ℝ+𝑐 ∈ ℝ ∀𝑥𝑆 (𝑐𝑥 → (abs‘𝐵) < 𝑒))
323a1i 11 . . . . . 6 ((𝜑𝑒 ∈ ℝ+) → 𝑆 ⊆ ℝ)
33 peano2re 11208 . . . . . . . . 9 (𝑇 ∈ ℝ → (𝑇 + 1) ∈ ℝ)
349, 33syl 17 . . . . . . . 8 (𝜑 → (𝑇 + 1) ∈ ℝ)
3534, 7ifcld 4510 . . . . . . 7 (𝜑 → if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷) ∈ ℝ)
3635adantr 481 . . . . . 6 ((𝜑𝑒 ∈ ℝ+) → if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷) ∈ ℝ)
37 rexico 15124 . . . . . 6 ((𝑆 ⊆ ℝ ∧ if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷) ∈ ℝ) → (∃𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)∀𝑥𝑆 (𝑐𝑥 → (abs‘𝐵) < 𝑒) ↔ ∃𝑐 ∈ ℝ ∀𝑥𝑆 (𝑐𝑥 → (abs‘𝐵) < 𝑒)))
3832, 36, 37syl2anc 584 . . . . 5 ((𝜑𝑒 ∈ ℝ+) → (∃𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)∀𝑥𝑆 (𝑐𝑥 → (abs‘𝐵) < 𝑒) ↔ ∃𝑐 ∈ ℝ ∀𝑥𝑆 (𝑐𝑥 → (abs‘𝐵) < 𝑒)))
39 elicopnf 13237 . . . . . . . . . . . . . 14 (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷) ∈ ℝ → (𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞) ↔ (𝑐 ∈ ℝ ∧ if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷) ≤ 𝑐)))
4035, 39syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞) ↔ (𝑐 ∈ ℝ ∧ if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷) ≤ 𝑐)))
4140simprbda 499 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → 𝑐 ∈ ℝ)
429adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → 𝑇 ∈ ℝ)
4342, 33syl 17 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → (𝑇 + 1) ∈ ℝ)
4442ltp1d 11965 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → 𝑇 < (𝑇 + 1))
4540simplbda 500 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷) ≤ 𝑐)
467adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → 𝐷 ∈ ℝ)
47 maxle 12985 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ ℝ ∧ (𝑇 + 1) ∈ ℝ ∧ 𝑐 ∈ ℝ) → (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷) ≤ 𝑐 ↔ (𝐷𝑐 ∧ (𝑇 + 1) ≤ 𝑐)))
4846, 43, 41, 47syl3anc 1370 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷) ≤ 𝑐 ↔ (𝐷𝑐 ∧ (𝑇 + 1) ≤ 𝑐)))
4945, 48mpbid 231 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → (𝐷𝑐 ∧ (𝑇 + 1) ≤ 𝑐))
5049simprd 496 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → (𝑇 + 1) ≤ 𝑐)
5142, 43, 41, 44, 50ltletrd 11195 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → 𝑇 < 𝑐)
5222adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → 𝑇 ∈ ℝ*)
53 elioopnf 13235 . . . . . . . . . . . . 13 (𝑇 ∈ ℝ* → (𝑐 ∈ (𝑇(,)+∞) ↔ (𝑐 ∈ ℝ ∧ 𝑇 < 𝑐)))
5452, 53syl 17 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → (𝑐 ∈ (𝑇(,)+∞) ↔ (𝑐 ∈ ℝ ∧ 𝑇 < 𝑐)))
5541, 51, 54mpbir2and 710 . . . . . . . . . . 11 ((𝜑𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → 𝑐 ∈ (𝑇(,)+∞))
5655, 1eleqtrrdi 2847 . . . . . . . . . 10 ((𝜑𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → 𝑐𝑆)
5749simpld 495 . . . . . . . . . 10 ((𝜑𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → 𝐷𝑐)
5856, 57jca 512 . . . . . . . . 9 ((𝜑𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → (𝑐𝑆𝐷𝑐))
5958adantlr 712 . . . . . . . 8 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → (𝑐𝑆𝐷𝑐))
60 simprrl 778 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐))) → 𝑐𝑆)
6160adantrr 714 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐)) ∧ (𝑦𝑆𝑐𝑦))) → 𝑐𝑆)
623, 61sselid 3923 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐)) ∧ (𝑦𝑆𝑐𝑦))) → 𝑐 ∈ ℝ)
6362leidd 11601 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐)) ∧ (𝑦𝑆𝑐𝑦))) → 𝑐𝑐)
64 nfv 1914 . . . . . . . . . . . . . . . . . . 19 𝑥 𝑐𝑐
65 nfcv 2903 . . . . . . . . . . . . . . . . . . . . 21 𝑥abs
66 nfcsb1v 3861 . . . . . . . . . . . . . . . . . . . . 21 𝑥𝑐 / 𝑥𝐵
6765, 66nffv 6814 . . . . . . . . . . . . . . . . . . . 20 𝑥(abs‘𝑐 / 𝑥𝐵)
68 nfcv 2903 . . . . . . . . . . . . . . . . . . . 20 𝑥 <
69 nfcv 2903 . . . . . . . . . . . . . . . . . . . 20 𝑥𝑒
7067, 68, 69nfbr 5127 . . . . . . . . . . . . . . . . . . 19 𝑥(abs‘𝑐 / 𝑥𝐵) < 𝑒
7164, 70nfim 1896 . . . . . . . . . . . . . . . . . 18 𝑥(𝑐𝑐 → (abs‘𝑐 / 𝑥𝐵) < 𝑒)
72 breq2 5084 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑐 → (𝑐𝑥𝑐𝑐))
73 csbeq1a 3850 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑐𝐵 = 𝑐 / 𝑥𝐵)
7473fveq2d 6808 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑐 → (abs‘𝐵) = (abs‘𝑐 / 𝑥𝐵))
7574breq1d 5090 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑐 → ((abs‘𝐵) < 𝑒 ↔ (abs‘𝑐 / 𝑥𝐵) < 𝑒))
7672, 75imbi12d 344 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑐 → ((𝑐𝑥 → (abs‘𝐵) < 𝑒) ↔ (𝑐𝑐 → (abs‘𝑐 / 𝑥𝐵) < 𝑒)))
7771, 76rspc 3553 . . . . . . . . . . . . . . . . 17 (𝑐𝑆 → (∀𝑥𝑆 (𝑐𝑥 → (abs‘𝐵) < 𝑒) → (𝑐𝑐 → (abs‘𝑐 / 𝑥𝐵) < 𝑒)))
7861, 77syl 17 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐)) ∧ (𝑦𝑆𝑐𝑦))) → (∀𝑥𝑆 (𝑐𝑥 → (abs‘𝐵) < 𝑒) → (𝑐𝑐 → (abs‘𝑐 / 𝑥𝐵) < 𝑒)))
7963, 78mpid 44 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐)) ∧ (𝑦𝑆𝑐𝑦))) → (∀𝑥𝑆 (𝑐𝑥 → (abs‘𝐵) < 𝑒) → (abs‘𝑐 / 𝑥𝐵) < 𝑒))
804, 10, 11, 13dvmptrecl 25251 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑥𝑆) → 𝐵 ∈ ℝ)
8180adantrr 714 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑥𝑆𝐷𝑥)) → 𝐵 ∈ ℝ)
82 dvfsumrlim.l . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑥𝑆𝑘𝑆) ∧ (𝐷𝑥𝑥𝑘)) → 𝐶𝐵)
831, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 82, 15, 27dvfsumrlimge0 25257 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑥𝑆𝐷𝑥)) → 0 ≤ 𝐵)
84 elrege0 13246 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐵 ∈ (0[,)+∞) ↔ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵))
8581, 83, 84sylanbrc 583 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑥𝑆𝐷𝑥)) → 𝐵 ∈ (0[,)+∞))
8685expr 457 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥𝑆) → (𝐷𝑥𝐵 ∈ (0[,)+∞)))
8786ralrimiva 3138 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ∀𝑥𝑆 (𝐷𝑥𝐵 ∈ (0[,)+∞)))
8887adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐)) ∧ (𝑦𝑆𝑐𝑦))) → ∀𝑥𝑆 (𝐷𝑥𝐵 ∈ (0[,)+∞)))
89 simprrr 779 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐))) → 𝐷𝑐)
9089adantrr 714 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐)) ∧ (𝑦𝑆𝑐𝑦))) → 𝐷𝑐)
91 nfv 1914 . . . . . . . . . . . . . . . . . . . . . 22 𝑥 𝐷𝑐
9266nfel1 2919 . . . . . . . . . . . . . . . . . . . . . 22 𝑥𝑐 / 𝑥𝐵 ∈ (0[,)+∞)
9391, 92nfim 1896 . . . . . . . . . . . . . . . . . . . . 21 𝑥(𝐷𝑐𝑐 / 𝑥𝐵 ∈ (0[,)+∞))
94 breq2 5084 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑐 → (𝐷𝑥𝐷𝑐))
9573eleq1d 2820 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑐 → (𝐵 ∈ (0[,)+∞) ↔ 𝑐 / 𝑥𝐵 ∈ (0[,)+∞)))
9694, 95imbi12d 344 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑐 → ((𝐷𝑥𝐵 ∈ (0[,)+∞)) ↔ (𝐷𝑐𝑐 / 𝑥𝐵 ∈ (0[,)+∞))))
9793, 96rspc 3553 . . . . . . . . . . . . . . . . . . . 20 (𝑐𝑆 → (∀𝑥𝑆 (𝐷𝑥𝐵 ∈ (0[,)+∞)) → (𝐷𝑐𝑐 / 𝑥𝐵 ∈ (0[,)+∞))))
9861, 88, 90, 97syl3c 66 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐)) ∧ (𝑦𝑆𝑐𝑦))) → 𝑐 / 𝑥𝐵 ∈ (0[,)+∞))
99 elrege0 13246 . . . . . . . . . . . . . . . . . . 19 (𝑐 / 𝑥𝐵 ∈ (0[,)+∞) ↔ (𝑐 / 𝑥𝐵 ∈ ℝ ∧ 0 ≤ 𝑐 / 𝑥𝐵))
10098, 99sylib 217 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐)) ∧ (𝑦𝑆𝑐𝑦))) → (𝑐 / 𝑥𝐵 ∈ ℝ ∧ 0 ≤ 𝑐 / 𝑥𝐵))
101 absid 15067 . . . . . . . . . . . . . . . . . 18 ((𝑐 / 𝑥𝐵 ∈ ℝ ∧ 0 ≤ 𝑐 / 𝑥𝐵) → (abs‘𝑐 / 𝑥𝐵) = 𝑐 / 𝑥𝐵)
102100, 101syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐)) ∧ (𝑦𝑆𝑐𝑦))) → (abs‘𝑐 / 𝑥𝐵) = 𝑐 / 𝑥𝐵)
103102breq1d 5090 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐)) ∧ (𝑦𝑆𝑐𝑦))) → ((abs‘𝑐 / 𝑥𝐵) < 𝑒𝑐 / 𝑥𝐵 < 𝑒))
1046adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐)) ∧ (𝑦𝑆𝑐𝑦))) → 𝑀 ∈ ℤ)
1057adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐)) ∧ (𝑦𝑆𝑐𝑦))) → 𝐷 ∈ ℝ)
1068adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐)) ∧ (𝑦𝑆𝑐𝑦))) → 𝑀 ≤ (𝐷 + 1))
1079adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐)) ∧ (𝑦𝑆𝑐𝑦))) → 𝑇 ∈ ℝ)
10810adantlr 712 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐)) ∧ (𝑦𝑆𝑐𝑦))) ∧ 𝑥𝑆) → 𝐴 ∈ ℝ)
10911adantlr 712 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐)) ∧ (𝑦𝑆𝑐𝑦))) ∧ 𝑥𝑆) → 𝐵𝑉)
11012adantlr 712 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐)) ∧ (𝑦𝑆𝑐𝑦))) ∧ 𝑥𝑍) → 𝐵 ∈ ℝ)
11113adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐)) ∧ (𝑦𝑆𝑐𝑦))) → (ℝ D (𝑥𝑆𝐴)) = (𝑥𝑆𝐵))
112 pnfxr 11089 . . . . . . . . . . . . . . . . . . 19 +∞ ∈ ℝ*
113112a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐)) ∧ (𝑦𝑆𝑐𝑦))) → +∞ ∈ ℝ*)
114 3simpa 1147 . . . . . . . . . . . . . . . . . . . 20 ((𝐷𝑥𝑥𝑘𝑘 ≤ +∞) → (𝐷𝑥𝑥𝑘))
115114, 82syl3an3 1164 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑥𝑆𝑘𝑆) ∧ (𝐷𝑥𝑥𝑘𝑘 ≤ +∞)) → 𝐶𝐵)
1161153adant1r 1176 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐)) ∧ (𝑦𝑆𝑐𝑦))) ∧ (𝑥𝑆𝑘𝑆) ∧ (𝐷𝑥𝑥𝑘𝑘 ≤ +∞)) → 𝐶𝐵)
117833adantr3 1170 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑥𝑆𝐷𝑥𝑥 ≤ +∞)) → 0 ≤ 𝐵)
118117adantlr 712 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐)) ∧ (𝑦𝑆𝑐𝑦))) ∧ (𝑥𝑆𝐷𝑥𝑥 ≤ +∞)) → 0 ≤ 𝐵)
119 simprrl 778 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐)) ∧ (𝑦𝑆𝑐𝑦))) → 𝑦𝑆)
120 simprrr 779 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐)) ∧ (𝑦𝑆𝑐𝑦))) → 𝑐𝑦)
1213, 21sstri 3934 . . . . . . . . . . . . . . . . . . . 20 𝑆 ⊆ ℝ*
122121, 119sselid 3923 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐)) ∧ (𝑦𝑆𝑐𝑦))) → 𝑦 ∈ ℝ*)
123 pnfge 12926 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ℝ*𝑦 ≤ +∞)
124122, 123syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐)) ∧ (𝑦𝑆𝑐𝑦))) → 𝑦 ≤ +∞)
1251, 5, 104, 105, 106, 107, 108, 109, 110, 111, 14, 113, 116, 15, 118, 61, 119, 90, 120, 124dvfsumlem4 25256 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐)) ∧ (𝑦𝑆𝑐𝑦))) → (abs‘((𝐺𝑦) − (𝐺𝑐))) ≤ 𝑐 / 𝑥𝐵)
12619adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐)) ∧ (𝑦𝑆𝑐𝑦))) → 𝐺:𝑆⟶ℂ)
127126, 119ffvelcdmd 6994 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐)) ∧ (𝑦𝑆𝑐𝑦))) → (𝐺𝑦) ∈ ℂ)
128126, 61ffvelcdmd 6994 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐)) ∧ (𝑦𝑆𝑐𝑦))) → (𝐺𝑐) ∈ ℂ)
129127, 128subcld 11392 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐)) ∧ (𝑦𝑆𝑐𝑦))) → ((𝐺𝑦) − (𝐺𝑐)) ∈ ℂ)
130129abscld 15207 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐)) ∧ (𝑦𝑆𝑐𝑦))) → (abs‘((𝐺𝑦) − (𝐺𝑐))) ∈ ℝ)
131100simpld 495 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐)) ∧ (𝑦𝑆𝑐𝑦))) → 𝑐 / 𝑥𝐵 ∈ ℝ)
132 simprll 776 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐)) ∧ (𝑦𝑆𝑐𝑦))) → 𝑒 ∈ ℝ+)
133132rpred 12832 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐)) ∧ (𝑦𝑆𝑐𝑦))) → 𝑒 ∈ ℝ)
134 lelttr 11125 . . . . . . . . . . . . . . . . . 18 (((abs‘((𝐺𝑦) − (𝐺𝑐))) ∈ ℝ ∧ 𝑐 / 𝑥𝐵 ∈ ℝ ∧ 𝑒 ∈ ℝ) → (((abs‘((𝐺𝑦) − (𝐺𝑐))) ≤ 𝑐 / 𝑥𝐵𝑐 / 𝑥𝐵 < 𝑒) → (abs‘((𝐺𝑦) − (𝐺𝑐))) < 𝑒))
135130, 131, 133, 134syl3anc 1370 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐)) ∧ (𝑦𝑆𝑐𝑦))) → (((abs‘((𝐺𝑦) − (𝐺𝑐))) ≤ 𝑐 / 𝑥𝐵𝑐 / 𝑥𝐵 < 𝑒) → (abs‘((𝐺𝑦) − (𝐺𝑐))) < 𝑒))
136125, 135mpand 692 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐)) ∧ (𝑦𝑆𝑐𝑦))) → (𝑐 / 𝑥𝐵 < 𝑒 → (abs‘((𝐺𝑦) − (𝐺𝑐))) < 𝑒))
137103, 136sylbid 239 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐)) ∧ (𝑦𝑆𝑐𝑦))) → ((abs‘𝑐 / 𝑥𝐵) < 𝑒 → (abs‘((𝐺𝑦) − (𝐺𝑐))) < 𝑒))
13879, 137syld 47 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐)) ∧ (𝑦𝑆𝑐𝑦))) → (∀𝑥𝑆 (𝑐𝑥 → (abs‘𝐵) < 𝑒) → (abs‘((𝐺𝑦) − (𝐺𝑐))) < 𝑒))
139138anassrs 468 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐))) ∧ (𝑦𝑆𝑐𝑦)) → (∀𝑥𝑆 (𝑐𝑥 → (abs‘𝐵) < 𝑒) → (abs‘((𝐺𝑦) − (𝐺𝑐))) < 𝑒))
140139expr 457 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐))) ∧ 𝑦𝑆) → (𝑐𝑦 → (∀𝑥𝑆 (𝑐𝑥 → (abs‘𝐵) < 𝑒) → (abs‘((𝐺𝑦) − (𝐺𝑐))) < 𝑒)))
141140com23 86 . . . . . . . . . . 11 (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐))) ∧ 𝑦𝑆) → (∀𝑥𝑆 (𝑐𝑥 → (abs‘𝐵) < 𝑒) → (𝑐𝑦 → (abs‘((𝐺𝑦) − (𝐺𝑐))) < 𝑒)))
142141ralrimdva 3146 . . . . . . . . . 10 ((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐))) → (∀𝑥𝑆 (𝑐𝑥 → (abs‘𝐵) < 𝑒) → ∀𝑦𝑆 (𝑐𝑦 → (abs‘((𝐺𝑦) − (𝐺𝑐))) < 𝑒)))
143142, 60jctild 526 . . . . . . . . 9 ((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ (𝑐𝑆𝐷𝑐))) → (∀𝑥𝑆 (𝑐𝑥 → (abs‘𝐵) < 𝑒) → (𝑐𝑆 ∧ ∀𝑦𝑆 (𝑐𝑦 → (abs‘((𝐺𝑦) − (𝐺𝑐))) < 𝑒))))
144143anassrs 468 . . . . . . . 8 (((𝜑𝑒 ∈ ℝ+) ∧ (𝑐𝑆𝐷𝑐)) → (∀𝑥𝑆 (𝑐𝑥 → (abs‘𝐵) < 𝑒) → (𝑐𝑆 ∧ ∀𝑦𝑆 (𝑐𝑦 → (abs‘((𝐺𝑦) − (𝐺𝑐))) < 𝑒))))
14559, 144syldan 591 . . . . . . 7 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → (∀𝑥𝑆 (𝑐𝑥 → (abs‘𝐵) < 𝑒) → (𝑐𝑆 ∧ ∀𝑦𝑆 (𝑐𝑦 → (abs‘((𝐺𝑦) − (𝐺𝑐))) < 𝑒))))
146145expimpd 454 . . . . . 6 ((𝜑𝑒 ∈ ℝ+) → ((𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞) ∧ ∀𝑥𝑆 (𝑐𝑥 → (abs‘𝐵) < 𝑒)) → (𝑐𝑆 ∧ ∀𝑦𝑆 (𝑐𝑦 → (abs‘((𝐺𝑦) − (𝐺𝑐))) < 𝑒))))
147146reximdv2 3156 . . . . 5 ((𝜑𝑒 ∈ ℝ+) → (∃𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)∀𝑥𝑆 (𝑐𝑥 → (abs‘𝐵) < 𝑒) → ∃𝑐𝑆𝑦𝑆 (𝑐𝑦 → (abs‘((𝐺𝑦) − (𝐺𝑐))) < 𝑒)))
14838, 147sylbird 259 . . . 4 ((𝜑𝑒 ∈ ℝ+) → (∃𝑐 ∈ ℝ ∀𝑥𝑆 (𝑐𝑥 → (abs‘𝐵) < 𝑒) → ∃𝑐𝑆𝑦𝑆 (𝑐𝑦 → (abs‘((𝐺𝑦) − (𝐺𝑐))) < 𝑒)))
149148ralimdva 3159 . . 3 (𝜑 → (∀𝑒 ∈ ℝ+𝑐 ∈ ℝ ∀𝑥𝑆 (𝑐𝑥 → (abs‘𝐵) < 𝑒) → ∀𝑒 ∈ ℝ+𝑐𝑆𝑦𝑆 (𝑐𝑦 → (abs‘((𝐺𝑦) − (𝐺𝑐))) < 𝑒)))
15031, 149mpd 15 . 2 (𝜑 → ∀𝑒 ∈ ℝ+𝑐𝑆𝑦𝑆 (𝑐𝑦 → (abs‘((𝐺𝑦) − (𝐺𝑐))) < 𝑒))
1514, 19, 26, 150caucvgr 15446 1 (𝜑𝐺 ∈ dom ⇝𝑟 )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1086   = wceq 1538  wcel 2103  wne 2939  wral 3060  wrex 3069  csb 3836  wss 3891  ifcif 4464   class class class wbr 5080  cmpt 5163  dom cdm 5600  wf 6454  cfv 6458  (class class class)co 7308  supcsup 9257  cc 10929  cr 10930  0cc0 10931  1c1 10932   + caddc 10934  +∞cpnf 11066  *cxr 11068   < clt 11069  cle 11070  cmin 11265  cz 12379  cuz 12642  +crp 12790  (,)cioo 13139  [,)cico 13141  ...cfz 13299  cfl 13570  abscabs 15004  𝑟 crli 15253  Σcsu 15456   D cdv 25090
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1910  ax-6 1968  ax-7 2008  ax-8 2105  ax-9 2113  ax-10 2134  ax-11 2151  ax-12 2168  ax-ext 2706  ax-rep 5217  ax-sep 5231  ax-nul 5238  ax-pow 5296  ax-pr 5360  ax-un 7621  ax-inf2 9457  ax-cnex 10987  ax-resscn 10988  ax-1cn 10989  ax-icn 10990  ax-addcl 10991  ax-addrcl 10992  ax-mulcl 10993  ax-mulrcl 10994  ax-mulcom 10995  ax-addass 10996  ax-mulass 10997  ax-distr 10998  ax-i2m1 10999  ax-1ne0 11000  ax-1rid 11001  ax-rnegex 11002  ax-rrecex 11003  ax-cnre 11004  ax-pre-lttri 11005  ax-pre-lttrn 11006  ax-pre-ltadd 11007  ax-pre-mulgt0 11008  ax-pre-sup 11009  ax-addf 11010  ax-mulf 11011
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1541  df-fal 1551  df-ex 1779  df-nf 1783  df-sb 2065  df-mo 2537  df-eu 2566  df-clab 2713  df-cleq 2727  df-clel 2813  df-nfc 2885  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3339  df-reu 3340  df-rab 3357  df-v 3438  df-sbc 3721  df-csb 3837  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-pss 3910  df-nul 4262  df-if 4465  df-pw 4540  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-uni 4844  df-int 4886  df-iun 4932  df-iin 4933  df-br 5081  df-opab 5143  df-mpt 5164  df-tr 5198  df-id 5500  df-eprel 5506  df-po 5514  df-so 5515  df-fr 5555  df-se 5556  df-we 5557  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613  df-pred 6217  df-ord 6284  df-on 6285  df-lim 6286  df-suc 6287  df-iota 6410  df-fun 6460  df-fn 6461  df-f 6462  df-f1 6463  df-fo 6464  df-f1o 6465  df-fv 6466  df-isom 6467  df-riota 7265  df-ov 7311  df-oprab 7312  df-mpo 7313  df-of 7566  df-om 7749  df-1st 7867  df-2nd 7868  df-supp 8013  df-frecs 8132  df-wrecs 8163  df-recs 8237  df-rdg 8276  df-1o 8332  df-2o 8333  df-er 8534  df-map 8653  df-pm 8654  df-ixp 8722  df-en 8770  df-dom 8771  df-sdom 8772  df-fin 8773  df-fsupp 9187  df-fi 9228  df-sup 9259  df-inf 9260  df-oi 9327  df-card 9755  df-pnf 11071  df-mnf 11072  df-xr 11073  df-ltxr 11074  df-le 11075  df-sub 11267  df-neg 11268  df-div 11693  df-nn 12034  df-2 12096  df-3 12097  df-4 12098  df-5 12099  df-6 12100  df-7 12101  df-8 12102  df-9 12103  df-n0 12294  df-z 12380  df-dec 12498  df-uz 12643  df-q 12749  df-rp 12791  df-xneg 12908  df-xadd 12909  df-xmul 12910  df-ioo 13143  df-ico 13145  df-icc 13146  df-fz 13300  df-fzo 13443  df-fl 13572  df-seq 13782  df-exp 13843  df-hash 14105  df-cj 14869  df-re 14870  df-im 14871  df-sqrt 15005  df-abs 15006  df-limsup 15239  df-clim 15256  df-rlim 15257  df-sum 15457  df-struct 16907  df-sets 16924  df-slot 16942  df-ndx 16954  df-base 16972  df-ress 17001  df-plusg 17034  df-mulr 17035  df-starv 17036  df-sca 17037  df-vsca 17038  df-ip 17039  df-tset 17040  df-ple 17041  df-ds 17043  df-unif 17044  df-hom 17045  df-cco 17046  df-rest 17192  df-topn 17193  df-0g 17211  df-gsum 17212  df-topgen 17213  df-pt 17214  df-prds 17217  df-xrs 17272  df-qtop 17277  df-imas 17278  df-xps 17280  df-mre 17354  df-mrc 17355  df-acs 17357  df-mgm 18385  df-sgrp 18434  df-mnd 18445  df-submnd 18490  df-mulg 18760  df-cntz 18982  df-cmn 19447  df-psmet 20652  df-xmet 20653  df-met 20654  df-bl 20655  df-mopn 20656  df-fbas 20657  df-fg 20658  df-cnfld 20661  df-top 22106  df-topon 22123  df-topsp 22145  df-bases 22159  df-cld 22233  df-ntr 22234  df-cls 22235  df-nei 22312  df-lp 22350  df-perf 22351  df-cn 22441  df-cnp 22442  df-haus 22529  df-cmp 22601  df-tx 22776  df-hmeo 22969  df-fil 23060  df-fm 23152  df-flim 23153  df-flf 23154  df-xms 23536  df-ms 23537  df-tms 23538  df-cncf 24104  df-limc 25093  df-dv 25094
This theorem is referenced by:  dvfsumrlim3  25260
  Copyright terms: Public domain W3C validator