dvfsumrlim2

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 x e. S |-> B is a decreasing function with antiderivative A converging to zero, then the difference between sum_ k e. ( M ... ( |_x ) ) B ( k ) and S. u e. ( M , x ) B ( u ) _d u = A ( x ) converges to a constant limit value, with the remainder term bounded by B ( x ) . (Contributed by Mario Carneiro, 18-May-2016)

	Ref	Expression
Hypotheses	dvfsum.s	$⊢ S = (T, +∞)$
	dvfsum.z	$⊢ Z = ℤ_{\geq M}$
	dvfsum.m	$⊢ φ \to M \in ℤ$
	dvfsum.d	$⊢ φ \to D \in ℝ$
	dvfsum.md	$⊢ φ \to M \leq D + 1$
	dvfsum.t	$⊢ φ \to T \in ℝ$
	dvfsum.a	$⊢ (φ \land x \in S) \to A \in ℝ$
	dvfsum.b1	$⊢ (φ \land x \in S) \to B \in V$
	dvfsum.b2	$⊢ (φ \land x \in Z) \to B \in ℝ$
	dvfsum.b3	$⊢ φ \to \frac{d (x \in S⟼ A)}{d_{ℝ} x} = (x \in S ⟼ B)$
	dvfsum.c	$⊢ x = k \to B = C$
	dvfsumrlim.l	$⊢ (φ \land (x \in S \land k \in S) \land (D \leq x \land x \leq k)) \to C \leq B$
	dvfsumrlim.g	$⊢ G = (x \in S ⟼ \sum_{k = M}^{⌊x⌋} C - A)$
	dvfsumrlim.k	$⊢ φ \to (x \in S ⟼ B) \underset{ℝ}{⇝} 0$
	dvfsumrlim2.1	$⊢ φ \to X \in S$
	dvfsumrlim2.2	$⊢ φ \to D \leq X$
Assertion	dvfsumrlim2	$⊢ (φ \land G \underset{ℝ}{⇝} L) \to \|G (X) - L\| \leq ⦋ X / x ⦌ B$

Proof

Step	Hyp	Ref	Expression
1		dvfsum.s	$⊢ S = (T, +∞)$
2		dvfsum.z	$⊢ Z = ℤ_{\geq M}$
3		dvfsum.m	$⊢ φ \to M \in ℤ$
4		dvfsum.d	$⊢ φ \to D \in ℝ$
5		dvfsum.md	$⊢ φ \to M \leq D + 1$
6		dvfsum.t	$⊢ φ \to T \in ℝ$
7		dvfsum.a	$⊢ (φ \land x \in S) \to A \in ℝ$
8		dvfsum.b1	$⊢ (φ \land x \in S) \to B \in V$
9		dvfsum.b2	$⊢ (φ \land x \in Z) \to B \in ℝ$
10		dvfsum.b3	$⊢ φ \to \frac{d (x \in S⟼ A)}{d_{ℝ} x} = (x \in S ⟼ B)$
11		dvfsum.c	$⊢ x = k \to B = C$
12		dvfsumrlim.l	$⊢ (φ \land (x \in S \land k \in S) \land (D \leq x \land x \leq k)) \to C \leq B$
13		dvfsumrlim.g	$⊢ G = (x \in S ⟼ \sum_{k = M}^{⌊x⌋} C - A)$
14		dvfsumrlim.k	$⊢ φ \to (x \in S ⟼ B) \underset{ℝ}{⇝} 0$
15		dvfsumrlim2.1	$⊢ φ \to X \in S$
16		dvfsumrlim2.2	$⊢ φ \to D \leq X$
17		ioossre	$⊢ (T, +∞) \subseteq ℝ$
18	1 17	eqsstri	$⊢ S \subseteq ℝ$
19	18 15	sselid	$⊢ φ \to X \in ℝ$
20	19	rexrd	$⊢ φ \to X \in ℝ^{*}$
21	19	renepnfd	$⊢ φ \to X \neq +∞$
22		icopnfsup	$⊢ (X \in ℝ^{} \land X \neq +∞) \to sup ([X, +∞) ℝ^{} <) = +∞$
23	20 21 22	syl2anc	$⊢ φ \to sup ([X, +∞) ℝ^{*} <) = +∞$
24	23	adantr	$⊢ (φ \land G \underset{ℝ}{⇝} L) \to sup ([X, +∞) ℝ^{*} <) = +∞$
25	1 2 3 4 5 6 7 8 9 10 11 13	dvfsumrlimf	$⊢ φ \to G : S ⟶ ℝ$
26	25	ad2antrr	$⊢ ((φ \land G \underset{ℝ}{⇝} L) \land y \in [X, +∞)) \to G : S ⟶ ℝ$
27	15	ad2antrr	$⊢ ((φ \land G \underset{ℝ}{⇝} L) \land y \in [X, +∞)) \to X \in S$
28	26 27	ffvelcdmd	$⊢ ((φ \land G \underset{ℝ}{⇝} L) \land y \in [X, +∞)) \to G (X) \in ℝ$
29	28	recnd	$⊢ ((φ \land G \underset{ℝ}{⇝} L) \land y \in [X, +∞)) \to G (X) \in ℂ$
30	6	rexrd	$⊢ φ \to T \in ℝ^{*}$
31	15 1	eleqtrdi	$⊢ φ \to X \in (T, +∞)$
32		elioopnf	$⊢ T \in ℝ^{*} \to (X \in (T, +∞) \leftrightarrow (X \in ℝ \land T < X))$
33	30 32	syl	$⊢ φ \to (X \in (T, +∞) \leftrightarrow (X \in ℝ \land T < X))$
34	31 33	mpbid	$⊢ φ \to (X \in ℝ \land T < X)$
35	34	simprd	$⊢ φ \to T < X$
36		df-ioo	$⊢ (.) = (u \in ℝ^{}, v \in ℝ^{} ⟼ \{w \in ℝ^{*} \| (u < w \land w < v)\})$
37		df-ico	$⊢ [.) = (u \in ℝ^{}, v \in ℝ^{} ⟼ \{w \in ℝ^{*} \| (u \leq w \land w < v)\})$
38		xrltletr	$⊢ (T \in ℝ^{} \land X \in ℝ^{} \land z \in ℝ^{*}) \to ((T < X \land X \leq z) \to T < z)$
39	36 37 38	ixxss1	$⊢ (T \in ℝ^{*} \land T < X) \to [X, +∞) \subseteq (T, +∞)$
40	30 35 39	syl2anc	$⊢ φ \to [X, +∞) \subseteq (T, +∞)$
41	40 1	sseqtrrdi	$⊢ φ \to [X, +∞) \subseteq S$
42	41	adantr	$⊢ (φ \land G \underset{ℝ}{⇝} L) \to [X, +∞) \subseteq S$
43	42	sselda	$⊢ ((φ \land G \underset{ℝ}{⇝} L) \land y \in [X, +∞)) \to y \in S$
44	26 43	ffvelcdmd	$⊢ ((φ \land G \underset{ℝ}{⇝} L) \land y \in [X, +∞)) \to G (y) \in ℝ$
45	44	recnd	$⊢ ((φ \land G \underset{ℝ}{⇝} L) \land y \in [X, +∞)) \to G (y) \in ℂ$
46	29 45	subcld	$⊢ ((φ \land G \underset{ℝ}{⇝} L) \land y \in [X, +∞)) \to G (X) - G (y) \in ℂ$
47		pnfxr	$⊢ +∞ \in ℝ^{*}$
48		icossre	$⊢ (X \in ℝ \land +∞ \in ℝ^{*}) \to [X, +∞) \subseteq ℝ$
49	19 47 48	sylancl	$⊢ φ \to [X, +∞) \subseteq ℝ$
50	49	adantr	$⊢ (φ \land G \underset{ℝ}{⇝} L) \to [X, +∞) \subseteq ℝ$
51		rlimf	$⊢ G \underset{ℝ}{⇝} L \to G : dom G ⟶ ℂ$
52	51	adantl	$⊢ (φ \land G \underset{ℝ}{⇝} L) \to G : dom G ⟶ ℂ$
53		ovex	$⊢ \sum_{k = M}^{⌊x⌋} C - A \in V$
54	53 13	dmmpti	$⊢ dom G = S$
55	54	feq2i	$⊢ G : dom G ⟶ ℂ \leftrightarrow G : S ⟶ ℂ$
56	52 55	sylib	$⊢ (φ \land G \underset{ℝ}{⇝} L) \to G : S ⟶ ℂ$
57	15	adantr	$⊢ (φ \land G \underset{ℝ}{⇝} L) \to X \in S$
58	56 57	ffvelcdmd	$⊢ (φ \land G \underset{ℝ}{⇝} L) \to G (X) \in ℂ$
59		rlimconst	$⊢ ([X, +∞) \subseteq ℝ \land G (X) \in ℂ) \to (y \in [X, +∞) ⟼ G (X)) \underset{ℝ}{⇝} G (X)$
60	50 58 59	syl2anc	$⊢ (φ \land G \underset{ℝ}{⇝} L) \to (y \in [X, +∞) ⟼ G (X)) \underset{ℝ}{⇝} G (X)$
61	56	feqmptd	$⊢ (φ \land G \underset{ℝ}{⇝} L) \to G = (y \in S ⟼ G (y))$
62		simpr	$⊢ (φ \land G \underset{ℝ}{⇝} L) \to G \underset{ℝ}{⇝} L$
63	61 62	eqbrtrrd	$⊢ (φ \land G \underset{ℝ}{⇝} L) \to (y \in S ⟼ G (y)) \underset{ℝ}{⇝} L$
64	42 63	rlimres2	$⊢ (φ \land G \underset{ℝ}{⇝} L) \to (y \in [X, +∞) ⟼ G (y)) \underset{ℝ}{⇝} L$
65	29 45 60 64	rlimsub	$⊢ (φ \land G \underset{ℝ}{⇝} L) \to (y \in [X, +∞) ⟼ G (X) - G (y)) \underset{ℝ}{⇝} (G (X) - L)$
66	46 65	rlimabs	$⊢ (φ \land G \underset{ℝ}{⇝} L) \to (y \in [X, +∞) ⟼ \|G (X) - G (y)\|) \underset{ℝ}{⇝} \|G (X) - L\|$
67	18	a1i	$⊢ φ \to S \subseteq ℝ$
68	67 7 8 10	dvmptrecl	$⊢ (φ \land x \in S) \to B \in ℝ$
69	68	ralrimiva	$⊢ φ \to \forall x \in S B \in ℝ$
70		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ X / x ⦌ B$
71	70	nfel1	$⊢ Ⅎ x ⦋ X / x ⦌ B \in ℝ$
72		csbeq1a	$⊢ x = X \to B = ⦋ X / x ⦌ B$
73	72	eleq1d	$⊢ x = X \to (B \in ℝ \leftrightarrow ⦋ X / x ⦌ B \in ℝ)$
74	71 73	rspc	$⊢ X \in S \to (\forall x \in S B \in ℝ \to ⦋ X / x ⦌ B \in ℝ)$
75	15 69 74	sylc	$⊢ φ \to ⦋ X / x ⦌ B \in ℝ$
76	75	recnd	$⊢ φ \to ⦋ X / x ⦌ B \in ℂ$
77		rlimconst	$⊢ ([X, +∞) \subseteq ℝ \land ⦋ X / x ⦌ B \in ℂ) \to (y \in [X, +∞) ⟼ ⦋ X / x ⦌ B) \underset{ℝ}{⇝} ⦋ X / x ⦌ B$
78	49 76 77	syl2anc	$⊢ φ \to (y \in [X, +∞) ⟼ ⦋ X / x ⦌ B) \underset{ℝ}{⇝} ⦋ X / x ⦌ B$
79	78	adantr	$⊢ (φ \land G \underset{ℝ}{⇝} L) \to (y \in [X, +∞) ⟼ ⦋ X / x ⦌ B) \underset{ℝ}{⇝} ⦋ X / x ⦌ B$
80	46	abscld	$⊢ ((φ \land G \underset{ℝ}{⇝} L) \land y \in [X, +∞)) \to \|G (X) - G (y)\| \in ℝ$
81	75	ad2antrr	$⊢ ((φ \land G \underset{ℝ}{⇝} L) \land y \in [X, +∞)) \to ⦋ X / x ⦌ B \in ℝ$
82	29 45	abssubd	$⊢ ((φ \land G \underset{ℝ}{⇝} L) \land y \in [X, +∞)) \to \|G (X) - G (y)\| = \|G (y) - G (X)\|$
83	3	adantr	$⊢ (φ \land y \in [X, +∞)) \to M \in ℤ$
84	4	adantr	$⊢ (φ \land y \in [X, +∞)) \to D \in ℝ$
85	5	adantr	$⊢ (φ \land y \in [X, +∞)) \to M \leq D + 1$
86	6	adantr	$⊢ (φ \land y \in [X, +∞)) \to T \in ℝ$
87	7	adantlr	$⊢ ((φ \land y \in [X, +∞)) \land x \in S) \to A \in ℝ$
88	8	adantlr	$⊢ ((φ \land y \in [X, +∞)) \land x \in S) \to B \in V$
89	9	adantlr	$⊢ ((φ \land y \in [X, +∞)) \land x \in Z) \to B \in ℝ$
90	10	adantr	$⊢ (φ \land y \in [X, +∞)) \to \frac{d (x \in S⟼ A)}{d_{ℝ} x} = (x \in S ⟼ B)$
91	47	a1i	$⊢ (φ \land y \in [X, +∞)) \to +∞ \in ℝ^{*}$
92		3simpa	$⊢ (D \leq x \land x \leq k \land k \leq +∞) \to (D \leq x \land x \leq k)$
93	92 12	syl3an3	$⊢ (φ \land (x \in S \land k \in S) \land (D \leq x \land x \leq k \land k \leq +∞)) \to C \leq B$
94	93	3adant1r	$⊢ ((φ \land y \in [X, +∞)) \land (x \in S \land k \in S) \land (D \leq x \land x \leq k \land k \leq +∞)) \to C \leq B$
95	1 2 3 4 5 6 7 8 9 10 11 12 13 14	dvfsumrlimge0	$⊢ (φ \land (x \in S \land D \leq x)) \to 0 \leq B$
96	95	3adantr3	$⊢ (φ \land (x \in S \land D \leq x \land x \leq +∞)) \to 0 \leq B$
97	96	adantlr	$⊢ ((φ \land y \in [X, +∞)) \land (x \in S \land D \leq x \land x \leq +∞)) \to 0 \leq B$
98	15	adantr	$⊢ (φ \land y \in [X, +∞)) \to X \in S$
99	41	sselda	$⊢ (φ \land y \in [X, +∞)) \to y \in S$
100	16	adantr	$⊢ (φ \land y \in [X, +∞)) \to D \leq X$
101		elicopnf	$⊢ X \in ℝ \to (y \in [X, +∞) \leftrightarrow (y \in ℝ \land X \leq y))$
102	19 101	syl	$⊢ φ \to (y \in [X, +∞) \leftrightarrow (y \in ℝ \land X \leq y))$
103	102	simplbda	$⊢ (φ \land y \in [X, +∞)) \to X \leq y$
104	102	simprbda	$⊢ (φ \land y \in [X, +∞)) \to y \in ℝ$
105	104	rexrd	$⊢ (φ \land y \in [X, +∞)) \to y \in ℝ^{*}$
106		pnfge	$⊢ y \in ℝ^{*} \to y \leq +∞$
107	105 106	syl	$⊢ (φ \land y \in [X, +∞)) \to y \leq +∞$
108	1 2 83 84 85 86 87 88 89 90 11 91 94 13 97 98 99 100 103 107	dvfsumlem4	$⊢ (φ \land y \in [X, +∞)) \to \|G (y) - G (X)\| \leq ⦋ X / x ⦌ B$
109	108	adantlr	$⊢ ((φ \land G \underset{ℝ}{⇝} L) \land y \in [X, +∞)) \to \|G (y) - G (X)\| \leq ⦋ X / x ⦌ B$
110	82 109	eqbrtrd	$⊢ ((φ \land G \underset{ℝ}{⇝} L) \land y \in [X, +∞)) \to \|G (X) - G (y)\| \leq ⦋ X / x ⦌ B$
111	24 66 79 80 81 110	rlimle	$⊢ (φ \land G \underset{ℝ}{⇝} L) \to \|G (X) - L\| \leq ⦋ X / x ⦌ B$

Metamath Proof Explorer

Theorem dvfsumrlim2

Proof