ovolunlem1a

	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	ovolunlem1a	$⊢ (φ \land k \in ℕ) \to U (k) \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		elovolmlem	$⊢ G \in ({(\leq \cap ℝ^{2})}^{ℕ}) \leftrightarrow G : ℕ ⟶ \leq \cap ℝ^{2}$
15	10 14	sylib	$⊢ φ \to G : ℕ ⟶ \leq \cap ℝ^{2}$
16	15	adantr	$⊢ (φ \land n \in ℕ) \to G : ℕ ⟶ \leq \cap ℝ^{2}$
17	16	ffvelrnda	$⊢ ((φ \land n \in ℕ) \land \frac{n}{2} \in ℕ) \to G (\frac{n}{2}) \in (\leq \cap ℝ^{2})$
18		nneo	$⊢ n \in ℕ \to (\frac{n}{2} \in ℕ \leftrightarrow \neg \frac{n + 1}{2} \in ℕ)$
19	18	adantl	$⊢ (φ \land n \in ℕ) \to (\frac{n}{2} \in ℕ \leftrightarrow \neg \frac{n + 1}{2} \in ℕ)$
20	19	con2bid	$⊢ (φ \land n \in ℕ) \to (\frac{n + 1}{2} \in ℕ \leftrightarrow \neg \frac{n}{2} \in ℕ)$
21	20	biimpar	$⊢ ((φ \land n \in ℕ) \land \neg \frac{n}{2} \in ℕ) \to \frac{n + 1}{2} \in ℕ$
22		elovolmlem	$⊢ F \in ({(\leq \cap ℝ^{2})}^{ℕ}) \leftrightarrow F : ℕ ⟶ \leq \cap ℝ^{2}$
23	7 22	sylib	$⊢ φ \to F : ℕ ⟶ \leq \cap ℝ^{2}$
24	23	adantr	$⊢ (φ \land n \in ℕ) \to F : ℕ ⟶ \leq \cap ℝ^{2}$
25	24	ffvelrnda	$⊢ ((φ \land n \in ℕ) \land \frac{n + 1}{2} \in ℕ) \to F (\frac{n + 1}{2}) \in (\leq \cap ℝ^{2})$
26	21 25	syldan	$⊢ ((φ \land n \in ℕ) \land \neg \frac{n}{2} \in ℕ) \to F (\frac{n + 1}{2}) \in (\leq \cap ℝ^{2})$
27	17 26	ifclda	$⊢ (φ \land n \in ℕ) \to if (\frac{n}{2} \in ℕ, G (\frac{n}{2}), F (\frac{n + 1}{2})) \in (\leq \cap ℝ^{2})$
28	27 13	fmptd	$⊢ φ \to H : ℕ ⟶ \leq \cap ℝ^{2}$
29		eqid	$⊢ (abs \circ -) \circ H = (abs \circ -) \circ H$
30	29 6	ovolsf	$⊢ H : ℕ ⟶ \leq \cap ℝ^{2} \to U : ℕ ⟶ [0, +∞)$
31	28 30	syl	$⊢ φ \to U : ℕ ⟶ [0, +∞)$
32		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
33		fss	$⊢ (U : ℕ ⟶ [0, +∞) \land [0, +∞) \subseteq ℝ) \to U : ℕ ⟶ ℝ$
34	31 32 33	sylancl	$⊢ φ \to U : ℕ ⟶ ℝ$
35	34	ffvelrnda	$⊢ (φ \land k \in ℕ) \to U (k) \in ℝ$
36		2nn	$⊢ 2 \in ℕ$
37		peano2nn	$⊢ k \in ℕ \to k + 1 \in ℕ$
38	37	adantl	$⊢ (φ \land k \in ℕ) \to k + 1 \in ℕ$
39	38	nnred	$⊢ (φ \land k \in ℕ) \to k + 1 \in ℝ$
40	39	rehalfcld	$⊢ (φ \land k \in ℕ) \to \frac{k + 1}{2} \in ℝ$
41	40	flcld	$⊢ (φ \land k \in ℕ) \to ⌊\frac{k + 1}{2}⌋ \in ℤ$
42		ax-1cn	$⊢ 1 \in ℂ$
43	42	2timesi	$⊢ 2 \cdot 1 = 1 + 1$
44		nnge1	$⊢ k \in ℕ \to 1 \leq k$
45	44	adantl	$⊢ (φ \land k \in ℕ) \to 1 \leq k$
46		nnre	$⊢ k \in ℕ \to k \in ℝ$
47	46	adantl	$⊢ (φ \land k \in ℕ) \to k \in ℝ$
48		1re	$⊢ 1 \in ℝ$
49		leadd1	$⊢ (1 \in ℝ \land k \in ℝ \land 1 \in ℝ) \to (1 \leq k \leftrightarrow 1 + 1 \leq k + 1)$
50	48 48 49	mp3an13	$⊢ k \in ℝ \to (1 \leq k \leftrightarrow 1 + 1 \leq k + 1)$
51	47 50	syl	$⊢ (φ \land k \in ℕ) \to (1 \leq k \leftrightarrow 1 + 1 \leq k + 1)$
52	45 51	mpbid	$⊢ (φ \land k \in ℕ) \to 1 + 1 \leq k + 1$
53	43 52	eqbrtrid	$⊢ (φ \land k \in ℕ) \to 2 \cdot 1 \leq k + 1$
54		2re	$⊢ 2 \in ℝ$
55		2pos	$⊢ 0 < 2$
56	54 55	pm3.2i	$⊢ (2 \in ℝ \land 0 < 2)$
57		lemuldiv2	$⊢ (1 \in ℝ \land k + 1 \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (2 \cdot 1 \leq k + 1 \leftrightarrow 1 \leq \frac{k + 1}{2})$
58	48 56 57	mp3an13	$⊢ k + 1 \in ℝ \to (2 \cdot 1 \leq k + 1 \leftrightarrow 1 \leq \frac{k + 1}{2})$
59	39 58	syl	$⊢ (φ \land k \in ℕ) \to (2 \cdot 1 \leq k + 1 \leftrightarrow 1 \leq \frac{k + 1}{2})$
60	53 59	mpbid	$⊢ (φ \land k \in ℕ) \to 1 \leq \frac{k + 1}{2}$
61		1z	$⊢ 1 \in ℤ$
62		flge	$⊢ (\frac{k + 1}{2} \in ℝ \land 1 \in ℤ) \to (1 \leq \frac{k + 1}{2} \leftrightarrow 1 \leq ⌊\frac{k + 1}{2}⌋)$
63	40 61 62	sylancl	$⊢ (φ \land k \in ℕ) \to (1 \leq \frac{k + 1}{2} \leftrightarrow 1 \leq ⌊\frac{k + 1}{2}⌋)$
64	60 63	mpbid	$⊢ (φ \land k \in ℕ) \to 1 \leq ⌊\frac{k + 1}{2}⌋$
65		elnnz1	$⊢ ⌊\frac{k + 1}{2}⌋ \in ℕ \leftrightarrow (⌊\frac{k + 1}{2}⌋ \in ℤ \land 1 \leq ⌊\frac{k + 1}{2}⌋)$
66	41 64 65	sylanbrc	$⊢ (φ \land k \in ℕ) \to ⌊\frac{k + 1}{2}⌋ \in ℕ$
67		nnmulcl	$⊢ (2 \in ℕ \land ⌊\frac{k + 1}{2}⌋ \in ℕ) \to 2 ⌊\frac{k + 1}{2}⌋ \in ℕ$
68	36 66 67	sylancr	$⊢ (φ \land k \in ℕ) \to 2 ⌊\frac{k + 1}{2}⌋ \in ℕ$
69	34	ffvelrnda	$⊢ (φ \land 2 ⌊\frac{k + 1}{2}⌋ \in ℕ) \to U (2 ⌊\frac{k + 1}{2}⌋) \in ℝ$
70	68 69	syldan	$⊢ (φ \land k \in ℕ) \to U (2 ⌊\frac{k + 1}{2}⌋) \in ℝ$
71	1	simprd	$⊢ φ \to {vol}^{*} (A) \in ℝ$
72	2	simprd	$⊢ φ \to {vol}^{*} (B) \in ℝ$
73	71 72	readdcld	$⊢ φ \to {vol}^{} (A) + {vol}^{} (B) \in ℝ$
74	3	rpred	$⊢ φ \to C \in ℝ$
75	73 74	readdcld	$⊢ φ \to {vol}^{} (A) + {vol}^{} (B) + C \in ℝ$
76	75	adantr	$⊢ (φ \land k \in ℕ) \to {vol}^{} (A) + {vol}^{} (B) + C \in ℝ$
77		simpr	$⊢ (φ \land k \in ℕ) \to k \in ℕ$
78		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
79	77 78	eleqtrdi	$⊢ (φ \land k \in ℕ) \to k \in ℤ_{\geq 1}$
80		nnz	$⊢ k \in ℕ \to k \in ℤ$
81	80	adantl	$⊢ (φ \land k \in ℕ) \to k \in ℤ$
82		flhalf	$⊢ k \in ℤ \to k \leq 2 ⌊\frac{k + 1}{2}⌋$
83	81 82	syl	$⊢ (φ \land k \in ℕ) \to k \leq 2 ⌊\frac{k + 1}{2}⌋$
84		nnz	$⊢ 2 ⌊\frac{k + 1}{2}⌋ \in ℕ \to 2 ⌊\frac{k + 1}{2}⌋ \in ℤ$
85		eluz	$⊢ (k \in ℤ \land 2 ⌊\frac{k + 1}{2}⌋ \in ℤ) \to (2 ⌊\frac{k + 1}{2}⌋ \in ℤ_{\geq k} \leftrightarrow k \leq 2 ⌊\frac{k + 1}{2}⌋)$
86	80 84 85	syl2an	$⊢ (k \in ℕ \land 2 ⌊\frac{k + 1}{2}⌋ \in ℕ) \to (2 ⌊\frac{k + 1}{2}⌋ \in ℤ_{\geq k} \leftrightarrow k \leq 2 ⌊\frac{k + 1}{2}⌋)$
87	77 68 86	syl2anc	$⊢ (φ \land k \in ℕ) \to (2 ⌊\frac{k + 1}{2}⌋ \in ℤ_{\geq k} \leftrightarrow k \leq 2 ⌊\frac{k + 1}{2}⌋)$
88	83 87	mpbird	$⊢ (φ \land k \in ℕ) \to 2 ⌊\frac{k + 1}{2}⌋ \in ℤ_{\geq k}$
89		elfznn	$⊢ j \in (1 \dots 2 ⌊\frac{k + 1}{2}⌋) \to j \in ℕ$
90	29	ovolfsf	$⊢ H : ℕ ⟶ \leq \cap ℝ^{2} \to ((abs \circ -) \circ H) : ℕ ⟶ [0, +∞)$
91	28 90	syl	$⊢ φ \to ((abs \circ -) \circ H) : ℕ ⟶ [0, +∞)$
92	91	adantr	$⊢ (φ \land k \in ℕ) \to ((abs \circ -) \circ H) : ℕ ⟶ [0, +∞)$
93	92	ffvelrnda	$⊢ ((φ \land k \in ℕ) \land j \in ℕ) \to ((abs \circ -) \circ H) (j) \in [0, +∞)$
94		elrege0	$⊢ ((abs \circ -) \circ H) (j) \in [0, +∞) \leftrightarrow (((abs \circ -) \circ H) (j) \in ℝ \land 0 \leq ((abs \circ -) \circ H) (j))$
95	93 94	sylib	$⊢ ((φ \land k \in ℕ) \land j \in ℕ) \to (((abs \circ -) \circ H) (j) \in ℝ \land 0 \leq ((abs \circ -) \circ H) (j))$
96	95	simpld	$⊢ ((φ \land k \in ℕ) \land j \in ℕ) \to ((abs \circ -) \circ H) (j) \in ℝ$
97	89 96	sylan2	$⊢ ((φ \land k \in ℕ) \land j \in (1 \dots 2 ⌊\frac{k + 1}{2}⌋)) \to ((abs \circ -) \circ H) (j) \in ℝ$
98		elfzuz	$⊢ j \in (k + 1 \dots 2 ⌊\frac{k + 1}{2}⌋) \to j \in ℤ_{\geq (k + 1)}$
99		eluznn	$⊢ (k + 1 \in ℕ \land j \in ℤ_{\geq (k + 1)}) \to j \in ℕ$
100	38 98 99	syl2an	$⊢ ((φ \land k \in ℕ) \land j \in (k + 1 \dots 2 ⌊\frac{k + 1}{2}⌋)) \to j \in ℕ$
101	95	simprd	$⊢ ((φ \land k \in ℕ) \land j \in ℕ) \to 0 \leq ((abs \circ -) \circ H) (j)$
102	100 101	syldan	$⊢ ((φ \land k \in ℕ) \land j \in (k + 1 \dots 2 ⌊\frac{k + 1}{2}⌋)) \to 0 \leq ((abs \circ -) \circ H) (j)$
103	79 88 97 102	sermono	$⊢ (φ \land k \in ℕ) \to seq 1 (+ ((abs \circ -) \circ H)) (k) \leq seq 1 (+ ((abs \circ -) \circ H)) (2 ⌊\frac{k + 1}{2}⌋)$
104	6	fveq1i	$⊢ U (k) = seq 1 (+ ((abs \circ -) \circ H)) (k)$
105	6	fveq1i	$⊢ U (2 ⌊\frac{k + 1}{2}⌋) = seq 1 (+ ((abs \circ -) \circ H)) (2 ⌊\frac{k + 1}{2}⌋)$
106	103 104 105	3brtr4g	$⊢ (φ \land k \in ℕ) \to U (k) \leq U (2 ⌊\frac{k + 1}{2}⌋)$
107		eqid	$⊢ (abs \circ -) \circ F = (abs \circ -) \circ F$
108	107 4	ovolsf	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to S : ℕ ⟶ [0, +∞)$
109	23 108	syl	$⊢ φ \to S : ℕ ⟶ [0, +∞)$
110	109	frnd	$⊢ φ \to ran S \subseteq [0, +∞)$
111	110 32	sstrdi	$⊢ φ \to ran S \subseteq ℝ$
112	111	adantr	$⊢ (φ \land k \in ℕ) \to ran S \subseteq ℝ$
113	109	ffnd	$⊢ φ \to S Fn ℕ$
114		fnfvelrn	$⊢ (S Fn ℕ \land ⌊\frac{k + 1}{2}⌋ \in ℕ) \to S (⌊\frac{k + 1}{2}⌋) \in ran S$
115	113 66 114	syl2an2r	$⊢ (φ \land k \in ℕ) \to S (⌊\frac{k + 1}{2}⌋) \in ran S$
116	112 115	sseldd	$⊢ (φ \land k \in ℕ) \to S (⌊\frac{k + 1}{2}⌋) \in ℝ$
117		eqid	$⊢ (abs \circ -) \circ G = (abs \circ -) \circ G$
118	117 5	ovolsf	$⊢ G : ℕ ⟶ \leq \cap ℝ^{2} \to T : ℕ ⟶ [0, +∞)$
119	15 118	syl	$⊢ φ \to T : ℕ ⟶ [0, +∞)$
120	119	frnd	$⊢ φ \to ran T \subseteq [0, +∞)$
121	120 32	sstrdi	$⊢ φ \to ran T \subseteq ℝ$
122	121	adantr	$⊢ (φ \land k \in ℕ) \to ran T \subseteq ℝ$
123	119	ffnd	$⊢ φ \to T Fn ℕ$
124		fnfvelrn	$⊢ (T Fn ℕ \land ⌊\frac{k + 1}{2}⌋ \in ℕ) \to T (⌊\frac{k + 1}{2}⌋) \in ran T$
125	123 66 124	syl2an2r	$⊢ (φ \land k \in ℕ) \to T (⌊\frac{k + 1}{2}⌋) \in ran T$
126	122 125	sseldd	$⊢ (φ \land k \in ℕ) \to T (⌊\frac{k + 1}{2}⌋) \in ℝ$
127	74	rehalfcld	$⊢ φ \to \frac{C}{2} \in ℝ$
128	71 127	readdcld	$⊢ φ \to {vol}^{*} (A) + (\frac{C}{2}) \in ℝ$
129	128	adantr	$⊢ (φ \land k \in ℕ) \to {vol}^{*} (A) + (\frac{C}{2}) \in ℝ$
130	72 127	readdcld	$⊢ φ \to {vol}^{*} (B) + (\frac{C}{2}) \in ℝ$
131	130	adantr	$⊢ (φ \land k \in ℕ) \to {vol}^{*} (B) + (\frac{C}{2}) \in ℝ$
132		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
133	111 132	sstrdi	$⊢ φ \to ran S \subseteq ℝ^{*}$
134		supxrcl	$⊢ ran S \subseteq ℝ^{} \to sup (ran S ℝ^{} <) \in ℝ^{*}$
135	133 134	syl	$⊢ φ \to sup (ran S ℝ^{} <) \in ℝ^{}$
136		1nn	$⊢ 1 \in ℕ$
137	109	fdmd	$⊢ φ \to dom S = ℕ$
138	136 137	eleqtrrid	$⊢ φ \to 1 \in dom S$
139	138	ne0d	$⊢ φ \to dom S \neq \emptyset$
140		dm0rn0	$⊢ dom S = \emptyset \leftrightarrow ran S = \emptyset$
141	140	necon3bii	$⊢ dom S \neq \emptyset \leftrightarrow ran S \neq \emptyset$
142	139 141	sylib	$⊢ φ \to ran S \neq \emptyset$
143		supxrgtmnf	$⊢ (ran S \subseteq ℝ \land ran S \neq \emptyset) \to −∞ < sup (ran S ℝ^{*} <)$
144	111 142 143	syl2anc	$⊢ φ \to −∞ < sup (ran S ℝ^{*} <)$
145		xrre	$⊢ ((sup (ran S ℝ^{} <) \in ℝ^{} \land {vol}^{} (A) + (\frac{C}{2}) \in ℝ) \land (−∞ < sup (ran S ℝ^{} <) \land sup (ran S ℝ^{} <) \leq {vol}^{} (A) + (\frac{C}{2}))) \to sup (ran S ℝ^{*} <) \in ℝ$
146	135 128 144 9 145	syl22anc	$⊢ φ \to sup (ran S ℝ^{*} <) \in ℝ$
147	146	adantr	$⊢ (φ \land k \in ℕ) \to sup (ran S ℝ^{*} <) \in ℝ$
148		supxrub	$⊢ (ran S \subseteq ℝ^{} \land S (⌊\frac{k + 1}{2}⌋) \in ran S) \to S (⌊\frac{k + 1}{2}⌋) \leq sup (ran S ℝ^{} <)$
149	133 115 148	syl2an2r	$⊢ (φ \land k \in ℕ) \to S (⌊\frac{k + 1}{2}⌋) \leq sup (ran S ℝ^{*} <)$
150	9	adantr	$⊢ (φ \land k \in ℕ) \to sup (ran S ℝ^{} <) \leq {vol}^{} (A) + (\frac{C}{2})$
151	116 147 129 149 150	letrd	$⊢ (φ \land k \in ℕ) \to S (⌊\frac{k + 1}{2}⌋) \leq {vol}^{*} (A) + (\frac{C}{2})$
152	121 132	sstrdi	$⊢ φ \to ran T \subseteq ℝ^{*}$
153		supxrcl	$⊢ ran T \subseteq ℝ^{} \to sup (ran T ℝ^{} <) \in ℝ^{*}$
154	152 153	syl	$⊢ φ \to sup (ran T ℝ^{} <) \in ℝ^{}$
155	119	fdmd	$⊢ φ \to dom T = ℕ$
156	136 155	eleqtrrid	$⊢ φ \to 1 \in dom T$
157	156	ne0d	$⊢ φ \to dom T \neq \emptyset$
158		dm0rn0	$⊢ dom T = \emptyset \leftrightarrow ran T = \emptyset$
159	158	necon3bii	$⊢ dom T \neq \emptyset \leftrightarrow ran T \neq \emptyset$
160	157 159	sylib	$⊢ φ \to ran T \neq \emptyset$
161		supxrgtmnf	$⊢ (ran T \subseteq ℝ \land ran T \neq \emptyset) \to −∞ < sup (ran T ℝ^{*} <)$
162	121 160 161	syl2anc	$⊢ φ \to −∞ < sup (ran T ℝ^{*} <)$
163		xrre	$⊢ ((sup (ran T ℝ^{} <) \in ℝ^{} \land {vol}^{} (B) + (\frac{C}{2}) \in ℝ) \land (−∞ < sup (ran T ℝ^{} <) \land sup (ran T ℝ^{} <) \leq {vol}^{} (B) + (\frac{C}{2}))) \to sup (ran T ℝ^{*} <) \in ℝ$
164	154 130 162 12 163	syl22anc	$⊢ φ \to sup (ran T ℝ^{*} <) \in ℝ$
165	164	adantr	$⊢ (φ \land k \in ℕ) \to sup (ran T ℝ^{*} <) \in ℝ$
166		supxrub	$⊢ (ran T \subseteq ℝ^{} \land T (⌊\frac{k + 1}{2}⌋) \in ran T) \to T (⌊\frac{k + 1}{2}⌋) \leq sup (ran T ℝ^{} <)$
167	152 125 166	syl2an2r	$⊢ (φ \land k \in ℕ) \to T (⌊\frac{k + 1}{2}⌋) \leq sup (ran T ℝ^{*} <)$
168	12	adantr	$⊢ (φ \land k \in ℕ) \to sup (ran T ℝ^{} <) \leq {vol}^{} (B) + (\frac{C}{2})$
169	126 165 131 167 168	letrd	$⊢ (φ \land k \in ℕ) \to T (⌊\frac{k + 1}{2}⌋) \leq {vol}^{*} (B) + (\frac{C}{2})$
170	116 126 129 131 151 169	le2addd	$⊢ (φ \land k \in ℕ) \to S (⌊\frac{k + 1}{2}⌋) + T (⌊\frac{k + 1}{2}⌋) \leq {vol}^{} (A) + (\frac{C}{2}) + {vol}^{} (B) + (\frac{C}{2})$
171		oveq2	$⊢ z = 1 \to 2 z = 2 \cdot 1$
172	171	fveq2d	$⊢ z = 1 \to U (2 z) = U (2 \cdot 1)$
173		fveq2	$⊢ z = 1 \to S (z) = S (1)$
174		fveq2	$⊢ z = 1 \to T (z) = T (1)$
175	173 174	oveq12d	$⊢ z = 1 \to S (z) + T (z) = S (1) + T (1)$
176	172 175	eqeq12d	$⊢ z = 1 \to (U (2 z) = S (z) + T (z) \leftrightarrow U (2 \cdot 1) = S (1) + T (1))$
177	176	imbi2d	$⊢ z = 1 \to ((φ \to U (2 z) = S (z) + T (z)) \leftrightarrow (φ \to U (2 \cdot 1) = S (1) + T (1)))$
178		oveq2	$⊢ z = k \to 2 z = 2 k$
179	178	fveq2d	$⊢ z = k \to U (2 z) = U (2 k)$
180		fveq2	$⊢ z = k \to S (z) = S (k)$
181		fveq2	$⊢ z = k \to T (z) = T (k)$
182	180 181	oveq12d	$⊢ z = k \to S (z) + T (z) = S (k) + T (k)$
183	179 182	eqeq12d	$⊢ z = k \to (U (2 z) = S (z) + T (z) \leftrightarrow U (2 k) = S (k) + T (k))$
184	183	imbi2d	$⊢ z = k \to ((φ \to U (2 z) = S (z) + T (z)) \leftrightarrow (φ \to U (2 k) = S (k) + T (k)))$
185		oveq2	$⊢ z = k + 1 \to 2 z = 2 (k + 1)$
186	185	fveq2d	$⊢ z = k + 1 \to U (2 z) = U (2 (k + 1))$
187		fveq2	$⊢ z = k + 1 \to S (z) = S (k + 1)$
188		fveq2	$⊢ z = k + 1 \to T (z) = T (k + 1)$
189	187 188	oveq12d	$⊢ z = k + 1 \to S (z) + T (z) = S (k + 1) + T (k + 1)$
190	186 189	eqeq12d	$⊢ z = k + 1 \to (U (2 z) = S (z) + T (z) \leftrightarrow U (2 (k + 1)) = S (k + 1) + T (k + 1))$
191	190	imbi2d	$⊢ z = k + 1 \to ((φ \to U (2 z) = S (z) + T (z)) \leftrightarrow (φ \to U (2 (k + 1)) = S (k + 1) + T (k + 1)))$
192		oveq2	$⊢ z = ⌊\frac{k + 1}{2}⌋ \to 2 z = 2 ⌊\frac{k + 1}{2}⌋$
193	192	fveq2d	$⊢ z = ⌊\frac{k + 1}{2}⌋ \to U (2 z) = U (2 ⌊\frac{k + 1}{2}⌋)$
194		fveq2	$⊢ z = ⌊\frac{k + 1}{2}⌋ \to S (z) = S (⌊\frac{k + 1}{2}⌋)$
195		fveq2	$⊢ z = ⌊\frac{k + 1}{2}⌋ \to T (z) = T (⌊\frac{k + 1}{2}⌋)$
196	194 195	oveq12d	$⊢ z = ⌊\frac{k + 1}{2}⌋ \to S (z) + T (z) = S (⌊\frac{k + 1}{2}⌋) + T (⌊\frac{k + 1}{2}⌋)$
197	193 196	eqeq12d	$⊢ z = ⌊\frac{k + 1}{2}⌋ \to (U (2 z) = S (z) + T (z) \leftrightarrow U (2 ⌊\frac{k + 1}{2}⌋) = S (⌊\frac{k + 1}{2}⌋) + T (⌊\frac{k + 1}{2}⌋))$
198	197	imbi2d	$⊢ z = ⌊\frac{k + 1}{2}⌋ \to ((φ \to U (2 z) = S (z) + T (z)) \leftrightarrow (φ \to U (2 ⌊\frac{k + 1}{2}⌋) = S (⌊\frac{k + 1}{2}⌋) + T (⌊\frac{k + 1}{2}⌋)))$
199	6	fveq1i	$⊢ U (2 \cdot 1) = seq 1 (+ ((abs \circ -) \circ H)) (2 \cdot 1)$
200	136	a1i	$⊢ φ \to 1 \in ℕ$
201	29	ovolfsval	$⊢ (H : ℕ ⟶ \leq \cap ℝ^{2} \land 1 \in ℕ) \to ((abs \circ -) \circ H) (1) = 2^{nd} (H (1)) - 1^{st} (H (1))$
202	28 136 201	sylancl	$⊢ φ \to ((abs \circ -) \circ H) (1) = 2^{nd} (H (1)) - 1^{st} (H (1))$
203		halfnz	$⊢ \neg \frac{1}{2} \in ℤ$
204		nnz	$⊢ \frac{n}{2} \in ℕ \to \frac{n}{2} \in ℤ$
205		oveq1	$⊢ n = 1 \to \frac{n}{2} = \frac{1}{2}$
206	205	eleq1d	$⊢ n = 1 \to (\frac{n}{2} \in ℤ \leftrightarrow \frac{1}{2} \in ℤ)$
207	204 206	syl5ib	$⊢ n = 1 \to (\frac{n}{2} \in ℕ \to \frac{1}{2} \in ℤ)$
208	203 207	mtoi	$⊢ n = 1 \to \neg \frac{n}{2} \in ℕ$
209	208	iffalsed	$⊢ n = 1 \to if (\frac{n}{2} \in ℕ, G (\frac{n}{2}), F (\frac{n + 1}{2})) = F (\frac{n + 1}{2})$
210		oveq1	$⊢ n = 1 \to n + 1 = 1 + 1$
211		df-2	$⊢ 2 = 1 + 1$
212	210 211	eqtr4di	$⊢ n = 1 \to n + 1 = 2$
213	212	oveq1d	$⊢ n = 1 \to \frac{n + 1}{2} = \frac{2}{2}$
214		2div2e1	$⊢ \frac{2}{2} = 1$
215	213 214	eqtrdi	$⊢ n = 1 \to \frac{n + 1}{2} = 1$
216	215	fveq2d	$⊢ n = 1 \to F (\frac{n + 1}{2}) = F (1)$
217	209 216	eqtrd	$⊢ n = 1 \to if (\frac{n}{2} \in ℕ, G (\frac{n}{2}), F (\frac{n + 1}{2})) = F (1)$
218		fvex	$⊢ F (1) \in V$
219	217 13 218	fvmpt	$⊢ 1 \in ℕ \to H (1) = F (1)$
220	136 219	ax-mp	$⊢ H (1) = F (1)$
221	220	fveq2i	$⊢ 2^{nd} (H (1)) = 2^{nd} (F (1))$
222	220	fveq2i	$⊢ 1^{st} (H (1)) = 1^{st} (F (1))$
223	221 222	oveq12i	$⊢ 2^{nd} (H (1)) - 1^{st} (H (1)) = 2^{nd} (F (1)) - 1^{st} (F (1))$
224	202 223	eqtrdi	$⊢ φ \to ((abs \circ -) \circ H) (1) = 2^{nd} (F (1)) - 1^{st} (F (1))$
225	61 224	seq1i	$⊢ φ \to seq 1 (+ ((abs \circ -) \circ H)) (1) = 2^{nd} (F (1)) - 1^{st} (F (1))$
226		2t1e2	$⊢ 2 \cdot 1 = 2$
227	226	fveq2i	$⊢ ((abs \circ -) \circ H) (2 \cdot 1) = ((abs \circ -) \circ H) (2)$
228	29	ovolfsval	$⊢ (H : ℕ ⟶ \leq \cap ℝ^{2} \land 2 \in ℕ) \to ((abs \circ -) \circ H) (2) = 2^{nd} (H (2)) - 1^{st} (H (2))$
229	28 36 228	sylancl	$⊢ φ \to ((abs \circ -) \circ H) (2) = 2^{nd} (H (2)) - 1^{st} (H (2))$
230		oveq1	$⊢ n = 2 \to \frac{n}{2} = \frac{2}{2}$
231	230 214	eqtrdi	$⊢ n = 2 \to \frac{n}{2} = 1$
232	231 136	eqeltrdi	$⊢ n = 2 \to \frac{n}{2} \in ℕ$
233	232	iftrued	$⊢ n = 2 \to if (\frac{n}{2} \in ℕ, G (\frac{n}{2}), F (\frac{n + 1}{2})) = G (\frac{n}{2})$
234	231	fveq2d	$⊢ n = 2 \to G (\frac{n}{2}) = G (1)$
235	233 234	eqtrd	$⊢ n = 2 \to if (\frac{n}{2} \in ℕ, G (\frac{n}{2}), F (\frac{n + 1}{2})) = G (1)$
236		fvex	$⊢ G (1) \in V$
237	235 13 236	fvmpt	$⊢ 2 \in ℕ \to H (2) = G (1)$
238	36 237	ax-mp	$⊢ H (2) = G (1)$
239	238	fveq2i	$⊢ 2^{nd} (H (2)) = 2^{nd} (G (1))$
240	238	fveq2i	$⊢ 1^{st} (H (2)) = 1^{st} (G (1))$
241	239 240	oveq12i	$⊢ 2^{nd} (H (2)) - 1^{st} (H (2)) = 2^{nd} (G (1)) - 1^{st} (G (1))$
242	229 241	eqtrdi	$⊢ φ \to ((abs \circ -) \circ H) (2) = 2^{nd} (G (1)) - 1^{st} (G (1))$
243	227 242	syl5eq	$⊢ φ \to ((abs \circ -) \circ H) (2 \cdot 1) = 2^{nd} (G (1)) - 1^{st} (G (1))$
244	78 200 43 225 243	seqp1d	$⊢ φ \to seq 1 (+ ((abs \circ -) \circ H)) (2 \cdot 1) = (2^{nd} (F (1)) - 1^{st} (F (1))) + 2^{nd} (G (1)) - 1^{st} (G (1))$
245	199 244	syl5eq	$⊢ φ \to U (2 \cdot 1) = (2^{nd} (F (1)) - 1^{st} (F (1))) + 2^{nd} (G (1)) - 1^{st} (G (1))$
246	4	fveq1i	$⊢ S (1) = seq 1 (+ ((abs \circ -) \circ F)) (1)$
247	107	ovolfsval	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land 1 \in ℕ) \to ((abs \circ -) \circ F) (1) = 2^{nd} (F (1)) - 1^{st} (F (1))$
248	23 136 247	sylancl	$⊢ φ \to ((abs \circ -) \circ F) (1) = 2^{nd} (F (1)) - 1^{st} (F (1))$
249	61 248	seq1i	$⊢ φ \to seq 1 (+ ((abs \circ -) \circ F)) (1) = 2^{nd} (F (1)) - 1^{st} (F (1))$
250	246 249	syl5eq	$⊢ φ \to S (1) = 2^{nd} (F (1)) - 1^{st} (F (1))$
251	5	fveq1i	$⊢ T (1) = seq 1 (+ ((abs \circ -) \circ G)) (1)$
252	117	ovolfsval	$⊢ (G : ℕ ⟶ \leq \cap ℝ^{2} \land 1 \in ℕ) \to ((abs \circ -) \circ G) (1) = 2^{nd} (G (1)) - 1^{st} (G (1))$
253	15 136 252	sylancl	$⊢ φ \to ((abs \circ -) \circ G) (1) = 2^{nd} (G (1)) - 1^{st} (G (1))$
254	61 253	seq1i	$⊢ φ \to seq 1 (+ ((abs \circ -) \circ G)) (1) = 2^{nd} (G (1)) - 1^{st} (G (1))$
255	251 254	syl5eq	$⊢ φ \to T (1) = 2^{nd} (G (1)) - 1^{st} (G (1))$
256	250 255	oveq12d	$⊢ φ \to S (1) + T (1) = (2^{nd} (F (1)) - 1^{st} (F (1))) + 2^{nd} (G (1)) - 1^{st} (G (1))$
257	245 256	eqtr4d	$⊢ φ \to U (2 \cdot 1) = S (1) + T (1)$
258		oveq1	$⊢ U (2 k) = S (k) + T (k) \to U (2 k) + ((abs \circ -) \circ F) (k + 1) + ((abs \circ -) \circ G) (k + 1) = S (k) + T (k) + ((abs \circ -) \circ F) (k + 1) + ((abs \circ -) \circ G) (k + 1)$
259	43	oveq2i	$⊢ 2 k + 2 \cdot 1 = 2 k + 1 + 1$
260		2cnd	$⊢ (φ \land k \in ℕ) \to 2 \in ℂ$
261	47	recnd	$⊢ (φ \land k \in ℕ) \to k \in ℂ$
262		1cnd	$⊢ (φ \land k \in ℕ) \to 1 \in ℂ$
263	260 261 262	adddid	$⊢ (φ \land k \in ℕ) \to 2 (k + 1) = 2 k + 2 \cdot 1$
264		nnmulcl	$⊢ (2 \in ℕ \land k \in ℕ) \to 2 k \in ℕ$
265	36 264	mpan	$⊢ k \in ℕ \to 2 k \in ℕ$
266	265	adantl	$⊢ (φ \land k \in ℕ) \to 2 k \in ℕ$
267	266	nncnd	$⊢ (φ \land k \in ℕ) \to 2 k \in ℂ$
268	267 262 262	addassd	$⊢ (φ \land k \in ℕ) \to 2 k + 1 + 1 = 2 k + 1 + 1$
269	259 263 268	3eqtr4a	$⊢ (φ \land k \in ℕ) \to 2 (k + 1) = 2 k + 1 + 1$
270	269	fveq2d	$⊢ (φ \land k \in ℕ) \to U (2 (k + 1)) = U (2 k + 1 + 1)$
271	6	fveq1i	$⊢ U (2 k + 1 + 1) = seq 1 (+ ((abs \circ -) \circ H)) (2 k + 1 + 1)$
272	266	peano2nnd	$⊢ (φ \land k \in ℕ) \to 2 k + 1 \in ℕ$
273	272 78	eleqtrdi	$⊢ (φ \land k \in ℕ) \to 2 k + 1 \in ℤ_{\geq 1}$
274		seqp1	$⊢ 2 k + 1 \in ℤ_{\geq 1} \to seq 1 (+ ((abs \circ -) \circ H)) (2 k + 1 + 1) = seq 1 (+ ((abs \circ -) \circ H)) (2 k + 1) + ((abs \circ -) \circ H) (2 k + 1 + 1)$
275	273 274	syl	$⊢ (φ \land k \in ℕ) \to seq 1 (+ ((abs \circ -) \circ H)) (2 k + 1 + 1) = seq 1 (+ ((abs \circ -) \circ H)) (2 k + 1) + ((abs \circ -) \circ H) (2 k + 1 + 1)$
276	266 78	eleqtrdi	$⊢ (φ \land k \in ℕ) \to 2 k \in ℤ_{\geq 1}$
277		seqp1	$⊢ 2 k \in ℤ_{\geq 1} \to seq 1 (+ ((abs \circ -) \circ H)) (2 k + 1) = seq 1 (+ ((abs \circ -) \circ H)) (2 k) + ((abs \circ -) \circ H) (2 k + 1)$
278	276 277	syl	$⊢ (φ \land k \in ℕ) \to seq 1 (+ ((abs \circ -) \circ H)) (2 k + 1) = seq 1 (+ ((abs \circ -) \circ H)) (2 k) + ((abs \circ -) \circ H) (2 k + 1)$
279	6	fveq1i	$⊢ U (2 k) = seq 1 (+ ((abs \circ -) \circ H)) (2 k)$
280	279	a1i	$⊢ (φ \land k \in ℕ) \to U (2 k) = seq 1 (+ ((abs \circ -) \circ H)) (2 k)$
281		oveq1	$⊢ n = 2 k + 1 \to \frac{n}{2} = \frac{2 k + 1}{2}$
282	281	eleq1d	$⊢ n = 2 k + 1 \to (\frac{n}{2} \in ℕ \leftrightarrow \frac{2 k + 1}{2} \in ℕ)$
283	281	fveq2d	$⊢ n = 2 k + 1 \to G (\frac{n}{2}) = G (\frac{2 k + 1}{2})$
284		oveq1	$⊢ n = 2 k + 1 \to n + 1 = 2 k + 1 + 1$
285	284	fvoveq1d	$⊢ n = 2 k + 1 \to F (\frac{n + 1}{2}) = F (\frac{2 k + 1 + 1}{2})$
286	282 283 285	ifbieq12d	$⊢ n = 2 k + 1 \to if (\frac{n}{2} \in ℕ, G (\frac{n}{2}), F (\frac{n + 1}{2})) = if (\frac{2 k + 1}{2} \in ℕ, G (\frac{2 k + 1}{2}), F (\frac{2 k + 1 + 1}{2}))$
287		fvex	$⊢ G (\frac{2 k + 1}{2}) \in V$
288		fvex	$⊢ F (\frac{2 k + 1 + 1}{2}) \in V$
289	287 288	ifex	$⊢ if (\frac{2 k + 1}{2} \in ℕ, G (\frac{2 k + 1}{2}), F (\frac{2 k + 1 + 1}{2})) \in V$
290	286 13 289	fvmpt	$⊢ 2 k + 1 \in ℕ \to H (2 k + 1) = if (\frac{2 k + 1}{2} \in ℕ, G (\frac{2 k + 1}{2}), F (\frac{2 k + 1 + 1}{2}))$
291	272 290	syl	$⊢ (φ \land k \in ℕ) \to H (2 k + 1) = if (\frac{2 k + 1}{2} \in ℕ, G (\frac{2 k + 1}{2}), F (\frac{2 k + 1 + 1}{2}))$
292		2ne0	$⊢ 2 \neq 0$
293	292	a1i	$⊢ (φ \land k \in ℕ) \to 2 \neq 0$
294	261 260 293	divcan3d	$⊢ (φ \land k \in ℕ) \to \frac{2 k}{2} = k$
295	294 77	eqeltrd	$⊢ (φ \land k \in ℕ) \to \frac{2 k}{2} \in ℕ$
296		nneo	$⊢ 2 k \in ℕ \to (\frac{2 k}{2} \in ℕ \leftrightarrow \neg \frac{2 k + 1}{2} \in ℕ)$
297	266 296	syl	$⊢ (φ \land k \in ℕ) \to (\frac{2 k}{2} \in ℕ \leftrightarrow \neg \frac{2 k + 1}{2} \in ℕ)$
298	295 297	mpbid	$⊢ (φ \land k \in ℕ) \to \neg \frac{2 k + 1}{2} \in ℕ$
299	298	iffalsed	$⊢ (φ \land k \in ℕ) \to if (\frac{2 k + 1}{2} \in ℕ, G (\frac{2 k + 1}{2}), F (\frac{2 k + 1 + 1}{2})) = F (\frac{2 k + 1 + 1}{2})$
300	269	oveq1d	$⊢ (φ \land k \in ℕ) \to \frac{2 (k + 1)}{2} = \frac{2 k + 1 + 1}{2}$
301	38	nncnd	$⊢ (φ \land k \in ℕ) \to k + 1 \in ℂ$
302		2cn	$⊢ 2 \in ℂ$
303		divcan3	$⊢ (k + 1 \in ℂ \land 2 \in ℂ \land 2 \neq 0) \to \frac{2 (k + 1)}{2} = k + 1$
304	302 292 303	mp3an23	$⊢ k + 1 \in ℂ \to \frac{2 (k + 1)}{2} = k + 1$
305	301 304	syl	$⊢ (φ \land k \in ℕ) \to \frac{2 (k + 1)}{2} = k + 1$
306	300 305	eqtr3d	$⊢ (φ \land k \in ℕ) \to \frac{2 k + 1 + 1}{2} = k + 1$
307	306	fveq2d	$⊢ (φ \land k \in ℕ) \to F (\frac{2 k + 1 + 1}{2}) = F (k + 1)$
308	291 299 307	3eqtrd	$⊢ (φ \land k \in ℕ) \to H (2 k + 1) = F (k + 1)$
309	308	fveq2d	$⊢ (φ \land k \in ℕ) \to 2^{nd} (H (2 k + 1)) = 2^{nd} (F (k + 1))$
310	308	fveq2d	$⊢ (φ \land k \in ℕ) \to 1^{st} (H (2 k + 1)) = 1^{st} (F (k + 1))$
311	309 310	oveq12d	$⊢ (φ \land k \in ℕ) \to 2^{nd} (H (2 k + 1)) - 1^{st} (H (2 k + 1)) = 2^{nd} (F (k + 1)) - 1^{st} (F (k + 1))$
312	29	ovolfsval	$⊢ (H : ℕ ⟶ \leq \cap ℝ^{2} \land 2 k + 1 \in ℕ) \to ((abs \circ -) \circ H) (2 k + 1) = 2^{nd} (H (2 k + 1)) - 1^{st} (H (2 k + 1))$
313	28 272 312	syl2an2r	$⊢ (φ \land k \in ℕ) \to ((abs \circ -) \circ H) (2 k + 1) = 2^{nd} (H (2 k + 1)) - 1^{st} (H (2 k + 1))$
314	107	ovolfsval	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land k + 1 \in ℕ) \to ((abs \circ -) \circ F) (k + 1) = 2^{nd} (F (k + 1)) - 1^{st} (F (k + 1))$
315	23 37 314	syl2an	$⊢ (φ \land k \in ℕ) \to ((abs \circ -) \circ F) (k + 1) = 2^{nd} (F (k + 1)) - 1^{st} (F (k + 1))$
316	311 313 315	3eqtr4rd	$⊢ (φ \land k \in ℕ) \to ((abs \circ -) \circ F) (k + 1) = ((abs \circ -) \circ H) (2 k + 1)$
317	280 316	oveq12d	$⊢ (φ \land k \in ℕ) \to U (2 k) + ((abs \circ -) \circ F) (k + 1) = seq 1 (+ ((abs \circ -) \circ H)) (2 k) + ((abs \circ -) \circ H) (2 k + 1)$
318	278 317	eqtr4d	$⊢ (φ \land k \in ℕ) \to seq 1 (+ ((abs \circ -) \circ H)) (2 k + 1) = U (2 k) + ((abs \circ -) \circ F) (k + 1)$
319	269	fveq2d	$⊢ (φ \land k \in ℕ) \to H (2 (k + 1)) = H (2 k + 1 + 1)$
320	272	peano2nnd	$⊢ (φ \land k \in ℕ) \to 2 k + 1 + 1 \in ℕ$
321	269 320	eqeltrd	$⊢ (φ \land k \in ℕ) \to 2 (k + 1) \in ℕ$
322		oveq1	$⊢ n = 2 (k + 1) \to \frac{n}{2} = \frac{2 (k + 1)}{2}$
323	322	eleq1d	$⊢ n = 2 (k + 1) \to (\frac{n}{2} \in ℕ \leftrightarrow \frac{2 (k + 1)}{2} \in ℕ)$
324	322	fveq2d	$⊢ n = 2 (k + 1) \to G (\frac{n}{2}) = G (\frac{2 (k + 1)}{2})$
325		oveq1	$⊢ n = 2 (k + 1) \to n + 1 = 2 (k + 1) + 1$
326	325	fvoveq1d	$⊢ n = 2 (k + 1) \to F (\frac{n + 1}{2}) = F (\frac{2 (k + 1) + 1}{2})$
327	323 324 326	ifbieq12d	$⊢ n = 2 (k + 1) \to if (\frac{n}{2} \in ℕ, G (\frac{n}{2}), F (\frac{n + 1}{2})) = if (\frac{2 (k + 1)}{2} \in ℕ, G (\frac{2 (k + 1)}{2}), F (\frac{2 (k + 1) + 1}{2}))$
328		fvex	$⊢ G (\frac{2 (k + 1)}{2}) \in V$
329		fvex	$⊢ F (\frac{2 (k + 1) + 1}{2}) \in V$
330	328 329	ifex	$⊢ if (\frac{2 (k + 1)}{2} \in ℕ, G (\frac{2 (k + 1)}{2}), F (\frac{2 (k + 1) + 1}{2})) \in V$
331	327 13 330	fvmpt	$⊢ 2 (k + 1) \in ℕ \to H (2 (k + 1)) = if (\frac{2 (k + 1)}{2} \in ℕ, G (\frac{2 (k + 1)}{2}), F (\frac{2 (k + 1) + 1}{2}))$
332	321 331	syl	$⊢ (φ \land k \in ℕ) \to H (2 (k + 1)) = if (\frac{2 (k + 1)}{2} \in ℕ, G (\frac{2 (k + 1)}{2}), F (\frac{2 (k + 1) + 1}{2}))$
333	305 38	eqeltrd	$⊢ (φ \land k \in ℕ) \to \frac{2 (k + 1)}{2} \in ℕ$
334	333	iftrued	$⊢ (φ \land k \in ℕ) \to if (\frac{2 (k + 1)}{2} \in ℕ, G (\frac{2 (k + 1)}{2}), F (\frac{2 (k + 1) + 1}{2})) = G (\frac{2 (k + 1)}{2})$
335	305	fveq2d	$⊢ (φ \land k \in ℕ) \to G (\frac{2 (k + 1)}{2}) = G (k + 1)$
336	332 334 335	3eqtrd	$⊢ (φ \land k \in ℕ) \to H (2 (k + 1)) = G (k + 1)$
337	319 336	eqtr3d	$⊢ (φ \land k \in ℕ) \to H (2 k + 1 + 1) = G (k + 1)$
338	337	fveq2d	$⊢ (φ \land k \in ℕ) \to 2^{nd} (H (2 k + 1 + 1)) = 2^{nd} (G (k + 1))$
339	337	fveq2d	$⊢ (φ \land k \in ℕ) \to 1^{st} (H (2 k + 1 + 1)) = 1^{st} (G (k + 1))$
340	338 339	oveq12d	$⊢ (φ \land k \in ℕ) \to 2^{nd} (H (2 k + 1 + 1)) - 1^{st} (H (2 k + 1 + 1)) = 2^{nd} (G (k + 1)) - 1^{st} (G (k + 1))$
341	29	ovolfsval	$⊢ (H : ℕ ⟶ \leq \cap ℝ^{2} \land 2 k + 1 + 1 \in ℕ) \to ((abs \circ -) \circ H) (2 k + 1 + 1) = 2^{nd} (H (2 k + 1 + 1)) - 1^{st} (H (2 k + 1 + 1))$
342	28 320 341	syl2an2r	$⊢ (φ \land k \in ℕ) \to ((abs \circ -) \circ H) (2 k + 1 + 1) = 2^{nd} (H (2 k + 1 + 1)) - 1^{st} (H (2 k + 1 + 1))$
343	117	ovolfsval	$⊢ (G : ℕ ⟶ \leq \cap ℝ^{2} \land k + 1 \in ℕ) \to ((abs \circ -) \circ G) (k + 1) = 2^{nd} (G (k + 1)) - 1^{st} (G (k + 1))$
344	15 37 343	syl2an	$⊢ (φ \land k \in ℕ) \to ((abs \circ -) \circ G) (k + 1) = 2^{nd} (G (k + 1)) - 1^{st} (G (k + 1))$
345	340 342 344	3eqtr4d	$⊢ (φ \land k \in ℕ) \to ((abs \circ -) \circ H) (2 k + 1 + 1) = ((abs \circ -) \circ G) (k + 1)$
346	318 345	oveq12d	$⊢ (φ \land k \in ℕ) \to seq 1 (+ ((abs \circ -) \circ H)) (2 k + 1) + ((abs \circ -) \circ H) (2 k + 1 + 1) = U (2 k) + ((abs \circ -) \circ F) (k + 1) + ((abs \circ -) \circ G) (k + 1)$
347	275 346	eqtrd	$⊢ (φ \land k \in ℕ) \to seq 1 (+ ((abs \circ -) \circ H)) (2 k + 1 + 1) = U (2 k) + ((abs \circ -) \circ F) (k + 1) + ((abs \circ -) \circ G) (k + 1)$
348	271 347	syl5eq	$⊢ (φ \land k \in ℕ) \to U (2 k + 1 + 1) = U (2 k) + ((abs \circ -) \circ F) (k + 1) + ((abs \circ -) \circ G) (k + 1)$
349		ffvelrn	$⊢ (U : ℕ ⟶ [0, +∞) \land 2 k \in ℕ) \to U (2 k) \in [0, +∞)$
350	31 265 349	syl2an	$⊢ (φ \land k \in ℕ) \to U (2 k) \in [0, +∞)$
351	32 350	sseldi	$⊢ (φ \land k \in ℕ) \to U (2 k) \in ℝ$
352	351	recnd	$⊢ (φ \land k \in ℕ) \to U (2 k) \in ℂ$
353	107	ovolfsf	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to ((abs \circ -) \circ F) : ℕ ⟶ [0, +∞)$
354	23 353	syl	$⊢ φ \to ((abs \circ -) \circ F) : ℕ ⟶ [0, +∞)$
355		ffvelrn	$⊢ (((abs \circ -) \circ F) : ℕ ⟶ [0, +∞) \land k + 1 \in ℕ) \to ((abs \circ -) \circ F) (k + 1) \in [0, +∞)$
356	354 37 355	syl2an	$⊢ (φ \land k \in ℕ) \to ((abs \circ -) \circ F) (k + 1) \in [0, +∞)$
357	32 356	sseldi	$⊢ (φ \land k \in ℕ) \to ((abs \circ -) \circ F) (k + 1) \in ℝ$
358	357	recnd	$⊢ (φ \land k \in ℕ) \to ((abs \circ -) \circ F) (k + 1) \in ℂ$
359	117	ovolfsf	$⊢ G : ℕ ⟶ \leq \cap ℝ^{2} \to ((abs \circ -) \circ G) : ℕ ⟶ [0, +∞)$
360	15 359	syl	$⊢ φ \to ((abs \circ -) \circ G) : ℕ ⟶ [0, +∞)$
361		ffvelrn	$⊢ (((abs \circ -) \circ G) : ℕ ⟶ [0, +∞) \land k + 1 \in ℕ) \to ((abs \circ -) \circ G) (k + 1) \in [0, +∞)$
362	360 37 361	syl2an	$⊢ (φ \land k \in ℕ) \to ((abs \circ -) \circ G) (k + 1) \in [0, +∞)$
363	32 362	sseldi	$⊢ (φ \land k \in ℕ) \to ((abs \circ -) \circ G) (k + 1) \in ℝ$
364	363	recnd	$⊢ (φ \land k \in ℕ) \to ((abs \circ -) \circ G) (k + 1) \in ℂ$
365	352 358 364	addassd	$⊢ (φ \land k \in ℕ) \to U (2 k) + ((abs \circ -) \circ F) (k + 1) + ((abs \circ -) \circ G) (k + 1) = U (2 k) + ((abs \circ -) \circ F) (k + 1) + ((abs \circ -) \circ G) (k + 1)$
366	270 348 365	3eqtrd	$⊢ (φ \land k \in ℕ) \to U (2 (k + 1)) = U (2 k) + ((abs \circ -) \circ F) (k + 1) + ((abs \circ -) \circ G) (k + 1)$
367		seqp1	$⊢ k \in ℤ_{\geq 1} \to seq 1 (+ ((abs \circ -) \circ F)) (k + 1) = seq 1 (+ ((abs \circ -) \circ F)) (k) + ((abs \circ -) \circ F) (k + 1)$
368	79 367	syl	$⊢ (φ \land k \in ℕ) \to seq 1 (+ ((abs \circ -) \circ F)) (k + 1) = seq 1 (+ ((abs \circ -) \circ F)) (k) + ((abs \circ -) \circ F) (k + 1)$
369	4	fveq1i	$⊢ S (k + 1) = seq 1 (+ ((abs \circ -) \circ F)) (k + 1)$
370	4	fveq1i	$⊢ S (k) = seq 1 (+ ((abs \circ -) \circ F)) (k)$
371	370	oveq1i	$⊢ S (k) + ((abs \circ -) \circ F) (k + 1) = seq 1 (+ ((abs \circ -) \circ F)) (k) + ((abs \circ -) \circ F) (k + 1)$
372	368 369 371	3eqtr4g	$⊢ (φ \land k \in ℕ) \to S (k + 1) = S (k) + ((abs \circ -) \circ F) (k + 1)$
373		seqp1	$⊢ k \in ℤ_{\geq 1} \to seq 1 (+ ((abs \circ -) \circ G)) (k + 1) = seq 1 (+ ((abs \circ -) \circ G)) (k) + ((abs \circ -) \circ G) (k + 1)$
374	79 373	syl	$⊢ (φ \land k \in ℕ) \to seq 1 (+ ((abs \circ -) \circ G)) (k + 1) = seq 1 (+ ((abs \circ -) \circ G)) (k) + ((abs \circ -) \circ G) (k + 1)$
375	5	fveq1i	$⊢ T (k + 1) = seq 1 (+ ((abs \circ -) \circ G)) (k + 1)$
376	5	fveq1i	$⊢ T (k) = seq 1 (+ ((abs \circ -) \circ G)) (k)$
377	376	oveq1i	$⊢ T (k) + ((abs \circ -) \circ G) (k + 1) = seq 1 (+ ((abs \circ -) \circ G)) (k) + ((abs \circ -) \circ G) (k + 1)$
378	374 375 377	3eqtr4g	$⊢ (φ \land k \in ℕ) \to T (k + 1) = T (k) + ((abs \circ -) \circ G) (k + 1)$
379	372 378	oveq12d	$⊢ (φ \land k \in ℕ) \to S (k + 1) + T (k + 1) = S (k) + ((abs \circ -) \circ F) (k + 1) + T (k) + ((abs \circ -) \circ G) (k + 1)$
380	109	ffvelrnda	$⊢ (φ \land k \in ℕ) \to S (k) \in [0, +∞)$
381	32 380	sseldi	$⊢ (φ \land k \in ℕ) \to S (k) \in ℝ$
382	381	recnd	$⊢ (φ \land k \in ℕ) \to S (k) \in ℂ$
383	119	ffvelrnda	$⊢ (φ \land k \in ℕ) \to T (k) \in [0, +∞)$
384	32 383	sseldi	$⊢ (φ \land k \in ℕ) \to T (k) \in ℝ$
385	384	recnd	$⊢ (φ \land k \in ℕ) \to T (k) \in ℂ$
386	382 358 385 364	add4d	$⊢ (φ \land k \in ℕ) \to S (k) + ((abs \circ -) \circ F) (k + 1) + T (k) + ((abs \circ -) \circ G) (k + 1) = S (k) + T (k) + ((abs \circ -) \circ F) (k + 1) + ((abs \circ -) \circ G) (k + 1)$
387	379 386	eqtrd	$⊢ (φ \land k \in ℕ) \to S (k + 1) + T (k + 1) = S (k) + T (k) + ((abs \circ -) \circ F) (k + 1) + ((abs \circ -) \circ G) (k + 1)$
388	366 387	eqeq12d	$⊢ (φ \land k \in ℕ) \to (U (2 (k + 1)) = S (k + 1) + T (k + 1) \leftrightarrow U (2 k) + ((abs \circ -) \circ F) (k + 1) + ((abs \circ -) \circ G) (k + 1) = S (k) + T (k) + ((abs \circ -) \circ F) (k + 1) + ((abs \circ -) \circ G) (k + 1))$
389	258 388	syl5ibr	$⊢ (φ \land k \in ℕ) \to (U (2 k) = S (k) + T (k) \to U (2 (k + 1)) = S (k + 1) + T (k + 1))$
390	389	expcom	$⊢ k \in ℕ \to (φ \to (U (2 k) = S (k) + T (k) \to U (2 (k + 1)) = S (k + 1) + T (k + 1)))$
391	390	a2d	$⊢ k \in ℕ \to ((φ \to U (2 k) = S (k) + T (k)) \to (φ \to U (2 (k + 1)) = S (k + 1) + T (k + 1)))$
392	177 184 191 198 257 391	nnind	$⊢ ⌊\frac{k + 1}{2}⌋ \in ℕ \to (φ \to U (2 ⌊\frac{k + 1}{2}⌋) = S (⌊\frac{k + 1}{2}⌋) + T (⌊\frac{k + 1}{2}⌋))$
393	392	impcom	$⊢ (φ \land ⌊\frac{k + 1}{2}⌋ \in ℕ) \to U (2 ⌊\frac{k + 1}{2}⌋) = S (⌊\frac{k + 1}{2}⌋) + T (⌊\frac{k + 1}{2}⌋)$
394	66 393	syldan	$⊢ (φ \land k \in ℕ) \to U (2 ⌊\frac{k + 1}{2}⌋) = S (⌊\frac{k + 1}{2}⌋) + T (⌊\frac{k + 1}{2}⌋)$
395	71	adantr	$⊢ (φ \land k \in ℕ) \to {vol}^{*} (A) \in ℝ$
396	395	recnd	$⊢ (φ \land k \in ℕ) \to {vol}^{*} (A) \in ℂ$
397	74	adantr	$⊢ (φ \land k \in ℕ) \to C \in ℝ$
398	397	rehalfcld	$⊢ (φ \land k \in ℕ) \to \frac{C}{2} \in ℝ$
399	398	recnd	$⊢ (φ \land k \in ℕ) \to \frac{C}{2} \in ℂ$
400	72	adantr	$⊢ (φ \land k \in ℕ) \to {vol}^{*} (B) \in ℝ$
401	400	recnd	$⊢ (φ \land k \in ℕ) \to {vol}^{*} (B) \in ℂ$
402	396 399 401 399	add4d	$⊢ (φ \land k \in ℕ) \to {vol}^{} (A) + (\frac{C}{2}) + {vol}^{} (B) + (\frac{C}{2}) = {vol}^{} (A) + {vol}^{} (B) + (\frac{C}{2}) + (\frac{C}{2})$
403	397	recnd	$⊢ (φ \land k \in ℕ) \to C \in ℂ$
404	403	2halvesd	$⊢ (φ \land k \in ℕ) \to (\frac{C}{2}) + (\frac{C}{2}) = C$
405	404	oveq2d	$⊢ (φ \land k \in ℕ) \to {vol}^{} (A) + {vol}^{} (B) + (\frac{C}{2}) + (\frac{C}{2}) = {vol}^{} (A) + {vol}^{} (B) + C$
406	402 405	eqtr2d	$⊢ (φ \land k \in ℕ) \to {vol}^{} (A) + {vol}^{} (B) + C = {vol}^{} (A) + (\frac{C}{2}) + {vol}^{} (B) + (\frac{C}{2})$
407	170 394 406	3brtr4d	$⊢ (φ \land k \in ℕ) \to U (2 ⌊\frac{k + 1}{2}⌋) \leq {vol}^{} (A) + {vol}^{} (B) + C$
408	35 70 76 106 407	letrd	$⊢ (φ \land k \in ℕ) \to U (k) \leq {vol}^{} (A) + {vol}^{} (B) + C$

Metamath Proof Explorer

Theorem ovolunlem1a

Proof