ioombl1lem4

	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	ioombl1lem4	$⊢ φ \to {vol}^{} (E \cap B) + {vol}^{} (E ∖ B) \leq {vol}^{*} (E) + C$

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		inss1	$⊢ E \cap B \subseteq E$
17		ovolsscl	$⊢ (E \cap B \subseteq E \land E \subseteq ℝ \land {vol}^{} (E) \in ℝ) \to {vol}^{} (E \cap B) \in ℝ$
18	16 3 4 17	mp3an2i	$⊢ φ \to {vol}^{*} (E \cap B) \in ℝ$
19		difss	$⊢ E ∖ B \subseteq E$
20		ovolsscl	$⊢ (E ∖ B \subseteq E \land E \subseteq ℝ \land {vol}^{} (E) \in ℝ) \to {vol}^{} (E ∖ B) \in ℝ$
21	19 3 4 20	mp3an2i	$⊢ φ \to {vol}^{*} (E ∖ B) \in ℝ$
22	18 21	readdcld	$⊢ φ \to {vol}^{} (E \cap B) + {vol}^{} (E ∖ B) \in ℝ$
23	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	ioombl1lem2	$⊢ φ \to sup (ran S ℝ^{*} <) \in ℝ$
24	5	rpred	$⊢ φ \to C \in ℝ$
25	4 24	readdcld	$⊢ φ \to {vol}^{*} (E) + C \in ℝ$
26	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	ioombl1lem1	$⊢ φ \to (G : ℕ ⟶ \leq \cap ℝ^{2} \land H : ℕ ⟶ \leq \cap ℝ^{2})$
27	26	simpld	$⊢ φ \to G : ℕ ⟶ \leq \cap ℝ^{2}$
28		eqid	$⊢ (abs \circ -) \circ G = (abs \circ -) \circ G$
29	28 7	ovolsf	$⊢ G : ℕ ⟶ \leq \cap ℝ^{2} \to T : ℕ ⟶ [0, +∞)$
30	27 29	syl	$⊢ φ \to T : ℕ ⟶ [0, +∞)$
31	30	frnd	$⊢ φ \to ran T \subseteq [0, +∞)$
32		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
33	31 32	sstrdi	$⊢ φ \to ran T \subseteq ℝ$
34		1nn	$⊢ 1 \in ℕ$
35	30	fdmd	$⊢ φ \to dom T = ℕ$
36	34 35	eleqtrrid	$⊢ φ \to 1 \in dom T$
37	36	ne0d	$⊢ φ \to dom T \neq \emptyset$
38		dm0rn0	$⊢ dom T = \emptyset \leftrightarrow ran T = \emptyset$
39	38	necon3bii	$⊢ dom T \neq \emptyset \leftrightarrow ran T \neq \emptyset$
40	37 39	sylib	$⊢ φ \to ran T \neq \emptyset$
41	30	ffvelrnda	$⊢ (φ \land j \in ℕ) \to T (j) \in [0, +∞)$
42	32 41	sseldi	$⊢ (φ \land j \in ℕ) \to T (j) \in ℝ$
43		eqid	$⊢ (abs \circ -) \circ F = (abs \circ -) \circ F$
44	43 6	ovolsf	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to S : ℕ ⟶ [0, +∞)$
45	9 44	syl	$⊢ φ \to S : ℕ ⟶ [0, +∞)$
46	45	ffvelrnda	$⊢ (φ \land j \in ℕ) \to S (j) \in [0, +∞)$
47	32 46	sseldi	$⊢ (φ \land j \in ℕ) \to S (j) \in ℝ$
48	23	adantr	$⊢ (φ \land j \in ℕ) \to sup (ran S ℝ^{*} <) \in ℝ$
49		simpr	$⊢ (φ \land j \in ℕ) \to j \in ℕ$
50		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
51	49 50	eleqtrdi	$⊢ (φ \land j \in ℕ) \to j \in ℤ_{\geq 1}$
52		simpl	$⊢ (φ \land j \in ℕ) \to φ$
53		elfznn	$⊢ n \in (1 \dots j) \to n \in ℕ$
54	28	ovolfsf	$⊢ G : ℕ ⟶ \leq \cap ℝ^{2} \to ((abs \circ -) \circ G) : ℕ ⟶ [0, +∞)$
55	27 54	syl	$⊢ φ \to ((abs \circ -) \circ G) : ℕ ⟶ [0, +∞)$
56	55	ffvelrnda	$⊢ (φ \land n \in ℕ) \to ((abs \circ -) \circ G) (n) \in [0, +∞)$
57	32 56	sseldi	$⊢ (φ \land n \in ℕ) \to ((abs \circ -) \circ G) (n) \in ℝ$
58	52 53 57	syl2an	$⊢ ((φ \land j \in ℕ) \land n \in (1 \dots j)) \to ((abs \circ -) \circ G) (n) \in ℝ$
59	43	ovolfsf	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to ((abs \circ -) \circ F) : ℕ ⟶ [0, +∞)$
60	9 59	syl	$⊢ φ \to ((abs \circ -) \circ F) : ℕ ⟶ [0, +∞)$
61	60	ffvelrnda	$⊢ (φ \land n \in ℕ) \to ((abs \circ -) \circ F) (n) \in [0, +∞)$
62		elrege0	$⊢ ((abs \circ -) \circ F) (n) \in [0, +∞) \leftrightarrow (((abs \circ -) \circ F) (n) \in ℝ \land 0 \leq ((abs \circ -) \circ F) (n))$
63	61 62	sylib	$⊢ (φ \land n \in ℕ) \to (((abs \circ -) \circ F) (n) \in ℝ \land 0 \leq ((abs \circ -) \circ F) (n))$
64	63	simpld	$⊢ (φ \land n \in ℕ) \to ((abs \circ -) \circ F) (n) \in ℝ$
65	52 53 64	syl2an	$⊢ ((φ \land j \in ℕ) \land n \in (1 \dots j)) \to ((abs \circ -) \circ F) (n) \in ℝ$
66	26	simprd	$⊢ φ \to H : ℕ ⟶ \leq \cap ℝ^{2}$
67		eqid	$⊢ (abs \circ -) \circ H = (abs \circ -) \circ H$
68	67	ovolfsf	$⊢ H : ℕ ⟶ \leq \cap ℝ^{2} \to ((abs \circ -) \circ H) : ℕ ⟶ [0, +∞)$
69	66 68	syl	$⊢ φ \to ((abs \circ -) \circ H) : ℕ ⟶ [0, +∞)$
70	69	ffvelrnda	$⊢ (φ \land n \in ℕ) \to ((abs \circ -) \circ H) (n) \in [0, +∞)$
71		elrege0	$⊢ ((abs \circ -) \circ H) (n) \in [0, +∞) \leftrightarrow (((abs \circ -) \circ H) (n) \in ℝ \land 0 \leq ((abs \circ -) \circ H) (n))$
72	70 71	sylib	$⊢ (φ \land n \in ℕ) \to (((abs \circ -) \circ H) (n) \in ℝ \land 0 \leq ((abs \circ -) \circ H) (n))$
73	72	simprd	$⊢ (φ \land n \in ℕ) \to 0 \leq ((abs \circ -) \circ H) (n)$
74	72	simpld	$⊢ (φ \land n \in ℕ) \to ((abs \circ -) \circ H) (n) \in ℝ$
75	57 74	addge01d	$⊢ (φ \land n \in ℕ) \to (0 \leq ((abs \circ -) \circ H) (n) \leftrightarrow ((abs \circ -) \circ G) (n) \leq ((abs \circ -) \circ G) (n) + ((abs \circ -) \circ H) (n))$
76	73 75	mpbid	$⊢ (φ \land n \in ℕ) \to ((abs \circ -) \circ G) (n) \leq ((abs \circ -) \circ G) (n) + ((abs \circ -) \circ H) (n)$
77	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	ioombl1lem3	$⊢ (φ \land n \in ℕ) \to ((abs \circ -) \circ G) (n) + ((abs \circ -) \circ H) (n) = ((abs \circ -) \circ F) (n)$
78	76 77	breqtrd	$⊢ (φ \land n \in ℕ) \to ((abs \circ -) \circ G) (n) \leq ((abs \circ -) \circ F) (n)$
79	52 53 78	syl2an	$⊢ ((φ \land j \in ℕ) \land n \in (1 \dots j)) \to ((abs \circ -) \circ G) (n) \leq ((abs \circ -) \circ F) (n)$
80	51 58 65 79	serle	$⊢ (φ \land j \in ℕ) \to seq 1 (+ ((abs \circ -) \circ G)) (j) \leq seq 1 (+ ((abs \circ -) \circ F)) (j)$
81	7	fveq1i	$⊢ T (j) = seq 1 (+ ((abs \circ -) \circ G)) (j)$
82	6	fveq1i	$⊢ S (j) = seq 1 (+ ((abs \circ -) \circ F)) (j)$
83	80 81 82	3brtr4g	$⊢ (φ \land j \in ℕ) \to T (j) \leq S (j)$
84		1zzd	$⊢ φ \to 1 \in ℤ$
85		eqidd	$⊢ (φ \land n \in ℕ) \to ((abs \circ -) \circ F) (n) = ((abs \circ -) \circ F) (n)$
86	63	simprd	$⊢ (φ \land n \in ℕ) \to 0 \leq ((abs \circ -) \circ F) (n)$
87	45	frnd	$⊢ φ \to ran S \subseteq [0, +∞)$
88		icossxr	$⊢ [0, +∞) \subseteq ℝ^{*}$
89	87 88	sstrdi	$⊢ φ \to ran S \subseteq ℝ^{*}$
90	89	adantr	$⊢ (φ \land k \in ℕ) \to ran S \subseteq ℝ^{*}$
91	45	ffnd	$⊢ φ \to S Fn ℕ$
92		fnfvelrn	$⊢ (S Fn ℕ \land k \in ℕ) \to S (k) \in ran S$
93	91 92	sylan	$⊢ (φ \land k \in ℕ) \to S (k) \in ran S$
94		supxrub	$⊢ (ran S \subseteq ℝ^{} \land S (k) \in ran S) \to S (k) \leq sup (ran S ℝ^{} <)$
95	90 93 94	syl2anc	$⊢ (φ \land k \in ℕ) \to S (k) \leq sup (ran S ℝ^{*} <)$
96	95	ralrimiva	$⊢ φ \to \forall k \in ℕ S (k) \leq sup (ran S ℝ^{*} <)$
97		brralrspcev	$⊢ (sup (ran S ℝ^{} <) \in ℝ \land \forall k \in ℕ S (k) \leq sup (ran S ℝ^{} <)) \to \exists x \in ℝ \forall k \in ℕ S (k) \leq x$
98	23 96 97	syl2anc	$⊢ φ \to \exists x \in ℝ \forall k \in ℕ S (k) \leq x$
99	50 6 84 85 64 86 98	isumsup2	$⊢ φ \to S ⇝ sup (ran S ℝ <)$
100	87 32	sstrdi	$⊢ φ \to ran S \subseteq ℝ$
101	45	fdmd	$⊢ φ \to dom S = ℕ$
102	34 101	eleqtrrid	$⊢ φ \to 1 \in dom S$
103	102	ne0d	$⊢ φ \to dom S \neq \emptyset$
104		dm0rn0	$⊢ dom S = \emptyset \leftrightarrow ran S = \emptyset$
105	104	necon3bii	$⊢ dom S \neq \emptyset \leftrightarrow ran S \neq \emptyset$
106	103 105	sylib	$⊢ φ \to ran S \neq \emptyset$
107		breq1	$⊢ z = S (k) \to (z \leq x \leftrightarrow S (k) \leq x)$
108	107	ralrn	$⊢ S Fn ℕ \to (\forall z \in ran S z \leq x \leftrightarrow \forall k \in ℕ S (k) \leq x)$
109	91 108	syl	$⊢ φ \to (\forall z \in ran S z \leq x \leftrightarrow \forall k \in ℕ S (k) \leq x)$
110	109	rexbidv	$⊢ φ \to (\exists x \in ℝ \forall z \in ran S z \leq x \leftrightarrow \exists x \in ℝ \forall k \in ℕ S (k) \leq x)$
111	98 110	mpbird	$⊢ φ \to \exists x \in ℝ \forall z \in ran S z \leq x$
112		supxrre	$⊢ (ran S \subseteq ℝ \land ran S \neq \emptyset \land \exists x \in ℝ \forall z \in ran S z \leq x) \to sup (ran S ℝ^{*} <) = sup (ran S ℝ <)$
113	100 106 111 112	syl3anc	$⊢ φ \to sup (ran S ℝ^{*} <) = sup (ran S ℝ <)$
114	99 113	breqtrrd	$⊢ φ \to S ⇝ sup (ran S ℝ^{*} <)$
115	114	adantr	$⊢ (φ \land j \in ℕ) \to S ⇝ sup (ran S ℝ^{*} <)$
116	6 115	eqbrtrrid	$⊢ (φ \land j \in ℕ) \to seq 1 (+ ((abs \circ -) \circ F)) ⇝ sup (ran S ℝ^{*} <)$
117	64	adantlr	$⊢ ((φ \land j \in ℕ) \land n \in ℕ) \to ((abs \circ -) \circ F) (n) \in ℝ$
118	86	adantlr	$⊢ ((φ \land j \in ℕ) \land n \in ℕ) \to 0 \leq ((abs \circ -) \circ F) (n)$
119	50 49 116 117 118	climserle	$⊢ (φ \land j \in ℕ) \to seq 1 (+ ((abs \circ -) \circ F)) (j) \leq sup (ran S ℝ^{*} <)$
120	82 119	eqbrtrid	$⊢ (φ \land j \in ℕ) \to S (j) \leq sup (ran S ℝ^{*} <)$
121	42 47 48 83 120	letrd	$⊢ (φ \land j \in ℕ) \to T (j) \leq sup (ran S ℝ^{*} <)$
122	121	ralrimiva	$⊢ φ \to \forall j \in ℕ T (j) \leq sup (ran S ℝ^{*} <)$
123		brralrspcev	$⊢ (sup (ran S ℝ^{} <) \in ℝ \land \forall j \in ℕ T (j) \leq sup (ran S ℝ^{} <)) \to \exists x \in ℝ \forall j \in ℕ T (j) \leq x$
124	23 122 123	syl2anc	$⊢ φ \to \exists x \in ℝ \forall j \in ℕ T (j) \leq x$
125	30	ffnd	$⊢ φ \to T Fn ℕ$
126		breq1	$⊢ z = T (j) \to (z \leq x \leftrightarrow T (j) \leq x)$
127	126	ralrn	$⊢ T Fn ℕ \to (\forall z \in ran T z \leq x \leftrightarrow \forall j \in ℕ T (j) \leq x)$
128	125 127	syl	$⊢ φ \to (\forall z \in ran T z \leq x \leftrightarrow \forall j \in ℕ T (j) \leq x)$
129	128	rexbidv	$⊢ φ \to (\exists x \in ℝ \forall z \in ran T z \leq x \leftrightarrow \exists x \in ℝ \forall j \in ℕ T (j) \leq x)$
130	124 129	mpbird	$⊢ φ \to \exists x \in ℝ \forall z \in ran T z \leq x$
131	33 40 130	suprcld	$⊢ φ \to sup (ran T ℝ <) \in ℝ$
132	67 8	ovolsf	$⊢ H : ℕ ⟶ \leq \cap ℝ^{2} \to U : ℕ ⟶ [0, +∞)$
133	66 132	syl	$⊢ φ \to U : ℕ ⟶ [0, +∞)$
134	133	frnd	$⊢ φ \to ran U \subseteq [0, +∞)$
135	134 32	sstrdi	$⊢ φ \to ran U \subseteq ℝ$
136	133	fdmd	$⊢ φ \to dom U = ℕ$
137	34 136	eleqtrrid	$⊢ φ \to 1 \in dom U$
138	137	ne0d	$⊢ φ \to dom U \neq \emptyset$
139		dm0rn0	$⊢ dom U = \emptyset \leftrightarrow ran U = \emptyset$
140	139	necon3bii	$⊢ dom U \neq \emptyset \leftrightarrow ran U \neq \emptyset$
141	138 140	sylib	$⊢ φ \to ran U \neq \emptyset$
142	133	ffvelrnda	$⊢ (φ \land j \in ℕ) \to U (j) \in [0, +∞)$
143	32 142	sseldi	$⊢ (φ \land j \in ℕ) \to U (j) \in ℝ$
144	52 53 74	syl2an	$⊢ ((φ \land j \in ℕ) \land n \in (1 \dots j)) \to ((abs \circ -) \circ H) (n) \in ℝ$
145		elrege0	$⊢ ((abs \circ -) \circ G) (n) \in [0, +∞) \leftrightarrow (((abs \circ -) \circ G) (n) \in ℝ \land 0 \leq ((abs \circ -) \circ G) (n))$
146	56 145	sylib	$⊢ (φ \land n \in ℕ) \to (((abs \circ -) \circ G) (n) \in ℝ \land 0 \leq ((abs \circ -) \circ G) (n))$
147	146	simprd	$⊢ (φ \land n \in ℕ) \to 0 \leq ((abs \circ -) \circ G) (n)$
148	74 57	addge02d	$⊢ (φ \land n \in ℕ) \to (0 \leq ((abs \circ -) \circ G) (n) \leftrightarrow ((abs \circ -) \circ H) (n) \leq ((abs \circ -) \circ G) (n) + ((abs \circ -) \circ H) (n))$
149	147 148	mpbid	$⊢ (φ \land n \in ℕ) \to ((abs \circ -) \circ H) (n) \leq ((abs \circ -) \circ G) (n) + ((abs \circ -) \circ H) (n)$
150	149 77	breqtrd	$⊢ (φ \land n \in ℕ) \to ((abs \circ -) \circ H) (n) \leq ((abs \circ -) \circ F) (n)$
151	52 53 150	syl2an	$⊢ ((φ \land j \in ℕ) \land n \in (1 \dots j)) \to ((abs \circ -) \circ H) (n) \leq ((abs \circ -) \circ F) (n)$
152	51 144 65 151	serle	$⊢ (φ \land j \in ℕ) \to seq 1 (+ ((abs \circ -) \circ H)) (j) \leq seq 1 (+ ((abs \circ -) \circ F)) (j)$
153	8	fveq1i	$⊢ U (j) = seq 1 (+ ((abs \circ -) \circ H)) (j)$
154	152 153 82	3brtr4g	$⊢ (φ \land j \in ℕ) \to U (j) \leq S (j)$
155	143 47 48 154 120	letrd	$⊢ (φ \land j \in ℕ) \to U (j) \leq sup (ran S ℝ^{*} <)$
156	155	ralrimiva	$⊢ φ \to \forall j \in ℕ U (j) \leq sup (ran S ℝ^{*} <)$
157		brralrspcev	$⊢ (sup (ran S ℝ^{} <) \in ℝ \land \forall j \in ℕ U (j) \leq sup (ran S ℝ^{} <)) \to \exists x \in ℝ \forall j \in ℕ U (j) \leq x$
158	23 156 157	syl2anc	$⊢ φ \to \exists x \in ℝ \forall j \in ℕ U (j) \leq x$
159	133	ffnd	$⊢ φ \to U Fn ℕ$
160		breq1	$⊢ z = U (j) \to (z \leq x \leftrightarrow U (j) \leq x)$
161	160	ralrn	$⊢ U Fn ℕ \to (\forall z \in ran U z \leq x \leftrightarrow \forall j \in ℕ U (j) \leq x)$
162	159 161	syl	$⊢ φ \to (\forall z \in ran U z \leq x \leftrightarrow \forall j \in ℕ U (j) \leq x)$
163	162	rexbidv	$⊢ φ \to (\exists x \in ℝ \forall z \in ran U z \leq x \leftrightarrow \exists x \in ℝ \forall j \in ℕ U (j) \leq x)$
164	158 163	mpbird	$⊢ φ \to \exists x \in ℝ \forall z \in ran U z \leq x$
165	135 141 164	suprcld	$⊢ φ \to sup (ran U ℝ <) \in ℝ$
166		ssralv	$⊢ E \cap B \subseteq E \to (\forall x \in E \exists n \in ℕ (1^{st} (F (n)) < x \land x < 2^{nd} (F (n))) \to \forall x \in (E \cap B) \exists n \in ℕ (1^{st} (F (n)) < x \land x < 2^{nd} (F (n))))$
167	16 166	ax-mp	$⊢ \forall x \in E \exists n \in ℕ (1^{st} (F (n)) < x \land x < 2^{nd} (F (n))) \to \forall x \in (E \cap B) \exists n \in ℕ (1^{st} (F (n)) < x \land x < 2^{nd} (F (n)))$
168	12	breq1i	$⊢ P < x \leftrightarrow 1^{st} (F (n)) < x$
169		ovolfcl	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land n \in ℕ) \to (1^{st} (F (n)) \in ℝ \land 2^{nd} (F (n)) \in ℝ \land 1^{st} (F (n)) \leq 2^{nd} (F (n)))$
170	9 169	sylan	$⊢ (φ \land n \in ℕ) \to (1^{st} (F (n)) \in ℝ \land 2^{nd} (F (n)) \in ℝ \land 1^{st} (F (n)) \leq 2^{nd} (F (n)))$
171	170	simp1d	$⊢ (φ \land n \in ℕ) \to 1^{st} (F (n)) \in ℝ$
172	12 171	eqeltrid	$⊢ (φ \land n \in ℕ) \to P \in ℝ$
173	172	adantlr	$⊢ ((φ \land x \in (E \cap B)) \land n \in ℕ) \to P \in ℝ$
174	16 3	sstrid	$⊢ φ \to E \cap B \subseteq ℝ$
175	174	sselda	$⊢ (φ \land x \in (E \cap B)) \to x \in ℝ$
176	175	adantr	$⊢ ((φ \land x \in (E \cap B)) \land n \in ℕ) \to x \in ℝ$
177		ltle	$⊢ (P \in ℝ \land x \in ℝ) \to (P < x \to P \leq x)$
178	173 176 177	syl2anc	$⊢ ((φ \land x \in (E \cap B)) \land n \in ℕ) \to (P < x \to P \leq x)$
179		simpr	$⊢ (φ \land n \in ℕ) \to n \in ℕ$
180		opex	$⊢ ⟨if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q), Q⟩ \in V$
181	14	fvmpt2	$⊢ (n \in ℕ \land ⟨if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q), Q⟩ \in V) \to G (n) = ⟨if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q), Q⟩$
182	179 180 181	sylancl	$⊢ (φ \land n \in ℕ) \to G (n) = ⟨if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q), Q⟩$
183	182	fveq2d	$⊢ (φ \land n \in ℕ) \to 1^{st} (G (n)) = 1^{st} (⟨if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q), Q⟩)$
184	2	adantr	$⊢ (φ \land n \in ℕ) \to A \in ℝ$
185	184 172	ifcld	$⊢ (φ \land n \in ℕ) \to if (P \leq A, A, P) \in ℝ$
186	170	simp2d	$⊢ (φ \land n \in ℕ) \to 2^{nd} (F (n)) \in ℝ$
187	13 186	eqeltrid	$⊢ (φ \land n \in ℕ) \to Q \in ℝ$
188	185 187	ifcld	$⊢ (φ \land n \in ℕ) \to if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q) \in ℝ$
189		op1stg	$⊢ (if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q) \in ℝ \land Q \in ℝ) \to 1^{st} (⟨if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q), Q⟩) = if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q)$
190	188 187 189	syl2anc	$⊢ (φ \land n \in ℕ) \to 1^{st} (⟨if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q), Q⟩) = if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q)$
191	183 190	eqtrd	$⊢ (φ \land n \in ℕ) \to 1^{st} (G (n)) = if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q)$
192	191	ad2ant2r	$⊢ ((φ \land x \in (E \cap B)) \land (n \in ℕ \land P \leq x)) \to 1^{st} (G (n)) = if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q)$
193	188	ad2ant2r	$⊢ ((φ \land x \in (E \cap B)) \land (n \in ℕ \land P \leq x)) \to if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q) \in ℝ$
194	185	ad2ant2r	$⊢ ((φ \land x \in (E \cap B)) \land (n \in ℕ \land P \leq x)) \to if (P \leq A, A, P) \in ℝ$
195	174	ad2antrr	$⊢ ((φ \land x \in (E \cap B)) \land (n \in ℕ \land P \leq x)) \to E \cap B \subseteq ℝ$
196		simplr	$⊢ ((φ \land x \in (E \cap B)) \land (n \in ℕ \land P \leq x)) \to x \in (E \cap B)$
197	195 196	sseldd	$⊢ ((φ \land x \in (E \cap B)) \land (n \in ℕ \land P \leq x)) \to x \in ℝ$
198	187	ad2ant2r	$⊢ ((φ \land x \in (E \cap B)) \land (n \in ℕ \land P \leq x)) \to Q \in ℝ$
199		min1	$⊢ (if (P \leq A, A, P) \in ℝ \land Q \in ℝ) \to if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q) \leq if (P \leq A, A, P)$
200	194 198 199	syl2anc	$⊢ ((φ \land x \in (E \cap B)) \land (n \in ℕ \land P \leq x)) \to if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q) \leq if (P \leq A, A, P)$
201	2	ad2antrr	$⊢ ((φ \land x \in (E \cap B)) \land (n \in ℕ \land P \leq x)) \to A \in ℝ$
202		elinel2	$⊢ x \in (E \cap B) \to x \in B$
203	202	ad2antlr	$⊢ ((φ \land x \in (E \cap B)) \land (n \in ℕ \land P \leq x)) \to x \in B$
204	2	rexrd	$⊢ φ \to A \in ℝ^{*}$
205		pnfxr	$⊢ +∞ \in ℝ^{*}$
206		elioo2	$⊢ (A \in ℝ^{} \land +∞ \in ℝ^{}) \to (x \in (A, +∞) \leftrightarrow (x \in ℝ \land A < x \land x < +∞))$
207	204 205 206	sylancl	$⊢ φ \to (x \in (A, +∞) \leftrightarrow (x \in ℝ \land A < x \land x < +∞))$
208	1	eleq2i	$⊢ x \in B \leftrightarrow x \in (A, +∞)$
209		ltpnf	$⊢ x \in ℝ \to x < +∞$
210	209	adantr	$⊢ (x \in ℝ \land A < x) \to x < +∞$
211	210	pm4.71i	$⊢ (x \in ℝ \land A < x) \leftrightarrow ((x \in ℝ \land A < x) \land x < +∞)$
212		df-3an	$⊢ (x \in ℝ \land A < x \land x < +∞) \leftrightarrow ((x \in ℝ \land A < x) \land x < +∞)$
213	211 212	bitr4i	$⊢ (x \in ℝ \land A < x) \leftrightarrow (x \in ℝ \land A < x \land x < +∞)$
214	207 208 213	3bitr4g	$⊢ φ \to (x \in B \leftrightarrow (x \in ℝ \land A < x))$
215		simpr	$⊢ (x \in ℝ \land A < x) \to A < x$
216	214 215	syl6bi	$⊢ φ \to (x \in B \to A < x)$
217	216	ad2antrr	$⊢ ((φ \land x \in (E \cap B)) \land (n \in ℕ \land P \leq x)) \to (x \in B \to A < x)$
218	203 217	mpd	$⊢ ((φ \land x \in (E \cap B)) \land (n \in ℕ \land P \leq x)) \to A < x$
219	201 197 218	ltled	$⊢ ((φ \land x \in (E \cap B)) \land (n \in ℕ \land P \leq x)) \to A \leq x$
220		simprr	$⊢ ((φ \land x \in (E \cap B)) \land (n \in ℕ \land P \leq x)) \to P \leq x$
221		breq1	$⊢ A = if (P \leq A, A, P) \to (A \leq x \leftrightarrow if (P \leq A, A, P) \leq x)$
222		breq1	$⊢ P = if (P \leq A, A, P) \to (P \leq x \leftrightarrow if (P \leq A, A, P) \leq x)$
223	221 222	ifboth	$⊢ (A \leq x \land P \leq x) \to if (P \leq A, A, P) \leq x$
224	219 220 223	syl2anc	$⊢ ((φ \land x \in (E \cap B)) \land (n \in ℕ \land P \leq x)) \to if (P \leq A, A, P) \leq x$
225	193 194 197 200 224	letrd	$⊢ ((φ \land x \in (E \cap B)) \land (n \in ℕ \land P \leq x)) \to if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q) \leq x$
226	192 225	eqbrtrd	$⊢ ((φ \land x \in (E \cap B)) \land (n \in ℕ \land P \leq x)) \to 1^{st} (G (n)) \leq x$
227	226	expr	$⊢ ((φ \land x \in (E \cap B)) \land n \in ℕ) \to (P \leq x \to 1^{st} (G (n)) \leq x)$
228	178 227	syld	$⊢ ((φ \land x \in (E \cap B)) \land n \in ℕ) \to (P < x \to 1^{st} (G (n)) \leq x)$
229	168 228	syl5bir	$⊢ ((φ \land x \in (E \cap B)) \land n \in ℕ) \to (1^{st} (F (n)) < x \to 1^{st} (G (n)) \leq x)$
230	13	breq2i	$⊢ x < Q \leftrightarrow x < 2^{nd} (F (n))$
231	187	adantlr	$⊢ ((φ \land x \in (E \cap B)) \land n \in ℕ) \to Q \in ℝ$
232		ltle	$⊢ (x \in ℝ \land Q \in ℝ) \to (x < Q \to x \leq Q)$
233	176 231 232	syl2anc	$⊢ ((φ \land x \in (E \cap B)) \land n \in ℕ) \to (x < Q \to x \leq Q)$
234	230 233	syl5bir	$⊢ ((φ \land x \in (E \cap B)) \land n \in ℕ) \to (x < 2^{nd} (F (n)) \to x \leq Q)$
235	182	fveq2d	$⊢ (φ \land n \in ℕ) \to 2^{nd} (G (n)) = 2^{nd} (⟨if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q), Q⟩)$
236		op2ndg	$⊢ (if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q) \in ℝ \land Q \in ℝ) \to 2^{nd} (⟨if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q), Q⟩) = Q$
237	188 187 236	syl2anc	$⊢ (φ \land n \in ℕ) \to 2^{nd} (⟨if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q), Q⟩) = Q$
238	235 237	eqtrd	$⊢ (φ \land n \in ℕ) \to 2^{nd} (G (n)) = Q$
239	238	adantlr	$⊢ ((φ \land x \in (E \cap B)) \land n \in ℕ) \to 2^{nd} (G (n)) = Q$
240	239	breq2d	$⊢ ((φ \land x \in (E \cap B)) \land n \in ℕ) \to (x \leq 2^{nd} (G (n)) \leftrightarrow x \leq Q)$
241	234 240	sylibrd	$⊢ ((φ \land x \in (E \cap B)) \land n \in ℕ) \to (x < 2^{nd} (F (n)) \to x \leq 2^{nd} (G (n)))$
242	229 241	anim12d	$⊢ ((φ \land x \in (E \cap B)) \land n \in ℕ) \to ((1^{st} (F (n)) < x \land x < 2^{nd} (F (n))) \to (1^{st} (G (n)) \leq x \land x \leq 2^{nd} (G (n))))$
243	242	reximdva	$⊢ (φ \land x \in (E \cap B)) \to (\exists n \in ℕ (1^{st} (F (n)) < x \land x < 2^{nd} (F (n))) \to \exists n \in ℕ (1^{st} (G (n)) \leq x \land x \leq 2^{nd} (G (n))))$
244	243	ralimdva	$⊢ φ \to (\forall x \in (E \cap B) \exists n \in ℕ (1^{st} (F (n)) < x \land x < 2^{nd} (F (n))) \to \forall x \in (E \cap B) \exists n \in ℕ (1^{st} (G (n)) \leq x \land x \leq 2^{nd} (G (n))))$
245	167 244	syl5	$⊢ φ \to (\forall x \in E \exists n \in ℕ (1^{st} (F (n)) < x \land x < 2^{nd} (F (n))) \to \forall x \in (E \cap B) \exists n \in ℕ (1^{st} (G (n)) \leq x \land x \leq 2^{nd} (G (n))))$
246		ovolfioo	$⊢ (E \subseteq ℝ \land F : ℕ ⟶ \leq \cap ℝ^{2}) \to (E \subseteq ⋃ ran ((.) \circ F) \leftrightarrow \forall x \in E \exists n \in ℕ (1^{st} (F (n)) < x \land x < 2^{nd} (F (n))))$
247	3 9 246	syl2anc	$⊢ φ \to (E \subseteq ⋃ ran ((.) \circ F) \leftrightarrow \forall x \in E \exists n \in ℕ (1^{st} (F (n)) < x \land x < 2^{nd} (F (n))))$
248		ovolficc	$⊢ (E \cap B \subseteq ℝ \land G : ℕ ⟶ \leq \cap ℝ^{2}) \to (E \cap B \subseteq ⋃ ran ([.] \circ G) \leftrightarrow \forall x \in (E \cap B) \exists n \in ℕ (1^{st} (G (n)) \leq x \land x \leq 2^{nd} (G (n))))$
249	174 27 248	syl2anc	$⊢ φ \to (E \cap B \subseteq ⋃ ran ([.] \circ G) \leftrightarrow \forall x \in (E \cap B) \exists n \in ℕ (1^{st} (G (n)) \leq x \land x \leq 2^{nd} (G (n))))$
250	245 247 249	3imtr4d	$⊢ φ \to (E \subseteq ⋃ ran ((.) \circ F) \to E \cap B \subseteq ⋃ ran ([.] \circ G))$
251	10 250	mpd	$⊢ φ \to E \cap B \subseteq ⋃ ran ([.] \circ G)$
252	7	ovollb2	$⊢ (G : ℕ ⟶ \leq \cap ℝ^{2} \land E \cap B \subseteq ⋃ ran ([.] \circ G)) \to {vol}^{} (E \cap B) \leq sup (ran T ℝ^{} <)$
253	27 251 252	syl2anc	$⊢ φ \to {vol}^{} (E \cap B) \leq sup (ran T ℝ^{} <)$
254		supxrre	$⊢ (ran T \subseteq ℝ \land ran T \neq \emptyset \land \exists x \in ℝ \forall z \in ran T z \leq x) \to sup (ran T ℝ^{*} <) = sup (ran T ℝ <)$
255	33 40 130 254	syl3anc	$⊢ φ \to sup (ran T ℝ^{*} <) = sup (ran T ℝ <)$
256	253 255	breqtrd	$⊢ φ \to {vol}^{*} (E \cap B) \leq sup (ran T ℝ <)$
257		ssralv	$⊢ E ∖ B \subseteq E \to (\forall x \in E \exists n \in ℕ (1^{st} (F (n)) < x \land x < 2^{nd} (F (n))) \to \forall x \in (E ∖ B) \exists n \in ℕ (1^{st} (F (n)) < x \land x < 2^{nd} (F (n))))$
258	19 257	ax-mp	$⊢ \forall x \in E \exists n \in ℕ (1^{st} (F (n)) < x \land x < 2^{nd} (F (n))) \to \forall x \in (E ∖ B) \exists n \in ℕ (1^{st} (F (n)) < x \land x < 2^{nd} (F (n)))$
259	172	adantlr	$⊢ ((φ \land x \in (E ∖ B)) \land n \in ℕ) \to P \in ℝ$
260	19 3	sstrid	$⊢ φ \to E ∖ B \subseteq ℝ$
261	260	sselda	$⊢ (φ \land x \in (E ∖ B)) \to x \in ℝ$
262	261	adantr	$⊢ ((φ \land x \in (E ∖ B)) \land n \in ℕ) \to x \in ℝ$
263	259 262 177	syl2anc	$⊢ ((φ \land x \in (E ∖ B)) \land n \in ℕ) \to (P < x \to P \leq x)$
264	168 263	syl5bir	$⊢ ((φ \land x \in (E ∖ B)) \land n \in ℕ) \to (1^{st} (F (n)) < x \to P \leq x)$
265		opex	$⊢ ⟨P, if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q)⟩ \in V$
266	15	fvmpt2	$⊢ (n \in ℕ \land ⟨P, if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q)⟩ \in V) \to H (n) = ⟨P, if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q)⟩$
267	179 265 266	sylancl	$⊢ (φ \land n \in ℕ) \to H (n) = ⟨P, if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q)⟩$
268	267	fveq2d	$⊢ (φ \land n \in ℕ) \to 1^{st} (H (n)) = 1^{st} (⟨P, if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q)⟩)$
269		op1stg	$⊢ (P \in ℝ \land if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q) \in ℝ) \to 1^{st} (⟨P, if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q)⟩) = P$
270	172 188 269	syl2anc	$⊢ (φ \land n \in ℕ) \to 1^{st} (⟨P, if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q)⟩) = P$
271	268 270	eqtrd	$⊢ (φ \land n \in ℕ) \to 1^{st} (H (n)) = P$
272	271	adantlr	$⊢ ((φ \land x \in (E ∖ B)) \land n \in ℕ) \to 1^{st} (H (n)) = P$
273	272	breq1d	$⊢ ((φ \land x \in (E ∖ B)) \land n \in ℕ) \to (1^{st} (H (n)) \leq x \leftrightarrow P \leq x)$
274	264 273	sylibrd	$⊢ ((φ \land x \in (E ∖ B)) \land n \in ℕ) \to (1^{st} (F (n)) < x \to 1^{st} (H (n)) \leq x)$
275	187	adantlr	$⊢ ((φ \land x \in (E ∖ B)) \land n \in ℕ) \to Q \in ℝ$
276	262 275 232	syl2anc	$⊢ ((φ \land x \in (E ∖ B)) \land n \in ℕ) \to (x < Q \to x \leq Q)$
277	260	ad2antrr	$⊢ ((φ \land x \in (E ∖ B)) \land (n \in ℕ \land x \leq Q)) \to E ∖ B \subseteq ℝ$
278		simplr	$⊢ ((φ \land x \in (E ∖ B)) \land (n \in ℕ \land x \leq Q)) \to x \in (E ∖ B)$
279	277 278	sseldd	$⊢ ((φ \land x \in (E ∖ B)) \land (n \in ℕ \land x \leq Q)) \to x \in ℝ$
280	2	ad2antrr	$⊢ ((φ \land x \in (E ∖ B)) \land (n \in ℕ \land x \leq Q)) \to A \in ℝ$
281	172	ad2ant2r	$⊢ ((φ \land x \in (E ∖ B)) \land (n \in ℕ \land x \leq Q)) \to P \in ℝ$
282	280 281	ifcld	$⊢ ((φ \land x \in (E ∖ B)) \land (n \in ℕ \land x \leq Q)) \to if (P \leq A, A, P) \in ℝ$
283		eldifn	$⊢ x \in (E ∖ B) \to \neg x \in B$
284	283	ad2antlr	$⊢ ((φ \land x \in (E ∖ B)) \land (n \in ℕ \land x \leq Q)) \to \neg x \in B$
285	279	biantrurd	$⊢ ((φ \land x \in (E ∖ B)) \land (n \in ℕ \land x \leq Q)) \to (A < x \leftrightarrow (x \in ℝ \land A < x))$
286	214	ad2antrr	$⊢ ((φ \land x \in (E ∖ B)) \land (n \in ℕ \land x \leq Q)) \to (x \in B \leftrightarrow (x \in ℝ \land A < x))$
287	285 286	bitr4d	$⊢ ((φ \land x \in (E ∖ B)) \land (n \in ℕ \land x \leq Q)) \to (A < x \leftrightarrow x \in B)$
288	284 287	mtbird	$⊢ ((φ \land x \in (E ∖ B)) \land (n \in ℕ \land x \leq Q)) \to \neg A < x$
289	279 280 288	nltled	$⊢ ((φ \land x \in (E ∖ B)) \land (n \in ℕ \land x \leq Q)) \to x \leq A$
290		max2	$⊢ (P \in ℝ \land A \in ℝ) \to A \leq if (P \leq A, A, P)$
291	281 280 290	syl2anc	$⊢ ((φ \land x \in (E ∖ B)) \land (n \in ℕ \land x \leq Q)) \to A \leq if (P \leq A, A, P)$
292	279 280 282 289 291	letrd	$⊢ ((φ \land x \in (E ∖ B)) \land (n \in ℕ \land x \leq Q)) \to x \leq if (P \leq A, A, P)$
293		simprr	$⊢ ((φ \land x \in (E ∖ B)) \land (n \in ℕ \land x \leq Q)) \to x \leq Q$
294		breq2	$⊢ if (P \leq A, A, P) = if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q) \to (x \leq if (P \leq A, A, P) \leftrightarrow x \leq if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q))$
295		breq2	$⊢ Q = if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q) \to (x \leq Q \leftrightarrow x \leq if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q))$
296	294 295	ifboth	$⊢ (x \leq if (P \leq A, A, P) \land x \leq Q) \to x \leq if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q)$
297	292 293 296	syl2anc	$⊢ ((φ \land x \in (E ∖ B)) \land (n \in ℕ \land x \leq Q)) \to x \leq if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q)$
298	267	fveq2d	$⊢ (φ \land n \in ℕ) \to 2^{nd} (H (n)) = 2^{nd} (⟨P, if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q)⟩)$
299		op2ndg	$⊢ (P \in ℝ \land if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q) \in ℝ) \to 2^{nd} (⟨P, if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q)⟩) = if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q)$
300	172 188 299	syl2anc	$⊢ (φ \land n \in ℕ) \to 2^{nd} (⟨P, if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q)⟩) = if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q)$
301	298 300	eqtrd	$⊢ (φ \land n \in ℕ) \to 2^{nd} (H (n)) = if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q)$
302	301	ad2ant2r	$⊢ ((φ \land x \in (E ∖ B)) \land (n \in ℕ \land x \leq Q)) \to 2^{nd} (H (n)) = if (if (P \leq A, A, P) \leq Q, if (P \leq A, A, P), Q)$
303	297 302	breqtrrd	$⊢ ((φ \land x \in (E ∖ B)) \land (n \in ℕ \land x \leq Q)) \to x \leq 2^{nd} (H (n))$
304	303	expr	$⊢ ((φ \land x \in (E ∖ B)) \land n \in ℕ) \to (x \leq Q \to x \leq 2^{nd} (H (n)))$
305	276 304	syld	$⊢ ((φ \land x \in (E ∖ B)) \land n \in ℕ) \to (x < Q \to x \leq 2^{nd} (H (n)))$
306	230 305	syl5bir	$⊢ ((φ \land x \in (E ∖ B)) \land n \in ℕ) \to (x < 2^{nd} (F (n)) \to x \leq 2^{nd} (H (n)))$
307	274 306	anim12d	$⊢ ((φ \land x \in (E ∖ B)) \land n \in ℕ) \to ((1^{st} (F (n)) < x \land x < 2^{nd} (F (n))) \to (1^{st} (H (n)) \leq x \land x \leq 2^{nd} (H (n))))$
308	307	reximdva	$⊢ (φ \land x \in (E ∖ B)) \to (\exists n \in ℕ (1^{st} (F (n)) < x \land x < 2^{nd} (F (n))) \to \exists n \in ℕ (1^{st} (H (n)) \leq x \land x \leq 2^{nd} (H (n))))$
309	308	ralimdva	$⊢ φ \to (\forall x \in (E ∖ B) \exists n \in ℕ (1^{st} (F (n)) < x \land x < 2^{nd} (F (n))) \to \forall x \in (E ∖ B) \exists n \in ℕ (1^{st} (H (n)) \leq x \land x \leq 2^{nd} (H (n))))$
310	258 309	syl5	$⊢ φ \to (\forall x \in E \exists n \in ℕ (1^{st} (F (n)) < x \land x < 2^{nd} (F (n))) \to \forall x \in (E ∖ B) \exists n \in ℕ (1^{st} (H (n)) \leq x \land x \leq 2^{nd} (H (n))))$
311		ovolficc	$⊢ (E ∖ B \subseteq ℝ \land H : ℕ ⟶ \leq \cap ℝ^{2}) \to (E ∖ B \subseteq ⋃ ran ([.] \circ H) \leftrightarrow \forall x \in (E ∖ B) \exists n \in ℕ (1^{st} (H (n)) \leq x \land x \leq 2^{nd} (H (n))))$
312	260 66 311	syl2anc	$⊢ φ \to (E ∖ B \subseteq ⋃ ran ([.] \circ H) \leftrightarrow \forall x \in (E ∖ B) \exists n \in ℕ (1^{st} (H (n)) \leq x \land x \leq 2^{nd} (H (n))))$
313	310 247 312	3imtr4d	$⊢ φ \to (E \subseteq ⋃ ran ((.) \circ F) \to E ∖ B \subseteq ⋃ ran ([.] \circ H))$
314	10 313	mpd	$⊢ φ \to E ∖ B \subseteq ⋃ ran ([.] \circ H)$
315	8	ovollb2	$⊢ (H : ℕ ⟶ \leq \cap ℝ^{2} \land E ∖ B \subseteq ⋃ ran ([.] \circ H)) \to {vol}^{} (E ∖ B) \leq sup (ran U ℝ^{} <)$
316	66 314 315	syl2anc	$⊢ φ \to {vol}^{} (E ∖ B) \leq sup (ran U ℝ^{} <)$
317		supxrre	$⊢ (ran U \subseteq ℝ \land ran U \neq \emptyset \land \exists x \in ℝ \forall z \in ran U z \leq x) \to sup (ran U ℝ^{*} <) = sup (ran U ℝ <)$
318	135 141 164 317	syl3anc	$⊢ φ \to sup (ran U ℝ^{*} <) = sup (ran U ℝ <)$
319	316 318	breqtrd	$⊢ φ \to {vol}^{*} (E ∖ B) \leq sup (ran U ℝ <)$
320	18 21 131 165 256 319	le2addd	$⊢ φ \to {vol}^{} (E \cap B) + {vol}^{} (E ∖ B) \leq sup (ran T ℝ <) + sup (ran U ℝ <)$
321		eqidd	$⊢ (φ \land n \in ℕ) \to ((abs \circ -) \circ G) (n) = ((abs \circ -) \circ G) (n)$
322	50 7 84 321 57 147 124	isumsup2	$⊢ φ \to T ⇝ sup (ran T ℝ <)$
323		seqex	$⊢ seq 1 (+ ((abs \circ -) \circ F)) \in V$
324	6 323	eqeltri	$⊢ S \in V$
325	324	a1i	$⊢ φ \to S \in V$
326		eqidd	$⊢ (φ \land n \in ℕ) \to ((abs \circ -) \circ H) (n) = ((abs \circ -) \circ H) (n)$
327	50 8 84 326 74 73 158	isumsup2	$⊢ φ \to U ⇝ sup (ran U ℝ <)$
328	42	recnd	$⊢ (φ \land j \in ℕ) \to T (j) \in ℂ$
329	143	recnd	$⊢ (φ \land j \in ℕ) \to U (j) \in ℂ$
330	57	recnd	$⊢ (φ \land n \in ℕ) \to ((abs \circ -) \circ G) (n) \in ℂ$
331	52 53 330	syl2an	$⊢ ((φ \land j \in ℕ) \land n \in (1 \dots j)) \to ((abs \circ -) \circ G) (n) \in ℂ$
332	74	recnd	$⊢ (φ \land n \in ℕ) \to ((abs \circ -) \circ H) (n) \in ℂ$
333	52 53 332	syl2an	$⊢ ((φ \land j \in ℕ) \land n \in (1 \dots j)) \to ((abs \circ -) \circ H) (n) \in ℂ$
334	77	eqcomd	$⊢ (φ \land n \in ℕ) \to ((abs \circ -) \circ F) (n) = ((abs \circ -) \circ G) (n) + ((abs \circ -) \circ H) (n)$
335	52 53 334	syl2an	$⊢ ((φ \land j \in ℕ) \land n \in (1 \dots j)) \to ((abs \circ -) \circ F) (n) = ((abs \circ -) \circ G) (n) + ((abs \circ -) \circ H) (n)$
336	51 331 333 335	seradd	$⊢ (φ \land j \in ℕ) \to seq 1 (+ ((abs \circ -) \circ F)) (j) = seq 1 (+ ((abs \circ -) \circ G)) (j) + seq 1 (+ ((abs \circ -) \circ H)) (j)$
337	81 153	oveq12i	$⊢ T (j) + U (j) = seq 1 (+ ((abs \circ -) \circ G)) (j) + seq 1 (+ ((abs \circ -) \circ H)) (j)$
338	336 82 337	3eqtr4g	$⊢ (φ \land j \in ℕ) \to S (j) = T (j) + U (j)$
339	50 84 322 325 327 328 329 338	climadd	$⊢ φ \to S ⇝ (sup (ran T ℝ <) + sup (ran U ℝ <))$
340		climuni	$⊢ (S ⇝ (sup (ran T ℝ <) + sup (ran U ℝ <)) \land S ⇝ sup (ran S ℝ^{} <)) \to sup (ran T ℝ <) + sup (ran U ℝ <) = sup (ran S ℝ^{} <)$
341	339 114 340	syl2anc	$⊢ φ \to sup (ran T ℝ <) + sup (ran U ℝ <) = sup (ran S ℝ^{*} <)$
342	320 341	breqtrd	$⊢ φ \to {vol}^{} (E \cap B) + {vol}^{} (E ∖ B) \leq sup (ran S ℝ^{*} <)$
343	22 23 25 342 11	letrd	$⊢ φ \to {vol}^{} (E \cap B) + {vol}^{} (E ∖ B) \leq {vol}^{*} (E) + C$

Metamath Proof Explorer

Theorem ioombl1lem4

Proof