ovolunlem2

	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 ℝ^{+}$
Assertion	ovolunlem2	$⊢ φ \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	1	simpld	$⊢ φ \to A \subseteq ℝ$
5	1	simprd	$⊢ φ \to {vol}^{*} (A) \in ℝ$
6	3	rphalfcld	$⊢ φ \to \frac{C}{2} \in ℝ^{+}$
7		eqid	$⊢ seq 1 (+ ((abs \circ -) \circ g)) = seq 1 (+ ((abs \circ -) \circ g))$
8	7	ovolgelb	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ \land \frac{C}{2} \in ℝ^{+}) \to \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <) \leq {vol}^{*} (A) + (\frac{C}{2}))$
9	4 5 6 8	syl3anc	$⊢ φ \to \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <) \leq {vol}^{} (A) + (\frac{C}{2}))$
10	2	simpld	$⊢ φ \to B \subseteq ℝ$
11	2	simprd	$⊢ φ \to {vol}^{*} (B) \in ℝ$
12		eqid	$⊢ seq 1 (+ ((abs \circ -) \circ h)) = seq 1 (+ ((abs \circ -) \circ h))$
13	12	ovolgelb	$⊢ (B \subseteq ℝ \land {vol}^{} (B) \in ℝ \land \frac{C}{2} \in ℝ^{+}) \to \exists h \in ({(\leq \cap ℝ^{2})}^{ℕ}) (B \subseteq ⋃ ran ((.) \circ h) \land sup (ran seq 1 (+ ((abs \circ -) \circ h)) ℝ^{} <) \leq {vol}^{*} (B) + (\frac{C}{2}))$
14	10 11 6 13	syl3anc	$⊢ φ \to \exists h \in ({(\leq \cap ℝ^{2})}^{ℕ}) (B \subseteq ⋃ ran ((.) \circ h) \land sup (ran seq 1 (+ ((abs \circ -) \circ h)) ℝ^{} <) \leq {vol}^{} (B) + (\frac{C}{2}))$
15		reeanv	$⊢ \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) \exists h \in ({(\leq \cap ℝ^{2})}^{ℕ}) ((A \subseteq ⋃ ran ((.) \circ g) \land sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <) \leq {vol}^{} (A) + (\frac{C}{2})) \land (B \subseteq ⋃ ran ((.) \circ h) \land sup (ran seq 1 (+ ((abs \circ -) \circ h)) ℝ^{} <) \leq {vol}^{} (B) + (\frac{C}{2}))) \leftrightarrow (\exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <) \leq {vol}^{} (A) + (\frac{C}{2})) \land \exists h \in ({(\leq \cap ℝ^{2})}^{ℕ}) (B \subseteq ⋃ ran ((.) \circ h) \land sup (ran seq 1 (+ ((abs \circ -) \circ h)) ℝ^{} <) \leq {vol}^{} (B) + (\frac{C}{2})))$
16	1	3ad2ant1	$⊢ (φ \land (g \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land h \in ({(\leq \cap ℝ^{2})}^{ℕ})) \land ((A \subseteq ⋃ ran ((.) \circ g) \land sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <) \leq {vol}^{} (A) + (\frac{C}{2})) \land (B \subseteq ⋃ ran ((.) \circ h) \land sup (ran seq 1 (+ ((abs \circ -) \circ h)) ℝ^{} <) \leq {vol}^{} (B) + (\frac{C}{2})))) \to (A \subseteq ℝ \land {vol}^{*} (A) \in ℝ)$
17	2	3ad2ant1	$⊢ (φ \land (g \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land h \in ({(\leq \cap ℝ^{2})}^{ℕ})) \land ((A \subseteq ⋃ ran ((.) \circ g) \land sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <) \leq {vol}^{} (A) + (\frac{C}{2})) \land (B \subseteq ⋃ ran ((.) \circ h) \land sup (ran seq 1 (+ ((abs \circ -) \circ h)) ℝ^{} <) \leq {vol}^{} (B) + (\frac{C}{2})))) \to (B \subseteq ℝ \land {vol}^{*} (B) \in ℝ)$
18	3	3ad2ant1	$⊢ (φ \land (g \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land h \in ({(\leq \cap ℝ^{2})}^{ℕ})) \land ((A \subseteq ⋃ ran ((.) \circ g) \land sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <) \leq {vol}^{} (A) + (\frac{C}{2})) \land (B \subseteq ⋃ ran ((.) \circ h) \land sup (ran seq 1 (+ ((abs \circ -) \circ h)) ℝ^{} <) \leq {vol}^{} (B) + (\frac{C}{2})))) \to C \in ℝ^{+}$
19		eqid	$⊢ seq 1 (+ ((abs \circ -) \circ (n \in ℕ ⟼ if (\frac{n}{2} \in ℕ, h (\frac{n}{2}), g (\frac{n + 1}{2}))))) = seq 1 (+ ((abs \circ -) \circ (n \in ℕ ⟼ if (\frac{n}{2} \in ℕ, h (\frac{n}{2}), g (\frac{n + 1}{2})))))$
20		simp2l	$⊢ (φ \land (g \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land h \in ({(\leq \cap ℝ^{2})}^{ℕ})) \land ((A \subseteq ⋃ ran ((.) \circ g) \land sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <) \leq {vol}^{} (A) + (\frac{C}{2})) \land (B \subseteq ⋃ ran ((.) \circ h) \land sup (ran seq 1 (+ ((abs \circ -) \circ h)) ℝ^{} <) \leq {vol}^{} (B) + (\frac{C}{2})))) \to g \in ({(\leq \cap ℝ^{2})}^{ℕ})$
21		simp3ll	$⊢ (φ \land (g \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land h \in ({(\leq \cap ℝ^{2})}^{ℕ})) \land ((A \subseteq ⋃ ran ((.) \circ g) \land sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <) \leq {vol}^{} (A) + (\frac{C}{2})) \land (B \subseteq ⋃ ran ((.) \circ h) \land sup (ran seq 1 (+ ((abs \circ -) \circ h)) ℝ^{} <) \leq {vol}^{} (B) + (\frac{C}{2})))) \to A \subseteq ⋃ ran ((.) \circ g)$
22		simp3lr	$⊢ (φ \land (g \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land h \in ({(\leq \cap ℝ^{2})}^{ℕ})) \land ((A \subseteq ⋃ ran ((.) \circ g) \land sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <) \leq {vol}^{} (A) + (\frac{C}{2})) \land (B \subseteq ⋃ ran ((.) \circ h) \land sup (ran seq 1 (+ ((abs \circ -) \circ h)) ℝ^{} <) \leq {vol}^{} (B) + (\frac{C}{2})))) \to sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <) \leq {vol}^{} (A) + (\frac{C}{2})$
23		simp2r	$⊢ (φ \land (g \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land h \in ({(\leq \cap ℝ^{2})}^{ℕ})) \land ((A \subseteq ⋃ ran ((.) \circ g) \land sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <) \leq {vol}^{} (A) + (\frac{C}{2})) \land (B \subseteq ⋃ ran ((.) \circ h) \land sup (ran seq 1 (+ ((abs \circ -) \circ h)) ℝ^{} <) \leq {vol}^{} (B) + (\frac{C}{2})))) \to h \in ({(\leq \cap ℝ^{2})}^{ℕ})$
24		simp3rl	$⊢ (φ \land (g \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land h \in ({(\leq \cap ℝ^{2})}^{ℕ})) \land ((A \subseteq ⋃ ran ((.) \circ g) \land sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <) \leq {vol}^{} (A) + (\frac{C}{2})) \land (B \subseteq ⋃ ran ((.) \circ h) \land sup (ran seq 1 (+ ((abs \circ -) \circ h)) ℝ^{} <) \leq {vol}^{} (B) + (\frac{C}{2})))) \to B \subseteq ⋃ ran ((.) \circ h)$
25		simp3rr	$⊢ (φ \land (g \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land h \in ({(\leq \cap ℝ^{2})}^{ℕ})) \land ((A \subseteq ⋃ ran ((.) \circ g) \land sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <) \leq {vol}^{} (A) + (\frac{C}{2})) \land (B \subseteq ⋃ ran ((.) \circ h) \land sup (ran seq 1 (+ ((abs \circ -) \circ h)) ℝ^{} <) \leq {vol}^{} (B) + (\frac{C}{2})))) \to sup (ran seq 1 (+ ((abs \circ -) \circ h)) ℝ^{} <) \leq {vol}^{} (B) + (\frac{C}{2})$
26		eqid	$⊢ (n \in ℕ ⟼ if (\frac{n}{2} \in ℕ, h (\frac{n}{2}), g (\frac{n + 1}{2}))) = (n \in ℕ ⟼ if (\frac{n}{2} \in ℕ, h (\frac{n}{2}), g (\frac{n + 1}{2})))$
27	16 17 18 7 12 19 20 21 22 23 24 25 26	ovolunlem1	$⊢ (φ \land (g \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land h \in ({(\leq \cap ℝ^{2})}^{ℕ})) \land ((A \subseteq ⋃ ran ((.) \circ g) \land sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <) \leq {vol}^{} (A) + (\frac{C}{2})) \land (B \subseteq ⋃ ran ((.) \circ h) \land sup (ran seq 1 (+ ((abs \circ -) \circ h)) ℝ^{} <) \leq {vol}^{} (B) + (\frac{C}{2})))) \to {vol}^{} (A \cup B) \leq {vol}^{} (A) + {vol}^{*} (B) + C$
28	27	3exp	$⊢ φ \to ((g \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land h \in ({(\leq \cap ℝ^{2})}^{ℕ})) \to (((A \subseteq ⋃ ran ((.) \circ g) \land sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <) \leq {vol}^{} (A) + (\frac{C}{2})) \land (B \subseteq ⋃ ran ((.) \circ h) \land sup (ran seq 1 (+ ((abs \circ -) \circ h)) ℝ^{} <) \leq {vol}^{} (B) + (\frac{C}{2}))) \to {vol}^{} (A \cup B) \leq {vol}^{} (A) + {vol}^{*} (B) + C))$
29	28	rexlimdvv	$⊢ φ \to (\exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) \exists h \in ({(\leq \cap ℝ^{2})}^{ℕ}) ((A \subseteq ⋃ ran ((.) \circ g) \land sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <) \leq {vol}^{} (A) + (\frac{C}{2})) \land (B \subseteq ⋃ ran ((.) \circ h) \land sup (ran seq 1 (+ ((abs \circ -) \circ h)) ℝ^{} <) \leq {vol}^{} (B) + (\frac{C}{2}))) \to {vol}^{} (A \cup B) \leq {vol}^{} (A) + {vol}^{*} (B) + C)$
30	15 29	syl5bir	$⊢ φ \to ((\exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <) \leq {vol}^{} (A) + (\frac{C}{2})) \land \exists h \in ({(\leq \cap ℝ^{2})}^{ℕ}) (B \subseteq ⋃ ran ((.) \circ h) \land sup (ran seq 1 (+ ((abs \circ -) \circ h)) ℝ^{} <) \leq {vol}^{} (B) + (\frac{C}{2}))) \to {vol}^{} (A \cup B) \leq {vol}^{} (A) + {vol}^{*} (B) + C)$
31	9 14 30	mp2and	$⊢ φ \to {vol}^{} (A \cup B) \leq {vol}^{} (A) + {vol}^{*} (B) + C$

Metamath Proof Explorer

Theorem ovolunlem2

Proof