itg2i1fseq2

Description: In an extension to the results of itg2i1fseq , if there is an upper bound on the integrals of the simple functions approaching F , then S.2 F is real and the standard limit relation applies. (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)))$
	itg2i1fseq2.7	$⊢ φ \to M \in ℝ$
	itg2i1fseq2.8	$⊢ (φ \land k \in ℕ) \to \int^{1} (P (k)) \leq M$
Assertion	itg2i1fseq2	$⊢ φ \to S ⇝ \int^{2} (F)$

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		itg2i1fseq2.7	$⊢ φ \to M \in ℝ$
8		itg2i1fseq2.8	$⊢ (φ \land k \in ℕ) \to \int^{1} (P (k)) \leq M$
9		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
10		1zzd	$⊢ φ \to 1 \in ℤ$
11	3	ffvelcdmda	$⊢ (φ \land m \in ℕ) \to P (m) \in dom \int^{1}$
12		itg1cl	$⊢ P (m) \in dom \int^{1} \to \int^{1} (P (m)) \in ℝ$
13	11 12	syl	$⊢ (φ \land m \in ℕ) \to \int^{1} (P (m)) \in ℝ$
14	13 6	fmptd	$⊢ φ \to S : ℕ ⟶ ℝ$
15	3	ffvelcdmda	$⊢ (φ \land k \in ℕ) \to P (k) \in dom \int^{1}$
16		peano2nn	$⊢ k \in ℕ \to k + 1 \in ℕ$
17		ffvelcdm	$⊢ (P : ℕ ⟶ dom \int^{1} \land k + 1 \in ℕ) \to P (k + 1) \in dom \int^{1}$
18	3 16 17	syl2an	$⊢ (φ \land k \in ℕ) \to P (k + 1) \in dom \int^{1}$
19		simpr	$⊢ (0_{𝑝} \leq_{f} P (n) \land P (n) \leq_{f} P (n + 1)) \to P (n) \leq_{f} P (n + 1)$
20	19	ralimi	$⊢ \forall n \in ℕ (0_{𝑝} \leq_{f} P (n) \land P (n) \leq_{f} P (n + 1)) \to \forall n \in ℕ P (n) \leq_{f} P (n + 1)$
21	4 20	syl	$⊢ φ \to \forall n \in ℕ P (n) \leq_{f} P (n + 1)$
22		fveq2	$⊢ n = k \to P (n) = P (k)$
23		fvoveq1	$⊢ n = k \to P (n + 1) = P (k + 1)$
24	22 23	breq12d	$⊢ n = k \to (P (n) \leq_{f} P (n + 1) \leftrightarrow P (k) \leq_{f} P (k + 1))$
25	24	rspccva	$⊢ (\forall n \in ℕ P (n) \leq_{f} P (n + 1) \land k \in ℕ) \to P (k) \leq_{f} P (k + 1)$
26	21 25	sylan	$⊢ (φ \land k \in ℕ) \to P (k) \leq_{f} P (k + 1)$
27		itg1le	$⊢ (P (k) \in dom \int^{1} \land P (k + 1) \in dom \int^{1} \land P (k) \leq_{f} P (k + 1)) \to \int^{1} (P (k)) \leq \int^{1} (P (k + 1))$
28	15 18 26 27	syl3anc	$⊢ (φ \land k \in ℕ) \to \int^{1} (P (k)) \leq \int^{1} (P (k + 1))$
29		2fveq3	$⊢ m = k \to \int^{1} (P (m)) = \int^{1} (P (k))$
30		fvex	$⊢ \int^{1} (P (k)) \in V$
31	29 6 30	fvmpt	$⊢ k \in ℕ \to S (k) = \int^{1} (P (k))$
32	31	adantl	$⊢ (φ \land k \in ℕ) \to S (k) = \int^{1} (P (k))$
33		2fveq3	$⊢ m = k + 1 \to \int^{1} (P (m)) = \int^{1} (P (k + 1))$
34		fvex	$⊢ \int^{1} (P (k + 1)) \in V$
35	33 6 34	fvmpt	$⊢ k + 1 \in ℕ \to S (k + 1) = \int^{1} (P (k + 1))$
36	16 35	syl	$⊢ k \in ℕ \to S (k + 1) = \int^{1} (P (k + 1))$
37	36	adantl	$⊢ (φ \land k \in ℕ) \to S (k + 1) = \int^{1} (P (k + 1))$
38	28 32 37	3brtr4d	$⊢ (φ \land k \in ℕ) \to S (k) \leq S (k + 1)$
39	32 8	eqbrtrd	$⊢ (φ \land k \in ℕ) \to S (k) \leq M$
40	39	ralrimiva	$⊢ φ \to \forall k \in ℕ S (k) \leq M$
41		brralrspcev	$⊢ (M \in ℝ \land \forall k \in ℕ S (k) \leq M) \to \exists z \in ℝ \forall k \in ℕ S (k) \leq z$
42	7 40 41	syl2anc	$⊢ φ \to \exists z \in ℝ \forall k \in ℕ S (k) \leq z$
43	9 10 14 38 42	climsup	$⊢ φ \to S ⇝ sup (ran S ℝ <)$
44	1 2 3 4 5 6	itg2i1fseq	$⊢ φ \to \int^{2} (F) = sup (ran S ℝ^{*} <)$
45	14	frnd	$⊢ φ \to ran S \subseteq ℝ$
46	6 13	dmmptd	$⊢ φ \to dom S = ℕ$
47		1nn	$⊢ 1 \in ℕ$
48		ne0i	$⊢ 1 \in ℕ \to ℕ \neq \emptyset$
49	47 48	mp1i	$⊢ φ \to ℕ \neq \emptyset$
50	46 49	eqnetrd	$⊢ φ \to dom S \neq \emptyset$
51		dm0rn0	$⊢ dom S = \emptyset \leftrightarrow ran S = \emptyset$
52	51	necon3bii	$⊢ dom S \neq \emptyset \leftrightarrow ran S \neq \emptyset$
53	50 52	sylib	$⊢ φ \to ran S \neq \emptyset$
54		ffn	$⊢ S : ℕ ⟶ ℝ \to S Fn ℕ$
55		breq1	$⊢ y = S (k) \to (y \leq z \leftrightarrow S (k) \leq z)$
56	55	ralrn	$⊢ S Fn ℕ \to (\forall y \in ran S y \leq z \leftrightarrow \forall k \in ℕ S (k) \leq z)$
57	14 54 56	3syl	$⊢ φ \to (\forall y \in ran S y \leq z \leftrightarrow \forall k \in ℕ S (k) \leq z)$
58	57	rexbidv	$⊢ φ \to (\exists z \in ℝ \forall y \in ran S y \leq z \leftrightarrow \exists z \in ℝ \forall k \in ℕ S (k) \leq z)$
59	42 58	mpbird	$⊢ φ \to \exists z \in ℝ \forall y \in ran S y \leq z$
60		supxrre	$⊢ (ran S \subseteq ℝ \land ran S \neq \emptyset \land \exists z \in ℝ \forall y \in ran S y \leq z) \to sup (ran S ℝ^{*} <) = sup (ran S ℝ <)$
61	45 53 59 60	syl3anc	$⊢ φ \to sup (ran S ℝ^{*} <) = sup (ran S ℝ <)$
62	44 61	eqtrd	$⊢ φ \to \int^{2} (F) = sup (ran S ℝ <)$
63	43 62	breqtrrd	$⊢ φ \to S ⇝ \int^{2} (F)$

Metamath Proof Explorer

Theorem itg2i1fseq2

Proof