itg2mono

Description: The Monotone Convergence Theorem for nonnegative functions. If { ( Fn ) : n e. NN } is a monotone increasing sequence of positive, measurable, real-valued functions, and G is the pointwise limit of the sequence, then ( S.2G ) is the limit of the sequence { ( S.2( Fn ) ) : n e. NN } . (Contributed by Mario Carneiro, 16-Aug-2014)

	Ref	Expression
Hypotheses	itg2mono.1	$⊢ G = (x \in ℝ ⟼ sup (ran (n \in ℕ ⟼ F (n) (x)) ℝ <))$
	itg2mono.2	$⊢ (φ \land n \in ℕ) \to F (n) \in MblFn$
	itg2mono.3	$⊢ (φ \land n \in ℕ) \to F (n) : ℝ ⟶ [0, +∞)$
	itg2mono.4	$⊢ (φ \land n \in ℕ) \to F (n) \leq_{f} F (n + 1)$
	itg2mono.5	$⊢ (φ \land x \in ℝ) \to \exists y \in ℝ \forall n \in ℕ F (n) (x) \leq y$
	itg2mono.6	$⊢ S = sup (ran (n \in ℕ ⟼ \int^{2} (F (n))) ℝ^{*} <)$
Assertion	itg2mono	$⊢ φ \to \int^{2} (G) = S$

Proof

Step	Hyp	Ref	Expression
1		itg2mono.1	$⊢ G = (x \in ℝ ⟼ sup (ran (n \in ℕ ⟼ F (n) (x)) ℝ <))$
2		itg2mono.2	$⊢ (φ \land n \in ℕ) \to F (n) \in MblFn$
3		itg2mono.3	$⊢ (φ \land n \in ℕ) \to F (n) : ℝ ⟶ [0, +∞)$
4		itg2mono.4	$⊢ (φ \land n \in ℕ) \to F (n) \leq_{f} F (n + 1)$
5		itg2mono.5	$⊢ (φ \land x \in ℝ) \to \exists y \in ℝ \forall n \in ℕ F (n) (x) \leq y$
6		itg2mono.6	$⊢ S = sup (ran (n \in ℕ ⟼ \int^{2} (F (n))) ℝ^{*} <)$
7		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
8		fss	$⊢ (F (n) : ℝ ⟶ [0, +∞) \land [0, +∞) \subseteq ℝ) \to F (n) : ℝ ⟶ ℝ$
9	3 7 8	sylancl	$⊢ (φ \land n \in ℕ) \to F (n) : ℝ ⟶ ℝ$
10	9	ffvelcdmda	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to F (n) (x) \in ℝ$
11	10	an32s	$⊢ ((φ \land x \in ℝ) \land n \in ℕ) \to F (n) (x) \in ℝ$
12	11	fmpttd	$⊢ (φ \land x \in ℝ) \to (n \in ℕ ⟼ F (n) (x)) : ℕ ⟶ ℝ$
13	12	frnd	$⊢ (φ \land x \in ℝ) \to ran (n \in ℕ ⟼ F (n) (x)) \subseteq ℝ$
14		1nn	$⊢ 1 \in ℕ$
15		eqid	$⊢ (n \in ℕ ⟼ F (n) (x)) = (n \in ℕ ⟼ F (n) (x))$
16	15 11	dmmptd	$⊢ (φ \land x \in ℝ) \to dom (n \in ℕ ⟼ F (n) (x)) = ℕ$
17	14 16	eleqtrrid	$⊢ (φ \land x \in ℝ) \to 1 \in dom (n \in ℕ ⟼ F (n) (x))$
18	17	ne0d	$⊢ (φ \land x \in ℝ) \to dom (n \in ℕ ⟼ F (n) (x)) \neq \emptyset$
19		dm0rn0	$⊢ dom (n \in ℕ ⟼ F (n) (x)) = \emptyset \leftrightarrow ran (n \in ℕ ⟼ F (n) (x)) = \emptyset$
20	19	necon3bii	$⊢ dom (n \in ℕ ⟼ F (n) (x)) \neq \emptyset \leftrightarrow ran (n \in ℕ ⟼ F (n) (x)) \neq \emptyset$
21	18 20	sylib	$⊢ (φ \land x \in ℝ) \to ran (n \in ℕ ⟼ F (n) (x)) \neq \emptyset$
22	12	ffnd	$⊢ (φ \land x \in ℝ) \to (n \in ℕ ⟼ F (n) (x)) Fn ℕ$
23		breq1	$⊢ z = (n \in ℕ ⟼ F (n) (x)) (m) \to (z \leq y \leftrightarrow (n \in ℕ ⟼ F (n) (x)) (m) \leq y)$
24	23	ralrn	$⊢ (n \in ℕ ⟼ F (n) (x)) Fn ℕ \to (\forall z \in ran (n \in ℕ ⟼ F (n) (x)) z \leq y \leftrightarrow \forall m \in ℕ (n \in ℕ ⟼ F (n) (x)) (m) \leq y)$
25	22 24	syl	$⊢ (φ \land x \in ℝ) \to (\forall z \in ran (n \in ℕ ⟼ F (n) (x)) z \leq y \leftrightarrow \forall m \in ℕ (n \in ℕ ⟼ F (n) (x)) (m) \leq y)$
26		fveq2	$⊢ n = m \to F (n) = F (m)$
27	26	fveq1d	$⊢ n = m \to F (n) (x) = F (m) (x)$
28		fvex	$⊢ F (m) (x) \in V$
29	27 15 28	fvmpt	$⊢ m \in ℕ \to (n \in ℕ ⟼ F (n) (x)) (m) = F (m) (x)$
30	29	breq1d	$⊢ m \in ℕ \to ((n \in ℕ ⟼ F (n) (x)) (m) \leq y \leftrightarrow F (m) (x) \leq y)$
31	30	ralbiia	$⊢ \forall m \in ℕ (n \in ℕ ⟼ F (n) (x)) (m) \leq y \leftrightarrow \forall m \in ℕ F (m) (x) \leq y$
32	27	breq1d	$⊢ n = m \to (F (n) (x) \leq y \leftrightarrow F (m) (x) \leq y)$
33	32	cbvralvw	$⊢ \forall n \in ℕ F (n) (x) \leq y \leftrightarrow \forall m \in ℕ F (m) (x) \leq y$
34	31 33	bitr4i	$⊢ \forall m \in ℕ (n \in ℕ ⟼ F (n) (x)) (m) \leq y \leftrightarrow \forall n \in ℕ F (n) (x) \leq y$
35	25 34	bitrdi	$⊢ (φ \land x \in ℝ) \to (\forall z \in ran (n \in ℕ ⟼ F (n) (x)) z \leq y \leftrightarrow \forall n \in ℕ F (n) (x) \leq y)$
36	35	rexbidv	$⊢ (φ \land x \in ℝ) \to (\exists y \in ℝ \forall z \in ran (n \in ℕ ⟼ F (n) (x)) z \leq y \leftrightarrow \exists y \in ℝ \forall n \in ℕ F (n) (x) \leq y)$
37	5 36	mpbird	$⊢ (φ \land x \in ℝ) \to \exists y \in ℝ \forall z \in ran (n \in ℕ ⟼ F (n) (x)) z \leq y$
38	13 21 37	suprcld	$⊢ (φ \land x \in ℝ) \to sup (ran (n \in ℕ ⟼ F (n) (x)) ℝ <) \in ℝ$
39	38	rexrd	$⊢ (φ \land x \in ℝ) \to sup (ran (n \in ℕ ⟼ F (n) (x)) ℝ <) \in ℝ^{*}$
40		0red	$⊢ (φ \land x \in ℝ) \to 0 \in ℝ$
41		fveq2	$⊢ n = 1 \to F (n) = F (1)$
42	41	feq1d	$⊢ n = 1 \to (F (n) : ℝ ⟶ [0, +∞) \leftrightarrow F (1) : ℝ ⟶ [0, +∞))$
43	3	ralrimiva	$⊢ φ \to \forall n \in ℕ F (n) : ℝ ⟶ [0, +∞)$
44	14	a1i	$⊢ φ \to 1 \in ℕ$
45	42 43 44	rspcdva	$⊢ φ \to F (1) : ℝ ⟶ [0, +∞)$
46	45	ffvelcdmda	$⊢ (φ \land x \in ℝ) \to F (1) (x) \in [0, +∞)$
47		elrege0	$⊢ F (1) (x) \in [0, +∞) \leftrightarrow (F (1) (x) \in ℝ \land 0 \leq F (1) (x))$
48	46 47	sylib	$⊢ (φ \land x \in ℝ) \to (F (1) (x) \in ℝ \land 0 \leq F (1) (x))$
49	48	simpld	$⊢ (φ \land x \in ℝ) \to F (1) (x) \in ℝ$
50	48	simprd	$⊢ (φ \land x \in ℝ) \to 0 \leq F (1) (x)$
51	41	fveq1d	$⊢ n = 1 \to F (n) (x) = F (1) (x)$
52		fvex	$⊢ F (1) (x) \in V$
53	51 15 52	fvmpt	$⊢ 1 \in ℕ \to (n \in ℕ ⟼ F (n) (x)) (1) = F (1) (x)$
54	14 53	ax-mp	$⊢ (n \in ℕ ⟼ F (n) (x)) (1) = F (1) (x)$
55		fnfvelrn	$⊢ ((n \in ℕ ⟼ F (n) (x)) Fn ℕ \land 1 \in ℕ) \to (n \in ℕ ⟼ F (n) (x)) (1) \in ran (n \in ℕ ⟼ F (n) (x))$
56	22 14 55	sylancl	$⊢ (φ \land x \in ℝ) \to (n \in ℕ ⟼ F (n) (x)) (1) \in ran (n \in ℕ ⟼ F (n) (x))$
57	54 56	eqeltrrid	$⊢ (φ \land x \in ℝ) \to F (1) (x) \in ran (n \in ℕ ⟼ F (n) (x))$
58	13 21 37 57	suprubd	$⊢ (φ \land x \in ℝ) \to F (1) (x) \leq sup (ran (n \in ℕ ⟼ F (n) (x)) ℝ <)$
59	40 49 38 50 58	letrd	$⊢ (φ \land x \in ℝ) \to 0 \leq sup (ran (n \in ℕ ⟼ F (n) (x)) ℝ <)$
60		elxrge0	$⊢ sup (ran (n \in ℕ ⟼ F (n) (x)) ℝ <) \in [0, +∞] \leftrightarrow (sup (ran (n \in ℕ ⟼ F (n) (x)) ℝ <) \in ℝ^{*} \land 0 \leq sup (ran (n \in ℕ ⟼ F (n) (x)) ℝ <))$
61	39 59 60	sylanbrc	$⊢ (φ \land x \in ℝ) \to sup (ran (n \in ℕ ⟼ F (n) (x)) ℝ <) \in [0, +∞]$
62	61 1	fmptd	$⊢ φ \to G : ℝ ⟶ [0, +∞]$
63		itg2cl	$⊢ G : ℝ ⟶ [0, +∞] \to \int^{2} (G) \in ℝ^{*}$
64	62 63	syl	$⊢ φ \to \int^{2} (G) \in ℝ^{*}$
65		icossicc	$⊢ [0, +∞) \subseteq [0, +∞]$
66		fss	$⊢ (F (n) : ℝ ⟶ [0, +∞) \land [0, +∞) \subseteq [0, +∞]) \to F (n) : ℝ ⟶ [0, +∞]$
67	3 65 66	sylancl	$⊢ (φ \land n \in ℕ) \to F (n) : ℝ ⟶ [0, +∞]$
68		itg2cl	$⊢ F (n) : ℝ ⟶ [0, +∞] \to \int^{2} (F (n)) \in ℝ^{*}$
69	67 68	syl	$⊢ (φ \land n \in ℕ) \to \int^{2} (F (n)) \in ℝ^{*}$
70	69	fmpttd	$⊢ φ \to (n \in ℕ ⟼ \int^{2} (F (n))) : ℕ ⟶ ℝ^{*}$
71	70	frnd	$⊢ φ \to ran (n \in ℕ ⟼ \int^{2} (F (n))) \subseteq ℝ^{*}$
72		supxrcl	$⊢ ran (n \in ℕ ⟼ \int^{2} (F (n))) \subseteq ℝ^{} \to sup (ran (n \in ℕ ⟼ \int^{2} (F (n))) ℝ^{} <) \in ℝ^{*}$
73	71 72	syl	$⊢ φ \to sup (ran (n \in ℕ ⟼ \int^{2} (F (n))) ℝ^{} <) \in ℝ^{}$
74	6 73	eqeltrid	$⊢ φ \to S \in ℝ^{*}$
75	2	adantlr	$⊢ ((φ \land ((f \in dom \int^{1} \land f \leq_{f} G) \land \neg \int^{1} (f) \leq S)) \land n \in ℕ) \to F (n) \in MblFn$
76	3	adantlr	$⊢ ((φ \land ((f \in dom \int^{1} \land f \leq_{f} G) \land \neg \int^{1} (f) \leq S)) \land n \in ℕ) \to F (n) : ℝ ⟶ [0, +∞)$
77	4	adantlr	$⊢ ((φ \land ((f \in dom \int^{1} \land f \leq_{f} G) \land \neg \int^{1} (f) \leq S)) \land n \in ℕ) \to F (n) \leq_{f} F (n + 1)$
78	5	adantlr	$⊢ ((φ \land ((f \in dom \int^{1} \land f \leq_{f} G) \land \neg \int^{1} (f) \leq S)) \land x \in ℝ) \to \exists y \in ℝ \forall n \in ℕ F (n) (x) \leq y$
79		simprll	$⊢ (φ \land ((f \in dom \int^{1} \land f \leq_{f} G) \land \neg \int^{1} (f) \leq S)) \to f \in dom \int^{1}$
80		simprlr	$⊢ (φ \land ((f \in dom \int^{1} \land f \leq_{f} G) \land \neg \int^{1} (f) \leq S)) \to f \leq_{f} G$
81		simprr	$⊢ (φ \land ((f \in dom \int^{1} \land f \leq_{f} G) \land \neg \int^{1} (f) \leq S)) \to \neg \int^{1} (f) \leq S$
82	1 75 76 77 78 6 79 80 81	itg2monolem3	$⊢ (φ \land ((f \in dom \int^{1} \land f \leq_{f} G) \land \neg \int^{1} (f) \leq S)) \to \int^{1} (f) \leq S$
83	82	expr	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} G)) \to (\neg \int^{1} (f) \leq S \to \int^{1} (f) \leq S)$
84	83	pm2.18d	$⊢ (φ \land (f \in dom \int^{1} \land f \leq_{f} G)) \to \int^{1} (f) \leq S$
85	84	expr	$⊢ (φ \land f \in dom \int^{1}) \to (f \leq_{f} G \to \int^{1} (f) \leq S)$
86	85	ralrimiva	$⊢ φ \to \forall f \in dom \int^{1} (f \leq_{f} G \to \int^{1} (f) \leq S)$
87		itg2leub	$⊢ (G : ℝ ⟶ [0, +∞] \land S \in ℝ^{*}) \to (\int^{2} (G) \leq S \leftrightarrow \forall f \in dom \int^{1} (f \leq_{f} G \to \int^{1} (f) \leq S))$
88	62 74 87	syl2anc	$⊢ φ \to (\int^{2} (G) \leq S \leftrightarrow \forall f \in dom \int^{1} (f \leq_{f} G \to \int^{1} (f) \leq S))$
89	86 88	mpbird	$⊢ φ \to \int^{2} (G) \leq S$
90	26	feq1d	$⊢ n = m \to (F (n) : ℝ ⟶ [0, +∞) \leftrightarrow F (m) : ℝ ⟶ [0, +∞))$
91	90	cbvralvw	$⊢ \forall n \in ℕ F (n) : ℝ ⟶ [0, +∞) \leftrightarrow \forall m \in ℕ F (m) : ℝ ⟶ [0, +∞)$
92	43 91	sylib	$⊢ φ \to \forall m \in ℕ F (m) : ℝ ⟶ [0, +∞)$
93	92	r19.21bi	$⊢ (φ \land m \in ℕ) \to F (m) : ℝ ⟶ [0, +∞)$
94		fss	$⊢ (F (m) : ℝ ⟶ [0, +∞) \land [0, +∞) \subseteq [0, +∞]) \to F (m) : ℝ ⟶ [0, +∞]$
95	93 65 94	sylancl	$⊢ (φ \land m \in ℕ) \to F (m) : ℝ ⟶ [0, +∞]$
96	62	adantr	$⊢ (φ \land m \in ℕ) \to G : ℝ ⟶ [0, +∞]$
97	13 21 37	3jca	$⊢ (φ \land x \in ℝ) \to (ran (n \in ℕ ⟼ F (n) (x)) \subseteq ℝ \land ran (n \in ℕ ⟼ F (n) (x)) \neq \emptyset \land \exists y \in ℝ \forall z \in ran (n \in ℕ ⟼ F (n) (x)) z \leq y)$
98	97	adantlr	$⊢ ((φ \land m \in ℕ) \land x \in ℝ) \to (ran (n \in ℕ ⟼ F (n) (x)) \subseteq ℝ \land ran (n \in ℕ ⟼ F (n) (x)) \neq \emptyset \land \exists y \in ℝ \forall z \in ran (n \in ℕ ⟼ F (n) (x)) z \leq y)$
99	29	ad2antlr	$⊢ ((φ \land m \in ℕ) \land x \in ℝ) \to (n \in ℕ ⟼ F (n) (x)) (m) = F (m) (x)$
100	22	adantlr	$⊢ ((φ \land m \in ℕ) \land x \in ℝ) \to (n \in ℕ ⟼ F (n) (x)) Fn ℕ$
101		simplr	$⊢ ((φ \land m \in ℕ) \land x \in ℝ) \to m \in ℕ$
102		fnfvelrn	$⊢ ((n \in ℕ ⟼ F (n) (x)) Fn ℕ \land m \in ℕ) \to (n \in ℕ ⟼ F (n) (x)) (m) \in ran (n \in ℕ ⟼ F (n) (x))$
103	100 101 102	syl2anc	$⊢ ((φ \land m \in ℕ) \land x \in ℝ) \to (n \in ℕ ⟼ F (n) (x)) (m) \in ran (n \in ℕ ⟼ F (n) (x))$
104	99 103	eqeltrrd	$⊢ ((φ \land m \in ℕ) \land x \in ℝ) \to F (m) (x) \in ran (n \in ℕ ⟼ F (n) (x))$
105		suprub	$⊢ ((ran (n \in ℕ ⟼ F (n) (x)) \subseteq ℝ \land ran (n \in ℕ ⟼ F (n) (x)) \neq \emptyset \land \exists y \in ℝ \forall z \in ran (n \in ℕ ⟼ F (n) (x)) z \leq y) \land F (m) (x) \in ran (n \in ℕ ⟼ F (n) (x))) \to F (m) (x) \leq sup (ran (n \in ℕ ⟼ F (n) (x)) ℝ <)$
106	98 104 105	syl2anc	$⊢ ((φ \land m \in ℕ) \land x \in ℝ) \to F (m) (x) \leq sup (ran (n \in ℕ ⟼ F (n) (x)) ℝ <)$
107		simpr	$⊢ ((φ \land m \in ℕ) \land x \in ℝ) \to x \in ℝ$
108		ltso	$⊢ < Or ℝ$
109	108	supex	$⊢ sup (ran (n \in ℕ ⟼ F (n) (x)) ℝ <) \in V$
110	1	fvmpt2	$⊢ (x \in ℝ \land sup (ran (n \in ℕ ⟼ F (n) (x)) ℝ <) \in V) \to G (x) = sup (ran (n \in ℕ ⟼ F (n) (x)) ℝ <)$
111	107 109 110	sylancl	$⊢ ((φ \land m \in ℕ) \land x \in ℝ) \to G (x) = sup (ran (n \in ℕ ⟼ F (n) (x)) ℝ <)$
112	106 111	breqtrrd	$⊢ ((φ \land m \in ℕ) \land x \in ℝ) \to F (m) (x) \leq G (x)$
113	112	ralrimiva	$⊢ (φ \land m \in ℕ) \to \forall x \in ℝ F (m) (x) \leq G (x)$
114		fveq2	$⊢ x = z \to F (m) (x) = F (m) (z)$
115		fveq2	$⊢ x = z \to G (x) = G (z)$
116	114 115	breq12d	$⊢ x = z \to (F (m) (x) \leq G (x) \leftrightarrow F (m) (z) \leq G (z))$
117	116	cbvralvw	$⊢ \forall x \in ℝ F (m) (x) \leq G (x) \leftrightarrow \forall z \in ℝ F (m) (z) \leq G (z)$
118	113 117	sylib	$⊢ (φ \land m \in ℕ) \to \forall z \in ℝ F (m) (z) \leq G (z)$
119	93	ffnd	$⊢ (φ \land m \in ℕ) \to F (m) Fn ℝ$
120	38 1	fmptd	$⊢ φ \to G : ℝ ⟶ ℝ$
121	120	ffnd	$⊢ φ \to G Fn ℝ$
122	121	adantr	$⊢ (φ \land m \in ℕ) \to G Fn ℝ$
123		reex	$⊢ ℝ \in V$
124	123	a1i	$⊢ (φ \land m \in ℕ) \to ℝ \in V$
125		inidm	$⊢ ℝ \cap ℝ = ℝ$
126		eqidd	$⊢ ((φ \land m \in ℕ) \land z \in ℝ) \to F (m) (z) = F (m) (z)$
127		eqidd	$⊢ ((φ \land m \in ℕ) \land z \in ℝ) \to G (z) = G (z)$
128	119 122 124 124 125 126 127	ofrfval	$⊢ (φ \land m \in ℕ) \to (F (m) \leq_{f} G \leftrightarrow \forall z \in ℝ F (m) (z) \leq G (z))$
129	118 128	mpbird	$⊢ (φ \land m \in ℕ) \to F (m) \leq_{f} G$
130		itg2le	$⊢ (F (m) : ℝ ⟶ [0, +∞] \land G : ℝ ⟶ [0, +∞] \land F (m) \leq_{f} G) \to \int^{2} (F (m)) \leq \int^{2} (G)$
131	95 96 129 130	syl3anc	$⊢ (φ \land m \in ℕ) \to \int^{2} (F (m)) \leq \int^{2} (G)$
132	131	ralrimiva	$⊢ φ \to \forall m \in ℕ \int^{2} (F (m)) \leq \int^{2} (G)$
133	70	ffnd	$⊢ φ \to (n \in ℕ ⟼ \int^{2} (F (n))) Fn ℕ$
134		breq1	$⊢ z = (n \in ℕ ⟼ \int^{2} (F (n))) (m) \to (z \leq \int^{2} (G) \leftrightarrow (n \in ℕ ⟼ \int^{2} (F (n))) (m) \leq \int^{2} (G))$
135	134	ralrn	$⊢ (n \in ℕ ⟼ \int^{2} (F (n))) Fn ℕ \to (\forall z \in ran (n \in ℕ ⟼ \int^{2} (F (n))) z \leq \int^{2} (G) \leftrightarrow \forall m \in ℕ (n \in ℕ ⟼ \int^{2} (F (n))) (m) \leq \int^{2} (G))$
136	133 135	syl	$⊢ φ \to (\forall z \in ran (n \in ℕ ⟼ \int^{2} (F (n))) z \leq \int^{2} (G) \leftrightarrow \forall m \in ℕ (n \in ℕ ⟼ \int^{2} (F (n))) (m) \leq \int^{2} (G))$
137		2fveq3	$⊢ n = m \to \int^{2} (F (n)) = \int^{2} (F (m))$
138		eqid	$⊢ (n \in ℕ ⟼ \int^{2} (F (n))) = (n \in ℕ ⟼ \int^{2} (F (n)))$
139		fvex	$⊢ \int^{2} (F (m)) \in V$
140	137 138 139	fvmpt	$⊢ m \in ℕ \to (n \in ℕ ⟼ \int^{2} (F (n))) (m) = \int^{2} (F (m))$
141	140	breq1d	$⊢ m \in ℕ \to ((n \in ℕ ⟼ \int^{2} (F (n))) (m) \leq \int^{2} (G) \leftrightarrow \int^{2} (F (m)) \leq \int^{2} (G))$
142	141	ralbiia	$⊢ \forall m \in ℕ (n \in ℕ ⟼ \int^{2} (F (n))) (m) \leq \int^{2} (G) \leftrightarrow \forall m \in ℕ \int^{2} (F (m)) \leq \int^{2} (G)$
143	136 142	bitrdi	$⊢ φ \to (\forall z \in ran (n \in ℕ ⟼ \int^{2} (F (n))) z \leq \int^{2} (G) \leftrightarrow \forall m \in ℕ \int^{2} (F (m)) \leq \int^{2} (G))$
144	132 143	mpbird	$⊢ φ \to \forall z \in ran (n \in ℕ ⟼ \int^{2} (F (n))) z \leq \int^{2} (G)$
145		supxrleub	$⊢ (ran (n \in ℕ ⟼ \int^{2} (F (n))) \subseteq ℝ^{} \land \int^{2} (G) \in ℝ^{}) \to (sup (ran (n \in ℕ ⟼ \int^{2} (F (n))) ℝ^{*} <) \leq \int^{2} (G) \leftrightarrow \forall z \in ran (n \in ℕ ⟼ \int^{2} (F (n))) z \leq \int^{2} (G))$
146	71 64 145	syl2anc	$⊢ φ \to (sup (ran (n \in ℕ ⟼ \int^{2} (F (n))) ℝ^{*} <) \leq \int^{2} (G) \leftrightarrow \forall z \in ran (n \in ℕ ⟼ \int^{2} (F (n))) z \leq \int^{2} (G))$
147	144 146	mpbird	$⊢ φ \to sup (ran (n \in ℕ ⟼ \int^{2} (F (n))) ℝ^{*} <) \leq \int^{2} (G)$
148	6 147	eqbrtrid	$⊢ φ \to S \leq \int^{2} (G)$
149	64 74 89 148	xrletrid	$⊢ φ \to \int^{2} (G) = S$

Metamath Proof Explorer

Theorem itg2mono

Proof