# Metamath Proof Explorer

## Theorem 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}=\left({T},\mathrm{+\infty }\right)$
dvfsum.z ${⊢}{Z}={ℤ}_{\ge {M}}$
dvfsum.m ${⊢}{\phi }\to {M}\in ℤ$
dvfsum.d ${⊢}{\phi }\to {D}\in ℝ$
dvfsum.md ${⊢}{\phi }\to {M}\le {D}+1$
dvfsum.t ${⊢}{\phi }\to {T}\in ℝ$
dvfsum.a ${⊢}\left({\phi }\wedge {x}\in {S}\right)\to {A}\in ℝ$
dvfsum.b1 ${⊢}\left({\phi }\wedge {x}\in {S}\right)\to {B}\in {V}$
dvfsum.b2 ${⊢}\left({\phi }\wedge {x}\in {Z}\right)\to {B}\in ℝ$
dvfsum.b3 ${⊢}{\phi }\to \frac{d\left({x}\in {S}⟼{A}\right)}{{d}_{ℝ}{x}}=\left({x}\in {S}⟼{B}\right)$
dvfsum.c ${⊢}{x}={k}\to {B}={C}$
dvfsumrlim.l ${⊢}\left({\phi }\wedge \left({x}\in {S}\wedge {k}\in {S}\right)\wedge \left({D}\le {x}\wedge {x}\le {k}\right)\right)\to {C}\le {B}$
dvfsumrlim.g ${⊢}{G}=\left({x}\in {S}⟼\sum _{{k}={M}}^{⌊{x}⌋}{C}-{A}\right)$
dvfsumrlim.k
Assertion dvfsumrlim

### Proof

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