uniioombllem4

	Ref	Expression
Hypotheses	uniioombl.1	$⊢ φ \to F : ℕ ⟶ \leq \cap ℝ^{2}$
	uniioombl.2	$⊢ φ \to \underset{x \in ℕ}{Disj} (.) (F (x))$
	uniioombl.3	$⊢ S = seq 1 (+ ((abs \circ -) \circ F))$
	uniioombl.a	$⊢ A = ⋃ ran ((.) \circ F)$
	uniioombl.e	$⊢ φ \to {vol}^{*} (E) \in ℝ$
	uniioombl.c	$⊢ φ \to C \in ℝ^{+}$
	uniioombl.g	$⊢ φ \to G : ℕ ⟶ \leq \cap ℝ^{2}$
	uniioombl.s	$⊢ φ \to E \subseteq ⋃ ran ((.) \circ G)$
	uniioombl.t	$⊢ T = seq 1 (+ ((abs \circ -) \circ G))$
	uniioombl.v	$⊢ φ \to sup (ran T ℝ^{} <) \leq {vol}^{} (E) + C$
	uniioombl.m	$⊢ φ \to M \in ℕ$
	uniioombl.m2	$⊢ φ \to \|T (M) - sup (ran T ℝ^{*} <)\| < C$
	uniioombl.k	$⊢ K = ⋃ ((.) \circ G) [(1 \dots M)]$
	uniioombl.n	$⊢ φ \to N \in ℕ$
	uniioombl.n2	$⊢ φ \to \forall j \in (1 \dots M) \|\sum_{i = 1}^{N} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{} ((.) (G (j)) \cap A)\| < \frac{C}{M}$
	uniioombl.l	$⊢ L = ⋃ ((.) \circ F) [(1 \dots N)]$
Assertion	uniioombllem4	$⊢ φ \to {vol}^{} (K \cap A) \leq {vol}^{} (K \cap L) + C$

Proof

Step	Hyp	Ref	Expression
1		uniioombl.1	$⊢ φ \to F : ℕ ⟶ \leq \cap ℝ^{2}$
2		uniioombl.2	$⊢ φ \to \underset{x \in ℕ}{Disj} (.) (F (x))$
3		uniioombl.3	$⊢ S = seq 1 (+ ((abs \circ -) \circ F))$
4		uniioombl.a	$⊢ A = ⋃ ran ((.) \circ F)$
5		uniioombl.e	$⊢ φ \to {vol}^{*} (E) \in ℝ$
6		uniioombl.c	$⊢ φ \to C \in ℝ^{+}$
7		uniioombl.g	$⊢ φ \to G : ℕ ⟶ \leq \cap ℝ^{2}$
8		uniioombl.s	$⊢ φ \to E \subseteq ⋃ ran ((.) \circ G)$
9		uniioombl.t	$⊢ T = seq 1 (+ ((abs \circ -) \circ G))$
10		uniioombl.v	$⊢ φ \to sup (ran T ℝ^{} <) \leq {vol}^{} (E) + C$
11		uniioombl.m	$⊢ φ \to M \in ℕ$
12		uniioombl.m2	$⊢ φ \to \|T (M) - sup (ran T ℝ^{*} <)\| < C$
13		uniioombl.k	$⊢ K = ⋃ ((.) \circ G) [(1 \dots M)]$
14		uniioombl.n	$⊢ φ \to N \in ℕ$
15		uniioombl.n2	$⊢ φ \to \forall j \in (1 \dots M) \|\sum_{i = 1}^{N} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{} ((.) (G (j)) \cap A)\| < \frac{C}{M}$
16		uniioombl.l	$⊢ L = ⋃ ((.) \circ F) [(1 \dots N)]$
17		inss1	$⊢ K \cap A \subseteq K$
18		imassrn	$⊢ ((.) \circ G) [(1 \dots M)] \subseteq ran ((.) \circ G)$
19	18	unissi	$⊢ ⋃ ((.) \circ G) [(1 \dots M)] \subseteq ⋃ ran ((.) \circ G)$
20	13 19	eqsstri	$⊢ K \subseteq ⋃ ran ((.) \circ G)$
21	7	uniiccdif	$⊢ φ \to (⋃ ran ((.) \circ G) \subseteq ⋃ ran ([.] \circ G) \land {vol}^{*} (⋃ ran ([.] \circ G) ∖ ⋃ ran ((.) \circ G)) = 0)$
22	21	simpld	$⊢ φ \to ⋃ ran ((.) \circ G) \subseteq ⋃ ran ([.] \circ G)$
23		ovolficcss	$⊢ G : ℕ ⟶ \leq \cap ℝ^{2} \to ⋃ ran ([.] \circ G) \subseteq ℝ$
24	7 23	syl	$⊢ φ \to ⋃ ran ([.] \circ G) \subseteq ℝ$
25	22 24	sstrd	$⊢ φ \to ⋃ ran ((.) \circ G) \subseteq ℝ$
26	20 25	sstrid	$⊢ φ \to K \subseteq ℝ$
27	1 2 3 4 5 6 7 8 9 10	uniioombllem1	$⊢ φ \to sup (ran T ℝ^{*} <) \in ℝ$
28		ssid	$⊢ ⋃ ran ((.) \circ G) \subseteq ⋃ ran ((.) \circ G)$
29	9	ovollb	$⊢ (G : ℕ ⟶ \leq \cap ℝ^{2} \land ⋃ ran ((.) \circ G) \subseteq ⋃ ran ((.) \circ G)) \to {vol}^{} (⋃ ran ((.) \circ G)) \leq sup (ran T ℝ^{} <)$
30	7 28 29	sylancl	$⊢ φ \to {vol}^{} (⋃ ran ((.) \circ G)) \leq sup (ran T ℝ^{} <)$
31		ovollecl	$⊢ (⋃ ran ((.) \circ G) \subseteq ℝ \land sup (ran T ℝ^{} <) \in ℝ \land {vol}^{} (⋃ ran ((.) \circ G)) \leq sup (ran T ℝ^{} <)) \to {vol}^{} (⋃ ran ((.) \circ G)) \in ℝ$
32	25 27 30 31	syl3anc	$⊢ φ \to {vol}^{*} (⋃ ran ((.) \circ G)) \in ℝ$
33		ovolsscl	$⊢ (K \subseteq ⋃ ran ((.) \circ G) \land ⋃ ran ((.) \circ G) \subseteq ℝ \land {vol}^{} (⋃ ran ((.) \circ G)) \in ℝ) \to {vol}^{} (K) \in ℝ$
34	20 25 32 33	mp3an2i	$⊢ φ \to {vol}^{*} (K) \in ℝ$
35		ovolsscl	$⊢ (K \cap A \subseteq K \land K \subseteq ℝ \land {vol}^{} (K) \in ℝ) \to {vol}^{} (K \cap A) \in ℝ$
36	17 26 34 35	mp3an2i	$⊢ φ \to {vol}^{*} (K \cap A) \in ℝ$
37		inss1	$⊢ K \cap L \subseteq K$
38		ovolsscl	$⊢ (K \cap L \subseteq K \land K \subseteq ℝ \land {vol}^{} (K) \in ℝ) \to {vol}^{} (K \cap L) \in ℝ$
39	37 26 34 38	mp3an2i	$⊢ φ \to {vol}^{*} (K \cap L) \in ℝ$
40		ssun2	$⊢ ⋃_{j = 1}^{M} ⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j))) \subseteq (K \cap L) \cup ⋃_{j = 1}^{M} ⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j)))$
41		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
42	14	peano2nnd	$⊢ φ \to N + 1 \in ℕ$
43	42 41	eleqtrdi	$⊢ φ \to N + 1 \in ℤ_{\geq 1}$
44		uzsplit	$⊢ N + 1 \in ℤ_{\geq 1} \to ℤ_{\geq 1} = (1 \dots N + 1 - 1) \cup ℤ_{\geq (N + 1)}$
45	43 44	syl	$⊢ φ \to ℤ_{\geq 1} = (1 \dots N + 1 - 1) \cup ℤ_{\geq (N + 1)}$
46	41 45	syl5eq	$⊢ φ \to ℕ = (1 \dots N + 1 - 1) \cup ℤ_{\geq (N + 1)}$
47	14	nncnd	$⊢ φ \to N \in ℂ$
48		ax-1cn	$⊢ 1 \in ℂ$
49		pncan	$⊢ (N \in ℂ \land 1 \in ℂ) \to N + 1 - 1 = N$
50	47 48 49	sylancl	$⊢ φ \to N + 1 - 1 = N$
51	50	oveq2d	$⊢ φ \to (1 \dots N + 1 - 1) = (1 \dots N)$
52	51	uneq1d	$⊢ φ \to (1 \dots N + 1 - 1) \cup ℤ_{\geq (N + 1)} = (1 \dots N) \cup ℤ_{\geq (N + 1)}$
53	46 52	eqtrd	$⊢ φ \to ℕ = (1 \dots N) \cup ℤ_{\geq (N + 1)}$
54	53	iuneq1d	$⊢ φ \to ⋃_{i \in ℕ} (.) (F (i)) = ⋃_{i \in (1 \dots N) \cup ℤ_{\geq (N + 1)}} (.) (F (i))$
55		iunxun	$⊢ ⋃_{i \in (1 \dots N) \cup ℤ_{\geq (N + 1)}} (.) (F (i)) = ⋃_{i = 1}^{N} (.) (F (i)) \cup ⋃_{i \in ℤ_{\geq (N + 1)}} (.) (F (i))$
56	54 55	eqtrdi	$⊢ φ \to ⋃_{i \in ℕ} (.) (F (i)) = ⋃_{i = 1}^{N} (.) (F (i)) \cup ⋃_{i \in ℤ_{\geq (N + 1)}} (.) (F (i))$
57		ioof	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
58		inss2	$⊢ \leq \cap ℝ^{2} \subseteq ℝ^{2}$
59		rexpssxrxp	$⊢ ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
60	58 59	sstri	$⊢ \leq \cap ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
61		fss	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land \leq \cap ℝ^{2} \subseteq ℝ^{} \times ℝ^{}) \to F : ℕ ⟶ ℝ^{} \times ℝ^{}$
62	1 60 61	sylancl	$⊢ φ \to F : ℕ ⟶ ℝ^{} \times ℝ^{}$
63		fco	$⊢ ((.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \land F : ℕ ⟶ ℝ^{} \times ℝ^{}) \to ((.) \circ F) : ℕ ⟶ 𝒫 ℝ$
64	57 62 63	sylancr	$⊢ φ \to ((.) \circ F) : ℕ ⟶ 𝒫 ℝ$
65		ffn	$⊢ ((.) \circ F) : ℕ ⟶ 𝒫 ℝ \to ((.) \circ F) Fn ℕ$
66		fniunfv	$⊢ ((.) \circ F) Fn ℕ \to ⋃_{i \in ℕ} ((.) \circ F) (i) = ⋃ ran ((.) \circ F)$
67	64 65 66	3syl	$⊢ φ \to ⋃_{i \in ℕ} ((.) \circ F) (i) = ⋃ ran ((.) \circ F)$
68		fvco3	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land i \in ℕ) \to ((.) \circ F) (i) = (.) (F (i))$
69	1 68	sylan	$⊢ (φ \land i \in ℕ) \to ((.) \circ F) (i) = (.) (F (i))$
70	69	iuneq2dv	$⊢ φ \to ⋃_{i \in ℕ} ((.) \circ F) (i) = ⋃_{i \in ℕ} (.) (F (i))$
71	67 70	eqtr3d	$⊢ φ \to ⋃ ran ((.) \circ F) = ⋃_{i \in ℕ} (.) (F (i))$
72	4 71	syl5eq	$⊢ φ \to A = ⋃_{i \in ℕ} (.) (F (i))$
73		ffun	$⊢ ((.) \circ F) : ℕ ⟶ 𝒫 ℝ \to Fun ((.) \circ F)$
74		funiunfv	$⊢ Fun ((.) \circ F) \to ⋃_{i = 1}^{N} ((.) \circ F) (i) = ⋃ ((.) \circ F) [(1 \dots N)]$
75	64 73 74	3syl	$⊢ φ \to ⋃_{i = 1}^{N} ((.) \circ F) (i) = ⋃ ((.) \circ F) [(1 \dots N)]$
76		elfznn	$⊢ i \in (1 \dots N) \to i \in ℕ$
77	1 76 68	syl2an	$⊢ (φ \land i \in (1 \dots N)) \to ((.) \circ F) (i) = (.) (F (i))$
78	77	iuneq2dv	$⊢ φ \to ⋃_{i = 1}^{N} ((.) \circ F) (i) = ⋃_{i = 1}^{N} (.) (F (i))$
79	75 78	eqtr3d	$⊢ φ \to ⋃ ((.) \circ F) [(1 \dots N)] = ⋃_{i = 1}^{N} (.) (F (i))$
80	16 79	syl5eq	$⊢ φ \to L = ⋃_{i = 1}^{N} (.) (F (i))$
81	80	uneq1d	$⊢ φ \to L \cup ⋃_{i \in ℤ_{\geq (N + 1)}} (.) (F (i)) = ⋃_{i = 1}^{N} (.) (F (i)) \cup ⋃_{i \in ℤ_{\geq (N + 1)}} (.) (F (i))$
82	56 72 81	3eqtr4d	$⊢ φ \to A = L \cup ⋃_{i \in ℤ_{\geq (N + 1)}} (.) (F (i))$
83	82	ineq2d	$⊢ φ \to K \cap A = K \cap (L \cup ⋃_{i \in ℤ_{\geq (N + 1)}} (.) (F (i)))$
84		indi	$⊢ K \cap (L \cup ⋃_{i \in ℤ_{\geq (N + 1)}} (.) (F (i))) = (K \cap L) \cup (K \cap ⋃_{i \in ℤ_{\geq (N + 1)}} (.) (F (i)))$
85	83 84	eqtrdi	$⊢ φ \to K \cap A = (K \cap L) \cup (K \cap ⋃_{i \in ℤ_{\geq (N + 1)}} (.) (F (i)))$
86		fss	$⊢ (G : ℕ ⟶ \leq \cap ℝ^{2} \land \leq \cap ℝ^{2} \subseteq ℝ^{} \times ℝ^{}) \to G : ℕ ⟶ ℝ^{} \times ℝ^{}$
87	7 60 86	sylancl	$⊢ φ \to G : ℕ ⟶ ℝ^{} \times ℝ^{}$
88		fco	$⊢ ((.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \land G : ℕ ⟶ ℝ^{} \times ℝ^{}) \to ((.) \circ G) : ℕ ⟶ 𝒫 ℝ$
89	57 87 88	sylancr	$⊢ φ \to ((.) \circ G) : ℕ ⟶ 𝒫 ℝ$
90		ffun	$⊢ ((.) \circ G) : ℕ ⟶ 𝒫 ℝ \to Fun ((.) \circ G)$
91		funiunfv	$⊢ Fun ((.) \circ G) \to ⋃_{j = 1}^{M} ((.) \circ G) (j) = ⋃ ((.) \circ G) [(1 \dots M)]$
92	89 90 91	3syl	$⊢ φ \to ⋃_{j = 1}^{M} ((.) \circ G) (j) = ⋃ ((.) \circ G) [(1 \dots M)]$
93		elfznn	$⊢ j \in (1 \dots M) \to j \in ℕ$
94		fvco3	$⊢ (G : ℕ ⟶ \leq \cap ℝ^{2} \land j \in ℕ) \to ((.) \circ G) (j) = (.) (G (j))$
95	7 93 94	syl2an	$⊢ (φ \land j \in (1 \dots M)) \to ((.) \circ G) (j) = (.) (G (j))$
96	95	iuneq2dv	$⊢ φ \to ⋃_{j = 1}^{M} ((.) \circ G) (j) = ⋃_{j = 1}^{M} (.) (G (j))$
97	92 96	eqtr3d	$⊢ φ \to ⋃ ((.) \circ G) [(1 \dots M)] = ⋃_{j = 1}^{M} (.) (G (j))$
98	13 97	syl5eq	$⊢ φ \to K = ⋃_{j = 1}^{M} (.) (G (j))$
99	98	ineq2d	$⊢ φ \to ⋃_{i \in ℤ_{\geq (N + 1)}} (.) (F (i)) \cap K = ⋃_{i \in ℤ_{\geq (N + 1)}} (.) (F (i)) \cap ⋃_{j = 1}^{M} (.) (G (j))$
100		incom	$⊢ K \cap ⋃_{i \in ℤ_{\geq (N + 1)}} (.) (F (i)) = ⋃_{i \in ℤ_{\geq (N + 1)}} (.) (F (i)) \cap K$
101		iunin2	$⊢ ⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (G (j)) \cap (.) (F (i))) = (.) (G (j)) \cap ⋃_{i \in ℤ_{\geq (N + 1)}} (.) (F (i))$
102		incom	$⊢ (.) (F (i)) \cap (.) (G (j)) = (.) (G (j)) \cap (.) (F (i))$
103	102	a1i	$⊢ i \in ℤ_{\geq (N + 1)} \to (.) (F (i)) \cap (.) (G (j)) = (.) (G (j)) \cap (.) (F (i))$
104	103	iuneq2i	$⊢ ⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j))) = ⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (G (j)) \cap (.) (F (i)))$
105		incom	$⊢ ⋃_{i \in ℤ_{\geq (N + 1)}} (.) (F (i)) \cap (.) (G (j)) = (.) (G (j)) \cap ⋃_{i \in ℤ_{\geq (N + 1)}} (.) (F (i))$
106	101 104 105	3eqtr4ri	$⊢ ⋃_{i \in ℤ_{\geq (N + 1)}} (.) (F (i)) \cap (.) (G (j)) = ⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j)))$
107	106	a1i	$⊢ j \in (1 \dots M) \to ⋃_{i \in ℤ_{\geq (N + 1)}} (.) (F (i)) \cap (.) (G (j)) = ⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j)))$
108	107	iuneq2i	$⊢ ⋃_{j = 1}^{M} (⋃_{i \in ℤ_{\geq (N + 1)}} (.) (F (i)) \cap (.) (G (j))) = ⋃_{j = 1}^{M} ⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j)))$
109		iunin2	$⊢ ⋃_{j = 1}^{M} (⋃_{i \in ℤ_{\geq (N + 1)}} (.) (F (i)) \cap (.) (G (j))) = ⋃_{i \in ℤ_{\geq (N + 1)}} (.) (F (i)) \cap ⋃_{j = 1}^{M} (.) (G (j))$
110	108 109	eqtr3i	$⊢ ⋃_{j = 1}^{M} ⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j))) = ⋃_{i \in ℤ_{\geq (N + 1)}} (.) (F (i)) \cap ⋃_{j = 1}^{M} (.) (G (j))$
111	99 100 110	3eqtr4g	$⊢ φ \to K \cap ⋃_{i \in ℤ_{\geq (N + 1)}} (.) (F (i)) = ⋃_{j = 1}^{M} ⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j)))$
112	111	uneq2d	$⊢ φ \to (K \cap L) \cup (K \cap ⋃_{i \in ℤ_{\geq (N + 1)}} (.) (F (i))) = (K \cap L) \cup ⋃_{j = 1}^{M} ⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j)))$
113	85 112	eqtrd	$⊢ φ \to K \cap A = (K \cap L) \cup ⋃_{j = 1}^{M} ⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j)))$
114	40 113	sseqtrrid	$⊢ φ \to ⋃_{j = 1}^{M} ⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j))) \subseteq K \cap A$
115	114 17	sstrdi	$⊢ φ \to ⋃_{j = 1}^{M} ⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j))) \subseteq K$
116		ovolsscl	$⊢ (⋃_{j = 1}^{M} ⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j))) \subseteq K \land K \subseteq ℝ \land {vol}^{} (K) \in ℝ) \to {vol}^{} (⋃_{j = 1}^{M} ⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j)))) \in ℝ$
117	115 26 34 116	syl3anc	$⊢ φ \to {vol}^{*} (⋃_{j = 1}^{M} ⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j)))) \in ℝ$
118	39 117	readdcld	$⊢ φ \to {vol}^{} (K \cap L) + {vol}^{} (⋃_{j = 1}^{M} ⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j)))) \in ℝ$
119	6	rpred	$⊢ φ \to C \in ℝ$
120	39 119	readdcld	$⊢ φ \to {vol}^{*} (K \cap L) + C \in ℝ$
121	113	fveq2d	$⊢ φ \to {vol}^{} (K \cap A) = {vol}^{} ((K \cap L) \cup ⋃_{j = 1}^{M} ⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j))))$
122	37 26	sstrid	$⊢ φ \to K \cap L \subseteq ℝ$
123	115 26	sstrd	$⊢ φ \to ⋃_{j = 1}^{M} ⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j))) \subseteq ℝ$
124		ovolun	$⊢ ((K \cap L \subseteq ℝ \land {vol}^{} (K \cap L) \in ℝ) \land (⋃_{j = 1}^{M} ⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j))) \subseteq ℝ \land {vol}^{} (⋃_{j = 1}^{M} ⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j)))) \in ℝ)) \to {vol}^{} ((K \cap L) \cup ⋃_{j = 1}^{M} ⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j)))) \leq {vol}^{} (K \cap L) + {vol}^{*} (⋃_{j = 1}^{M} ⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j))))$
125	122 39 123 117 124	syl22anc	$⊢ φ \to {vol}^{} ((K \cap L) \cup ⋃_{j = 1}^{M} ⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j)))) \leq {vol}^{} (K \cap L) + {vol}^{*} (⋃_{j = 1}^{M} ⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j))))$
126	121 125	eqbrtrd	$⊢ φ \to {vol}^{} (K \cap A) \leq {vol}^{} (K \cap L) + {vol}^{*} (⋃_{j = 1}^{M} ⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j))))$
127		fzfid	$⊢ φ \to (1 \dots M) \in Fin$
128		iunss	$⊢ ⋃_{j = 1}^{M} ⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j))) \subseteq K \leftrightarrow \forall j \in (1 \dots M) ⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j))) \subseteq K$
129	115 128	sylib	$⊢ φ \to \forall j \in (1 \dots M) ⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j))) \subseteq K$
130	129	r19.21bi	$⊢ (φ \land j \in (1 \dots M)) \to ⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j))) \subseteq K$
131	26	adantr	$⊢ (φ \land j \in (1 \dots M)) \to K \subseteq ℝ$
132	34	adantr	$⊢ (φ \land j \in (1 \dots M)) \to {vol}^{*} (K) \in ℝ$
133		ovolsscl	$⊢ (⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j))) \subseteq K \land K \subseteq ℝ \land {vol}^{} (K) \in ℝ) \to {vol}^{} (⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j)))) \in ℝ$
134	130 131 132 133	syl3anc	$⊢ (φ \land j \in (1 \dots M)) \to {vol}^{*} (⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j)))) \in ℝ$
135	127 134	fsumrecl	$⊢ φ \to \sum_{j = 1}^{M} {vol}^{*} (⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j)))) \in ℝ$
136	130 131	sstrd	$⊢ (φ \land j \in (1 \dots M)) \to ⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j))) \subseteq ℝ$
137	136 134	jca	$⊢ (φ \land j \in (1 \dots M)) \to (⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j))) \subseteq ℝ \land {vol}^{*} (⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j)))) \in ℝ)$
138	137	ralrimiva	$⊢ φ \to \forall j \in (1 \dots M) (⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j))) \subseteq ℝ \land {vol}^{*} (⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j)))) \in ℝ)$
139		ovolfiniun	$⊢ ((1 \dots M) \in Fin \land \forall j \in (1 \dots M) (⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j))) \subseteq ℝ \land {vol}^{} (⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j)))) \in ℝ)) \to {vol}^{} (⋃_{j = 1}^{M} ⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j)))) \leq \sum_{j = 1}^{M} {vol}^{*} (⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j))))$
140	127 138 139	syl2anc	$⊢ φ \to {vol}^{} (⋃_{j = 1}^{M} ⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j)))) \leq \sum_{j = 1}^{M} {vol}^{} (⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j))))$
141	119 11	nndivred	$⊢ φ \to \frac{C}{M} \in ℝ$
142	141	adantr	$⊢ (φ \land j \in (1 \dots M)) \to \frac{C}{M} \in ℝ$
143	80	ineq2d	$⊢ φ \to (.) (G (j)) \cap L = (.) (G (j)) \cap ⋃_{i = 1}^{N} (.) (F (i))$
144	143	adantr	$⊢ (φ \land j \in (1 \dots M)) \to (.) (G (j)) \cap L = (.) (G (j)) \cap ⋃_{i = 1}^{N} (.) (F (i))$
145	102	a1i	$⊢ i \in (1 \dots N) \to (.) (F (i)) \cap (.) (G (j)) = (.) (G (j)) \cap (.) (F (i))$
146	145	iuneq2i	$⊢ ⋃_{i = 1}^{N} ((.) (F (i)) \cap (.) (G (j))) = ⋃_{i = 1}^{N} ((.) (G (j)) \cap (.) (F (i)))$
147		iunin2	$⊢ ⋃_{i = 1}^{N} ((.) (G (j)) \cap (.) (F (i))) = (.) (G (j)) \cap ⋃_{i = 1}^{N} (.) (F (i))$
148	146 147	eqtri	$⊢ ⋃_{i = 1}^{N} ((.) (F (i)) \cap (.) (G (j))) = (.) (G (j)) \cap ⋃_{i = 1}^{N} (.) (F (i))$
149	144 148	eqtr4di	$⊢ (φ \land j \in (1 \dots M)) \to (.) (G (j)) \cap L = ⋃_{i = 1}^{N} ((.) (F (i)) \cap (.) (G (j)))$
150		fzfid	$⊢ (φ \land j \in (1 \dots M)) \to (1 \dots N) \in Fin$
151		ffvelrn	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land i \in ℕ) \to F (i) \in (\leq \cap ℝ^{2})$
152	1 76 151	syl2an	$⊢ (φ \land i \in (1 \dots N)) \to F (i) \in (\leq \cap ℝ^{2})$
153	152	elin2d	$⊢ (φ \land i \in (1 \dots N)) \to F (i) \in ℝ^{2}$
154		1st2nd2	$⊢ F (i) \in ℝ^{2} \to F (i) = ⟨1^{st} (F (i)), 2^{nd} (F (i))⟩$
155	153 154	syl	$⊢ (φ \land i \in (1 \dots N)) \to F (i) = ⟨1^{st} (F (i)), 2^{nd} (F (i))⟩$
156	155	fveq2d	$⊢ (φ \land i \in (1 \dots N)) \to (.) (F (i)) = (.) (⟨1^{st} (F (i)), 2^{nd} (F (i))⟩)$
157		df-ov	$⊢ (1^{st} (F (i)), 2^{nd} (F (i))) = (.) (⟨1^{st} (F (i)), 2^{nd} (F (i))⟩)$
158	156 157	eqtr4di	$⊢ (φ \land i \in (1 \dots N)) \to (.) (F (i)) = (1^{st} (F (i)), 2^{nd} (F (i)))$
159		ioombl	$⊢ (1^{st} (F (i)), 2^{nd} (F (i))) \in dom vol$
160	158 159	eqeltrdi	$⊢ (φ \land i \in (1 \dots N)) \to (.) (F (i)) \in dom vol$
161	160	adantlr	$⊢ ((φ \land j \in (1 \dots M)) \land i \in (1 \dots N)) \to (.) (F (i)) \in dom vol$
162		ffvelrn	$⊢ (G : ℕ ⟶ \leq \cap ℝ^{2} \land j \in ℕ) \to G (j) \in (\leq \cap ℝ^{2})$
163	7 93 162	syl2an	$⊢ (φ \land j \in (1 \dots M)) \to G (j) \in (\leq \cap ℝ^{2})$
164	163	elin2d	$⊢ (φ \land j \in (1 \dots M)) \to G (j) \in ℝ^{2}$
165		1st2nd2	$⊢ G (j) \in ℝ^{2} \to G (j) = ⟨1^{st} (G (j)), 2^{nd} (G (j))⟩$
166	164 165	syl	$⊢ (φ \land j \in (1 \dots M)) \to G (j) = ⟨1^{st} (G (j)), 2^{nd} (G (j))⟩$
167	166	fveq2d	$⊢ (φ \land j \in (1 \dots M)) \to (.) (G (j)) = (.) (⟨1^{st} (G (j)), 2^{nd} (G (j))⟩)$
168		df-ov	$⊢ (1^{st} (G (j)), 2^{nd} (G (j))) = (.) (⟨1^{st} (G (j)), 2^{nd} (G (j))⟩)$
169	167 168	eqtr4di	$⊢ (φ \land j \in (1 \dots M)) \to (.) (G (j)) = (1^{st} (G (j)), 2^{nd} (G (j)))$
170		ioombl	$⊢ (1^{st} (G (j)), 2^{nd} (G (j))) \in dom vol$
171	169 170	eqeltrdi	$⊢ (φ \land j \in (1 \dots M)) \to (.) (G (j)) \in dom vol$
172	171	adantr	$⊢ ((φ \land j \in (1 \dots M)) \land i \in (1 \dots N)) \to (.) (G (j)) \in dom vol$
173		inmbl	$⊢ ((.) (F (i)) \in dom vol \land (.) (G (j)) \in dom vol) \to (.) (F (i)) \cap (.) (G (j)) \in dom vol$
174	161 172 173	syl2anc	$⊢ ((φ \land j \in (1 \dots M)) \land i \in (1 \dots N)) \to (.) (F (i)) \cap (.) (G (j)) \in dom vol$
175	174	ralrimiva	$⊢ (φ \land j \in (1 \dots M)) \to \forall i \in (1 \dots N) (.) (F (i)) \cap (.) (G (j)) \in dom vol$
176		finiunmbl	$⊢ ((1 \dots N) \in Fin \land \forall i \in (1 \dots N) (.) (F (i)) \cap (.) (G (j)) \in dom vol) \to ⋃_{i = 1}^{N} ((.) (F (i)) \cap (.) (G (j))) \in dom vol$
177	150 175 176	syl2anc	$⊢ (φ \land j \in (1 \dots M)) \to ⋃_{i = 1}^{N} ((.) (F (i)) \cap (.) (G (j))) \in dom vol$
178	149 177	eqeltrd	$⊢ (φ \land j \in (1 \dots M)) \to (.) (G (j)) \cap L \in dom vol$
179		inss2	$⊢ (.) (G (j)) \cap A \subseteq A$
180	1	uniiccdif	$⊢ φ \to (⋃ ran ((.) \circ F) \subseteq ⋃ ran ([.] \circ F) \land {vol}^{*} (⋃ ran ([.] \circ F) ∖ ⋃ ran ((.) \circ F)) = 0)$
181	180	simpld	$⊢ φ \to ⋃ ran ((.) \circ F) \subseteq ⋃ ran ([.] \circ F)$
182		ovolficcss	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to ⋃ ran ([.] \circ F) \subseteq ℝ$
183	1 182	syl	$⊢ φ \to ⋃ ran ([.] \circ F) \subseteq ℝ$
184	181 183	sstrd	$⊢ φ \to ⋃ ran ((.) \circ F) \subseteq ℝ$
185	4 184	eqsstrid	$⊢ φ \to A \subseteq ℝ$
186	185	adantr	$⊢ (φ \land j \in (1 \dots M)) \to A \subseteq ℝ$
187	179 186	sstrid	$⊢ (φ \land j \in (1 \dots M)) \to (.) (G (j)) \cap A \subseteq ℝ$
188		inss1	$⊢ (.) (G (j)) \cap A \subseteq (.) (G (j))$
189		ioossre	$⊢ (1^{st} (G (j)), 2^{nd} (G (j))) \subseteq ℝ$
190	169 189	eqsstrdi	$⊢ (φ \land j \in (1 \dots M)) \to (.) (G (j)) \subseteq ℝ$
191	169	fveq2d	$⊢ (φ \land j \in (1 \dots M)) \to {vol}^{} ((.) (G (j))) = {vol}^{} ((1^{st} (G (j)), 2^{nd} (G (j))))$
192		ovolfcl	$⊢ (G : ℕ ⟶ \leq \cap ℝ^{2} \land j \in ℕ) \to (1^{st} (G (j)) \in ℝ \land 2^{nd} (G (j)) \in ℝ \land 1^{st} (G (j)) \leq 2^{nd} (G (j)))$
193	7 93 192	syl2an	$⊢ (φ \land j \in (1 \dots M)) \to (1^{st} (G (j)) \in ℝ \land 2^{nd} (G (j)) \in ℝ \land 1^{st} (G (j)) \leq 2^{nd} (G (j)))$
194		ovolioo	$⊢ (1^{st} (G (j)) \in ℝ \land 2^{nd} (G (j)) \in ℝ \land 1^{st} (G (j)) \leq 2^{nd} (G (j))) \to {vol}^{*} ((1^{st} (G (j)), 2^{nd} (G (j)))) = 2^{nd} (G (j)) - 1^{st} (G (j))$
195	193 194	syl	$⊢ (φ \land j \in (1 \dots M)) \to {vol}^{*} ((1^{st} (G (j)), 2^{nd} (G (j)))) = 2^{nd} (G (j)) - 1^{st} (G (j))$
196	191 195	eqtrd	$⊢ (φ \land j \in (1 \dots M)) \to {vol}^{*} ((.) (G (j))) = 2^{nd} (G (j)) - 1^{st} (G (j))$
197	193	simp2d	$⊢ (φ \land j \in (1 \dots M)) \to 2^{nd} (G (j)) \in ℝ$
198	193	simp1d	$⊢ (φ \land j \in (1 \dots M)) \to 1^{st} (G (j)) \in ℝ$
199	197 198	resubcld	$⊢ (φ \land j \in (1 \dots M)) \to 2^{nd} (G (j)) - 1^{st} (G (j)) \in ℝ$
200	196 199	eqeltrd	$⊢ (φ \land j \in (1 \dots M)) \to {vol}^{*} ((.) (G (j))) \in ℝ$
201		ovolsscl	$⊢ ((.) (G (j)) \cap A \subseteq (.) (G (j)) \land (.) (G (j)) \subseteq ℝ \land {vol}^{} ((.) (G (j))) \in ℝ) \to {vol}^{} ((.) (G (j)) \cap A) \in ℝ$
202	188 190 200 201	mp3an2i	$⊢ (φ \land j \in (1 \dots M)) \to {vol}^{*} ((.) (G (j)) \cap A) \in ℝ$
203		mblsplit	$⊢ ((.) (G (j)) \cap L \in dom vol \land (.) (G (j)) \cap A \subseteq ℝ \land {vol}^{} ((.) (G (j)) \cap A) \in ℝ) \to {vol}^{} ((.) (G (j)) \cap A) = {vol}^{} (((.) (G (j)) \cap A) \cap ((.) (G (j)) \cap L)) + {vol}^{} (((.) (G (j)) \cap A) ∖ ((.) (G (j)) \cap L))$
204	178 187 202 203	syl3anc	$⊢ (φ \land j \in (1 \dots M)) \to {vol}^{} ((.) (G (j)) \cap A) = {vol}^{} (((.) (G (j)) \cap A) \cap ((.) (G (j)) \cap L)) + {vol}^{*} (((.) (G (j)) \cap A) ∖ ((.) (G (j)) \cap L))$
205		imassrn	$⊢ ((.) \circ F) [(1 \dots N)] \subseteq ran ((.) \circ F)$
206	205	unissi	$⊢ ⋃ ((.) \circ F) [(1 \dots N)] \subseteq ⋃ ran ((.) \circ F)$
207	206 16 4	3sstr4i	$⊢ L \subseteq A$
208		sslin	$⊢ L \subseteq A \to (.) (G (j)) \cap L \subseteq (.) (G (j)) \cap A$
209	207 208	mp1i	$⊢ (φ \land j \in (1 \dots M)) \to (.) (G (j)) \cap L \subseteq (.) (G (j)) \cap A$
210		sseqin2	$⊢ (.) (G (j)) \cap L \subseteq (.) (G (j)) \cap A \leftrightarrow ((.) (G (j)) \cap A) \cap ((.) (G (j)) \cap L) = (.) (G (j)) \cap L$
211	209 210	sylib	$⊢ (φ \land j \in (1 \dots M)) \to ((.) (G (j)) \cap A) \cap ((.) (G (j)) \cap L) = (.) (G (j)) \cap L$
212	211	fveq2d	$⊢ (φ \land j \in (1 \dots M)) \to {vol}^{} (((.) (G (j)) \cap A) \cap ((.) (G (j)) \cap L)) = {vol}^{} ((.) (G (j)) \cap L)$
213		indifdir	$⊢ (A ∖ L) \cap (.) (G (j)) = (A \cap (.) (G (j))) ∖ (L \cap (.) (G (j)))$
214		incom	$⊢ A \cap (.) (G (j)) = (.) (G (j)) \cap A$
215		incom	$⊢ L \cap (.) (G (j)) = (.) (G (j)) \cap L$
216	214 215	difeq12i	$⊢ (A \cap (.) (G (j))) ∖ (L \cap (.) (G (j))) = ((.) (G (j)) \cap A) ∖ ((.) (G (j)) \cap L)$
217	213 216	eqtri	$⊢ (A ∖ L) \cap (.) (G (j)) = ((.) (G (j)) \cap A) ∖ ((.) (G (j)) \cap L)$
218	82	eqcomd	$⊢ φ \to L \cup ⋃_{i \in ℤ_{\geq (N + 1)}} (.) (F (i)) = A$
219	80	ineq1d	$⊢ φ \to L \cap ⋃_{i \in ℤ_{\geq (N + 1)}} (.) (F (i)) = ⋃_{i = 1}^{N} (.) (F (i)) \cap ⋃_{i \in ℤ_{\geq (N + 1)}} (.) (F (i))$
220		2fveq3	$⊢ x = i \to (.) (F (x)) = (.) (F (i))$
221	220	cbvdisjv	$⊢ \underset{x \in ℕ}{Disj} (.) (F (x)) \leftrightarrow \underset{i \in ℕ}{Disj} (.) (F (i))$
222	2 221	sylib	$⊢ φ \to \underset{i \in ℕ}{Disj} (.) (F (i))$
223		fz1ssnn	$⊢ (1 \dots N) \subseteq ℕ$
224	223	a1i	$⊢ φ \to (1 \dots N) \subseteq ℕ$
225		uzss	$⊢ N + 1 \in ℤ_{\geq 1} \to ℤ_{\geq (N + 1)} \subseteq ℤ_{\geq 1}$
226	43 225	syl	$⊢ φ \to ℤ_{\geq (N + 1)} \subseteq ℤ_{\geq 1}$
227	226 41	sseqtrrdi	$⊢ φ \to ℤ_{\geq (N + 1)} \subseteq ℕ$
228	51	ineq1d	$⊢ φ \to (1 \dots N + 1 - 1) \cap ℤ_{\geq (N + 1)} = (1 \dots N) \cap ℤ_{\geq (N + 1)}$
229		uzdisj	$⊢ (1 \dots N + 1 - 1) \cap ℤ_{\geq (N + 1)} = \emptyset$
230	228 229	eqtr3di	$⊢ φ \to (1 \dots N) \cap ℤ_{\geq (N + 1)} = \emptyset$
231		disjiun	$⊢ (\underset{i \in ℕ}{Disj} (.) (F (i)) \land ((1 \dots N) \subseteq ℕ \land ℤ_{\geq (N + 1)} \subseteq ℕ \land (1 \dots N) \cap ℤ_{\geq (N + 1)} = \emptyset)) \to ⋃_{i = 1}^{N} (.) (F (i)) \cap ⋃_{i \in ℤ_{\geq (N + 1)}} (.) (F (i)) = \emptyset$
232	222 224 227 230 231	syl13anc	$⊢ φ \to ⋃_{i = 1}^{N} (.) (F (i)) \cap ⋃_{i \in ℤ_{\geq (N + 1)}} (.) (F (i)) = \emptyset$
233	219 232	eqtrd	$⊢ φ \to L \cap ⋃_{i \in ℤ_{\geq (N + 1)}} (.) (F (i)) = \emptyset$
234		uneqdifeq	$⊢ (L \subseteq A \land L \cap ⋃_{i \in ℤ_{\geq (N + 1)}} (.) (F (i)) = \emptyset) \to (L \cup ⋃_{i \in ℤ_{\geq (N + 1)}} (.) (F (i)) = A \leftrightarrow A ∖ L = ⋃_{i \in ℤ_{\geq (N + 1)}} (.) (F (i)))$
235	207 233 234	sylancr	$⊢ φ \to (L \cup ⋃_{i \in ℤ_{\geq (N + 1)}} (.) (F (i)) = A \leftrightarrow A ∖ L = ⋃_{i \in ℤ_{\geq (N + 1)}} (.) (F (i)))$
236	218 235	mpbid	$⊢ φ \to A ∖ L = ⋃_{i \in ℤ_{\geq (N + 1)}} (.) (F (i))$
237	236	adantr	$⊢ (φ \land j \in (1 \dots M)) \to A ∖ L = ⋃_{i \in ℤ_{\geq (N + 1)}} (.) (F (i))$
238	237	ineq2d	$⊢ (φ \land j \in (1 \dots M)) \to (.) (G (j)) \cap (A ∖ L) = (.) (G (j)) \cap ⋃_{i \in ℤ_{\geq (N + 1)}} (.) (F (i))$
239		incom	$⊢ (A ∖ L) \cap (.) (G (j)) = (.) (G (j)) \cap (A ∖ L)$
240	104 101	eqtri	$⊢ ⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j))) = (.) (G (j)) \cap ⋃_{i \in ℤ_{\geq (N + 1)}} (.) (F (i))$
241	238 239 240	3eqtr4g	$⊢ (φ \land j \in (1 \dots M)) \to (A ∖ L) \cap (.) (G (j)) = ⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j)))$
242	217 241	eqtr3id	$⊢ (φ \land j \in (1 \dots M)) \to ((.) (G (j)) \cap A) ∖ ((.) (G (j)) \cap L) = ⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j)))$
243	242	fveq2d	$⊢ (φ \land j \in (1 \dots M)) \to {vol}^{} (((.) (G (j)) \cap A) ∖ ((.) (G (j)) \cap L)) = {vol}^{} (⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j))))$
244	212 243	oveq12d	$⊢ (φ \land j \in (1 \dots M)) \to {vol}^{} (((.) (G (j)) \cap A) \cap ((.) (G (j)) \cap L)) + {vol}^{} (((.) (G (j)) \cap A) ∖ ((.) (G (j)) \cap L)) = {vol}^{} ((.) (G (j)) \cap L) + {vol}^{} (⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j))))$
245	204 244	eqtrd	$⊢ (φ \land j \in (1 \dots M)) \to {vol}^{} ((.) (G (j)) \cap A) = {vol}^{} ((.) (G (j)) \cap L) + {vol}^{*} (⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j))))$
246	202 142	resubcld	$⊢ (φ \land j \in (1 \dots M)) \to {vol}^{*} ((.) (G (j)) \cap A) - (\frac{C}{M}) \in ℝ$
247		inss2	$⊢ (.) (F (i)) \cap (.) (G (j)) \subseteq (.) (G (j))$
248	190	adantr	$⊢ ((φ \land j \in (1 \dots M)) \land i \in (1 \dots N)) \to (.) (G (j)) \subseteq ℝ$
249	200	adantr	$⊢ ((φ \land j \in (1 \dots M)) \land i \in (1 \dots N)) \to {vol}^{*} ((.) (G (j))) \in ℝ$
250		ovolsscl	$⊢ ((.) (F (i)) \cap (.) (G (j)) \subseteq (.) (G (j)) \land (.) (G (j)) \subseteq ℝ \land {vol}^{} ((.) (G (j))) \in ℝ) \to {vol}^{} ((.) (F (i)) \cap (.) (G (j))) \in ℝ$
251	247 248 249 250	mp3an2i	$⊢ ((φ \land j \in (1 \dots M)) \land i \in (1 \dots N)) \to {vol}^{*} ((.) (F (i)) \cap (.) (G (j))) \in ℝ$
252	150 251	fsumrecl	$⊢ (φ \land j \in (1 \dots M)) \to \sum_{i = 1}^{N} {vol}^{*} ((.) (F (i)) \cap (.) (G (j))) \in ℝ$
253	15	r19.21bi	$⊢ (φ \land j \in (1 \dots M)) \to \|\sum_{i = 1}^{N} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{} ((.) (G (j)) \cap A)\| < \frac{C}{M}$
254	252 202 142	absdifltd	$⊢ (φ \land j \in (1 \dots M)) \to (\|\sum_{i = 1}^{N} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{} ((.) (G (j)) \cap A)\| < \frac{C}{M} \leftrightarrow ({vol}^{} ((.) (G (j)) \cap A) - (\frac{C}{M}) < \sum_{i = 1}^{N} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) \land \sum_{i = 1}^{N} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) < {vol}^{} ((.) (G (j)) \cap A) + (\frac{C}{M})))$
255	253 254	mpbid	$⊢ (φ \land j \in (1 \dots M)) \to ({vol}^{} ((.) (G (j)) \cap A) - (\frac{C}{M}) < \sum_{i = 1}^{N} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) \land \sum_{i = 1}^{N} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) < {vol}^{} ((.) (G (j)) \cap A) + (\frac{C}{M}))$
256	255	simpld	$⊢ (φ \land j \in (1 \dots M)) \to {vol}^{} ((.) (G (j)) \cap A) - (\frac{C}{M}) < \sum_{i = 1}^{N} {vol}^{} ((.) (F (i)) \cap (.) (G (j)))$
257	246 252 256	ltled	$⊢ (φ \land j \in (1 \dots M)) \to {vol}^{} ((.) (G (j)) \cap A) - (\frac{C}{M}) \leq \sum_{i = 1}^{N} {vol}^{} ((.) (F (i)) \cap (.) (G (j)))$
258	149	fveq2d	$⊢ (φ \land j \in (1 \dots M)) \to {vol}^{} ((.) (G (j)) \cap L) = {vol}^{} (⋃_{i = 1}^{N} ((.) (F (i)) \cap (.) (G (j))))$
259		mblvol	$⊢ (.) (F (i)) \cap (.) (G (j)) \in dom vol \to vol ((.) (F (i)) \cap (.) (G (j))) = {vol}^{*} ((.) (F (i)) \cap (.) (G (j)))$
260	174 259	syl	$⊢ ((φ \land j \in (1 \dots M)) \land i \in (1 \dots N)) \to vol ((.) (F (i)) \cap (.) (G (j))) = {vol}^{*} ((.) (F (i)) \cap (.) (G (j)))$
261	260 251	eqeltrd	$⊢ ((φ \land j \in (1 \dots M)) \land i \in (1 \dots N)) \to vol ((.) (F (i)) \cap (.) (G (j))) \in ℝ$
262	174 261	jca	$⊢ ((φ \land j \in (1 \dots M)) \land i \in (1 \dots N)) \to ((.) (F (i)) \cap (.) (G (j)) \in dom vol \land vol ((.) (F (i)) \cap (.) (G (j))) \in ℝ)$
263	262	ralrimiva	$⊢ (φ \land j \in (1 \dots M)) \to \forall i \in (1 \dots N) ((.) (F (i)) \cap (.) (G (j)) \in dom vol \land vol ((.) (F (i)) \cap (.) (G (j))) \in ℝ)$
264		inss1	$⊢ (.) (F (i)) \cap (.) (G (j)) \subseteq (.) (F (i))$
265	264	rgenw	$⊢ \forall i \in ℕ (.) (F (i)) \cap (.) (G (j)) \subseteq (.) (F (i))$
266	222	adantr	$⊢ (φ \land j \in (1 \dots M)) \to \underset{i \in ℕ}{Disj} (.) (F (i))$
267		disjss2	$⊢ \forall i \in ℕ (.) (F (i)) \cap (.) (G (j)) \subseteq (.) (F (i)) \to (\underset{i \in ℕ}{Disj} (.) (F (i)) \to \underset{i \in ℕ}{Disj} ((.) (F (i)) \cap (.) (G (j))))$
268	265 266 267	mpsyl	$⊢ (φ \land j \in (1 \dots M)) \to \underset{i \in ℕ}{Disj} ((.) (F (i)) \cap (.) (G (j)))$
269		disjss1	$⊢ (1 \dots N) \subseteq ℕ \to (\underset{i \in ℕ}{Disj} ((.) (F (i)) \cap (.) (G (j))) \to {Disj}_{i = 1}^{N} ((.) (F (i)) \cap (.) (G (j))))$
270	223 268 269	mpsyl	$⊢ (φ \land j \in (1 \dots M)) \to {Disj}_{i = 1}^{N} ((.) (F (i)) \cap (.) (G (j)))$
271		volfiniun	$⊢ ((1 \dots N) \in Fin \land \forall i \in (1 \dots N) ((.) (F (i)) \cap (.) (G (j)) \in dom vol \land vol ((.) (F (i)) \cap (.) (G (j))) \in ℝ) \land {Disj}_{i = 1}^{N} ((.) (F (i)) \cap (.) (G (j)))) \to vol (⋃_{i = 1}^{N} ((.) (F (i)) \cap (.) (G (j)))) = \sum_{i = 1}^{N} vol ((.) (F (i)) \cap (.) (G (j)))$
272	150 263 270 271	syl3anc	$⊢ (φ \land j \in (1 \dots M)) \to vol (⋃_{i = 1}^{N} ((.) (F (i)) \cap (.) (G (j)))) = \sum_{i = 1}^{N} vol ((.) (F (i)) \cap (.) (G (j)))$
273		mblvol	$⊢ ⋃_{i = 1}^{N} ((.) (F (i)) \cap (.) (G (j))) \in dom vol \to vol (⋃_{i = 1}^{N} ((.) (F (i)) \cap (.) (G (j)))) = {vol}^{*} (⋃_{i = 1}^{N} ((.) (F (i)) \cap (.) (G (j))))$
274	177 273	syl	$⊢ (φ \land j \in (1 \dots M)) \to vol (⋃_{i = 1}^{N} ((.) (F (i)) \cap (.) (G (j)))) = {vol}^{*} (⋃_{i = 1}^{N} ((.) (F (i)) \cap (.) (G (j))))$
275	260	sumeq2dv	$⊢ (φ \land j \in (1 \dots M)) \to \sum_{i = 1}^{N} vol ((.) (F (i)) \cap (.) (G (j))) = \sum_{i = 1}^{N} {vol}^{*} ((.) (F (i)) \cap (.) (G (j)))$
276	272 274 275	3eqtr3d	$⊢ (φ \land j \in (1 \dots M)) \to {vol}^{} (⋃_{i = 1}^{N} ((.) (F (i)) \cap (.) (G (j)))) = \sum_{i = 1}^{N} {vol}^{} ((.) (F (i)) \cap (.) (G (j)))$
277	258 276	eqtrd	$⊢ (φ \land j \in (1 \dots M)) \to {vol}^{} ((.) (G (j)) \cap L) = \sum_{i = 1}^{N} {vol}^{} ((.) (F (i)) \cap (.) (G (j)))$
278	257 277	breqtrrd	$⊢ (φ \land j \in (1 \dots M)) \to {vol}^{} ((.) (G (j)) \cap A) - (\frac{C}{M}) \leq {vol}^{} ((.) (G (j)) \cap L)$
279	277 252	eqeltrd	$⊢ (φ \land j \in (1 \dots M)) \to {vol}^{*} ((.) (G (j)) \cap L) \in ℝ$
280	202 142 279	lesubaddd	$⊢ (φ \land j \in (1 \dots M)) \to ({vol}^{} ((.) (G (j)) \cap A) - (\frac{C}{M}) \leq {vol}^{} ((.) (G (j)) \cap L) \leftrightarrow {vol}^{} ((.) (G (j)) \cap A) \leq {vol}^{} ((.) (G (j)) \cap L) + (\frac{C}{M}))$
281	278 280	mpbid	$⊢ (φ \land j \in (1 \dots M)) \to {vol}^{} ((.) (G (j)) \cap A) \leq {vol}^{} ((.) (G (j)) \cap L) + (\frac{C}{M})$
282	245 281	eqbrtrrd	$⊢ (φ \land j \in (1 \dots M)) \to {vol}^{} ((.) (G (j)) \cap L) + {vol}^{} (⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j)))) \leq {vol}^{*} ((.) (G (j)) \cap L) + (\frac{C}{M})$
283	134 142 279	leadd2d	$⊢ (φ \land j \in (1 \dots M)) \to ({vol}^{} (⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j)))) \leq \frac{C}{M} \leftrightarrow {vol}^{} ((.) (G (j)) \cap L) + {vol}^{} (⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j)))) \leq {vol}^{} ((.) (G (j)) \cap L) + (\frac{C}{M}))$
284	282 283	mpbird	$⊢ (φ \land j \in (1 \dots M)) \to {vol}^{*} (⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j)))) \leq \frac{C}{M}$
285	127 134 142 284	fsumle	$⊢ φ \to \sum_{j = 1}^{M} {vol}^{*} (⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j)))) \leq \sum_{j = 1}^{M} (\frac{C}{M})$
286	141	recnd	$⊢ φ \to \frac{C}{M} \in ℂ$
287		fsumconst	$⊢ ((1 \dots M) \in Fin \land \frac{C}{M} \in ℂ) \to \sum_{j = 1}^{M} (\frac{C}{M}) = \|(1 \dots M)\| (\frac{C}{M})$
288	127 286 287	syl2anc	$⊢ φ \to \sum_{j = 1}^{M} (\frac{C}{M}) = \|(1 \dots M)\| (\frac{C}{M})$
289		nnnn0	$⊢ M \in ℕ \to M \in ℕ_{0}$
290		hashfz1	$⊢ M \in ℕ_{0} \to \|(1 \dots M)\| = M$
291	11 289 290	3syl	$⊢ φ \to \|(1 \dots M)\| = M$
292	291	oveq1d	$⊢ φ \to \|(1 \dots M)\| (\frac{C}{M}) = M (\frac{C}{M})$
293	119	recnd	$⊢ φ \to C \in ℂ$
294	11	nncnd	$⊢ φ \to M \in ℂ$
295	11	nnne0d	$⊢ φ \to M \neq 0$
296	293 294 295	divcan2d	$⊢ φ \to M (\frac{C}{M}) = C$
297	288 292 296	3eqtrd	$⊢ φ \to \sum_{j = 1}^{M} (\frac{C}{M}) = C$
298	285 297	breqtrd	$⊢ φ \to \sum_{j = 1}^{M} {vol}^{*} (⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j)))) \leq C$
299	117 135 119 140 298	letrd	$⊢ φ \to {vol}^{*} (⋃_{j = 1}^{M} ⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j)))) \leq C$
300	117 119 39 299	leadd2dd	$⊢ φ \to {vol}^{} (K \cap L) + {vol}^{} (⋃_{j = 1}^{M} ⋃_{i \in ℤ_{\geq (N + 1)}} ((.) (F (i)) \cap (.) (G (j)))) \leq {vol}^{*} (K \cap L) + C$
301	36 118 120 126 300	letrd	$⊢ φ \to {vol}^{} (K \cap A) \leq {vol}^{} (K \cap L) + C$

Metamath Proof Explorer

Theorem uniioombllem4

Proof