uniioombllem3

	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)]$
Assertion	uniioombllem3	$⊢ φ \to {vol}^{} (E \cap A) + {vol}^{} (E ∖ A) < {vol}^{} (K \cap A) + {vol}^{} (K ∖ A) + C + 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		inss1	$⊢ E \cap A \subseteq E$
15	14	a1i	$⊢ φ \to E \cap A \subseteq E$
16	7	uniiccdif	$⊢ φ \to (⋃ ran ((.) \circ G) \subseteq ⋃ ran ([.] \circ G) \land {vol}^{*} (⋃ ran ([.] \circ G) ∖ ⋃ ran ((.) \circ G)) = 0)$
17	16	simpld	$⊢ φ \to ⋃ ran ((.) \circ G) \subseteq ⋃ ran ([.] \circ G)$
18		ovolficcss	$⊢ G : ℕ ⟶ \leq \cap ℝ^{2} \to ⋃ ran ([.] \circ G) \subseteq ℝ$
19	7 18	syl	$⊢ φ \to ⋃ ran ([.] \circ G) \subseteq ℝ$
20	17 19	sstrd	$⊢ φ \to ⋃ ran ((.) \circ G) \subseteq ℝ$
21	8 20	sstrd	$⊢ φ \to E \subseteq ℝ$
22		ovolsscl	$⊢ (E \cap A \subseteq E \land E \subseteq ℝ \land {vol}^{} (E) \in ℝ) \to {vol}^{} (E \cap A) \in ℝ$
23	15 21 5 22	syl3anc	$⊢ φ \to {vol}^{*} (E \cap A) \in ℝ$
24		difssd	$⊢ φ \to E ∖ A \subseteq E$
25		ovolsscl	$⊢ (E ∖ A \subseteq E \land E \subseteq ℝ \land {vol}^{} (E) \in ℝ) \to {vol}^{} (E ∖ A) \in ℝ$
26	24 21 5 25	syl3anc	$⊢ φ \to {vol}^{*} (E ∖ A) \in ℝ$
27		inss1	$⊢ K \cap A \subseteq K$
28	27	a1i	$⊢ φ \to K \cap A \subseteq K$
29	1 2 3 4 5 6 7 8 9 10 11 12 13	uniioombllem3a	$⊢ φ \to (K = ⋃_{j = 1}^{M} (.) (G (j)) \land {vol}^{*} (K) \in ℝ)$
30	29	simpld	$⊢ φ \to K = ⋃_{j = 1}^{M} (.) (G (j))$
31		inss2	$⊢ \leq \cap ℝ^{2} \subseteq ℝ^{2}$
32		elfznn	$⊢ j \in (1 \dots M) \to j \in ℕ$
33		ffvelrn	$⊢ (G : ℕ ⟶ \leq \cap ℝ^{2} \land j \in ℕ) \to G (j) \in (\leq \cap ℝ^{2})$
34	7 32 33	syl2an	$⊢ (φ \land j \in (1 \dots M)) \to G (j) \in (\leq \cap ℝ^{2})$
35	31 34	sselid	$⊢ (φ \land j \in (1 \dots M)) \to G (j) \in ℝ^{2}$
36		1st2nd2	$⊢ G (j) \in ℝ^{2} \to G (j) = ⟨1^{st} (G (j)), 2^{nd} (G (j))⟩$
37	35 36	syl	$⊢ (φ \land j \in (1 \dots M)) \to G (j) = ⟨1^{st} (G (j)), 2^{nd} (G (j))⟩$
38	37	fveq2d	$⊢ (φ \land j \in (1 \dots M)) \to (.) (G (j)) = (.) (⟨1^{st} (G (j)), 2^{nd} (G (j))⟩)$
39		df-ov	$⊢ (1^{st} (G (j)), 2^{nd} (G (j))) = (.) (⟨1^{st} (G (j)), 2^{nd} (G (j))⟩)$
40	38 39	eqtr4di	$⊢ (φ \land j \in (1 \dots M)) \to (.) (G (j)) = (1^{st} (G (j)), 2^{nd} (G (j)))$
41		ioossre	$⊢ (1^{st} (G (j)), 2^{nd} (G (j))) \subseteq ℝ$
42	40 41	eqsstrdi	$⊢ (φ \land j \in (1 \dots M)) \to (.) (G (j)) \subseteq ℝ$
43	42	ralrimiva	$⊢ φ \to \forall j \in (1 \dots M) (.) (G (j)) \subseteq ℝ$
44		iunss	$⊢ ⋃_{j = 1}^{M} (.) (G (j)) \subseteq ℝ \leftrightarrow \forall j \in (1 \dots M) (.) (G (j)) \subseteq ℝ$
45	43 44	sylibr	$⊢ φ \to ⋃_{j = 1}^{M} (.) (G (j)) \subseteq ℝ$
46	30 45	eqsstrd	$⊢ φ \to K \subseteq ℝ$
47	29	simprd	$⊢ φ \to {vol}^{*} (K) \in ℝ$
48		ovolsscl	$⊢ (K \cap A \subseteq K \land K \subseteq ℝ \land {vol}^{} (K) \in ℝ) \to {vol}^{} (K \cap A) \in ℝ$
49	28 46 47 48	syl3anc	$⊢ φ \to {vol}^{*} (K \cap A) \in ℝ$
50	6	rpred	$⊢ φ \to C \in ℝ$
51	49 50	readdcld	$⊢ φ \to {vol}^{*} (K \cap A) + C \in ℝ$
52		difssd	$⊢ φ \to K ∖ A \subseteq K$
53		ovolsscl	$⊢ (K ∖ A \subseteq K \land K \subseteq ℝ \land {vol}^{} (K) \in ℝ) \to {vol}^{} (K ∖ A) \in ℝ$
54	52 46 47 53	syl3anc	$⊢ φ \to {vol}^{*} (K ∖ A) \in ℝ$
55	54 50	readdcld	$⊢ φ \to {vol}^{*} (K ∖ A) + C \in ℝ$
56		ssun2	$⊢ ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}] \subseteq K \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]$
57		ioof	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
58		rexpssxrxp	$⊢ ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
59	31 58	sstri	$⊢ \leq \cap ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
60		fss	$⊢ (G : ℕ ⟶ \leq \cap ℝ^{2} \land \leq \cap ℝ^{2} \subseteq ℝ^{} \times ℝ^{}) \to G : ℕ ⟶ ℝ^{} \times ℝ^{}$
61	7 59 60	sylancl	$⊢ φ \to G : ℕ ⟶ ℝ^{} \times ℝ^{}$
62		fco	$⊢ ((.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \land G : ℕ ⟶ ℝ^{} \times ℝ^{}) \to ((.) \circ G) : ℕ ⟶ 𝒫 ℝ$
63	57 61 62	sylancr	$⊢ φ \to ((.) \circ G) : ℕ ⟶ 𝒫 ℝ$
64	63	ffnd	$⊢ φ \to ((.) \circ G) Fn ℕ$
65		fnima	$⊢ ((.) \circ G) Fn ℕ \to ((.) \circ G) [ℕ] = ran ((.) \circ G)$
66	64 65	syl	$⊢ φ \to ((.) \circ G) [ℕ] = ran ((.) \circ G)$
67		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
68	11	peano2nnd	$⊢ φ \to M + 1 \in ℕ$
69	68 67	eleqtrdi	$⊢ φ \to M + 1 \in ℤ_{\geq 1}$
70		uzsplit	$⊢ M + 1 \in ℤ_{\geq 1} \to ℤ_{\geq 1} = (1 \dots M + 1 - 1) \cup ℤ_{\geq (M + 1)}$
71	69 70	syl	$⊢ φ \to ℤ_{\geq 1} = (1 \dots M + 1 - 1) \cup ℤ_{\geq (M + 1)}$
72	67 71	syl5eq	$⊢ φ \to ℕ = (1 \dots M + 1 - 1) \cup ℤ_{\geq (M + 1)}$
73	11	nncnd	$⊢ φ \to M \in ℂ$
74		ax-1cn	$⊢ 1 \in ℂ$
75		pncan	$⊢ (M \in ℂ \land 1 \in ℂ) \to M + 1 - 1 = M$
76	73 74 75	sylancl	$⊢ φ \to M + 1 - 1 = M$
77	76	oveq2d	$⊢ φ \to (1 \dots M + 1 - 1) = (1 \dots M)$
78	77	uneq1d	$⊢ φ \to (1 \dots M + 1 - 1) \cup ℤ_{\geq (M + 1)} = (1 \dots M) \cup ℤ_{\geq (M + 1)}$
79	72 78	eqtrd	$⊢ φ \to ℕ = (1 \dots M) \cup ℤ_{\geq (M + 1)}$
80	79	imaeq2d	$⊢ φ \to ((.) \circ G) [ℕ] = ((.) \circ G) [(1 \dots M) \cup ℤ_{\geq (M + 1)}]$
81	66 80	eqtr3d	$⊢ φ \to ran ((.) \circ G) = ((.) \circ G) [(1 \dots M) \cup ℤ_{\geq (M + 1)}]$
82		imaundi	$⊢ ((.) \circ G) [(1 \dots M) \cup ℤ_{\geq (M + 1)}] = ((.) \circ G) [(1 \dots M)] \cup ((.) \circ G) [ℤ_{\geq (M + 1)}]$
83	81 82	eqtrdi	$⊢ φ \to ran ((.) \circ G) = ((.) \circ G) [(1 \dots M)] \cup ((.) \circ G) [ℤ_{\geq (M + 1)}]$
84	83	unieqd	$⊢ φ \to ⋃ ran ((.) \circ G) = ⋃ (((.) \circ G) [(1 \dots M)] \cup ((.) \circ G) [ℤ_{\geq (M + 1)}])$
85		uniun	$⊢ ⋃ (((.) \circ G) [(1 \dots M)] \cup ((.) \circ G) [ℤ_{\geq (M + 1)}]) = ⋃ ((.) \circ G) [(1 \dots M)] \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]$
86	84 85	eqtrdi	$⊢ φ \to ⋃ ran ((.) \circ G) = ⋃ ((.) \circ G) [(1 \dots M)] \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]$
87	13	uneq1i	$⊢ K \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}] = ⋃ ((.) \circ G) [(1 \dots M)] \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]$
88	86 87	eqtr4di	$⊢ φ \to ⋃ ran ((.) \circ G) = K \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]$
89	56 88	sseqtrrid	$⊢ φ \to ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}] \subseteq ⋃ ran ((.) \circ G)$
90	1 2 3 4 5 6 7 8 9 10	uniioombllem1	$⊢ φ \to sup (ran T ℝ^{*} <) \in ℝ$
91		ssid	$⊢ ⋃ ran ((.) \circ G) \subseteq ⋃ ran ((.) \circ G)$
92	9	ovollb	$⊢ (G : ℕ ⟶ \leq \cap ℝ^{2} \land ⋃ ran ((.) \circ G) \subseteq ⋃ ran ((.) \circ G)) \to {vol}^{} (⋃ ran ((.) \circ G)) \leq sup (ran T ℝ^{} <)$
93	7 91 92	sylancl	$⊢ φ \to {vol}^{} (⋃ ran ((.) \circ G)) \leq sup (ran T ℝ^{} <)$
94		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 ℝ$
95	20 90 93 94	syl3anc	$⊢ φ \to {vol}^{*} (⋃ ran ((.) \circ G)) \in ℝ$
96		ovolsscl	$⊢ (⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}] \subseteq ⋃ ran ((.) \circ G) \land ⋃ ran ((.) \circ G) \subseteq ℝ \land {vol}^{} (⋃ ran ((.) \circ G)) \in ℝ) \to {vol}^{} (⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]) \in ℝ$
97	89 20 95 96	syl3anc	$⊢ φ \to {vol}^{*} (⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]) \in ℝ$
98	49 97	readdcld	$⊢ φ \to {vol}^{} (K \cap A) + {vol}^{} (⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]) \in ℝ$
99		unss1	$⊢ K \cap A \subseteq K \to (K \cap A) \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}] \subseteq K \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]$
100	27 99	ax-mp	$⊢ (K \cap A) \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}] \subseteq K \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]$
101	100 88	sseqtrrid	$⊢ φ \to (K \cap A) \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}] \subseteq ⋃ ran ((.) \circ G)$
102		ovolsscl	$⊢ ((K \cap A) \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}] \subseteq ⋃ ran ((.) \circ G) \land ⋃ ran ((.) \circ G) \subseteq ℝ \land {vol}^{} (⋃ ran ((.) \circ G)) \in ℝ) \to {vol}^{} ((K \cap A) \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]) \in ℝ$
103	101 20 95 102	syl3anc	$⊢ φ \to {vol}^{*} ((K \cap A) \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]) \in ℝ$
104	8 88	sseqtrd	$⊢ φ \to E \subseteq K \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]$
105	104	ssrind	$⊢ φ \to E \cap A \subseteq (K \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]) \cap A$
106		indir	$⊢ (K \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]) \cap A = (K \cap A) \cup (⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}] \cap A)$
107		inss1	$⊢ ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}] \cap A \subseteq ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]$
108		unss2	$⊢ ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}] \cap A \subseteq ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}] \to (K \cap A) \cup (⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}] \cap A) \subseteq (K \cap A) \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]$
109	107 108	ax-mp	$⊢ (K \cap A) \cup (⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}] \cap A) \subseteq (K \cap A) \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]$
110	106 109	eqsstri	$⊢ (K \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]) \cap A \subseteq (K \cap A) \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]$
111	105 110	sstrdi	$⊢ φ \to E \cap A \subseteq (K \cap A) \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]$
112	101 20	sstrd	$⊢ φ \to (K \cap A) \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}] \subseteq ℝ$
113		ovolss	$⊢ (E \cap A \subseteq (K \cap A) \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}] \land (K \cap A) \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}] \subseteq ℝ) \to {vol}^{} (E \cap A) \leq {vol}^{} ((K \cap A) \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}])$
114	111 112 113	syl2anc	$⊢ φ \to {vol}^{} (E \cap A) \leq {vol}^{} ((K \cap A) \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}])$
115	28 46	sstrd	$⊢ φ \to K \cap A \subseteq ℝ$
116	89 20	sstrd	$⊢ φ \to ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}] \subseteq ℝ$
117		ovolun	$⊢ ((K \cap A \subseteq ℝ \land {vol}^{} (K \cap A) \in ℝ) \land (⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}] \subseteq ℝ \land {vol}^{} (⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]) \in ℝ)) \to {vol}^{} ((K \cap A) \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]) \leq {vol}^{} (K \cap A) + {vol}^{*} (⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}])$
118	115 49 116 97 117	syl22anc	$⊢ φ \to {vol}^{} ((K \cap A) \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]) \leq {vol}^{} (K \cap A) + {vol}^{*} (⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}])$
119	23 103 98 114 118	letrd	$⊢ φ \to {vol}^{} (E \cap A) \leq {vol}^{} (K \cap A) + {vol}^{*} (⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}])$
120		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
121		eqid	$⊢ (abs \circ -) \circ G = (abs \circ -) \circ G$
122	121 9	ovolsf	$⊢ G : ℕ ⟶ \leq \cap ℝ^{2} \to T : ℕ ⟶ [0, +∞)$
123	7 122	syl	$⊢ φ \to T : ℕ ⟶ [0, +∞)$
124	123 11	ffvelrnd	$⊢ φ \to T (M) \in [0, +∞)$
125	120 124	sselid	$⊢ φ \to T (M) \in ℝ$
126	90 125	resubcld	$⊢ φ \to sup (ran T ℝ^{*} <) - T (M) \in ℝ$
127	97	rexrd	$⊢ φ \to {vol}^{} (⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]) \in ℝ^{}$
128		id	$⊢ z \in ℕ \to z \in ℕ$
129		nnaddcl	$⊢ (z \in ℕ \land M \in ℕ) \to z + M \in ℕ$
130	128 11 129	syl2anr	$⊢ (φ \land z \in ℕ) \to z + M \in ℕ$
131	7	ffvelrnda	$⊢ (φ \land z + M \in ℕ) \to G (z + M) \in (\leq \cap ℝ^{2})$
132	130 131	syldan	$⊢ (φ \land z \in ℕ) \to G (z + M) \in (\leq \cap ℝ^{2})$
133	132	fmpttd	$⊢ φ \to (z \in ℕ ⟼ G (z + M)) : ℕ ⟶ \leq \cap ℝ^{2}$
134		eqid	$⊢ (abs \circ -) \circ (z \in ℕ ⟼ G (z + M)) = (abs \circ -) \circ (z \in ℕ ⟼ G (z + M))$
135		eqid	$⊢ seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ G (z + M)))) = seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ G (z + M))))$
136	134 135	ovolsf	$⊢ (z \in ℕ ⟼ G (z + M)) : ℕ ⟶ \leq \cap ℝ^{2} \to seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ G (z + M)))) : ℕ ⟶ [0, +∞)$
137	133 136	syl	$⊢ φ \to seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ G (z + M)))) : ℕ ⟶ [0, +∞)$
138	137	frnd	$⊢ φ \to ran seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ G (z + M)))) \subseteq [0, +∞)$
139		icossxr	$⊢ [0, +∞) \subseteq ℝ^{*}$
140	138 139	sstrdi	$⊢ φ \to ran seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ G (z + M)))) \subseteq ℝ^{*}$
141		supxrcl	$⊢ ran seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ G (z + M)))) \subseteq ℝ^{} \to sup (ran seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ G (z + M)))) ℝ^{} <) \in ℝ^{*}$
142	140 141	syl	$⊢ φ \to sup (ran seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ G (z + M)))) ℝ^{} <) \in ℝ^{}$
143	126	rexrd	$⊢ φ \to sup (ran T ℝ^{} <) - T (M) \in ℝ^{}$
144		1zzd	$⊢ (φ \land x \in ℤ_{\geq (M + 1)}) \to 1 \in ℤ$
145	11	nnzd	$⊢ φ \to M \in ℤ$
146	145	adantr	$⊢ (φ \land x \in ℤ_{\geq (M + 1)}) \to M \in ℤ$
147		addcom	$⊢ (M \in ℂ \land 1 \in ℂ) \to M + 1 = 1 + M$
148	73 74 147	sylancl	$⊢ φ \to M + 1 = 1 + M$
149	148	fveq2d	$⊢ φ \to ℤ_{\geq (M + 1)} = ℤ_{\geq (1 + M)}$
150	149	eleq2d	$⊢ φ \to (x \in ℤ_{\geq (M + 1)} \leftrightarrow x \in ℤ_{\geq (1 + M)})$
151	150	biimpa	$⊢ (φ \land x \in ℤ_{\geq (M + 1)}) \to x \in ℤ_{\geq (1 + M)}$
152		eluzsub	$⊢ (1 \in ℤ \land M \in ℤ \land x \in ℤ_{\geq (1 + M)}) \to x - M \in ℤ_{\geq 1}$
153	144 146 151 152	syl3anc	$⊢ (φ \land x \in ℤ_{\geq (M + 1)}) \to x - M \in ℤ_{\geq 1}$
154	153 67	eleqtrrdi	$⊢ (φ \land x \in ℤ_{\geq (M + 1)}) \to x - M \in ℕ$
155		eluzelz	$⊢ x \in ℤ_{\geq (M + 1)} \to x \in ℤ$
156	155	adantl	$⊢ (φ \land x \in ℤ_{\geq (M + 1)}) \to x \in ℤ$
157	156	zcnd	$⊢ (φ \land x \in ℤ_{\geq (M + 1)}) \to x \in ℂ$
158	73	adantr	$⊢ (φ \land x \in ℤ_{\geq (M + 1)}) \to M \in ℂ$
159	157 158	npcand	$⊢ (φ \land x \in ℤ_{\geq (M + 1)}) \to x - M + M = x$
160	159	eqcomd	$⊢ (φ \land x \in ℤ_{\geq (M + 1)}) \to x = x - M + M$
161		oveq1	$⊢ z = x - M \to z + M = x - M + M$
162	161	rspceeqv	$⊢ (x - M \in ℕ \land x = x - M + M) \to \exists z \in ℕ x = z + M$
163	154 160 162	syl2anc	$⊢ (φ \land x \in ℤ_{\geq (M + 1)}) \to \exists z \in ℕ x = z + M$
164		eqid	$⊢ (z \in ℕ ⟼ z + M) = (z \in ℕ ⟼ z + M)$
165	164	elrnmpt	$⊢ x \in V \to (x \in ran (z \in ℕ ⟼ z + M) \leftrightarrow \exists z \in ℕ x = z + M)$
166	165	elv	$⊢ x \in ran (z \in ℕ ⟼ z + M) \leftrightarrow \exists z \in ℕ x = z + M$
167	163 166	sylibr	$⊢ (φ \land x \in ℤ_{\geq (M + 1)}) \to x \in ran (z \in ℕ ⟼ z + M)$
168	167	ex	$⊢ φ \to (x \in ℤ_{\geq (M + 1)} \to x \in ran (z \in ℕ ⟼ z + M))$
169	168	ssrdv	$⊢ φ \to ℤ_{\geq (M + 1)} \subseteq ran (z \in ℕ ⟼ z + M)$
170		imass2	$⊢ ℤ_{\geq (M + 1)} \subseteq ran (z \in ℕ ⟼ z + M) \to G [ℤ_{\geq (M + 1)}] \subseteq G [ran (z \in ℕ ⟼ z + M)]$
171	169 170	syl	$⊢ φ \to G [ℤ_{\geq (M + 1)}] \subseteq G [ran (z \in ℕ ⟼ z + M)]$
172		rnco2	$⊢ ran (G \circ (z \in ℕ ⟼ z + M)) = G [ran (z \in ℕ ⟼ z + M)]$
173	7 130	cofmpt	$⊢ φ \to G \circ (z \in ℕ ⟼ z + M) = (z \in ℕ ⟼ G (z + M))$
174	173	rneqd	$⊢ φ \to ran (G \circ (z \in ℕ ⟼ z + M)) = ran (z \in ℕ ⟼ G (z + M))$
175	172 174	eqtr3id	$⊢ φ \to G [ran (z \in ℕ ⟼ z + M)] = ran (z \in ℕ ⟼ G (z + M))$
176	171 175	sseqtrd	$⊢ φ \to G [ℤ_{\geq (M + 1)}] \subseteq ran (z \in ℕ ⟼ G (z + M))$
177		imass2	$⊢ G [ℤ_{\geq (M + 1)}] \subseteq ran (z \in ℕ ⟼ G (z + M)) \to (.) [G [ℤ_{\geq (M + 1)}]] \subseteq (.) [ran (z \in ℕ ⟼ G (z + M))]$
178	176 177	syl	$⊢ φ \to (.) [G [ℤ_{\geq (M + 1)}]] \subseteq (.) [ran (z \in ℕ ⟼ G (z + M))]$
179		imaco	$⊢ ((.) \circ G) [ℤ_{\geq (M + 1)}] = (.) [G [ℤ_{\geq (M + 1)}]]$
180		rnco2	$⊢ ran ((.) \circ (z \in ℕ ⟼ G (z + M))) = (.) [ran (z \in ℕ ⟼ G (z + M))]$
181	178 179 180	3sstr4g	$⊢ φ \to ((.) \circ G) [ℤ_{\geq (M + 1)}] \subseteq ran ((.) \circ (z \in ℕ ⟼ G (z + M)))$
182	181	unissd	$⊢ φ \to ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}] \subseteq ⋃ ran ((.) \circ (z \in ℕ ⟼ G (z + M)))$
183	135	ovollb	$⊢ ((z \in ℕ ⟼ G (z + M)) : ℕ ⟶ \leq \cap ℝ^{2} \land ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}] \subseteq ⋃ ran ((.) \circ (z \in ℕ ⟼ G (z + M)))) \to {vol}^{} (⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]) \leq sup (ran seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ G (z + M)))) ℝ^{} <)$
184	133 182 183	syl2anc	$⊢ φ \to {vol}^{} (⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]) \leq sup (ran seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ G (z + M)))) ℝ^{} <)$
185	123	frnd	$⊢ φ \to ran T \subseteq [0, +∞)$
186	185 139	sstrdi	$⊢ φ \to ran T \subseteq ℝ^{*}$
187	9	fveq1i	$⊢ T (M + n) = seq 1 (+ ((abs \circ -) \circ G)) (M + n)$
188	11	nnred	$⊢ φ \to M \in ℝ$
189	188	ltp1d	$⊢ φ \to M < M + 1$
190		fzdisj	$⊢ M < M + 1 \to (1 \dots M) \cap (M + 1 \dots M + n) = \emptyset$
191	189 190	syl	$⊢ φ \to (1 \dots M) \cap (M + 1 \dots M + n) = \emptyset$
192	191	adantr	$⊢ (φ \land n \in ℕ) \to (1 \dots M) \cap (M + 1 \dots M + n) = \emptyset$
193		nnnn0	$⊢ n \in ℕ \to n \in ℕ_{0}$
194		nn0addge1	$⊢ (M \in ℝ \land n \in ℕ_{0}) \to M \leq M + n$
195	188 193 194	syl2an	$⊢ (φ \land n \in ℕ) \to M \leq M + n$
196	11	adantr	$⊢ (φ \land n \in ℕ) \to M \in ℕ$
197	196 67	eleqtrdi	$⊢ (φ \land n \in ℕ) \to M \in ℤ_{\geq 1}$
198		nnaddcl	$⊢ (M \in ℕ \land n \in ℕ) \to M + n \in ℕ$
199	11 198	sylan	$⊢ (φ \land n \in ℕ) \to M + n \in ℕ$
200	199	nnzd	$⊢ (φ \land n \in ℕ) \to M + n \in ℤ$
201		elfz5	$⊢ (M \in ℤ_{\geq 1} \land M + n \in ℤ) \to (M \in (1 \dots M + n) \leftrightarrow M \leq M + n)$
202	197 200 201	syl2anc	$⊢ (φ \land n \in ℕ) \to (M \in (1 \dots M + n) \leftrightarrow M \leq M + n)$
203	195 202	mpbird	$⊢ (φ \land n \in ℕ) \to M \in (1 \dots M + n)$
204		fzsplit	$⊢ M \in (1 \dots M + n) \to (1 \dots M + n) = (1 \dots M) \cup (M + 1 \dots M + n)$
205	203 204	syl	$⊢ (φ \land n \in ℕ) \to (1 \dots M + n) = (1 \dots M) \cup (M + 1 \dots M + n)$
206		fzfid	$⊢ (φ \land n \in ℕ) \to (1 \dots M + n) \in Fin$
207	7	adantr	$⊢ (φ \land n \in ℕ) \to G : ℕ ⟶ \leq \cap ℝ^{2}$
208		elfznn	$⊢ j \in (1 \dots M + n) \to j \in ℕ$
209		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)))$
210	207 208 209	syl2an	$⊢ ((φ \land n \in ℕ) \land j \in (1 \dots M + n)) \to (1^{st} (G (j)) \in ℝ \land 2^{nd} (G (j)) \in ℝ \land 1^{st} (G (j)) \leq 2^{nd} (G (j)))$
211	210	simp2d	$⊢ ((φ \land n \in ℕ) \land j \in (1 \dots M + n)) \to 2^{nd} (G (j)) \in ℝ$
212	210	simp1d	$⊢ ((φ \land n \in ℕ) \land j \in (1 \dots M + n)) \to 1^{st} (G (j)) \in ℝ$
213	211 212	resubcld	$⊢ ((φ \land n \in ℕ) \land j \in (1 \dots M + n)) \to 2^{nd} (G (j)) - 1^{st} (G (j)) \in ℝ$
214	213	recnd	$⊢ ((φ \land n \in ℕ) \land j \in (1 \dots M + n)) \to 2^{nd} (G (j)) - 1^{st} (G (j)) \in ℂ$
215	192 205 206 214	fsumsplit	$⊢ (φ \land n \in ℕ) \to \sum_{j = 1}^{M + n} (2^{nd} (G (j)) - 1^{st} (G (j))) = \sum_{j = 1}^{M} (2^{nd} (G (j)) - 1^{st} (G (j))) + \sum_{j = M + 1}^{M + n} (2^{nd} (G (j)) - 1^{st} (G (j)))$
216	121	ovolfsval	$⊢ (G : ℕ ⟶ \leq \cap ℝ^{2} \land j \in ℕ) \to ((abs \circ -) \circ G) (j) = 2^{nd} (G (j)) - 1^{st} (G (j))$
217	207 208 216	syl2an	$⊢ ((φ \land n \in ℕ) \land j \in (1 \dots M + n)) \to ((abs \circ -) \circ G) (j) = 2^{nd} (G (j)) - 1^{st} (G (j))$
218	199 67	eleqtrdi	$⊢ (φ \land n \in ℕ) \to M + n \in ℤ_{\geq 1}$
219	217 218 214	fsumser	$⊢ (φ \land n \in ℕ) \to \sum_{j = 1}^{M + n} (2^{nd} (G (j)) - 1^{st} (G (j))) = seq 1 (+ ((abs \circ -) \circ G)) (M + n)$
220	7	ad2antrr	$⊢ ((φ \land n \in ℕ) \land j \in (1 \dots M)) \to G : ℕ ⟶ \leq \cap ℝ^{2}$
221	32	adantl	$⊢ ((φ \land n \in ℕ) \land j \in (1 \dots M)) \to j \in ℕ$
222	220 221 216	syl2anc	$⊢ ((φ \land n \in ℕ) \land j \in (1 \dots M)) \to ((abs \circ -) \circ G) (j) = 2^{nd} (G (j)) - 1^{st} (G (j))$
223	7 32 209	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)))$
224	223	simp2d	$⊢ (φ \land j \in (1 \dots M)) \to 2^{nd} (G (j)) \in ℝ$
225	223	simp1d	$⊢ (φ \land j \in (1 \dots M)) \to 1^{st} (G (j)) \in ℝ$
226	224 225	resubcld	$⊢ (φ \land j \in (1 \dots M)) \to 2^{nd} (G (j)) - 1^{st} (G (j)) \in ℝ$
227	226	adantlr	$⊢ ((φ \land n \in ℕ) \land j \in (1 \dots M)) \to 2^{nd} (G (j)) - 1^{st} (G (j)) \in ℝ$
228	227	recnd	$⊢ ((φ \land n \in ℕ) \land j \in (1 \dots M)) \to 2^{nd} (G (j)) - 1^{st} (G (j)) \in ℂ$
229	222 197 228	fsumser	$⊢ (φ \land n \in ℕ) \to \sum_{j = 1}^{M} (2^{nd} (G (j)) - 1^{st} (G (j))) = seq 1 (+ ((abs \circ -) \circ G)) (M)$
230	9	fveq1i	$⊢ T (M) = seq 1 (+ ((abs \circ -) \circ G)) (M)$
231	229 230	eqtr4di	$⊢ (φ \land n \in ℕ) \to \sum_{j = 1}^{M} (2^{nd} (G (j)) - 1^{st} (G (j))) = T (M)$
232	196	nnzd	$⊢ (φ \land n \in ℕ) \to M \in ℤ$
233	232	peano2zd	$⊢ (φ \land n \in ℕ) \to M + 1 \in ℤ$
234	7	ad2antrr	$⊢ ((φ \land n \in ℕ) \land j \in (M + 1 \dots M + n)) \to G : ℕ ⟶ \leq \cap ℝ^{2}$
235	196	peano2nnd	$⊢ (φ \land n \in ℕ) \to M + 1 \in ℕ$
236		elfzuz	$⊢ j \in (M + 1 \dots M + n) \to j \in ℤ_{\geq (M + 1)}$
237		eluznn	$⊢ (M + 1 \in ℕ \land j \in ℤ_{\geq (M + 1)}) \to j \in ℕ$
238	235 236 237	syl2an	$⊢ ((φ \land n \in ℕ) \land j \in (M + 1 \dots M + n)) \to j \in ℕ$
239	234 238 209	syl2anc	$⊢ ((φ \land n \in ℕ) \land j \in (M + 1 \dots M + n)) \to (1^{st} (G (j)) \in ℝ \land 2^{nd} (G (j)) \in ℝ \land 1^{st} (G (j)) \leq 2^{nd} (G (j)))$
240	239	simp2d	$⊢ ((φ \land n \in ℕ) \land j \in (M + 1 \dots M + n)) \to 2^{nd} (G (j)) \in ℝ$
241	239	simp1d	$⊢ ((φ \land n \in ℕ) \land j \in (M + 1 \dots M + n)) \to 1^{st} (G (j)) \in ℝ$
242	240 241	resubcld	$⊢ ((φ \land n \in ℕ) \land j \in (M + 1 \dots M + n)) \to 2^{nd} (G (j)) - 1^{st} (G (j)) \in ℝ$
243	242	recnd	$⊢ ((φ \land n \in ℕ) \land j \in (M + 1 \dots M + n)) \to 2^{nd} (G (j)) - 1^{st} (G (j)) \in ℂ$
244		2fveq3	$⊢ j = k + M \to 2^{nd} (G (j)) = 2^{nd} (G (k + M))$
245		2fveq3	$⊢ j = k + M \to 1^{st} (G (j)) = 1^{st} (G (k + M))$
246	244 245	oveq12d	$⊢ j = k + M \to 2^{nd} (G (j)) - 1^{st} (G (j)) = 2^{nd} (G (k + M)) - 1^{st} (G (k + M))$
247	232 233 200 243 246	fsumshftm	$⊢ (φ \land n \in ℕ) \to \sum_{j = M + 1}^{M + n} (2^{nd} (G (j)) - 1^{st} (G (j))) = \sum_{k = M + 1 - M}^{M + n - M} (2^{nd} (G (k + M)) - 1^{st} (G (k + M)))$
248	196	nncnd	$⊢ (φ \land n \in ℕ) \to M \in ℂ$
249		pncan2	$⊢ (M \in ℂ \land 1 \in ℂ) \to M + 1 - M = 1$
250	248 74 249	sylancl	$⊢ (φ \land n \in ℕ) \to M + 1 - M = 1$
251		nncn	$⊢ n \in ℕ \to n \in ℂ$
252	251	adantl	$⊢ (φ \land n \in ℕ) \to n \in ℂ$
253	248 252	pncan2d	$⊢ (φ \land n \in ℕ) \to M + n - M = n$
254	250 253	oveq12d	$⊢ (φ \land n \in ℕ) \to (M + 1 - M \dots M + n - M) = (1 \dots n)$
255	254	sumeq1d	$⊢ (φ \land n \in ℕ) \to \sum_{k = M + 1 - M}^{M + n - M} (2^{nd} (G (k + M)) - 1^{st} (G (k + M))) = \sum_{k = 1}^{n} (2^{nd} (G (k + M)) - 1^{st} (G (k + M)))$
256	133	adantr	$⊢ (φ \land n \in ℕ) \to (z \in ℕ ⟼ G (z + M)) : ℕ ⟶ \leq \cap ℝ^{2}$
257		elfznn	$⊢ k \in (1 \dots n) \to k \in ℕ$
258	134	ovolfsval	$⊢ ((z \in ℕ ⟼ G (z + M)) : ℕ ⟶ \leq \cap ℝ^{2} \land k \in ℕ) \to ((abs \circ -) \circ (z \in ℕ ⟼ G (z + M))) (k) = 2^{nd} ((z \in ℕ ⟼ G (z + M)) (k)) - 1^{st} ((z \in ℕ ⟼ G (z + M)) (k))$
259	256 257 258	syl2an	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to ((abs \circ -) \circ (z \in ℕ ⟼ G (z + M))) (k) = 2^{nd} ((z \in ℕ ⟼ G (z + M)) (k)) - 1^{st} ((z \in ℕ ⟼ G (z + M)) (k))$
260	257	adantl	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to k \in ℕ$
261		fvoveq1	$⊢ z = k \to G (z + M) = G (k + M)$
262		eqid	$⊢ (z \in ℕ ⟼ G (z + M)) = (z \in ℕ ⟼ G (z + M))$
263		fvex	$⊢ G (k + M) \in V$
264	261 262 263	fvmpt	$⊢ k \in ℕ \to (z \in ℕ ⟼ G (z + M)) (k) = G (k + M)$
265	260 264	syl	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to (z \in ℕ ⟼ G (z + M)) (k) = G (k + M)$
266	265	fveq2d	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to 2^{nd} ((z \in ℕ ⟼ G (z + M)) (k)) = 2^{nd} (G (k + M))$
267	265	fveq2d	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to 1^{st} ((z \in ℕ ⟼ G (z + M)) (k)) = 1^{st} (G (k + M))$
268	266 267	oveq12d	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to 2^{nd} ((z \in ℕ ⟼ G (z + M)) (k)) - 1^{st} ((z \in ℕ ⟼ G (z + M)) (k)) = 2^{nd} (G (k + M)) - 1^{st} (G (k + M))$
269	259 268	eqtrd	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to ((abs \circ -) \circ (z \in ℕ ⟼ G (z + M))) (k) = 2^{nd} (G (k + M)) - 1^{st} (G (k + M))$
270		simpr	$⊢ (φ \land n \in ℕ) \to n \in ℕ$
271	270 67	eleqtrdi	$⊢ (φ \land n \in ℕ) \to n \in ℤ_{\geq 1}$
272	7	ad2antrr	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to G : ℕ ⟶ \leq \cap ℝ^{2}$
273		nnaddcl	$⊢ (k \in ℕ \land M \in ℕ) \to k + M \in ℕ$
274	257 196 273	syl2anr	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to k + M \in ℕ$
275		ovolfcl	$⊢ (G : ℕ ⟶ \leq \cap ℝ^{2} \land k + M \in ℕ) \to (1^{st} (G (k + M)) \in ℝ \land 2^{nd} (G (k + M)) \in ℝ \land 1^{st} (G (k + M)) \leq 2^{nd} (G (k + M)))$
276	272 274 275	syl2anc	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to (1^{st} (G (k + M)) \in ℝ \land 2^{nd} (G (k + M)) \in ℝ \land 1^{st} (G (k + M)) \leq 2^{nd} (G (k + M)))$
277	276	simp2d	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to 2^{nd} (G (k + M)) \in ℝ$
278	276	simp1d	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to 1^{st} (G (k + M)) \in ℝ$
279	277 278	resubcld	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to 2^{nd} (G (k + M)) - 1^{st} (G (k + M)) \in ℝ$
280	279	recnd	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to 2^{nd} (G (k + M)) - 1^{st} (G (k + M)) \in ℂ$
281	269 271 280	fsumser	$⊢ (φ \land n \in ℕ) \to \sum_{k = 1}^{n} (2^{nd} (G (k + M)) - 1^{st} (G (k + M))) = seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ G (z + M)))) (n)$
282	247 255 281	3eqtrd	$⊢ (φ \land n \in ℕ) \to \sum_{j = M + 1}^{M + n} (2^{nd} (G (j)) - 1^{st} (G (j))) = seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ G (z + M)))) (n)$
283	231 282	oveq12d	$⊢ (φ \land n \in ℕ) \to \sum_{j = 1}^{M} (2^{nd} (G (j)) - 1^{st} (G (j))) + \sum_{j = M + 1}^{M + n} (2^{nd} (G (j)) - 1^{st} (G (j))) = T (M) + seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ G (z + M)))) (n)$
284	215 219 283	3eqtr3d	$⊢ (φ \land n \in ℕ) \to seq 1 (+ ((abs \circ -) \circ G)) (M + n) = T (M) + seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ G (z + M)))) (n)$
285	187 284	syl5eq	$⊢ (φ \land n \in ℕ) \to T (M + n) = T (M) + seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ G (z + M)))) (n)$
286	123	ffnd	$⊢ φ \to T Fn ℕ$
287		fnfvelrn	$⊢ (T Fn ℕ \land M + n \in ℕ) \to T (M + n) \in ran T$
288	286 199 287	syl2an2r	$⊢ (φ \land n \in ℕ) \to T (M + n) \in ran T$
289	285 288	eqeltrrd	$⊢ (φ \land n \in ℕ) \to T (M) + seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ G (z + M)))) (n) \in ran T$
290		supxrub	$⊢ (ran T \subseteq ℝ^{} \land T (M) + seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ G (z + M)))) (n) \in ran T) \to T (M) + seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ G (z + M)))) (n) \leq sup (ran T ℝ^{} <)$
291	186 289 290	syl2an2r	$⊢ (φ \land n \in ℕ) \to T (M) + seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ G (z + M)))) (n) \leq sup (ran T ℝ^{*} <)$
292	125	adantr	$⊢ (φ \land n \in ℕ) \to T (M) \in ℝ$
293	137	ffvelrnda	$⊢ (φ \land n \in ℕ) \to seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ G (z + M)))) (n) \in [0, +∞)$
294	120 293	sselid	$⊢ (φ \land n \in ℕ) \to seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ G (z + M)))) (n) \in ℝ$
295	90	adantr	$⊢ (φ \land n \in ℕ) \to sup (ran T ℝ^{*} <) \in ℝ$
296	292 294 295	leaddsub2d	$⊢ (φ \land n \in ℕ) \to (T (M) + seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ G (z + M)))) (n) \leq sup (ran T ℝ^{} <) \leftrightarrow seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ G (z + M)))) (n) \leq sup (ran T ℝ^{} <) - T (M))$
297	291 296	mpbid	$⊢ (φ \land n \in ℕ) \to seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ G (z + M)))) (n) \leq sup (ran T ℝ^{*} <) - T (M)$
298	297	ralrimiva	$⊢ φ \to \forall n \in ℕ seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ G (z + M)))) (n) \leq sup (ran T ℝ^{*} <) - T (M)$
299	137	ffnd	$⊢ φ \to seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ G (z + M)))) Fn ℕ$
300		breq1	$⊢ x = seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ G (z + M)))) (n) \to (x \leq sup (ran T ℝ^{} <) - T (M) \leftrightarrow seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ G (z + M)))) (n) \leq sup (ran T ℝ^{} <) - T (M))$
301	300	ralrn	$⊢ seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ G (z + M)))) Fn ℕ \to (\forall x \in ran seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ G (z + M)))) x \leq sup (ran T ℝ^{} <) - T (M) \leftrightarrow \forall n \in ℕ seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ G (z + M)))) (n) \leq sup (ran T ℝ^{} <) - T (M))$
302	299 301	syl	$⊢ φ \to (\forall x \in ran seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ G (z + M)))) x \leq sup (ran T ℝ^{} <) - T (M) \leftrightarrow \forall n \in ℕ seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ G (z + M)))) (n) \leq sup (ran T ℝ^{} <) - T (M))$
303	298 302	mpbird	$⊢ φ \to \forall x \in ran seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ G (z + M)))) x \leq sup (ran T ℝ^{*} <) - T (M)$
304		supxrleub	$⊢ (ran seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ G (z + M)))) \subseteq ℝ^{} \land sup (ran T ℝ^{} <) - T (M) \in ℝ^{}) \to (sup (ran seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ G (z + M)))) ℝ^{} <) \leq sup (ran T ℝ^{} <) - T (M) \leftrightarrow \forall x \in ran seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ G (z + M)))) x \leq sup (ran T ℝ^{} <) - T (M))$
305	140 143 304	syl2anc	$⊢ φ \to (sup (ran seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ G (z + M)))) ℝ^{} <) \leq sup (ran T ℝ^{} <) - T (M) \leftrightarrow \forall x \in ran seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ G (z + M)))) x \leq sup (ran T ℝ^{*} <) - T (M))$
306	303 305	mpbird	$⊢ φ \to sup (ran seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ G (z + M)))) ℝ^{} <) \leq sup (ran T ℝ^{} <) - T (M)$
307	127 142 143 184 306	xrletrd	$⊢ φ \to {vol}^{} (⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]) \leq sup (ran T ℝ^{} <) - T (M)$
308	125 90 50	absdifltd	$⊢ φ \to (\|T (M) - sup (ran T ℝ^{} <)\| < C \leftrightarrow (sup (ran T ℝ^{} <) - C < T (M) \land T (M) < sup (ran T ℝ^{*} <) + C))$
309	12 308	mpbid	$⊢ φ \to (sup (ran T ℝ^{} <) - C < T (M) \land T (M) < sup (ran T ℝ^{} <) + C)$
310	309	simpld	$⊢ φ \to sup (ran T ℝ^{*} <) - C < T (M)$
311	90 50 125 310	ltsub23d	$⊢ φ \to sup (ran T ℝ^{*} <) - T (M) < C$
312	97 126 50 307 311	lelttrd	$⊢ φ \to {vol}^{*} (⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]) < C$
313	97 50 49 312	ltadd2dd	$⊢ φ \to {vol}^{} (K \cap A) + {vol}^{} (⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]) < {vol}^{*} (K \cap A) + C$
314	23 98 51 119 313	lelttrd	$⊢ φ \to {vol}^{} (E \cap A) < {vol}^{} (K \cap A) + C$
315	54 97	readdcld	$⊢ φ \to {vol}^{} (K ∖ A) + {vol}^{} (⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]) \in ℝ$
316		difss	$⊢ K ∖ A \subseteq K$
317		unss1	$⊢ K ∖ A \subseteq K \to (K ∖ A) \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}] \subseteq K \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]$
318	316 317	ax-mp	$⊢ (K ∖ A) \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}] \subseteq K \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]$
319	318 88	sseqtrrid	$⊢ φ \to (K ∖ A) \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}] \subseteq ⋃ ran ((.) \circ G)$
320		ovolsscl	$⊢ ((K ∖ A) \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}] \subseteq ⋃ ran ((.) \circ G) \land ⋃ ran ((.) \circ G) \subseteq ℝ \land {vol}^{} (⋃ ran ((.) \circ G)) \in ℝ) \to {vol}^{} ((K ∖ A) \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]) \in ℝ$
321	319 20 95 320	syl3anc	$⊢ φ \to {vol}^{*} ((K ∖ A) \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]) \in ℝ$
322	104	ssdifd	$⊢ φ \to E ∖ A \subseteq (K \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]) ∖ A$
323		difundir	$⊢ (K \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]) ∖ A = (K ∖ A) \cup (⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}] ∖ A)$
324		difss	$⊢ ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}] ∖ A \subseteq ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]$
325		unss2	$⊢ ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}] ∖ A \subseteq ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}] \to (K ∖ A) \cup (⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}] ∖ A) \subseteq (K ∖ A) \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]$
326	324 325	ax-mp	$⊢ (K ∖ A) \cup (⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}] ∖ A) \subseteq (K ∖ A) \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]$
327	323 326	eqsstri	$⊢ (K \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]) ∖ A \subseteq (K ∖ A) \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]$
328	322 327	sstrdi	$⊢ φ \to E ∖ A \subseteq (K ∖ A) \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]$
329	319 20	sstrd	$⊢ φ \to (K ∖ A) \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}] \subseteq ℝ$
330		ovolss	$⊢ (E ∖ A \subseteq (K ∖ A) \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}] \land (K ∖ A) \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}] \subseteq ℝ) \to {vol}^{} (E ∖ A) \leq {vol}^{} ((K ∖ A) \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}])$
331	328 329 330	syl2anc	$⊢ φ \to {vol}^{} (E ∖ A) \leq {vol}^{} ((K ∖ A) \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}])$
332	52 46	sstrd	$⊢ φ \to K ∖ A \subseteq ℝ$
333		ovolun	$⊢ ((K ∖ A \subseteq ℝ \land {vol}^{} (K ∖ A) \in ℝ) \land (⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}] \subseteq ℝ \land {vol}^{} (⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]) \in ℝ)) \to {vol}^{} ((K ∖ A) \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]) \leq {vol}^{} (K ∖ A) + {vol}^{*} (⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}])$
334	332 54 116 97 333	syl22anc	$⊢ φ \to {vol}^{} ((K ∖ A) \cup ⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]) \leq {vol}^{} (K ∖ A) + {vol}^{*} (⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}])$
335	26 321 315 331 334	letrd	$⊢ φ \to {vol}^{} (E ∖ A) \leq {vol}^{} (K ∖ A) + {vol}^{*} (⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}])$
336	97 50 54 312	ltadd2dd	$⊢ φ \to {vol}^{} (K ∖ A) + {vol}^{} (⋃ ((.) \circ G) [ℤ_{\geq (M + 1)}]) < {vol}^{*} (K ∖ A) + C$
337	26 315 55 335 336	lelttrd	$⊢ φ \to {vol}^{} (E ∖ A) < {vol}^{} (K ∖ A) + C$
338	23 26 51 55 314 337	lt2addd	$⊢ φ \to {vol}^{} (E \cap A) + {vol}^{} (E ∖ A) < {vol}^{} (K \cap A) + C + {vol}^{} (K ∖ A) + C$
339	49	recnd	$⊢ φ \to {vol}^{*} (K \cap A) \in ℂ$
340	50	recnd	$⊢ φ \to C \in ℂ$
341	54	recnd	$⊢ φ \to {vol}^{*} (K ∖ A) \in ℂ$
342	339 340 341 340	add4d	$⊢ φ \to {vol}^{} (K \cap A) + C + {vol}^{} (K ∖ A) + C = {vol}^{} (K \cap A) + {vol}^{} (K ∖ A) + C + C$
343	338 342	breqtrd	$⊢ φ \to {vol}^{} (E \cap A) + {vol}^{} (E ∖ A) < {vol}^{} (K \cap A) + {vol}^{} (K ∖ A) + C + C$

Metamath Proof Explorer

Theorem uniioombllem3

Proof