dvfsumrlim

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 A ( x ) = S. u e. ( M , x ) B ( u ) _d u 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$
Assertion	dvfsumrlim	$⊢ φ \to G \in dom \underset{ℝ}{⇝}$

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		ioossre	$⊢ (T, +∞) \subseteq ℝ$
16	1 15	eqsstri	$⊢ S \subseteq ℝ$
17	16	a1i	$⊢ φ \to S \subseteq ℝ$
18	1 2 3 4 5 6 7 8 9 10 11 13	dvfsumrlimf	$⊢ φ \to G : S ⟶ ℝ$
19		ax-resscn	$⊢ ℝ \subseteq ℂ$
20		fss	$⊢ (G : S ⟶ ℝ \land ℝ \subseteq ℂ) \to G : S ⟶ ℂ$
21	18 19 20	sylancl	$⊢ φ \to G : S ⟶ ℂ$
22	1	supeq1i	$⊢ sup (S ℝ^{} <) = sup ((T, +∞) ℝ^{} <)$
23		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
24	23 6	sselid	$⊢ φ \to T \in ℝ^{*}$
25	6	renepnfd	$⊢ φ \to T \neq +∞$
26		ioopnfsup	$⊢ (T \in ℝ^{} \land T \neq +∞) \to sup ((T, +∞) ℝ^{} <) = +∞$
27	24 25 26	syl2anc	$⊢ φ \to sup ((T, +∞) ℝ^{*} <) = +∞$
28	22 27	eqtrid	$⊢ φ \to sup (S ℝ^{*} <) = +∞$
29	8 14	rlimmptrcl	$⊢ (φ \land x \in S) \to B \in ℂ$
30	29	ralrimiva	$⊢ φ \to \forall x \in S B \in ℂ$
31	30 17	rlim0	$⊢ φ \to ((x \in S ⟼ B) \underset{ℝ}{⇝} 0 \leftrightarrow \forall e \in ℝ^{+} \exists c \in ℝ \forall x \in S (c \leq x \to \|B\| < e))$
32	14 31	mpbid	$⊢ φ \to \forall e \in ℝ^{+} \exists c \in ℝ \forall x \in S (c \leq x \to \|B\| < e)$
33	16	a1i	$⊢ (φ \land e \in ℝ^{+}) \to S \subseteq ℝ$
34		peano2re	$⊢ T \in ℝ \to T + 1 \in ℝ$
35	6 34	syl	$⊢ φ \to T + 1 \in ℝ$
36	35 4	ifcld	$⊢ φ \to if (D \leq T + 1, T + 1, D) \in ℝ$
37	36	adantr	$⊢ (φ \land e \in ℝ^{+}) \to if (D \leq T + 1, T + 1, D) \in ℝ$
38		rexico	$⊢ (S \subseteq ℝ \land if (D \leq T + 1, T + 1, D) \in ℝ) \to (\exists c \in [if (D \leq T + 1, T + 1, D), +∞) \forall x \in S (c \leq x \to \|B\| < e) \leftrightarrow \exists c \in ℝ \forall x \in S (c \leq x \to \|B\| < e))$
39	33 37 38	syl2anc	$⊢ (φ \land e \in ℝ^{+}) \to (\exists c \in [if (D \leq T + 1, T + 1, D), +∞) \forall x \in S (c \leq x \to \|B\| < e) \leftrightarrow \exists c \in ℝ \forall x \in S (c \leq x \to \|B\| < e))$
40		elicopnf	$⊢ if (D \leq T + 1, T + 1, D) \in ℝ \to (c \in [if (D \leq T + 1, T + 1, D), +∞) \leftrightarrow (c \in ℝ \land if (D \leq T + 1, T + 1, D) \leq c))$
41	36 40	syl	$⊢ φ \to (c \in [if (D \leq T + 1, T + 1, D), +∞) \leftrightarrow (c \in ℝ \land if (D \leq T + 1, T + 1, D) \leq c))$
42	41	simprbda	$⊢ (φ \land c \in [if (D \leq T + 1, T + 1, D), +∞)) \to c \in ℝ$
43	6	adantr	$⊢ (φ \land c \in [if (D \leq T + 1, T + 1, D), +∞)) \to T \in ℝ$
44	43 34	syl	$⊢ (φ \land c \in [if (D \leq T + 1, T + 1, D), +∞)) \to T + 1 \in ℝ$
45	43	ltp1d	$⊢ (φ \land c \in [if (D \leq T + 1, T + 1, D), +∞)) \to T < T + 1$
46	41	simplbda	$⊢ (φ \land c \in [if (D \leq T + 1, T + 1, D), +∞)) \to if (D \leq T + 1, T + 1, D) \leq c$
47	4	adantr	$⊢ (φ \land c \in [if (D \leq T + 1, T + 1, D), +∞)) \to D \in ℝ$
48		maxle	$⊢ (D \in ℝ \land T + 1 \in ℝ \land c \in ℝ) \to (if (D \leq T + 1, T + 1, D) \leq c \leftrightarrow (D \leq c \land T + 1 \leq c))$
49	47 44 42 48	syl3anc	$⊢ (φ \land c \in [if (D \leq T + 1, T + 1, D), +∞)) \to (if (D \leq T + 1, T + 1, D) \leq c \leftrightarrow (D \leq c \land T + 1 \leq c))$
50	46 49	mpbid	$⊢ (φ \land c \in [if (D \leq T + 1, T + 1, D), +∞)) \to (D \leq c \land T + 1 \leq c)$
51	50	simprd	$⊢ (φ \land c \in [if (D \leq T + 1, T + 1, D), +∞)) \to T + 1 \leq c$
52	43 44 42 45 51	ltletrd	$⊢ (φ \land c \in [if (D \leq T + 1, T + 1, D), +∞)) \to T < c$
53	24	adantr	$⊢ (φ \land c \in [if (D \leq T + 1, T + 1, D), +∞)) \to T \in ℝ^{*}$
54		elioopnf	$⊢ T \in ℝ^{*} \to (c \in (T, +∞) \leftrightarrow (c \in ℝ \land T < c))$
55	53 54	syl	$⊢ (φ \land c \in [if (D \leq T + 1, T + 1, D), +∞)) \to (c \in (T, +∞) \leftrightarrow (c \in ℝ \land T < c))$
56	42 52 55	mpbir2and	$⊢ (φ \land c \in [if (D \leq T + 1, T + 1, D), +∞)) \to c \in (T, +∞)$
57	56 1	eleqtrrdi	$⊢ (φ \land c \in [if (D \leq T + 1, T + 1, D), +∞)) \to c \in S$
58	50	simpld	$⊢ (φ \land c \in [if (D \leq T + 1, T + 1, D), +∞)) \to D \leq c$
59	57 58	jca	$⊢ (φ \land c \in [if (D \leq T + 1, T + 1, D), +∞)) \to (c \in S \land D \leq c)$
60	59	adantlr	$⊢ ((φ \land e \in ℝ^{+}) \land c \in [if (D \leq T + 1, T + 1, D), +∞)) \to (c \in S \land D \leq c)$
61		simprrl	$⊢ (φ \land (e \in ℝ^{+} \land (c \in S \land D \leq c))) \to c \in S$
62	61	adantrr	$⊢ (φ \land ((e \in ℝ^{+} \land (c \in S \land D \leq c)) \land (y \in S \land c \leq y))) \to c \in S$
63	16 62	sselid	$⊢ (φ \land ((e \in ℝ^{+} \land (c \in S \land D \leq c)) \land (y \in S \land c \leq y))) \to c \in ℝ$
64	63	leidd	$⊢ (φ \land ((e \in ℝ^{+} \land (c \in S \land D \leq c)) \land (y \in S \land c \leq y))) \to c \leq c$
65		nfv	$⊢ Ⅎ x c \leq c$
66		nfcv	$⊢ \underline{Ⅎ} x abs$
67		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ c / x ⦌ B$
68	66 67	nffv	$⊢ \underline{Ⅎ} x \|⦋ c / x ⦌ B\|$
69		nfcv	$⊢ \underline{Ⅎ} x <$
70		nfcv	$⊢ \underline{Ⅎ} x e$
71	68 69 70	nfbr	$⊢ Ⅎ x \|⦋ c / x ⦌ B\| < e$
72	65 71	nfim	$⊢ Ⅎ x (c \leq c \to \|⦋ c / x ⦌ B\| < e)$
73		breq2	$⊢ x = c \to (c \leq x \leftrightarrow c \leq c)$
74		csbeq1a	$⊢ x = c \to B = ⦋ c / x ⦌ B$
75	74	fveq2d	$⊢ x = c \to \|B\| = \|⦋ c / x ⦌ B\|$
76	75	breq1d	$⊢ x = c \to (\|B\| < e \leftrightarrow \|⦋ c / x ⦌ B\| < e)$
77	73 76	imbi12d	$⊢ x = c \to ((c \leq x \to \|B\| < e) \leftrightarrow (c \leq c \to \|⦋ c / x ⦌ B\| < e))$
78	72 77	rspc	$⊢ c \in S \to (\forall x \in S (c \leq x \to \|B\| < e) \to (c \leq c \to \|⦋ c / x ⦌ B\| < e))$
79	62 78	syl	$⊢ (φ \land ((e \in ℝ^{+} \land (c \in S \land D \leq c)) \land (y \in S \land c \leq y))) \to (\forall x \in S (c \leq x \to \|B\| < e) \to (c \leq c \to \|⦋ c / x ⦌ B\| < e))$
80	64 79	mpid	$⊢ (φ \land ((e \in ℝ^{+} \land (c \in S \land D \leq c)) \land (y \in S \land c \leq y))) \to (\forall x \in S (c \leq x \to \|B\| < e) \to \|⦋ c / x ⦌ B\| < e)$
81	17 7 8 10	dvmptrecl	$⊢ (φ \land x \in S) \to B \in ℝ$
82	81	adantrr	$⊢ (φ \land (x \in S \land D \leq x)) \to B \in ℝ$
83	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$
84		elrege0	$⊢ B \in [0, +∞) \leftrightarrow (B \in ℝ \land 0 \leq B)$
85	82 83 84	sylanbrc	$⊢ (φ \land (x \in S \land D \leq x)) \to B \in [0, +∞)$
86	85	expr	$⊢ (φ \land x \in S) \to (D \leq x \to B \in [0, +∞))$
87	86	ralrimiva	$⊢ φ \to \forall x \in S (D \leq x \to B \in [0, +∞))$
88	87	adantr	$⊢ (φ \land ((e \in ℝ^{+} \land (c \in S \land D \leq c)) \land (y \in S \land c \leq y))) \to \forall x \in S (D \leq x \to B \in [0, +∞))$
89		simprrr	$⊢ (φ \land (e \in ℝ^{+} \land (c \in S \land D \leq c))) \to D \leq c$
90	89	adantrr	$⊢ (φ \land ((e \in ℝ^{+} \land (c \in S \land D \leq c)) \land (y \in S \land c \leq y))) \to D \leq c$
91		nfv	$⊢ Ⅎ x D \leq c$
92	67	nfel1	$⊢ Ⅎ x ⦋ c / x ⦌ B \in [0, +∞)$
93	91 92	nfim	$⊢ Ⅎ x (D \leq c \to ⦋ c / x ⦌ B \in [0, +∞))$
94		breq2	$⊢ x = c \to (D \leq x \leftrightarrow D \leq c)$
95	74	eleq1d	$⊢ x = c \to (B \in [0, +∞) \leftrightarrow ⦋ c / x ⦌ B \in [0, +∞))$
96	94 95	imbi12d	$⊢ x = c \to ((D \leq x \to B \in [0, +∞)) \leftrightarrow (D \leq c \to ⦋ c / x ⦌ B \in [0, +∞)))$
97	93 96	rspc	$⊢ c \in S \to (\forall x \in S (D \leq x \to B \in [0, +∞)) \to (D \leq c \to ⦋ c / x ⦌ B \in [0, +∞)))$
98	62 88 90 97	syl3c	$⊢ (φ \land ((e \in ℝ^{+} \land (c \in S \land D \leq c)) \land (y \in S \land c \leq y))) \to ⦋ c / x ⦌ B \in [0, +∞)$
99		elrege0	$⊢ ⦋ c / x ⦌ B \in [0, +∞) \leftrightarrow (⦋ c / x ⦌ B \in ℝ \land 0 \leq ⦋ c / x ⦌ B)$
100	98 99	sylib	$⊢ (φ \land ((e \in ℝ^{+} \land (c \in S \land D \leq c)) \land (y \in S \land c \leq y))) \to (⦋ c / x ⦌ B \in ℝ \land 0 \leq ⦋ c / x ⦌ B)$
101		absid	$⊢ (⦋ c / x ⦌ B \in ℝ \land 0 \leq ⦋ c / x ⦌ B) \to \|⦋ c / x ⦌ B\| = ⦋ c / x ⦌ B$
102	100 101	syl	$⊢ (φ \land ((e \in ℝ^{+} \land (c \in S \land D \leq c)) \land (y \in S \land c \leq y))) \to \|⦋ c / x ⦌ B\| = ⦋ c / x ⦌ B$
103	102	breq1d	$⊢ (φ \land ((e \in ℝ^{+} \land (c \in S \land D \leq c)) \land (y \in S \land c \leq y))) \to (\|⦋ c / x ⦌ B\| < e \leftrightarrow ⦋ c / x ⦌ B < e)$
104	3	adantr	$⊢ (φ \land ((e \in ℝ^{+} \land (c \in S \land D \leq c)) \land (y \in S \land c \leq y))) \to M \in ℤ$
105	4	adantr	$⊢ (φ \land ((e \in ℝ^{+} \land (c \in S \land D \leq c)) \land (y \in S \land c \leq y))) \to D \in ℝ$
106	5	adantr	$⊢ (φ \land ((e \in ℝ^{+} \land (c \in S \land D \leq c)) \land (y \in S \land c \leq y))) \to M \leq D + 1$
107	6	adantr	$⊢ (φ \land ((e \in ℝ^{+} \land (c \in S \land D \leq c)) \land (y \in S \land c \leq y))) \to T \in ℝ$
108	7	adantlr	$⊢ ((φ \land ((e \in ℝ^{+} \land (c \in S \land D \leq c)) \land (y \in S \land c \leq y))) \land x \in S) \to A \in ℝ$
109	8	adantlr	$⊢ ((φ \land ((e \in ℝ^{+} \land (c \in S \land D \leq c)) \land (y \in S \land c \leq y))) \land x \in S) \to B \in V$
110	9	adantlr	$⊢ ((φ \land ((e \in ℝ^{+} \land (c \in S \land D \leq c)) \land (y \in S \land c \leq y))) \land x \in Z) \to B \in ℝ$
111	10	adantr	$⊢ (φ \land ((e \in ℝ^{+} \land (c \in S \land D \leq c)) \land (y \in S \land c \leq y))) \to \frac{d (x \in S⟼ A)}{d_{ℝ} x} = (x \in S ⟼ B)$
112		pnfxr	$⊢ +∞ \in ℝ^{*}$
113	112	a1i	$⊢ (φ \land ((e \in ℝ^{+} \land (c \in S \land D \leq c)) \land (y \in S \land c \leq y))) \to +∞ \in ℝ^{*}$
114		3simpa	$⊢ (D \leq x \land x \leq k \land k \leq +∞) \to (D \leq x \land x \leq k)$
115	114 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$
116	115	3adant1r	$⊢ ((φ \land ((e \in ℝ^{+} \land (c \in S \land D \leq c)) \land (y \in S \land c \leq y))) \land (x \in S \land k \in S) \land (D \leq x \land x \leq k \land k \leq +∞)) \to C \leq B$
117	83	3adantr3	$⊢ (φ \land (x \in S \land D \leq x \land x \leq +∞)) \to 0 \leq B$
118	117	adantlr	$⊢ ((φ \land ((e \in ℝ^{+} \land (c \in S \land D \leq c)) \land (y \in S \land c \leq y))) \land (x \in S \land D \leq x \land x \leq +∞)) \to 0 \leq B$
119		simprrl	$⊢ (φ \land ((e \in ℝ^{+} \land (c \in S \land D \leq c)) \land (y \in S \land c \leq y))) \to y \in S$
120		simprrr	$⊢ (φ \land ((e \in ℝ^{+} \land (c \in S \land D \leq c)) \land (y \in S \land c \leq y))) \to c \leq y$
121	16 23	sstri	$⊢ S \subseteq ℝ^{*}$
122	121 119	sselid	$⊢ (φ \land ((e \in ℝ^{+} \land (c \in S \land D \leq c)) \land (y \in S \land c \leq y))) \to y \in ℝ^{*}$
123		pnfge	$⊢ y \in ℝ^{*} \to y \leq +∞$
124	122 123	syl	$⊢ (φ \land ((e \in ℝ^{+} \land (c \in S \land D \leq c)) \land (y \in S \land c \leq y))) \to y \leq +∞$
125	1 2 104 105 106 107 108 109 110 111 11 113 116 13 118 62 119 90 120 124	dvfsumlem4	$⊢ (φ \land ((e \in ℝ^{+} \land (c \in S \land D \leq c)) \land (y \in S \land c \leq y))) \to \|G (y) - G (c)\| \leq ⦋ c / x ⦌ B$
126	21	adantr	$⊢ (φ \land ((e \in ℝ^{+} \land (c \in S \land D \leq c)) \land (y \in S \land c \leq y))) \to G : S ⟶ ℂ$
127	126 119	ffvelrnd	$⊢ (φ \land ((e \in ℝ^{+} \land (c \in S \land D \leq c)) \land (y \in S \land c \leq y))) \to G (y) \in ℂ$
128	126 62	ffvelrnd	$⊢ (φ \land ((e \in ℝ^{+} \land (c \in S \land D \leq c)) \land (y \in S \land c \leq y))) \to G (c) \in ℂ$
129	127 128	subcld	$⊢ (φ \land ((e \in ℝ^{+} \land (c \in S \land D \leq c)) \land (y \in S \land c \leq y))) \to G (y) - G (c) \in ℂ$
130	129	abscld	$⊢ (φ \land ((e \in ℝ^{+} \land (c \in S \land D \leq c)) \land (y \in S \land c \leq y))) \to \|G (y) - G (c)\| \in ℝ$
131	100	simpld	$⊢ (φ \land ((e \in ℝ^{+} \land (c \in S \land D \leq c)) \land (y \in S \land c \leq y))) \to ⦋ c / x ⦌ B \in ℝ$
132		simprll	$⊢ (φ \land ((e \in ℝ^{+} \land (c \in S \land D \leq c)) \land (y \in S \land c \leq y))) \to e \in ℝ^{+}$
133	132	rpred	$⊢ (φ \land ((e \in ℝ^{+} \land (c \in S \land D \leq c)) \land (y \in S \land c \leq y))) \to e \in ℝ$
134		lelttr	$⊢ (\|G (y) - G (c)\| \in ℝ \land ⦋ c / x ⦌ B \in ℝ \land e \in ℝ) \to ((\|G (y) - G (c)\| \leq ⦋ c / x ⦌ B \land ⦋ c / x ⦌ B < e) \to \|G (y) - G (c)\| < e)$
135	130 131 133 134	syl3anc	$⊢ (φ \land ((e \in ℝ^{+} \land (c \in S \land D \leq c)) \land (y \in S \land c \leq y))) \to ((\|G (y) - G (c)\| \leq ⦋ c / x ⦌ B \land ⦋ c / x ⦌ B < e) \to \|G (y) - G (c)\| < e)$
136	125 135	mpand	$⊢ (φ \land ((e \in ℝ^{+} \land (c \in S \land D \leq c)) \land (y \in S \land c \leq y))) \to (⦋ c / x ⦌ B < e \to \|G (y) - G (c)\| < e)$
137	103 136	sylbid	$⊢ (φ \land ((e \in ℝ^{+} \land (c \in S \land D \leq c)) \land (y \in S \land c \leq y))) \to (\|⦋ c / x ⦌ B\| < e \to \|G (y) - G (c)\| < e)$
138	80 137	syld	$⊢ (φ \land ((e \in ℝ^{+} \land (c \in S \land D \leq c)) \land (y \in S \land c \leq y))) \to (\forall x \in S (c \leq x \to \|B\| < e) \to \|G (y) - G (c)\| < e)$
139	138	anassrs	$⊢ ((φ \land (e \in ℝ^{+} \land (c \in S \land D \leq c))) \land (y \in S \land c \leq y)) \to (\forall x \in S (c \leq x \to \|B\| < e) \to \|G (y) - G (c)\| < e)$
140	139	expr	$⊢ ((φ \land (e \in ℝ^{+} \land (c \in S \land D \leq c))) \land y \in S) \to (c \leq y \to (\forall x \in S (c \leq x \to \|B\| < e) \to \|G (y) - G (c)\| < e))$
141	140	com23	$⊢ ((φ \land (e \in ℝ^{+} \land (c \in S \land D \leq c))) \land y \in S) \to (\forall x \in S (c \leq x \to \|B\| < e) \to (c \leq y \to \|G (y) - G (c)\| < e))$
142	141	ralrimdva	$⊢ (φ \land (e \in ℝ^{+} \land (c \in S \land D \leq c))) \to (\forall x \in S (c \leq x \to \|B\| < e) \to \forall y \in S (c \leq y \to \|G (y) - G (c)\| < e))$
143	142 61	jctild	$⊢ (φ \land (e \in ℝ^{+} \land (c \in S \land D \leq c))) \to (\forall x \in S (c \leq x \to \|B\| < e) \to (c \in S \land \forall y \in S (c \leq y \to \|G (y) - G (c)\| < e)))$
144	143	anassrs	$⊢ ((φ \land e \in ℝ^{+}) \land (c \in S \land D \leq c)) \to (\forall x \in S (c \leq x \to \|B\| < e) \to (c \in S \land \forall y \in S (c \leq y \to \|G (y) - G (c)\| < e)))$
145	60 144	syldan	$⊢ ((φ \land e \in ℝ^{+}) \land c \in [if (D \leq T + 1, T + 1, D), +∞)) \to (\forall x \in S (c \leq x \to \|B\| < e) \to (c \in S \land \forall y \in S (c \leq y \to \|G (y) - G (c)\| < e)))$
146	145	expimpd	$⊢ (φ \land e \in ℝ^{+}) \to ((c \in [if (D \leq T + 1, T + 1, D), +∞) \land \forall x \in S (c \leq x \to \|B\| < e)) \to (c \in S \land \forall y \in S (c \leq y \to \|G (y) - G (c)\| < e)))$
147	146	reximdv2	$⊢ (φ \land e \in ℝ^{+}) \to (\exists c \in [if (D \leq T + 1, T + 1, D), +∞) \forall x \in S (c \leq x \to \|B\| < e) \to \exists c \in S \forall y \in S (c \leq y \to \|G (y) - G (c)\| < e))$
148	39 147	sylbird	$⊢ (φ \land e \in ℝ^{+}) \to (\exists c \in ℝ \forall x \in S (c \leq x \to \|B\| < e) \to \exists c \in S \forall y \in S (c \leq y \to \|G (y) - G (c)\| < e))$
149	148	ralimdva	$⊢ φ \to (\forall e \in ℝ^{+} \exists c \in ℝ \forall x \in S (c \leq x \to \|B\| < e) \to \forall e \in ℝ^{+} \exists c \in S \forall y \in S (c \leq y \to \|G (y) - G (c)\| < e))$
150	32 149	mpd	$⊢ φ \to \forall e \in ℝ^{+} \exists c \in S \forall y \in S (c \leq y \to \|G (y) - G (c)\| < e)$
151	17 21 28 150	caucvgr	$⊢ φ \to G \in dom \underset{ℝ}{⇝}$

Metamath Proof Explorer

Theorem dvfsumrlim

Proof