ioombl1lem2

	Ref	Expression
Hypotheses	ioombl1.b	$⊢ B = (A, +∞)$
	ioombl1.a	$⊢ φ \to A \in ℝ$
	ioombl1.e	$⊢ φ \to E \subseteq ℝ$
	ioombl1.v	$⊢ φ \to {vol}^{*} (E) \in ℝ$
	ioombl1.c	$⊢ φ \to C \in ℝ^{+}$
	ioombl1.s	$⊢ S = seq 1 (+ ((abs \circ -) \circ F))$
	ioombl1.t	$⊢ T = seq 1 (+ ((abs \circ -) \circ G))$
	ioombl1.u	$⊢ U = seq 1 (+ ((abs \circ -) \circ H))$
	ioombl1.f1	$⊢ φ \to F : ℕ ⟶ \leq \cap ℝ^{2}$
	ioombl1.f2	$⊢ φ \to E \subseteq ⋃ ran ((.) \circ F)$
	ioombl1.f3	$⊢ φ \to sup (ran S ℝ^{} <) \leq {vol}^{} (E) + C$
	ioombl1.p	$⊢ P = 1^{st} (F (n))$
	ioombl1.q	$⊢ Q = 2^{nd} (F (n))$
	ioombl1.g	$⊢ G = (n \in ℕ ⟼ ⟨if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q), Q⟩)$
	ioombl1.h	$⊢ H = (n \in ℕ ⟼ ⟨P, if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q)⟩)$
Assertion	ioombl1lem2	$⊢ φ \to sup (ran S ℝ^{*} <) \in ℝ$

Proof

Step	Hyp	Ref	Expression
1		ioombl1.b	$⊢ B = (A, +∞)$
2		ioombl1.a	$⊢ φ \to A \in ℝ$
3		ioombl1.e	$⊢ φ \to E \subseteq ℝ$
4		ioombl1.v	$⊢ φ \to {vol}^{*} (E) \in ℝ$
5		ioombl1.c	$⊢ φ \to C \in ℝ^{+}$
6		ioombl1.s	$⊢ S = seq 1 (+ ((abs \circ -) \circ F))$
7		ioombl1.t	$⊢ T = seq 1 (+ ((abs \circ -) \circ G))$
8		ioombl1.u	$⊢ U = seq 1 (+ ((abs \circ -) \circ H))$
9		ioombl1.f1	$⊢ φ \to F : ℕ ⟶ \leq \cap ℝ^{2}$
10		ioombl1.f2	$⊢ φ \to E \subseteq ⋃ ran ((.) \circ F)$
11		ioombl1.f3	$⊢ φ \to sup (ran S ℝ^{} <) \leq {vol}^{} (E) + C$
12		ioombl1.p	$⊢ P = 1^{st} (F (n))$
13		ioombl1.q	$⊢ Q = 2^{nd} (F (n))$
14		ioombl1.g	$⊢ G = (n \in ℕ ⟼ ⟨if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q), Q⟩)$
15		ioombl1.h	$⊢ H = (n \in ℕ ⟼ ⟨P, if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q)⟩)$
16		eqid	$⊢ (abs \circ -) \circ F = (abs \circ -) \circ F$
17	16 6	ovolsf	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to S : ℕ ⟶ [0, +∞)$
18	9 17	syl	$⊢ φ \to S : ℕ ⟶ [0, +∞)$
19	18	frnd	$⊢ φ \to ran S \subseteq [0, +∞)$
20		icossxr	$⊢ [0, +∞) \subseteq ℝ^{*}$
21	19 20	sstrdi	$⊢ φ \to ran S \subseteq ℝ^{*}$
22		supxrcl	$⊢ ran S \subseteq ℝ^{} \to sup (ran S ℝ^{} <) \in ℝ^{*}$
23	21 22	syl	$⊢ φ \to sup (ran S ℝ^{} <) \in ℝ^{}$
24	5	rpred	$⊢ φ \to C \in ℝ$
25	4 24	readdcld	$⊢ φ \to {vol}^{*} (E) + C \in ℝ$
26		mnfxr	$⊢ −∞ \in ℝ^{*}$
27	26	a1i	$⊢ φ \to −∞ \in ℝ^{*}$
28	18	ffnd	$⊢ φ \to S Fn ℕ$
29		1nn	$⊢ 1 \in ℕ$
30		fnfvelrn	$⊢ (S Fn ℕ \land 1 \in ℕ) \to S (1) \in ran S$
31	28 29 30	sylancl	$⊢ φ \to S (1) \in ran S$
32	21 31	sseldd	$⊢ φ \to S (1) \in ℝ^{*}$
33		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
34		ffvelcdm	$⊢ (S : ℕ ⟶ [0, +∞) \land 1 \in ℕ) \to S (1) \in [0, +∞)$
35	18 29 34	sylancl	$⊢ φ \to S (1) \in [0, +∞)$
36	33 35	sselid	$⊢ φ \to S (1) \in ℝ$
37	36	mnfltd	$⊢ φ \to −∞ < S (1)$
38		supxrub	$⊢ (ran S \subseteq ℝ^{} \land S (1) \in ran S) \to S (1) \leq sup (ran S ℝ^{} <)$
39	21 31 38	syl2anc	$⊢ φ \to S (1) \leq sup (ran S ℝ^{*} <)$
40	27 32 23 37 39	xrltletrd	$⊢ φ \to −∞ < sup (ran S ℝ^{*} <)$
41		xrre	$⊢ ((sup (ran S ℝ^{} <) \in ℝ^{} \land {vol}^{} (E) + C \in ℝ) \land (−∞ < sup (ran S ℝ^{} <) \land sup (ran S ℝ^{} <) \leq {vol}^{} (E) + C)) \to sup (ran S ℝ^{*} <) \in ℝ$
42	23 25 40 11 41	syl22anc	$⊢ φ \to sup (ran S ℝ^{*} <) \in ℝ$

Metamath Proof Explorer

Theorem ioombl1lem2

Proof