itg2monolem2

	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))) ℝ^{*} <)$
	itg2monolem2.7	$⊢ φ \to P \in dom \int^{1}$
	itg2monolem2.8	$⊢ φ \to P \leq_{f} G$
	itg2monolem2.9	$⊢ φ \to \neg \int^{1} (P) \leq S$
Assertion	itg2monolem2	$⊢ φ \to S \in ℝ$

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		itg2monolem2.7	$⊢ φ \to P \in dom \int^{1}$
8		itg2monolem2.8	$⊢ φ \to P \leq_{f} G$
9		itg2monolem2.9	$⊢ φ \to \neg \int^{1} (P) \leq S$
10		icossicc	$⊢ [0, +∞) \subseteq [0, +∞]$
11		fss	$⊢ (F (n) : ℝ ⟶ [0, +∞) \land [0, +∞) \subseteq [0, +∞]) \to F (n) : ℝ ⟶ [0, +∞]$
12	3 10 11	sylancl	$⊢ (φ \land n \in ℕ) \to F (n) : ℝ ⟶ [0, +∞]$
13		itg2cl	$⊢ F (n) : ℝ ⟶ [0, +∞] \to \int^{2} (F (n)) \in ℝ^{*}$
14	12 13	syl	$⊢ (φ \land n \in ℕ) \to \int^{2} (F (n)) \in ℝ^{*}$
15	14	fmpttd	$⊢ φ \to (n \in ℕ ⟼ \int^{2} (F (n))) : ℕ ⟶ ℝ^{*}$
16	15	frnd	$⊢ φ \to ran (n \in ℕ ⟼ \int^{2} (F (n))) \subseteq ℝ^{*}$
17		supxrcl	$⊢ ran (n \in ℕ ⟼ \int^{2} (F (n))) \subseteq ℝ^{} \to sup (ran (n \in ℕ ⟼ \int^{2} (F (n))) ℝ^{} <) \in ℝ^{*}$
18	16 17	syl	$⊢ φ \to sup (ran (n \in ℕ ⟼ \int^{2} (F (n))) ℝ^{} <) \in ℝ^{}$
19	6 18	eqeltrid	$⊢ φ \to S \in ℝ^{*}$
20		itg1cl	$⊢ P \in dom \int^{1} \to \int^{1} (P) \in ℝ$
21	7 20	syl	$⊢ φ \to \int^{1} (P) \in ℝ$
22		mnfxr	$⊢ −∞ \in ℝ^{*}$
23	22	a1i	$⊢ φ \to −∞ \in ℝ^{*}$
24		fveq2	$⊢ n = 1 \to F (n) = F (1)$
25	24	feq1d	$⊢ n = 1 \to (F (n) : ℝ ⟶ [0, +∞] \leftrightarrow F (1) : ℝ ⟶ [0, +∞])$
26	12	ralrimiva	$⊢ φ \to \forall n \in ℕ F (n) : ℝ ⟶ [0, +∞]$
27		1nn	$⊢ 1 \in ℕ$
28	27	a1i	$⊢ φ \to 1 \in ℕ$
29	25 26 28	rspcdva	$⊢ φ \to F (1) : ℝ ⟶ [0, +∞]$
30		itg2cl	$⊢ F (1) : ℝ ⟶ [0, +∞] \to \int^{2} (F (1)) \in ℝ^{*}$
31	29 30	syl	$⊢ φ \to \int^{2} (F (1)) \in ℝ^{*}$
32		itg2ge0	$⊢ F (1) : ℝ ⟶ [0, +∞] \to 0 \leq \int^{2} (F (1))$
33	29 32	syl	$⊢ φ \to 0 \leq \int^{2} (F (1))$
34		mnflt0	$⊢ −∞ < 0$
35		0xr	$⊢ 0 \in ℝ^{*}$
36		xrltletr	$⊢ (−∞ \in ℝ^{} \land 0 \in ℝ^{} \land \int^{2} (F (1)) \in ℝ^{*}) \to ((−∞ < 0 \land 0 \leq \int^{2} (F (1))) \to −∞ < \int^{2} (F (1)))$
37	22 35 31 36	mp3an12i	$⊢ φ \to ((−∞ < 0 \land 0 \leq \int^{2} (F (1))) \to −∞ < \int^{2} (F (1)))$
38	34 37	mpani	$⊢ φ \to (0 \leq \int^{2} (F (1)) \to −∞ < \int^{2} (F (1)))$
39	33 38	mpd	$⊢ φ \to −∞ < \int^{2} (F (1))$
40		2fveq3	$⊢ n = 1 \to \int^{2} (F (n)) = \int^{2} (F (1))$
41		eqid	$⊢ (n \in ℕ ⟼ \int^{2} (F (n))) = (n \in ℕ ⟼ \int^{2} (F (n)))$
42		fvex	$⊢ \int^{2} (F (1)) \in V$
43	40 41 42	fvmpt	$⊢ 1 \in ℕ \to (n \in ℕ ⟼ \int^{2} (F (n))) (1) = \int^{2} (F (1))$
44	27 43	ax-mp	$⊢ (n \in ℕ ⟼ \int^{2} (F (n))) (1) = \int^{2} (F (1))$
45	15	ffnd	$⊢ φ \to (n \in ℕ ⟼ \int^{2} (F (n))) Fn ℕ$
46		fnfvelrn	$⊢ ((n \in ℕ ⟼ \int^{2} (F (n))) Fn ℕ \land 1 \in ℕ) \to (n \in ℕ ⟼ \int^{2} (F (n))) (1) \in ran (n \in ℕ ⟼ \int^{2} (F (n)))$
47	45 27 46	sylancl	$⊢ φ \to (n \in ℕ ⟼ \int^{2} (F (n))) (1) \in ran (n \in ℕ ⟼ \int^{2} (F (n)))$
48	44 47	eqeltrrid	$⊢ φ \to \int^{2} (F (1)) \in ran (n \in ℕ ⟼ \int^{2} (F (n)))$
49		supxrub	$⊢ (ran (n \in ℕ ⟼ \int^{2} (F (n))) \subseteq ℝ^{} \land \int^{2} (F (1)) \in ran (n \in ℕ ⟼ \int^{2} (F (n)))) \to \int^{2} (F (1)) \leq sup (ran (n \in ℕ ⟼ \int^{2} (F (n))) ℝ^{} <)$
50	16 48 49	syl2anc	$⊢ φ \to \int^{2} (F (1)) \leq sup (ran (n \in ℕ ⟼ \int^{2} (F (n))) ℝ^{*} <)$
51	50 6	breqtrrdi	$⊢ φ \to \int^{2} (F (1)) \leq S$
52	23 31 19 39 51	xrltletrd	$⊢ φ \to −∞ < S$
53	21	rexrd	$⊢ φ \to \int^{1} (P) \in ℝ^{*}$
54		xrltnle	$⊢ (S \in ℝ^{} \land \int^{1} (P) \in ℝ^{}) \to (S < \int^{1} (P) \leftrightarrow \neg \int^{1} (P) \leq S)$
55	19 53 54	syl2anc	$⊢ φ \to (S < \int^{1} (P) \leftrightarrow \neg \int^{1} (P) \leq S)$
56	9 55	mpbird	$⊢ φ \to S < \int^{1} (P)$
57	19 53 56	xrltled	$⊢ φ \to S \leq \int^{1} (P)$
58		xrre	$⊢ ((S \in ℝ^{*} \land \int^{1} (P) \in ℝ) \land (−∞ < S \land S \leq \int^{1} (P))) \to S \in ℝ$
59	19 21 52 57 58	syl22anc	$⊢ φ \to S \in ℝ$

Metamath Proof Explorer

Theorem itg2monolem2

Proof