itg2i1fseq

Description: Subject to the conditions coming from mbfi1fseq , the integral of the sequence of simple functions converges to the integral of the target function. (Contributed by Mario Carneiro, 17-Aug-2014)

	Ref	Expression
Hypotheses	itg2i1fseq.1	$⊢ φ \to F \in MblFn$
	itg2i1fseq.2	$⊢ φ \to F : ℝ ⟶ [0, +∞)$
	itg2i1fseq.3	$⊢ φ \to P : ℕ ⟶ dom \int^{1}$
	itg2i1fseq.4	$⊢ φ \to \forall n \in ℕ (0_{𝑝} \leq_{f} P (n) \land P (n) \leq_{f} P (n + 1))$
	itg2i1fseq.5	$⊢ φ \to \forall x \in ℝ (n \in ℕ ⟼ P (n) (x)) ⇝ F (x)$
	itg2i1fseq.6	$⊢ S = (m \in ℕ ⟼ \int^{1} (P (m)))$
Assertion	itg2i1fseq	$⊢ φ \to \int^{2} (F) = sup (ran S ℝ^{*} <)$

Proof

Step	Hyp	Ref	Expression
1		itg2i1fseq.1	$⊢ φ \to F \in MblFn$
2		itg2i1fseq.2	$⊢ φ \to F : ℝ ⟶ [0, +∞)$
3		itg2i1fseq.3	$⊢ φ \to P : ℕ ⟶ dom \int^{1}$
4		itg2i1fseq.4	$⊢ φ \to \forall n \in ℕ (0_{𝑝} \leq_{f} P (n) \land P (n) \leq_{f} P (n + 1))$
5		itg2i1fseq.5	$⊢ φ \to \forall x \in ℝ (n \in ℕ ⟼ P (n) (x)) ⇝ F (x)$
6		itg2i1fseq.6	$⊢ S = (m \in ℕ ⟼ \int^{1} (P (m)))$
7		fveq2	$⊢ n = m \to P (n) = P (m)$
8	7	fveq1d	$⊢ n = m \to P (n) (x) = P (m) (x)$
9	8	cbvmptv	$⊢ (n \in ℕ ⟼ P (n) (x)) = (m \in ℕ ⟼ P (m) (x))$
10		fveq2	$⊢ x = y \to P (m) (x) = P (m) (y)$
11	10	mpteq2dv	$⊢ x = y \to (m \in ℕ ⟼ P (m) (x)) = (m \in ℕ ⟼ P (m) (y))$
12	9 11	syl5eq	$⊢ x = y \to (n \in ℕ ⟼ P (n) (x)) = (m \in ℕ ⟼ P (m) (y))$
13	12	rneqd	$⊢ x = y \to ran (n \in ℕ ⟼ P (n) (x)) = ran (m \in ℕ ⟼ P (m) (y))$
14	13	supeq1d	$⊢ x = y \to sup (ran (n \in ℕ ⟼ P (n) (x)) ℝ <) = sup (ran (m \in ℕ ⟼ P (m) (y)) ℝ <)$
15	14	cbvmptv	$⊢ (x \in ℝ ⟼ sup (ran (n \in ℕ ⟼ P (n) (x)) ℝ <)) = (y \in ℝ ⟼ sup (ran (m \in ℕ ⟼ P (m) (y)) ℝ <))$
16	3	ffvelrnda	$⊢ (φ \land m \in ℕ) \to P (m) \in dom \int^{1}$
17		i1fmbf	$⊢ P (m) \in dom \int^{1} \to P (m) \in MblFn$
18	16 17	syl	$⊢ (φ \land m \in ℕ) \to P (m) \in MblFn$
19		i1ff	$⊢ P (m) \in dom \int^{1} \to P (m) : ℝ ⟶ ℝ$
20	16 19	syl	$⊢ (φ \land m \in ℕ) \to P (m) : ℝ ⟶ ℝ$
21	7	breq2d	$⊢ n = m \to (0_{𝑝} \leq_{f} P (n) \leftrightarrow 0_{𝑝} \leq_{f} P (m))$
22		fvoveq1	$⊢ n = m \to P (n + 1) = P (m + 1)$
23	7 22	breq12d	$⊢ n = m \to (P (n) \leq_{f} P (n + 1) \leftrightarrow P (m) \leq_{f} P (m + 1))$
24	21 23	anbi12d	$⊢ n = m \to ((0_{𝑝} \leq_{f} P (n) \land P (n) \leq_{f} P (n + 1)) \leftrightarrow (0_{𝑝} \leq_{f} P (m) \land P (m) \leq_{f} P (m + 1)))$
25	24	rspccva	$⊢ (\forall n \in ℕ (0_{𝑝} \leq_{f} P (n) \land P (n) \leq_{f} P (n + 1)) \land m \in ℕ) \to (0_{𝑝} \leq_{f} P (m) \land P (m) \leq_{f} P (m + 1))$
26	4 25	sylan	$⊢ (φ \land m \in ℕ) \to (0_{𝑝} \leq_{f} P (m) \land P (m) \leq_{f} P (m + 1))$
27	26	simpld	$⊢ (φ \land m \in ℕ) \to 0_{𝑝} \leq_{f} P (m)$
28		0plef	$⊢ P (m) : ℝ ⟶ [0, +∞) \leftrightarrow (P (m) : ℝ ⟶ ℝ \land 0_{𝑝} \leq_{f} P (m))$
29	20 27 28	sylanbrc	$⊢ (φ \land m \in ℕ) \to P (m) : ℝ ⟶ [0, +∞)$
30	26	simprd	$⊢ (φ \land m \in ℕ) \to P (m) \leq_{f} P (m + 1)$
31		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
32	2	ffvelrnda	$⊢ (φ \land y \in ℝ) \to F (y) \in [0, +∞)$
33	31 32	sseldi	$⊢ (φ \land y \in ℝ) \to F (y) \in ℝ$
34	1 2 3 4 5	itg2i1fseqle	$⊢ (φ \land m \in ℕ) \to P (m) \leq_{f} F$
35	20	ffnd	$⊢ (φ \land m \in ℕ) \to P (m) Fn ℝ$
36	2	ffnd	$⊢ φ \to F Fn ℝ$
37	36	adantr	$⊢ (φ \land m \in ℕ) \to F Fn ℝ$
38		reex	$⊢ ℝ \in V$
39	38	a1i	$⊢ (φ \land m \in ℕ) \to ℝ \in V$
40		inidm	$⊢ ℝ \cap ℝ = ℝ$
41		eqidd	$⊢ ((φ \land m \in ℕ) \land y \in ℝ) \to P (m) (y) = P (m) (y)$
42		eqidd	$⊢ ((φ \land m \in ℕ) \land y \in ℝ) \to F (y) = F (y)$
43	35 37 39 39 40 41 42	ofrfval	$⊢ (φ \land m \in ℕ) \to (P (m) \leq_{f} F \leftrightarrow \forall y \in ℝ P (m) (y) \leq F (y))$
44	34 43	mpbid	$⊢ (φ \land m \in ℕ) \to \forall y \in ℝ P (m) (y) \leq F (y)$
45	44	r19.21bi	$⊢ ((φ \land m \in ℕ) \land y \in ℝ) \to P (m) (y) \leq F (y)$
46	45	an32s	$⊢ ((φ \land y \in ℝ) \land m \in ℕ) \to P (m) (y) \leq F (y)$
47	46	ralrimiva	$⊢ (φ \land y \in ℝ) \to \forall m \in ℕ P (m) (y) \leq F (y)$
48		brralrspcev	$⊢ (F (y) \in ℝ \land \forall m \in ℕ P (m) (y) \leq F (y)) \to \exists z \in ℝ \forall m \in ℕ P (m) (y) \leq z$
49	33 47 48	syl2anc	$⊢ (φ \land y \in ℝ) \to \exists z \in ℝ \forall m \in ℕ P (m) (y) \leq z$
50	7	fveq2d	$⊢ n = m \to \int^{2} (P (n)) = \int^{2} (P (m))$
51	50	cbvmptv	$⊢ (n \in ℕ ⟼ \int^{2} (P (n))) = (m \in ℕ ⟼ \int^{2} (P (m)))$
52	51	rneqi	$⊢ ran (n \in ℕ ⟼ \int^{2} (P (n))) = ran (m \in ℕ ⟼ \int^{2} (P (m)))$
53	52	supeq1i	$⊢ sup (ran (n \in ℕ ⟼ \int^{2} (P (n))) ℝ^{} <) = sup (ran (m \in ℕ ⟼ \int^{2} (P (m))) ℝ^{} <)$
54	15 18 29 30 49 53	itg2mono	$⊢ φ \to \int^{2} ((x \in ℝ ⟼ sup (ran (n \in ℕ ⟼ P (n) (x)) ℝ <))) = sup (ran (n \in ℕ ⟼ \int^{2} (P (n))) ℝ^{*} <)$
55	2	feqmptd	$⊢ φ \to F = (y \in ℝ ⟼ F (y))$
56	7	fveq1d	$⊢ n = m \to P (n) (y) = P (m) (y)$
57	56	cbvmptv	$⊢ (n \in ℕ ⟼ P (n) (y)) = (m \in ℕ ⟼ P (m) (y))$
58	57	rneqi	$⊢ ran (n \in ℕ ⟼ P (n) (y)) = ran (m \in ℕ ⟼ P (m) (y))$
59	58	supeq1i	$⊢ sup (ran (n \in ℕ ⟼ P (n) (y)) ℝ <) = sup (ran (m \in ℕ ⟼ P (m) (y)) ℝ <)$
60		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
61		1zzd	$⊢ (φ \land y \in ℝ) \to 1 \in ℤ$
62	20	ffvelrnda	$⊢ ((φ \land m \in ℕ) \land y \in ℝ) \to P (m) (y) \in ℝ$
63	62	an32s	$⊢ ((φ \land y \in ℝ) \land m \in ℕ) \to P (m) (y) \in ℝ$
64	63 57	fmptd	$⊢ (φ \land y \in ℝ) \to (n \in ℕ ⟼ P (n) (y)) : ℕ ⟶ ℝ$
65		peano2nn	$⊢ m \in ℕ \to m + 1 \in ℕ$
66		ffvelrn	$⊢ (P : ℕ ⟶ dom \int^{1} \land m + 1 \in ℕ) \to P (m + 1) \in dom \int^{1}$
67	3 65 66	syl2an	$⊢ (φ \land m \in ℕ) \to P (m + 1) \in dom \int^{1}$
68		i1ff	$⊢ P (m + 1) \in dom \int^{1} \to P (m + 1) : ℝ ⟶ ℝ$
69	67 68	syl	$⊢ (φ \land m \in ℕ) \to P (m + 1) : ℝ ⟶ ℝ$
70	69	ffnd	$⊢ (φ \land m \in ℕ) \to P (m + 1) Fn ℝ$
71		eqidd	$⊢ ((φ \land m \in ℕ) \land y \in ℝ) \to P (m + 1) (y) = P (m + 1) (y)$
72	35 70 39 39 40 41 71	ofrfval	$⊢ (φ \land m \in ℕ) \to (P (m) \leq_{f} P (m + 1) \leftrightarrow \forall y \in ℝ P (m) (y) \leq P (m + 1) (y))$
73	30 72	mpbid	$⊢ (φ \land m \in ℕ) \to \forall y \in ℝ P (m) (y) \leq P (m + 1) (y)$
74	73	r19.21bi	$⊢ ((φ \land m \in ℕ) \land y \in ℝ) \to P (m) (y) \leq P (m + 1) (y)$
75	74	an32s	$⊢ ((φ \land y \in ℝ) \land m \in ℕ) \to P (m) (y) \leq P (m + 1) (y)$
76		eqid	$⊢ (n \in ℕ ⟼ P (n) (y)) = (n \in ℕ ⟼ P (n) (y))$
77		fvex	$⊢ P (m) (y) \in V$
78	56 76 77	fvmpt	$⊢ m \in ℕ \to (n \in ℕ ⟼ P (n) (y)) (m) = P (m) (y)$
79	78	adantl	$⊢ ((φ \land y \in ℝ) \land m \in ℕ) \to (n \in ℕ ⟼ P (n) (y)) (m) = P (m) (y)$
80		fveq2	$⊢ n = m + 1 \to P (n) = P (m + 1)$
81	80	fveq1d	$⊢ n = m + 1 \to P (n) (y) = P (m + 1) (y)$
82		fvex	$⊢ P (m + 1) (y) \in V$
83	81 76 82	fvmpt	$⊢ m + 1 \in ℕ \to (n \in ℕ ⟼ P (n) (y)) (m + 1) = P (m + 1) (y)$
84	65 83	syl	$⊢ m \in ℕ \to (n \in ℕ ⟼ P (n) (y)) (m + 1) = P (m + 1) (y)$
85	84	adantl	$⊢ ((φ \land y \in ℝ) \land m \in ℕ) \to (n \in ℕ ⟼ P (n) (y)) (m + 1) = P (m + 1) (y)$
86	75 79 85	3brtr4d	$⊢ ((φ \land y \in ℝ) \land m \in ℕ) \to (n \in ℕ ⟼ P (n) (y)) (m) \leq (n \in ℕ ⟼ P (n) (y)) (m + 1)$
87	78	breq1d	$⊢ m \in ℕ \to ((n \in ℕ ⟼ P (n) (y)) (m) \leq z \leftrightarrow P (m) (y) \leq z)$
88	87	ralbiia	$⊢ \forall m \in ℕ (n \in ℕ ⟼ P (n) (y)) (m) \leq z \leftrightarrow \forall m \in ℕ P (m) (y) \leq z$
89	88	rexbii	$⊢ \exists z \in ℝ \forall m \in ℕ (n \in ℕ ⟼ P (n) (y)) (m) \leq z \leftrightarrow \exists z \in ℝ \forall m \in ℕ P (m) (y) \leq z$
90	49 89	sylibr	$⊢ (φ \land y \in ℝ) \to \exists z \in ℝ \forall m \in ℕ (n \in ℕ ⟼ P (n) (y)) (m) \leq z$
91	60 61 64 86 90	climsup	$⊢ (φ \land y \in ℝ) \to (n \in ℕ ⟼ P (n) (y)) ⇝ sup (ran (n \in ℕ ⟼ P (n) (y)) ℝ <)$
92		fveq2	$⊢ x = y \to P (n) (x) = P (n) (y)$
93	92	mpteq2dv	$⊢ x = y \to (n \in ℕ ⟼ P (n) (x)) = (n \in ℕ ⟼ P (n) (y))$
94		fveq2	$⊢ x = y \to F (x) = F (y)$
95	93 94	breq12d	$⊢ x = y \to ((n \in ℕ ⟼ P (n) (x)) ⇝ F (x) \leftrightarrow (n \in ℕ ⟼ P (n) (y)) ⇝ F (y))$
96	95	rspccva	$⊢ (\forall x \in ℝ (n \in ℕ ⟼ P (n) (x)) ⇝ F (x) \land y \in ℝ) \to (n \in ℕ ⟼ P (n) (y)) ⇝ F (y)$
97	5 96	sylan	$⊢ (φ \land y \in ℝ) \to (n \in ℕ ⟼ P (n) (y)) ⇝ F (y)$
98		climuni	$⊢ ((n \in ℕ ⟼ P (n) (y)) ⇝ sup (ran (n \in ℕ ⟼ P (n) (y)) ℝ <) \land (n \in ℕ ⟼ P (n) (y)) ⇝ F (y)) \to sup (ran (n \in ℕ ⟼ P (n) (y)) ℝ <) = F (y)$
99	91 97 98	syl2anc	$⊢ (φ \land y \in ℝ) \to sup (ran (n \in ℕ ⟼ P (n) (y)) ℝ <) = F (y)$
100	59 99	syl5eqr	$⊢ (φ \land y \in ℝ) \to sup (ran (m \in ℕ ⟼ P (m) (y)) ℝ <) = F (y)$
101	100	mpteq2dva	$⊢ φ \to (y \in ℝ ⟼ sup (ran (m \in ℕ ⟼ P (m) (y)) ℝ <)) = (y \in ℝ ⟼ F (y))$
102	55 101	eqtr4d	$⊢ φ \to F = (y \in ℝ ⟼ sup (ran (m \in ℕ ⟼ P (m) (y)) ℝ <))$
103	102 15	eqtr4di	$⊢ φ \to F = (x \in ℝ ⟼ sup (ran (n \in ℕ ⟼ P (n) (x)) ℝ <))$
104	103	fveq2d	$⊢ φ \to \int^{2} (F) = \int^{2} ((x \in ℝ ⟼ sup (ran (n \in ℕ ⟼ P (n) (x)) ℝ <)))$
105		itg2itg1	$⊢ (P (m) \in dom \int^{1} \land 0_{𝑝} \leq_{f} P (m)) \to \int^{2} (P (m)) = \int^{1} (P (m))$
106	16 27 105	syl2anc	$⊢ (φ \land m \in ℕ) \to \int^{2} (P (m)) = \int^{1} (P (m))$
107	106	mpteq2dva	$⊢ φ \to (m \in ℕ ⟼ \int^{2} (P (m))) = (m \in ℕ ⟼ \int^{1} (P (m)))$
108	6 107	eqtr4id	$⊢ φ \to S = (m \in ℕ ⟼ \int^{2} (P (m)))$
109	108 51	eqtr4di	$⊢ φ \to S = (n \in ℕ ⟼ \int^{2} (P (n)))$
110	109	rneqd	$⊢ φ \to ran S = ran (n \in ℕ ⟼ \int^{2} (P (n)))$
111	110	supeq1d	$⊢ φ \to sup (ran S ℝ^{} <) = sup (ran (n \in ℕ ⟼ \int^{2} (P (n))) ℝ^{} <)$
112	54 104 111	3eqtr4d	$⊢ φ \to \int^{2} (F) = sup (ran S ℝ^{*} <)$

Metamath Proof Explorer

Theorem itg2i1fseq

Proof