# Metamath Proof Explorer

## Theorem itgulm

Description: A uniform limit of integrals of integrable functions converges to the integral of the limit function. (Contributed by Mario Carneiro, 18-Mar-2015)

Ref Expression
Hypotheses itgulm.z ${⊢}{Z}={ℤ}_{\ge {M}}$
itgulm.m ${⊢}{\phi }\to {M}\in ℤ$
itgulm.f ${⊢}{\phi }\to {F}:{Z}⟶{𝐿}^{1}$
itgulm.u
itgulm.s ${⊢}{\phi }\to vol\left({S}\right)\in ℝ$
Assertion itgulm ${⊢}{\phi }\to \left({k}\in {Z}⟼{\int }_{{S}}{F}\left({k}\right)\left({x}\right)d{x}\right)⇝{\int }_{{S}}{G}\left({x}\right)d{x}$

### Proof

Step Hyp Ref Expression
1 itgulm.z ${⊢}{Z}={ℤ}_{\ge {M}}$
2 itgulm.m ${⊢}{\phi }\to {M}\in ℤ$
3 itgulm.f ${⊢}{\phi }\to {F}:{Z}⟶{𝐿}^{1}$
4 itgulm.u
5 itgulm.s ${⊢}{\phi }\to vol\left({S}\right)\in ℝ$
6 2 adantr ${⊢}\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\to {M}\in ℤ$
7 3 ffnd ${⊢}{\phi }\to {F}Fn{Z}$
8 ulmf2
9 7 4 8 syl2anc ${⊢}{\phi }\to {F}:{Z}⟶{ℂ}^{{S}}$
10 9 adantr ${⊢}\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\to {F}:{Z}⟶{ℂ}^{{S}}$
11 eqidd ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge {z}\in {S}\right)\right)\to {F}\left({n}\right)\left({z}\right)={F}\left({n}\right)\left({z}\right)$
12 eqidd ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge {z}\in {S}\right)\to {G}\left({z}\right)={G}\left({z}\right)$
14 simpr ${⊢}\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\to {r}\in {ℝ}^{+}$
15 5 adantr ${⊢}\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\to vol\left({S}\right)\in ℝ$
16 ulmcl
17 fdm ${⊢}{G}:{S}⟶ℂ\to \mathrm{dom}{G}={S}$
18 4 16 17 3syl ${⊢}{\phi }\to \mathrm{dom}{G}={S}$
19 1 2 3 4 5 iblulm ${⊢}{\phi }\to {G}\in {𝐿}^{1}$
20 iblmbf ${⊢}{G}\in {𝐿}^{1}\to {G}\in MblFn$
21 mbfdm ${⊢}{G}\in MblFn\to \mathrm{dom}{G}\in \mathrm{dom}vol$
22 19 20 21 3syl ${⊢}{\phi }\to \mathrm{dom}{G}\in \mathrm{dom}vol$
23 18 22 eqeltrrd ${⊢}{\phi }\to {S}\in \mathrm{dom}vol$
24 mblss ${⊢}{S}\in \mathrm{dom}vol\to {S}\subseteq ℝ$
25 ovolge0 ${⊢}{S}\subseteq ℝ\to 0\le {vol}^{*}\left({S}\right)$
26 23 24 25 3syl ${⊢}{\phi }\to 0\le {vol}^{*}\left({S}\right)$
27 mblvol ${⊢}{S}\in \mathrm{dom}vol\to vol\left({S}\right)={vol}^{*}\left({S}\right)$
28 23 27 syl ${⊢}{\phi }\to vol\left({S}\right)={vol}^{*}\left({S}\right)$
29 26 28 breqtrrd ${⊢}{\phi }\to 0\le vol\left({S}\right)$
30 29 adantr ${⊢}\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\to 0\le vol\left({S}\right)$
31 15 30 ge0p1rpd ${⊢}\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\to vol\left({S}\right)+1\in {ℝ}^{+}$
32 14 31 rpdivcld ${⊢}\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\to \frac{{r}}{vol\left({S}\right)+1}\in {ℝ}^{+}$
33 1 6 10 11 12 13 32 ulmi ${⊢}\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}$
34 1 uztrn2 ${⊢}\left({j}\in {Z}\wedge {n}\in {ℤ}_{\ge {j}}\right)\to {n}\in {Z}$
35 9 ffvelrnda ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {F}\left({n}\right)\in \left({ℂ}^{{S}}\right)$
36 elmapi ${⊢}{F}\left({n}\right)\in \left({ℂ}^{{S}}\right)\to {F}\left({n}\right):{S}⟶ℂ$
37 35 36 syl ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {F}\left({n}\right):{S}⟶ℂ$
38 37 ffvelrnda ${⊢}\left(\left({\phi }\wedge {n}\in {Z}\right)\wedge {x}\in {S}\right)\to {F}\left({n}\right)\left({x}\right)\in ℂ$
39 38 adantllr ${⊢}\left(\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge {n}\in {Z}\right)\wedge {x}\in {S}\right)\to {F}\left({n}\right)\left({x}\right)\in ℂ$
40 39 adantlrr ${⊢}\left(\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\wedge {x}\in {S}\right)\to {F}\left({n}\right)\left({x}\right)\in ℂ$
41 37 feqmptd ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {F}\left({n}\right)=\left({x}\in {S}⟼{F}\left({n}\right)\left({x}\right)\right)$
42 3 ffvelrnda ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {F}\left({n}\right)\in {𝐿}^{1}$
43 41 42 eqeltrrd ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to \left({x}\in {S}⟼{F}\left({n}\right)\left({x}\right)\right)\in {𝐿}^{1}$
44 43 ad2ant2r ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\to \left({x}\in {S}⟼{F}\left({n}\right)\left({x}\right)\right)\in {𝐿}^{1}$
45 4 16 syl ${⊢}{\phi }\to {G}:{S}⟶ℂ$
46 45 ffvelrnda ${⊢}\left({\phi }\wedge {x}\in {S}\right)\to {G}\left({x}\right)\in ℂ$
47 46 ad4ant14 ${⊢}\left(\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\wedge {x}\in {S}\right)\to {G}\left({x}\right)\in ℂ$
48 45 feqmptd ${⊢}{\phi }\to {G}=\left({x}\in {S}⟼{G}\left({x}\right)\right)$
49 48 19 eqeltrrd ${⊢}{\phi }\to \left({x}\in {S}⟼{G}\left({x}\right)\right)\in {𝐿}^{1}$
50 49 ad2antrr ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\to \left({x}\in {S}⟼{G}\left({x}\right)\right)\in {𝐿}^{1}$
51 40 44 47 50 itgsub ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\to {\int }_{{S}}\left({F}\left({n}\right)\left({x}\right)-{G}\left({x}\right)\right)d{x}={\int }_{{S}}{F}\left({n}\right)\left({x}\right)d{x}-{\int }_{{S}}{G}\left({x}\right)d{x}$
52 51 fveq2d ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\to \left|{\int }_{{S}}\left({F}\left({n}\right)\left({x}\right)-{G}\left({x}\right)\right)d{x}\right|=\left|{\int }_{{S}}{F}\left({n}\right)\left({x}\right)d{x}-{\int }_{{S}}{G}\left({x}\right)d{x}\right|$
53 40 47 subcld ${⊢}\left(\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\wedge {x}\in {S}\right)\to {F}\left({n}\right)\left({x}\right)-{G}\left({x}\right)\in ℂ$
54 40 44 47 50 iblsub ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\to \left({x}\in {S}⟼{F}\left({n}\right)\left({x}\right)-{G}\left({x}\right)\right)\in {𝐿}^{1}$
55 53 54 itgcl ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\to {\int }_{{S}}\left({F}\left({n}\right)\left({x}\right)-{G}\left({x}\right)\right)d{x}\in ℂ$
56 55 abscld ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\to \left|{\int }_{{S}}\left({F}\left({n}\right)\left({x}\right)-{G}\left({x}\right)\right)d{x}\right|\in ℝ$
57 53 abscld ${⊢}\left(\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\wedge {x}\in {S}\right)\to \left|{F}\left({n}\right)\left({x}\right)-{G}\left({x}\right)\right|\in ℝ$
58 53 54 iblabs ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\to \left({x}\in {S}⟼\left|{F}\left({n}\right)\left({x}\right)-{G}\left({x}\right)\right|\right)\in {𝐿}^{1}$
59 57 58 itgrecl ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\to {\int }_{{S}}\left|{F}\left({n}\right)\left({x}\right)-{G}\left({x}\right)\right|d{x}\in ℝ$
60 rpre ${⊢}{r}\in {ℝ}^{+}\to {r}\in ℝ$
61 60 ad2antlr ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\to {r}\in ℝ$
62 53 54 itgabs ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\to \left|{\int }_{{S}}\left({F}\left({n}\right)\left({x}\right)-{G}\left({x}\right)\right)d{x}\right|\le {\int }_{{S}}\left|{F}\left({n}\right)\left({x}\right)-{G}\left({x}\right)\right|d{x}$
63 32 adantr ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\to \frac{{r}}{vol\left({S}\right)+1}\in {ℝ}^{+}$
64 63 rpred ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\to \frac{{r}}{vol\left({S}\right)+1}\in ℝ$
65 5 ad2antrr ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\to vol\left({S}\right)\in ℝ$
66 64 65 remulcld ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\to \left(\frac{{r}}{vol\left({S}\right)+1}\right)vol\left({S}\right)\in ℝ$
67 fconstmpt ${⊢}{S}×\left\{\frac{{r}}{vol\left({S}\right)+1}\right\}=\left({x}\in {S}⟼\frac{{r}}{vol\left({S}\right)+1}\right)$
68 23 ad2antrr ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\to {S}\in \mathrm{dom}vol$
69 63 rpcnd ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\to \frac{{r}}{vol\left({S}\right)+1}\in ℂ$
70 iblconst ${⊢}\left({S}\in \mathrm{dom}vol\wedge vol\left({S}\right)\in ℝ\wedge \frac{{r}}{vol\left({S}\right)+1}\in ℂ\right)\to {S}×\left\{\frac{{r}}{vol\left({S}\right)+1}\right\}\in {𝐿}^{1}$
71 68 65 69 70 syl3anc ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\to {S}×\left\{\frac{{r}}{vol\left({S}\right)+1}\right\}\in {𝐿}^{1}$
72 67 71 eqeltrrid ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\to \left({x}\in {S}⟼\frac{{r}}{vol\left({S}\right)+1}\right)\in {𝐿}^{1}$
73 64 adantr ${⊢}\left(\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\wedge {x}\in {S}\right)\to \frac{{r}}{vol\left({S}\right)+1}\in ℝ$
74 simprr ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\to \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}$
75 fveq2 ${⊢}{z}={x}\to {F}\left({n}\right)\left({z}\right)={F}\left({n}\right)\left({x}\right)$
76 fveq2 ${⊢}{z}={x}\to {G}\left({z}\right)={G}\left({x}\right)$
77 75 76 oveq12d ${⊢}{z}={x}\to {F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)={F}\left({n}\right)\left({x}\right)-{G}\left({x}\right)$
78 77 fveq2d ${⊢}{z}={x}\to \left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|=\left|{F}\left({n}\right)\left({x}\right)-{G}\left({x}\right)\right|$
79 78 breq1d ${⊢}{z}={x}\to \left(\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}↔\left|{F}\left({n}\right)\left({x}\right)-{G}\left({x}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)$
80 79 rspccva ${⊢}\left(\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\wedge {x}\in {S}\right)\to \left|{F}\left({n}\right)\left({x}\right)-{G}\left({x}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}$
81 74 80 sylan ${⊢}\left(\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\wedge {x}\in {S}\right)\to \left|{F}\left({n}\right)\left({x}\right)-{G}\left({x}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}$
82 57 73 81 ltled ${⊢}\left(\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\wedge {x}\in {S}\right)\to \left|{F}\left({n}\right)\left({x}\right)-{G}\left({x}\right)\right|\le \frac{{r}}{vol\left({S}\right)+1}$
83 58 72 57 73 82 itgle ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\to {\int }_{{S}}\left|{F}\left({n}\right)\left({x}\right)-{G}\left({x}\right)\right|d{x}\le {\int }_{{S}}\left(\frac{{r}}{vol\left({S}\right)+1}\right)d{x}$
84 itgconst ${⊢}\left({S}\in \mathrm{dom}vol\wedge vol\left({S}\right)\in ℝ\wedge \frac{{r}}{vol\left({S}\right)+1}\in ℂ\right)\to {\int }_{{S}}\left(\frac{{r}}{vol\left({S}\right)+1}\right)d{x}=\left(\frac{{r}}{vol\left({S}\right)+1}\right)vol\left({S}\right)$
85 68 65 69 84 syl3anc ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\to {\int }_{{S}}\left(\frac{{r}}{vol\left({S}\right)+1}\right)d{x}=\left(\frac{{r}}{vol\left({S}\right)+1}\right)vol\left({S}\right)$
86 83 85 breqtrd ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\to {\int }_{{S}}\left|{F}\left({n}\right)\left({x}\right)-{G}\left({x}\right)\right|d{x}\le \left(\frac{{r}}{vol\left({S}\right)+1}\right)vol\left({S}\right)$
87 61 recnd ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\to {r}\in ℂ$
88 65 recnd ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\to vol\left({S}\right)\in ℂ$
89 31 adantr ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\to vol\left({S}\right)+1\in {ℝ}^{+}$
90 89 rpcnd ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\to vol\left({S}\right)+1\in ℂ$
91 89 rpne0d ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\to vol\left({S}\right)+1\ne 0$
92 87 88 90 91 div23d ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\to \frac{{r}vol\left({S}\right)}{vol\left({S}\right)+1}=\left(\frac{{r}}{vol\left({S}\right)+1}\right)vol\left({S}\right)$
93 65 ltp1d ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\to vol\left({S}\right)
94 peano2re ${⊢}vol\left({S}\right)\in ℝ\to vol\left({S}\right)+1\in ℝ$
95 65 94 syl ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\to vol\left({S}\right)+1\in ℝ$
96 rpgt0 ${⊢}{r}\in {ℝ}^{+}\to 0<{r}$
97 96 ad2antlr ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\to 0<{r}$
98 ltmul2 ${⊢}\left(vol\left({S}\right)\in ℝ\wedge vol\left({S}\right)+1\in ℝ\wedge \left({r}\in ℝ\wedge 0<{r}\right)\right)\to \left(vol\left({S}\right)
99 65 95 61 97 98 syl112anc ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\to \left(vol\left({S}\right)
100 93 99 mpbid ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\to {r}vol\left({S}\right)<{r}\left(vol\left({S}\right)+1\right)$
101 61 65 remulcld ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\to {r}vol\left({S}\right)\in ℝ$
102 101 61 89 ltdivmul2d ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\to \left(\frac{{r}vol\left({S}\right)}{vol\left({S}\right)+1}<{r}↔{r}vol\left({S}\right)<{r}\left(vol\left({S}\right)+1\right)\right)$
103 100 102 mpbird ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\to \frac{{r}vol\left({S}\right)}{vol\left({S}\right)+1}<{r}$
104 92 103 eqbrtrrd ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\to \left(\frac{{r}}{vol\left({S}\right)+1}\right)vol\left({S}\right)<{r}$
105 59 66 61 86 104 lelttrd ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\to {\int }_{{S}}\left|{F}\left({n}\right)\left({x}\right)-{G}\left({x}\right)\right|d{x}<{r}$
106 56 59 61 62 105 lelttrd ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\to \left|{\int }_{{S}}\left({F}\left({n}\right)\left({x}\right)-{G}\left({x}\right)\right)d{x}\right|<{r}$
107 52 106 eqbrtrrd ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({n}\in {Z}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\right)\right)\to \left|{\int }_{{S}}{F}\left({n}\right)\left({x}\right)d{x}-{\int }_{{S}}{G}\left({x}\right)d{x}\right|<{r}$
108 107 expr ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge {n}\in {Z}\right)\to \left(\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\to \left|{\int }_{{S}}{F}\left({n}\right)\left({x}\right)d{x}-{\int }_{{S}}{G}\left({x}\right)d{x}\right|<{r}\right)$
109 34 108 sylan2 ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge \left({j}\in {Z}\wedge {n}\in {ℤ}_{\ge {j}}\right)\right)\to \left(\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\to \left|{\int }_{{S}}{F}\left({n}\right)\left({x}\right)d{x}-{\int }_{{S}}{G}\left({x}\right)d{x}\right|<{r}\right)$
110 109 anassrs ${⊢}\left(\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge {j}\in {Z}\right)\wedge {n}\in {ℤ}_{\ge {j}}\right)\to \left(\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\to \left|{\int }_{{S}}{F}\left({n}\right)\left({x}\right)d{x}-{\int }_{{S}}{G}\left({x}\right)d{x}\right|<{r}\right)$
111 110 ralimdva ${⊢}\left(\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\wedge {j}\in {Z}\right)\to \left(\forall {n}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\to \forall {n}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{\int }_{{S}}{F}\left({n}\right)\left({x}\right)d{x}-{\int }_{{S}}{G}\left({x}\right)d{x}\right|<{r}\right)$
112 111 reximdva ${⊢}\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\to \left(\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({n}\right)\left({z}\right)-{G}\left({z}\right)\right|<\frac{{r}}{vol\left({S}\right)+1}\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{\int }_{{S}}{F}\left({n}\right)\left({x}\right)d{x}-{\int }_{{S}}{G}\left({x}\right)d{x}\right|<{r}\right)$
113 33 112 mpd ${⊢}\left({\phi }\wedge {r}\in {ℝ}^{+}\right)\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{\int }_{{S}}{F}\left({n}\right)\left({x}\right)d{x}-{\int }_{{S}}{G}\left({x}\right)d{x}\right|<{r}$
114 113 ralrimiva ${⊢}{\phi }\to \forall {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{\int }_{{S}}{F}\left({n}\right)\left({x}\right)d{x}-{\int }_{{S}}{G}\left({x}\right)d{x}\right|<{r}$
115 1 fvexi ${⊢}{Z}\in \mathrm{V}$
116 115 mptex ${⊢}\left({k}\in {Z}⟼{\int }_{{S}}{F}\left({k}\right)\left({x}\right)d{x}\right)\in \mathrm{V}$
117 116 a1i ${⊢}{\phi }\to \left({k}\in {Z}⟼{\int }_{{S}}{F}\left({k}\right)\left({x}\right)d{x}\right)\in \mathrm{V}$
118 fveq2 ${⊢}{k}={n}\to {F}\left({k}\right)={F}\left({n}\right)$
119 118 fveq1d ${⊢}{k}={n}\to {F}\left({k}\right)\left({x}\right)={F}\left({n}\right)\left({x}\right)$
120 119 adantr ${⊢}\left({k}={n}\wedge {x}\in {S}\right)\to {F}\left({k}\right)\left({x}\right)={F}\left({n}\right)\left({x}\right)$
121 120 itgeq2dv ${⊢}{k}={n}\to {\int }_{{S}}{F}\left({k}\right)\left({x}\right)d{x}={\int }_{{S}}{F}\left({n}\right)\left({x}\right)d{x}$
122 eqid ${⊢}\left({k}\in {Z}⟼{\int }_{{S}}{F}\left({k}\right)\left({x}\right)d{x}\right)=\left({k}\in {Z}⟼{\int }_{{S}}{F}\left({k}\right)\left({x}\right)d{x}\right)$
123 itgex ${⊢}{\int }_{{S}}{F}\left({n}\right)\left({x}\right)d{x}\in \mathrm{V}$
124 121 122 123 fvmpt ${⊢}{n}\in {Z}\to \left({k}\in {Z}⟼{\int }_{{S}}{F}\left({k}\right)\left({x}\right)d{x}\right)\left({n}\right)={\int }_{{S}}{F}\left({n}\right)\left({x}\right)d{x}$
125 124 adantl ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to \left({k}\in {Z}⟼{\int }_{{S}}{F}\left({k}\right)\left({x}\right)d{x}\right)\left({n}\right)={\int }_{{S}}{F}\left({n}\right)\left({x}\right)d{x}$
126 46 49 itgcl ${⊢}{\phi }\to {\int }_{{S}}{G}\left({x}\right)d{x}\in ℂ$
127 38 43 itgcl ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {\int }_{{S}}{F}\left({n}\right)\left({x}\right)d{x}\in ℂ$
128 1 2 117 125 126 127 clim2c ${⊢}{\phi }\to \left(\left({k}\in {Z}⟼{\int }_{{S}}{F}\left({k}\right)\left({x}\right)d{x}\right)⇝{\int }_{{S}}{G}\left({x}\right)d{x}↔\forall {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {n}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{\int }_{{S}}{F}\left({n}\right)\left({x}\right)d{x}-{\int }_{{S}}{G}\left({x}\right)d{x}\right|<{r}\right)$
129 114 128 mpbird ${⊢}{\phi }\to \left({k}\in {Z}⟼{\int }_{{S}}{F}\left({k}\right)\left({x}\right)d{x}\right)⇝{\int }_{{S}}{G}\left({x}\right)d{x}$