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 = ℤ_{\geq M}$
	itgulm.m	$⊢ φ \to M \in ℤ$
	itgulm.f	$⊢ φ \to F : Z ⟶ 𝐿^{1}$
	itgulm.u	$⊢ φ \to F \underset{u}{⇝} (S) G$
	itgulm.s	$⊢ φ \to vol (S) \in ℝ$
Assertion	itgulm	$⊢ φ \to (k \in Z ⟼ \int_{S} F (k) (x) d x) ⇝ \int_{S} G (x) d x$

Proof

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

Metamath Proof Explorer

Theorem itgulm

Proof