ovolunlem1

	Ref	Expression
Hypotheses	ovolun.a	$⊢ φ \to (A \subseteq ℝ \land {vol}^{*} (A) \in ℝ)$
	ovolun.b	$⊢ φ \to (B \subseteq ℝ \land {vol}^{*} (B) \in ℝ)$
	ovolun.c	$⊢ φ \to C \in ℝ^{+}$
	ovolun.s	$⊢ S = seq 1 (+ ((abs \circ -) \circ F))$
	ovolun.t	$⊢ T = seq 1 (+ ((abs \circ -) \circ G))$
	ovolun.u	$⊢ U = seq 1 (+ ((abs \circ -) \circ H))$
	ovolun.f1	$⊢ φ \to F \in ({(\leq \cap ℝ^{2})}^{ℕ})$
	ovolun.f2	$⊢ φ \to A \subseteq ⋃ ran ((.) \circ F)$
	ovolun.f3	$⊢ φ \to sup (ran S ℝ^{} <) \leq {vol}^{} (A) + (\frac{C}{2})$
	ovolun.g1	$⊢ φ \to G \in ({(\leq \cap ℝ^{2})}^{ℕ})$
	ovolun.g2	$⊢ φ \to B \subseteq ⋃ ran ((.) \circ G)$
	ovolun.g3	$⊢ φ \to sup (ran T ℝ^{} <) \leq {vol}^{} (B) + (\frac{C}{2})$
	ovolun.h	$⊢ H = (n \in ℕ ⟼ if (\frac{n}{2} \in ℕ, G (\frac{n}{2}), F (\frac{n + 1}{2})))$
Assertion	ovolunlem1	$⊢ φ \to {vol}^{} (A \cup B) \leq {vol}^{} (A) + {vol}^{*} (B) + C$

Proof

Step	Hyp	Ref	Expression
1		ovolun.a	$⊢ φ \to (A \subseteq ℝ \land {vol}^{*} (A) \in ℝ)$
2		ovolun.b	$⊢ φ \to (B \subseteq ℝ \land {vol}^{*} (B) \in ℝ)$
3		ovolun.c	$⊢ φ \to C \in ℝ^{+}$
4		ovolun.s	$⊢ S = seq 1 (+ ((abs \circ -) \circ F))$
5		ovolun.t	$⊢ T = seq 1 (+ ((abs \circ -) \circ G))$
6		ovolun.u	$⊢ U = seq 1 (+ ((abs \circ -) \circ H))$
7		ovolun.f1	$⊢ φ \to F \in ({(\leq \cap ℝ^{2})}^{ℕ})$
8		ovolun.f2	$⊢ φ \to A \subseteq ⋃ ran ((.) \circ F)$
9		ovolun.f3	$⊢ φ \to sup (ran S ℝ^{} <) \leq {vol}^{} (A) + (\frac{C}{2})$
10		ovolun.g1	$⊢ φ \to G \in ({(\leq \cap ℝ^{2})}^{ℕ})$
11		ovolun.g2	$⊢ φ \to B \subseteq ⋃ ran ((.) \circ G)$
12		ovolun.g3	$⊢ φ \to sup (ran T ℝ^{} <) \leq {vol}^{} (B) + (\frac{C}{2})$
13		ovolun.h	$⊢ H = (n \in ℕ ⟼ if (\frac{n}{2} \in ℕ, G (\frac{n}{2}), F (\frac{n + 1}{2})))$
14	1	simpld	$⊢ φ \to A \subseteq ℝ$
15	2	simpld	$⊢ φ \to B \subseteq ℝ$
16	14 15	unssd	$⊢ φ \to A \cup B \subseteq ℝ$
17		elovolmlem	$⊢ G \in ({(\leq \cap ℝ^{2})}^{ℕ}) \leftrightarrow G : ℕ ⟶ \leq \cap ℝ^{2}$
18	10 17	sylib	$⊢ φ \to G : ℕ ⟶ \leq \cap ℝ^{2}$
19	18	adantr	$⊢ (φ \land n \in ℕ) \to G : ℕ ⟶ \leq \cap ℝ^{2}$
20	19	ffvelrnda	$⊢ ((φ \land n \in ℕ) \land \frac{n}{2} \in ℕ) \to G (\frac{n}{2}) \in (\leq \cap ℝ^{2})$
21		nneo	$⊢ n \in ℕ \to (\frac{n}{2} \in ℕ \leftrightarrow \neg \frac{n + 1}{2} \in ℕ)$
22	21	adantl	$⊢ (φ \land n \in ℕ) \to (\frac{n}{2} \in ℕ \leftrightarrow \neg \frac{n + 1}{2} \in ℕ)$
23	22	con2bid	$⊢ (φ \land n \in ℕ) \to (\frac{n + 1}{2} \in ℕ \leftrightarrow \neg \frac{n}{2} \in ℕ)$
24	23	biimpar	$⊢ ((φ \land n \in ℕ) \land \neg \frac{n}{2} \in ℕ) \to \frac{n + 1}{2} \in ℕ$
25		elovolmlem	$⊢ F \in ({(\leq \cap ℝ^{2})}^{ℕ}) \leftrightarrow F : ℕ ⟶ \leq \cap ℝ^{2}$
26	7 25	sylib	$⊢ φ \to F : ℕ ⟶ \leq \cap ℝ^{2}$
27	26	adantr	$⊢ (φ \land n \in ℕ) \to F : ℕ ⟶ \leq \cap ℝ^{2}$
28	27	ffvelrnda	$⊢ ((φ \land n \in ℕ) \land \frac{n + 1}{2} \in ℕ) \to F (\frac{n + 1}{2}) \in (\leq \cap ℝ^{2})$
29	24 28	syldan	$⊢ ((φ \land n \in ℕ) \land \neg \frac{n}{2} \in ℕ) \to F (\frac{n + 1}{2}) \in (\leq \cap ℝ^{2})$
30	20 29	ifclda	$⊢ (φ \land n \in ℕ) \to if (\frac{n}{2} \in ℕ, G (\frac{n}{2}), F (\frac{n + 1}{2})) \in (\leq \cap ℝ^{2})$
31	30 13	fmptd	$⊢ φ \to H : ℕ ⟶ \leq \cap ℝ^{2}$
32		eqid	$⊢ (abs \circ -) \circ H = (abs \circ -) \circ H$
33	32 6	ovolsf	$⊢ H : ℕ ⟶ \leq \cap ℝ^{2} \to U : ℕ ⟶ [0, +∞)$
34	31 33	syl	$⊢ φ \to U : ℕ ⟶ [0, +∞)$
35		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
36		fss	$⊢ (U : ℕ ⟶ [0, +∞) \land [0, +∞) \subseteq ℝ) \to U : ℕ ⟶ ℝ$
37	34 35 36	sylancl	$⊢ φ \to U : ℕ ⟶ ℝ$
38	37	frnd	$⊢ φ \to ran U \subseteq ℝ$
39		1nn	$⊢ 1 \in ℕ$
40		1z	$⊢ 1 \in ℤ$
41		seqfn	$⊢ 1 \in ℤ \to seq 1 (+ ((abs \circ -) \circ H)) Fn ℤ_{\geq 1}$
42	40 41	mp1i	$⊢ φ \to seq 1 (+ ((abs \circ -) \circ H)) Fn ℤ_{\geq 1}$
43	6	fneq1i	$⊢ U Fn ℕ \leftrightarrow seq 1 (+ ((abs \circ -) \circ H)) Fn ℕ$
44		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
45	44	fneq2i	$⊢ seq 1 (+ ((abs \circ -) \circ H)) Fn ℕ \leftrightarrow seq 1 (+ ((abs \circ -) \circ H)) Fn ℤ_{\geq 1}$
46	43 45	bitri	$⊢ U Fn ℕ \leftrightarrow seq 1 (+ ((abs \circ -) \circ H)) Fn ℤ_{\geq 1}$
47	42 46	sylibr	$⊢ φ \to U Fn ℕ$
48	47	fndmd	$⊢ φ \to dom U = ℕ$
49	39 48	eleqtrrid	$⊢ φ \to 1 \in dom U$
50	49	ne0d	$⊢ φ \to dom U \neq \emptyset$
51		dm0rn0	$⊢ dom U = \emptyset \leftrightarrow ran U = \emptyset$
52	51	necon3bii	$⊢ dom U \neq \emptyset \leftrightarrow ran U \neq \emptyset$
53	50 52	sylib	$⊢ φ \to ran U \neq \emptyset$
54	1	simprd	$⊢ φ \to {vol}^{*} (A) \in ℝ$
55	2	simprd	$⊢ φ \to {vol}^{*} (B) \in ℝ$
56	54 55	readdcld	$⊢ φ \to {vol}^{} (A) + {vol}^{} (B) \in ℝ$
57	3	rpred	$⊢ φ \to C \in ℝ$
58	56 57	readdcld	$⊢ φ \to {vol}^{} (A) + {vol}^{} (B) + C \in ℝ$
59	1 2 3 4 5 6 7 8 9 10 11 12 13	ovolunlem1a	$⊢ (φ \land k \in ℕ) \to U (k) \leq {vol}^{} (A) + {vol}^{} (B) + C$
60	59	ralrimiva	$⊢ φ \to \forall k \in ℕ U (k) \leq {vol}^{} (A) + {vol}^{} (B) + C$
61		breq1	$⊢ z = U (k) \to (z \leq {vol}^{} (A) + {vol}^{} (B) + C \leftrightarrow U (k) \leq {vol}^{} (A) + {vol}^{} (B) + C)$
62	61	ralrn	$⊢ U Fn ℕ \to (\forall z \in ran U z \leq {vol}^{} (A) + {vol}^{} (B) + C \leftrightarrow \forall k \in ℕ U (k) \leq {vol}^{} (A) + {vol}^{} (B) + C)$
63	47 62	syl	$⊢ φ \to (\forall z \in ran U z \leq {vol}^{} (A) + {vol}^{} (B) + C \leftrightarrow \forall k \in ℕ U (k) \leq {vol}^{} (A) + {vol}^{} (B) + C)$
64	60 63	mpbird	$⊢ φ \to \forall z \in ran U z \leq {vol}^{} (A) + {vol}^{} (B) + C$
65		brralrspcev	$⊢ ({vol}^{} (A) + {vol}^{} (B) + C \in ℝ \land \forall z \in ran U z \leq {vol}^{} (A) + {vol}^{} (B) + C) \to \exists k \in ℝ \forall z \in ran U z \leq k$
66	58 64 65	syl2anc	$⊢ φ \to \exists k \in ℝ \forall z \in ran U z \leq k$
67		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
68	38 67	sstrdi	$⊢ φ \to ran U \subseteq ℝ^{*}$
69		supxrbnd2	$⊢ ran U \subseteq ℝ^{} \to (\exists k \in ℝ \forall z \in ran U z \leq k \leftrightarrow sup (ran U ℝ^{} <) < +∞)$
70	68 69	syl	$⊢ φ \to (\exists k \in ℝ \forall z \in ran U z \leq k \leftrightarrow sup (ran U ℝ^{*} <) < +∞)$
71	66 70	mpbid	$⊢ φ \to sup (ran U ℝ^{*} <) < +∞$
72		supxrbnd	$⊢ (ran U \subseteq ℝ \land ran U \neq \emptyset \land sup (ran U ℝ^{} <) < +∞) \to sup (ran U ℝ^{} <) \in ℝ$
73	38 53 71 72	syl3anc	$⊢ φ \to sup (ran U ℝ^{*} <) \in ℝ$
74		nncn	$⊢ m \in ℕ \to m \in ℂ$
75	74	adantl	$⊢ (φ \land m \in ℕ) \to m \in ℂ$
76		1cnd	$⊢ (φ \land m \in ℕ) \to 1 \in ℂ$
77	75	2timesd	$⊢ (φ \land m \in ℕ) \to 2 m = m + m$
78	77	oveq1d	$⊢ (φ \land m \in ℕ) \to 2 m - 1 = m + m - 1$
79	75 75 76 78	assraddsubd	$⊢ (φ \land m \in ℕ) \to 2 m - 1 = m + m - 1$
80		simpr	$⊢ (φ \land m \in ℕ) \to m \in ℕ$
81		nnm1nn0	$⊢ m \in ℕ \to m - 1 \in ℕ_{0}$
82		nnnn0addcl	$⊢ (m \in ℕ \land m - 1 \in ℕ_{0}) \to m + m - 1 \in ℕ$
83	80 81 82	syl2anc2	$⊢ (φ \land m \in ℕ) \to m + m - 1 \in ℕ$
84	79 83	eqeltrd	$⊢ (φ \land m \in ℕ) \to 2 m - 1 \in ℕ$
85		oveq1	$⊢ n = 2 m - 1 \to \frac{n}{2} = \frac{2 m - 1}{2}$
86	85	eleq1d	$⊢ n = 2 m - 1 \to (\frac{n}{2} \in ℕ \leftrightarrow \frac{2 m - 1}{2} \in ℕ)$
87	85	fveq2d	$⊢ n = 2 m - 1 \to G (\frac{n}{2}) = G (\frac{2 m - 1}{2})$
88		oveq1	$⊢ n = 2 m - 1 \to n + 1 = 2 m - 1 + 1$
89	88	fvoveq1d	$⊢ n = 2 m - 1 \to F (\frac{n + 1}{2}) = F (\frac{2 m - 1 + 1}{2})$
90	86 87 89	ifbieq12d	$⊢ n = 2 m - 1 \to if (\frac{n}{2} \in ℕ, G (\frac{n}{2}), F (\frac{n + 1}{2})) = if (\frac{2 m - 1}{2} \in ℕ, G (\frac{2 m - 1}{2}), F (\frac{2 m - 1 + 1}{2}))$
91		fvex	$⊢ G (\frac{2 m - 1}{2}) \in V$
92		fvex	$⊢ F (\frac{2 m - 1 + 1}{2}) \in V$
93	91 92	ifex	$⊢ if (\frac{2 m - 1}{2} \in ℕ, G (\frac{2 m - 1}{2}), F (\frac{2 m - 1 + 1}{2})) \in V$
94	90 13 93	fvmpt	$⊢ 2 m - 1 \in ℕ \to H (2 m - 1) = if (\frac{2 m - 1}{2} \in ℕ, G (\frac{2 m - 1}{2}), F (\frac{2 m - 1 + 1}{2}))$
95	84 94	syl	$⊢ (φ \land m \in ℕ) \to H (2 m - 1) = if (\frac{2 m - 1}{2} \in ℕ, G (\frac{2 m - 1}{2}), F (\frac{2 m - 1 + 1}{2}))$
96		2nn	$⊢ 2 \in ℕ$
97		nnmulcl	$⊢ (2 \in ℕ \land m \in ℕ) \to 2 m \in ℕ$
98	96 80 97	sylancr	$⊢ (φ \land m \in ℕ) \to 2 m \in ℕ$
99	98	nncnd	$⊢ (φ \land m \in ℕ) \to 2 m \in ℂ$
100		ax-1cn	$⊢ 1 \in ℂ$
101		npcan	$⊢ (2 m \in ℂ \land 1 \in ℂ) \to 2 m - 1 + 1 = 2 m$
102	99 100 101	sylancl	$⊢ (φ \land m \in ℕ) \to 2 m - 1 + 1 = 2 m$
103	102	oveq1d	$⊢ (φ \land m \in ℕ) \to \frac{2 m - 1 + 1}{2} = \frac{2 m}{2}$
104		2cn	$⊢ 2 \in ℂ$
105		2ne0	$⊢ 2 \neq 0$
106		divcan3	$⊢ (m \in ℂ \land 2 \in ℂ \land 2 \neq 0) \to \frac{2 m}{2} = m$
107	104 105 106	mp3an23	$⊢ m \in ℂ \to \frac{2 m}{2} = m$
108	75 107	syl	$⊢ (φ \land m \in ℕ) \to \frac{2 m}{2} = m$
109	103 108	eqtrd	$⊢ (φ \land m \in ℕ) \to \frac{2 m - 1 + 1}{2} = m$
110	109 80	eqeltrd	$⊢ (φ \land m \in ℕ) \to \frac{2 m - 1 + 1}{2} \in ℕ$
111		nneo	$⊢ 2 m - 1 \in ℕ \to (\frac{2 m - 1}{2} \in ℕ \leftrightarrow \neg \frac{2 m - 1 + 1}{2} \in ℕ)$
112	84 111	syl	$⊢ (φ \land m \in ℕ) \to (\frac{2 m - 1}{2} \in ℕ \leftrightarrow \neg \frac{2 m - 1 + 1}{2} \in ℕ)$
113	112	con2bid	$⊢ (φ \land m \in ℕ) \to (\frac{2 m - 1 + 1}{2} \in ℕ \leftrightarrow \neg \frac{2 m - 1}{2} \in ℕ)$
114	110 113	mpbid	$⊢ (φ \land m \in ℕ) \to \neg \frac{2 m - 1}{2} \in ℕ$
115	114	iffalsed	$⊢ (φ \land m \in ℕ) \to if (\frac{2 m - 1}{2} \in ℕ, G (\frac{2 m - 1}{2}), F (\frac{2 m - 1 + 1}{2})) = F (\frac{2 m - 1 + 1}{2})$
116	109	fveq2d	$⊢ (φ \land m \in ℕ) \to F (\frac{2 m - 1 + 1}{2}) = F (m)$
117	95 115 116	3eqtrd	$⊢ (φ \land m \in ℕ) \to H (2 m - 1) = F (m)$
118		fveqeq2	$⊢ k = 2 m - 1 \to (H (k) = F (m) \leftrightarrow H (2 m - 1) = F (m))$
119	118	rspcev	$⊢ (2 m - 1 \in ℕ \land H (2 m - 1) = F (m)) \to \exists k \in ℕ H (k) = F (m)$
120	84 117 119	syl2anc	$⊢ (φ \land m \in ℕ) \to \exists k \in ℕ H (k) = F (m)$
121		fveq2	$⊢ H (k) = F (m) \to 1^{st} (H (k)) = 1^{st} (F (m))$
122	121	breq1d	$⊢ H (k) = F (m) \to (1^{st} (H (k)) < z \leftrightarrow 1^{st} (F (m)) < z)$
123		fveq2	$⊢ H (k) = F (m) \to 2^{nd} (H (k)) = 2^{nd} (F (m))$
124	123	breq2d	$⊢ H (k) = F (m) \to (z < 2^{nd} (H (k)) \leftrightarrow z < 2^{nd} (F (m)))$
125	122 124	anbi12d	$⊢ H (k) = F (m) \to ((1^{st} (H (k)) < z \land z < 2^{nd} (H (k))) \leftrightarrow (1^{st} (F (m)) < z \land z < 2^{nd} (F (m))))$
126	125	biimprcd	$⊢ (1^{st} (F (m)) < z \land z < 2^{nd} (F (m))) \to (H (k) = F (m) \to (1^{st} (H (k)) < z \land z < 2^{nd} (H (k))))$
127	126	reximdv	$⊢ (1^{st} (F (m)) < z \land z < 2^{nd} (F (m))) \to (\exists k \in ℕ H (k) = F (m) \to \exists k \in ℕ (1^{st} (H (k)) < z \land z < 2^{nd} (H (k))))$
128	120 127	syl5com	$⊢ (φ \land m \in ℕ) \to ((1^{st} (F (m)) < z \land z < 2^{nd} (F (m))) \to \exists k \in ℕ (1^{st} (H (k)) < z \land z < 2^{nd} (H (k))))$
129	128	rexlimdva	$⊢ φ \to (\exists m \in ℕ (1^{st} (F (m)) < z \land z < 2^{nd} (F (m))) \to \exists k \in ℕ (1^{st} (H (k)) < z \land z < 2^{nd} (H (k))))$
130	129	ralimdv	$⊢ φ \to (\forall z \in A \exists m \in ℕ (1^{st} (F (m)) < z \land z < 2^{nd} (F (m))) \to \forall z \in A \exists k \in ℕ (1^{st} (H (k)) < z \land z < 2^{nd} (H (k))))$
131		ovolfioo	$⊢ (A \subseteq ℝ \land F : ℕ ⟶ \leq \cap ℝ^{2}) \to (A \subseteq ⋃ ran ((.) \circ F) \leftrightarrow \forall z \in A \exists m \in ℕ (1^{st} (F (m)) < z \land z < 2^{nd} (F (m))))$
132	14 26 131	syl2anc	$⊢ φ \to (A \subseteq ⋃ ran ((.) \circ F) \leftrightarrow \forall z \in A \exists m \in ℕ (1^{st} (F (m)) < z \land z < 2^{nd} (F (m))))$
133		ovolfioo	$⊢ (A \subseteq ℝ \land H : ℕ ⟶ \leq \cap ℝ^{2}) \to (A \subseteq ⋃ ran ((.) \circ H) \leftrightarrow \forall z \in A \exists k \in ℕ (1^{st} (H (k)) < z \land z < 2^{nd} (H (k))))$
134	14 31 133	syl2anc	$⊢ φ \to (A \subseteq ⋃ ran ((.) \circ H) \leftrightarrow \forall z \in A \exists k \in ℕ (1^{st} (H (k)) < z \land z < 2^{nd} (H (k))))$
135	130 132 134	3imtr4d	$⊢ φ \to (A \subseteq ⋃ ran ((.) \circ F) \to A \subseteq ⋃ ran ((.) \circ H))$
136	8 135	mpd	$⊢ φ \to A \subseteq ⋃ ran ((.) \circ H)$
137		oveq1	$⊢ n = 2 m \to \frac{n}{2} = \frac{2 m}{2}$
138	137	eleq1d	$⊢ n = 2 m \to (\frac{n}{2} \in ℕ \leftrightarrow \frac{2 m}{2} \in ℕ)$
139	137	fveq2d	$⊢ n = 2 m \to G (\frac{n}{2}) = G (\frac{2 m}{2})$
140		oveq1	$⊢ n = 2 m \to n + 1 = 2 m + 1$
141	140	fvoveq1d	$⊢ n = 2 m \to F (\frac{n + 1}{2}) = F (\frac{2 m + 1}{2})$
142	138 139 141	ifbieq12d	$⊢ n = 2 m \to if (\frac{n}{2} \in ℕ, G (\frac{n}{2}), F (\frac{n + 1}{2})) = if (\frac{2 m}{2} \in ℕ, G (\frac{2 m}{2}), F (\frac{2 m + 1}{2}))$
143		fvex	$⊢ G (\frac{2 m}{2}) \in V$
144		fvex	$⊢ F (\frac{2 m + 1}{2}) \in V$
145	143 144	ifex	$⊢ if (\frac{2 m}{2} \in ℕ, G (\frac{2 m}{2}), F (\frac{2 m + 1}{2})) \in V$
146	142 13 145	fvmpt	$⊢ 2 m \in ℕ \to H (2 m) = if (\frac{2 m}{2} \in ℕ, G (\frac{2 m}{2}), F (\frac{2 m + 1}{2}))$
147	98 146	syl	$⊢ (φ \land m \in ℕ) \to H (2 m) = if (\frac{2 m}{2} \in ℕ, G (\frac{2 m}{2}), F (\frac{2 m + 1}{2}))$
148	108 80	eqeltrd	$⊢ (φ \land m \in ℕ) \to \frac{2 m}{2} \in ℕ$
149	148	iftrued	$⊢ (φ \land m \in ℕ) \to if (\frac{2 m}{2} \in ℕ, G (\frac{2 m}{2}), F (\frac{2 m + 1}{2})) = G (\frac{2 m}{2})$
150	108	fveq2d	$⊢ (φ \land m \in ℕ) \to G (\frac{2 m}{2}) = G (m)$
151	147 149 150	3eqtrd	$⊢ (φ \land m \in ℕ) \to H (2 m) = G (m)$
152		fveqeq2	$⊢ k = 2 m \to (H (k) = G (m) \leftrightarrow H (2 m) = G (m))$
153	152	rspcev	$⊢ (2 m \in ℕ \land H (2 m) = G (m)) \to \exists k \in ℕ H (k) = G (m)$
154	98 151 153	syl2anc	$⊢ (φ \land m \in ℕ) \to \exists k \in ℕ H (k) = G (m)$
155		fveq2	$⊢ H (k) = G (m) \to 1^{st} (H (k)) = 1^{st} (G (m))$
156	155	breq1d	$⊢ H (k) = G (m) \to (1^{st} (H (k)) < z \leftrightarrow 1^{st} (G (m)) < z)$
157		fveq2	$⊢ H (k) = G (m) \to 2^{nd} (H (k)) = 2^{nd} (G (m))$
158	157	breq2d	$⊢ H (k) = G (m) \to (z < 2^{nd} (H (k)) \leftrightarrow z < 2^{nd} (G (m)))$
159	156 158	anbi12d	$⊢ H (k) = G (m) \to ((1^{st} (H (k)) < z \land z < 2^{nd} (H (k))) \leftrightarrow (1^{st} (G (m)) < z \land z < 2^{nd} (G (m))))$
160	159	biimprcd	$⊢ (1^{st} (G (m)) < z \land z < 2^{nd} (G (m))) \to (H (k) = G (m) \to (1^{st} (H (k)) < z \land z < 2^{nd} (H (k))))$
161	160	reximdv	$⊢ (1^{st} (G (m)) < z \land z < 2^{nd} (G (m))) \to (\exists k \in ℕ H (k) = G (m) \to \exists k \in ℕ (1^{st} (H (k)) < z \land z < 2^{nd} (H (k))))$
162	154 161	syl5com	$⊢ (φ \land m \in ℕ) \to ((1^{st} (G (m)) < z \land z < 2^{nd} (G (m))) \to \exists k \in ℕ (1^{st} (H (k)) < z \land z < 2^{nd} (H (k))))$
163	162	rexlimdva	$⊢ φ \to (\exists m \in ℕ (1^{st} (G (m)) < z \land z < 2^{nd} (G (m))) \to \exists k \in ℕ (1^{st} (H (k)) < z \land z < 2^{nd} (H (k))))$
164	163	ralimdv	$⊢ φ \to (\forall z \in B \exists m \in ℕ (1^{st} (G (m)) < z \land z < 2^{nd} (G (m))) \to \forall z \in B \exists k \in ℕ (1^{st} (H (k)) < z \land z < 2^{nd} (H (k))))$
165		ovolfioo	$⊢ (B \subseteq ℝ \land G : ℕ ⟶ \leq \cap ℝ^{2}) \to (B \subseteq ⋃ ran ((.) \circ G) \leftrightarrow \forall z \in B \exists m \in ℕ (1^{st} (G (m)) < z \land z < 2^{nd} (G (m))))$
166	15 18 165	syl2anc	$⊢ φ \to (B \subseteq ⋃ ran ((.) \circ G) \leftrightarrow \forall z \in B \exists m \in ℕ (1^{st} (G (m)) < z \land z < 2^{nd} (G (m))))$
167		ovolfioo	$⊢ (B \subseteq ℝ \land H : ℕ ⟶ \leq \cap ℝ^{2}) \to (B \subseteq ⋃ ran ((.) \circ H) \leftrightarrow \forall z \in B \exists k \in ℕ (1^{st} (H (k)) < z \land z < 2^{nd} (H (k))))$
168	15 31 167	syl2anc	$⊢ φ \to (B \subseteq ⋃ ran ((.) \circ H) \leftrightarrow \forall z \in B \exists k \in ℕ (1^{st} (H (k)) < z \land z < 2^{nd} (H (k))))$
169	164 166 168	3imtr4d	$⊢ φ \to (B \subseteq ⋃ ran ((.) \circ G) \to B \subseteq ⋃ ran ((.) \circ H))$
170	11 169	mpd	$⊢ φ \to B \subseteq ⋃ ran ((.) \circ H)$
171	136 170	unssd	$⊢ φ \to A \cup B \subseteq ⋃ ran ((.) \circ H)$
172	6	ovollb	$⊢ (H : ℕ ⟶ \leq \cap ℝ^{2} \land A \cup B \subseteq ⋃ ran ((.) \circ H)) \to {vol}^{} (A \cup B) \leq sup (ran U ℝ^{} <)$
173	31 171 172	syl2anc	$⊢ φ \to {vol}^{} (A \cup B) \leq sup (ran U ℝ^{} <)$
174		ovollecl	$⊢ (A \cup B \subseteq ℝ \land sup (ran U ℝ^{} <) \in ℝ \land {vol}^{} (A \cup B) \leq sup (ran U ℝ^{} <)) \to {vol}^{} (A \cup B) \in ℝ$
175	16 73 173 174	syl3anc	$⊢ φ \to {vol}^{*} (A \cup B) \in ℝ$
176	58	rexrd	$⊢ φ \to {vol}^{} (A) + {vol}^{} (B) + C \in ℝ^{*}$
177		supxrleub	$⊢ (ran U \subseteq ℝ^{} \land {vol}^{} (A) + {vol}^{} (B) + C \in ℝ^{}) \to (sup (ran U ℝ^{} <) \leq {vol}^{} (A) + {vol}^{} (B) + C \leftrightarrow \forall z \in ran U z \leq {vol}^{} (A) + {vol}^{*} (B) + C)$
178	68 176 177	syl2anc	$⊢ φ \to (sup (ran U ℝ^{} <) \leq {vol}^{} (A) + {vol}^{} (B) + C \leftrightarrow \forall z \in ran U z \leq {vol}^{} (A) + {vol}^{*} (B) + C)$
179	64 178	mpbird	$⊢ φ \to sup (ran U ℝ^{} <) \leq {vol}^{} (A) + {vol}^{*} (B) + C$
180	175 73 58 173 179	letrd	$⊢ φ \to {vol}^{} (A \cup B) \leq {vol}^{} (A) + {vol}^{*} (B) + C$

Metamath Proof Explorer

Theorem ovolunlem1

Proof