Theorem dvfsumrlim 26008

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.

Step	Hyp	Ref	Expression
1		dvfsum.s	. . . 4 ⊢ 𝑆 = (𝑇(,)+∞)
2		ioossre 13351	. . . 4 ⊢ (𝑇(,)+∞) ⊆ ℝ
3	1, 2	eqsstri 3969	. . 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 26002	. . 3 ⊢ (𝜑 → 𝐺:𝑆⟶ℝ)
17		ax-resscn 11086	. . 3 ⊢ ℝ ⊆ ℂ
18		fss 6678	. . 3 ⊢ ((𝐺:𝑆⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐺:𝑆⟶ℂ)
19	16, 17, 18	sylancl 587	. 2 ⊢ (𝜑 → 𝐺:𝑆⟶ℂ)
20	1	supeq1i 9353	. . 3 ⊢ sup(𝑆, ℝ*, < ) = sup((𝑇(,)+∞), ℝ*, < )
21		ressxr 11180	. . . . 5 ⊢ ℝ ⊆ ℝ*
22	21, 9	sselid 3920	. . . 4 ⊢ (𝜑 → 𝑇 ∈ ℝ*)
23	9	renepnfd 11187	. . . 4 ⊢ (𝜑 → 𝑇 ≠ +∞)
24		ioopnfsup 13814	. . . 4 ⊢ ((𝑇 ∈ ℝ* ∧ 𝑇 ≠ +∞) → sup((𝑇(,)+∞), ℝ*, < ) = +∞)
25	22, 23, 24	syl2anc 585	. . 3 ⊢ (𝜑 → sup((𝑇(,)+∞), ℝ*, < ) = +∞)
26	20, 25	eqtrid 2784	. 2 ⊢ (𝜑 → sup(𝑆, ℝ*, < ) = +∞)
27		dvfsumrlim.k	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ 𝐵) ⇝𝑟 0)
28	11, 27	rlimmptrcl 15561	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ ℂ)
29	28	ralrimiva 3130	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ 𝑆 𝐵 ∈ ℂ)
30	29, 4	rlim0 15461	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ 𝐵) ⇝𝑟 0 ↔ ∀𝑒 ∈ ℝ+ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒)))
31	27, 30	mpbid 232	. . 3 ⊢ (𝜑 → ∀𝑒 ∈ ℝ+ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒))
32	3	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → 𝑆 ⊆ ℝ)
33		peano2re 11310	. . . . . . . . 9 ⊢ (𝑇 ∈ ℝ → (𝑇 + 1) ∈ ℝ)
34	9, 33	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑇 + 1) ∈ ℝ)
35	34, 7	ifcld 4514	. . . . . . 7 ⊢ (𝜑 → if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷) ∈ ℝ)
36	35	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷) ∈ ℝ)
37		rexico 15307	. . . . . 6 ⊢ ((𝑆 ⊆ ℝ ∧ if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷) ∈ ℝ) → (∃𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒) ↔ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒)))
38	32, 36, 37	syl2anc 585	. . . . 5 ⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → (∃𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒) ↔ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒)))
39		elicopnf 13389	. . . . . . . . . . . . . 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 12077	. . . . . . . . . . . . 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 13134	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ ℝ ∧ (𝑇 + 1) ∈ ℝ ∧ 𝑐 ∈ ℝ) → (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷) ≤ 𝑐 ↔ (𝐷 ≤ 𝑐 ∧ (𝑇 + 1) ≤ 𝑐)))
48	46, 43, 41, 47	syl3anc 1374	. . . . . . . . . . . . . . 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 11297	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → 𝑇 < 𝑐)
52	22	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → 𝑇 ∈ ℝ*)
53		elioopnf 13387	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ ℝ* → (𝑐 ∈ (𝑇(,)+∞) ↔ (𝑐 ∈ ℝ ∧ 𝑇 < 𝑐)))
54	52, 53	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → (𝑐 ∈ (𝑇(,)+∞) ↔ (𝑐 ∈ ℝ ∧ 𝑇 < 𝑐)))
55	41, 51, 54	mpbir2and 714	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → 𝑐 ∈ (𝑇(,)+∞))
56	55, 1	eleqtrrdi 2848	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → 𝑐 ∈ 𝑆)
57	49	simpld 494	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → 𝐷 ≤ 𝑐)
58	56, 57	jca 511	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐))
59	58	adantlr 716	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐))
60		simprrl 781	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐))) → 𝑐 ∈ 𝑆)
61	60	adantrr 718	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → 𝑐 ∈ 𝑆)
62	3, 61	sselid 3920	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → 𝑐 ∈ ℝ)
63	62	leidd 11707	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → 𝑐 ≤ 𝑐)
64		nfv 1916	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥 𝑐 ≤ 𝑐
65		nfcv 2899	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑥abs
66		nfcsb1v 3862	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑥⦋𝑐 / 𝑥⦌𝐵
67	65, 66	nffv 6844	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥(abs‘⦋𝑐 / 𝑥⦌𝐵)
68		nfcv 2899	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥 <
69		nfcv 2899	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥𝑒
70	67, 68, 69	nfbr 5133	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥(abs‘⦋𝑐 / 𝑥⦌𝐵) < 𝑒
71	64, 70	nfim 1898	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥(𝑐 ≤ 𝑐 → (abs‘⦋𝑐 / 𝑥⦌𝐵) < 𝑒)
72		breq2 5090	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑐 → (𝑐 ≤ 𝑥 ↔ 𝑐 ≤ 𝑐))
73		csbeq1a 3852	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑐 → 𝐵 = ⦋𝑐 / 𝑥⦌𝐵)
74	73	fveq2d 6838	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑐 → (abs‘𝐵) = (abs‘⦋𝑐 / 𝑥⦌𝐵))
75	74	breq1d 5096	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑐 → ((abs‘𝐵) < 𝑒 ↔ (abs‘⦋𝑐 / 𝑥⦌𝐵) < 𝑒))
76	72, 75	imbi12d 344	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑐 → ((𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒) ↔ (𝑐 ≤ 𝑐 → (abs‘⦋𝑐 / 𝑥⦌𝐵) < 𝑒)))
77	71, 76	rspc 3553	. . . . . . . . . . . . . . . . 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 26001	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ ℝ)
81	80	adantrr 718	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) → 𝐵 ∈ ℝ)
82		dvfsumrlim.l	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘)) → 𝐶 ≤ 𝐵)
83	1, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 82, 15, 27	dvfsumrlimge0 26007	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) → 0 ≤ 𝐵)
84		elrege0 13398	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐵 ∈ (0[,)+∞) ↔ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵))
85	81, 83, 84	sylanbrc 584	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥)) → 𝐵 ∈ (0[,)+∞))
86	85	expr 456	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐷 ≤ 𝑥 → 𝐵 ∈ (0[,)+∞)))
87	86	ralrimiva 3130	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ∀𝑥 ∈ 𝑆 (𝐷 ≤ 𝑥 → 𝐵 ∈ (0[,)+∞)))
88	87	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → ∀𝑥 ∈ 𝑆 (𝐷 ≤ 𝑥 → 𝐵 ∈ (0[,)+∞)))
89		simprrr 782	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐))) → 𝐷 ≤ 𝑐)
90	89	adantrr 718	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → 𝐷 ≤ 𝑐)
91		nfv 1916	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑥 𝐷 ≤ 𝑐
92	66	nfel1 2916	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑥⦋𝑐 / 𝑥⦌𝐵 ∈ (0[,)+∞)
93	91, 92	nfim 1898	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑥(𝐷 ≤ 𝑐 → ⦋𝑐 / 𝑥⦌𝐵 ∈ (0[,)+∞))
94		breq2 5090	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑐 → (𝐷 ≤ 𝑥 ↔ 𝐷 ≤ 𝑐))
95	73	eleq1d 2822	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑐 → (𝐵 ∈ (0[,)+∞) ↔ ⦋𝑐 / 𝑥⦌𝐵 ∈ (0[,)+∞)))
96	94, 95	imbi12d 344	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑐 → ((𝐷 ≤ 𝑥 → 𝐵 ∈ (0[,)+∞)) ↔ (𝐷 ≤ 𝑐 → ⦋𝑐 / 𝑥⦌𝐵 ∈ (0[,)+∞))))
97	93, 96	rspc 3553	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 (𝐷 ≤ 𝑥 → 𝐵 ∈ (0[,)+∞)) → (𝐷 ≤ 𝑐 → ⦋𝑐 / 𝑥⦌𝐵 ∈ (0[,)+∞))))
98	61, 88, 90, 97	syl3c 66	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → ⦋𝑐 / 𝑥⦌𝐵 ∈ (0[,)+∞))
99		elrege0 13398	. . . . . . . . . . . . . . . . . . 19 ⊢ (⦋𝑐 / 𝑥⦌𝐵 ∈ (0[,)+∞) ↔ (⦋𝑐 / 𝑥⦌𝐵 ∈ ℝ ∧ 0 ≤ ⦋𝑐 / 𝑥⦌𝐵))
100	98, 99	sylib 218	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → (⦋𝑐 / 𝑥⦌𝐵 ∈ ℝ ∧ 0 ≤ ⦋𝑐 / 𝑥⦌𝐵))
101		absid 15249	. . . . . . . . . . . . . . . . . 18 ⊢ ((⦋𝑐 / 𝑥⦌𝐵 ∈ ℝ ∧ 0 ≤ ⦋𝑐 / 𝑥⦌𝐵) → (abs‘⦋𝑐 / 𝑥⦌𝐵) = ⦋𝑐 / 𝑥⦌𝐵)
102	100, 101	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → (abs‘⦋𝑐 / 𝑥⦌𝐵) = ⦋𝑐 / 𝑥⦌𝐵)
103	102	breq1d 5096	. . . . . . . . . . . . . . . 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 716	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ)
109	11	adantlr 716	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉)
110	12	adantlr 716	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ)
111	13	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵))
112		pnfxr 11190	. . . . . . . . . . . . . . . . . . 19 ⊢ +∞ ∈ ℝ*
113	112	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → +∞ ∈ ℝ*)
114		3simpa 1149	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ +∞) → (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘))
115	114, 82	syl3an3 1166	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ +∞)) → 𝐶 ≤ 𝐵)
116	115	3adant1r 1179	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ +∞)) → 𝐶 ≤ 𝐵)
117	83	3adantr3 1173	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ +∞)) → 0 ≤ 𝐵)
118	117	adantlr 716	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) ∧ (𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ +∞)) → 0 ≤ 𝐵)
119		simprrl 781	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → 𝑦 ∈ 𝑆)
120		simprrr 782	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → 𝑐 ≤ 𝑦)
121	3, 21	sstri 3932	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑆 ⊆ ℝ*
122	121, 119	sselid 3920	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → 𝑦 ∈ ℝ*)
123		pnfge 13072	. . . . . . . . . . . . . . . . . . 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 26006	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) ≤ ⦋𝑐 / 𝑥⦌𝐵)
126	19	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → 𝐺:𝑆⟶ℂ)
127	126, 119	ffvelcdmd 7031	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → (𝐺‘𝑦) ∈ ℂ)
128	126, 61	ffvelcdmd 7031	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → (𝐺‘𝑐) ∈ ℂ)
129	127, 128	subcld 11496	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → ((𝐺‘𝑦) − (𝐺‘𝑐)) ∈ ℂ)
130	129	abscld 15392	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) ∈ ℝ)
131	100	simpld 494	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → ⦋𝑐 / 𝑥⦌𝐵 ∈ ℝ)
132		simprll 779	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → 𝑒 ∈ ℝ+)
133	132	rpred 12977	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → 𝑒 ∈ ℝ)
134		lelttr 11227	. . . . . . . . . . . . . . . . . 18 ⊢ (((abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) ∈ ℝ ∧ ⦋𝑐 / 𝑥⦌𝐵 ∈ ℝ ∧ 𝑒 ∈ ℝ) → (((abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) ≤ ⦋𝑐 / 𝑥⦌𝐵 ∧ ⦋𝑐 / 𝑥⦌𝐵 < 𝑒) → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) < 𝑒))
135	130, 131, 133, 134	syl3anc 1374	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) ∧ (𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦))) → (((abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) ≤ ⦋𝑐 / 𝑥⦌𝐵 ∧ ⦋𝑐 / 𝑥⦌𝐵 < 𝑒) → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) < 𝑒))
136	125, 135	mpand 696	. . . . . . . . . . . . . . . 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 3138	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐))) → (∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒) → ∀𝑦 ∈ 𝑆 (𝑐 ≤ 𝑦 → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) < 𝑒)))
143	142, 60	jctild 525	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐))) → (∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒) → (𝑐 ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 (𝑐 ≤ 𝑦 → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) < 𝑒))))
144	143	anassrs 467	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ (𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐)) → (∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒) → (𝑐 ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 (𝑐 ≤ 𝑦 → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) < 𝑒))))
145	59, 144	syldan 592	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)) → (∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒) → (𝑐 ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 (𝑐 ≤ 𝑦 → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) < 𝑒))))
146	145	expimpd 453	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → ((𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞) ∧ ∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒)) → (𝑐 ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 (𝑐 ≤ 𝑦 → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) < 𝑒))))
147	146	reximdv2 3148	. . . . 5 ⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → (∃𝑐 ∈ (if(𝐷 ≤ (𝑇 + 1), (𝑇 + 1), 𝐷)[,)+∞)∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒) → ∃𝑐 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑐 ≤ 𝑦 → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) < 𝑒)))
148	38, 147	sylbird 260	. . . 4 ⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → (∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒) → ∃𝑐 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑐 ≤ 𝑦 → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) < 𝑒)))
149	148	ralimdva 3150	. . 3 ⊢ (𝜑 → (∀𝑒 ∈ ℝ+ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝑆 (𝑐 ≤ 𝑥 → (abs‘𝐵) < 𝑒) → ∀𝑒 ∈ ℝ+ ∃𝑐 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑐 ≤ 𝑦 → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) < 𝑒)))
150	31, 149	mpd 15	. 2 ⊢ (𝜑 → ∀𝑒 ∈ ℝ+ ∃𝑐 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑐 ≤ 𝑦 → (abs‘((𝐺‘𝑦) − (𝐺‘𝑐))) < 𝑒))
151	4, 19, 26, 150	caucvgr 15629	1 ⊢ (𝜑 → 𝐺 ∈ dom ⇝𝑟 )

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114   ≠ wne 2933  ∀wral 3052  ∃wrex 3062  ⦋csb 3838   ⊆ wss 3890  ifcif 4467   class class class wbr 5086   ↦ cmpt 5167  dom cdm 5624  ⟶wf 6488  ‘cfv 6492  (class class class)co 7360  supcsup 9346  ℂcc 11027  ℝcr 11028  0cc0 11029  1c1 11030   + caddc 11032  +∞cpnf 11167  ℝ^*cxr 11169   < clt 11170   ≤ cle 11171   − cmin 11368  ℤcz 12515  ℤ_≥cuz 12779  ℝ⁺crp 12933  (,)cioo 13289  [,)cico 13291  ...cfz 13452  ⌊cfl 13740  abscabs 15187   ⇝_𝑟 crli 15438  Σcsu 15639   D cdv 25840

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-inf2 9553  ax-cnex 11085  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106  ax-pre-sup 11107  ax-addf 11108

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-tp 4573  df-op 4575  df-uni 4852  df-int 4891  df-iun 4936  df-iin 4937  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-se 5578  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-isom 6501  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-of 7624  df-om 7811  df-1st 7935  df-2nd 7936  df-supp 8104  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-1o 8398  df-2o 8399  df-er 8636  df-map 8768  df-pm 8769  df-ixp 8839  df-en 8887  df-dom 8888  df-sdom 8889  df-fin 8890  df-fsupp 9268  df-fi 9317  df-sup 9348  df-inf 9349  df-oi 9418  df-card 9854  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-div 11799  df-nn 12166  df-2 12235  df-3 12236  df-4 12237  df-5 12238  df-6 12239  df-7 12240  df-8 12241  df-9 12242  df-n0 12429  df-z 12516  df-dec 12636  df-uz 12780  df-q 12890  df-rp 12934  df-xneg 13054  df-xadd 13055  df-xmul 13056  df-ioo 13293  df-ico 13295  df-icc 13296  df-fz 13453  df-fzo 13600  df-fl 13742  df-seq 13955  df-exp 14015  df-hash 14284  df-cj 15052  df-re 15053  df-im 15054  df-sqrt 15188  df-abs 15189  df-limsup 15424  df-clim 15441  df-rlim 15442  df-sum 15640  df-struct 17108  df-sets 17125  df-slot 17143  df-ndx 17155  df-base 17171  df-ress 17192  df-plusg 17224  df-mulr 17225  df-starv 17226  df-sca 17227  df-vsca 17228  df-ip 17229  df-tset 17230  df-ple 17231  df-ds 17233  df-unif 17234  df-hom 17235  df-cco 17236  df-rest 17376  df-topn 17377  df-0g 17395  df-gsum 17396  df-topgen 17397  df-pt 17398  df-prds 17401  df-xrs 17457  df-qtop 17462  df-imas 17463  df-xps 17465  df-mre 17539  df-mrc 17540  df-acs 17542  df-mgm 18599  df-sgrp 18678  df-mnd 18694  df-submnd 18743  df-mulg 19035  df-cntz 19283  df-cmn 19748  df-psmet 21336  df-xmet 21337  df-met 21338  df-bl 21339  df-mopn 21340  df-fbas 21341  df-fg 21342  df-cnfld 21345  df-top 22869  df-topon 22886  df-topsp 22908  df-bases 22921  df-cld 22994  df-ntr 22995  df-cls 22996  df-nei 23073  df-lp 23111  df-perf 23112  df-cn 23202  df-cnp 23203  df-haus 23290  df-cmp 23362  df-tx 23537  df-hmeo 23730  df-fil 23821  df-fm 23913  df-flim 23914  df-flf 23915  df-xms 24295  df-ms 24296  df-tms 24297  df-cncf 24855  df-limc 25843  df-dv 25844

This theorem is referenced by:  dvfsumrlim3  26010