ovoliunlem1

	Ref	Expression
Hypotheses	ovoliun.t	$⊢ T = seq 1 (+ G)$
	ovoliun.g	$⊢ G = (n \in ℕ ⟼ {vol}^{*} (A))$
	ovoliun.a	$⊢ (φ \land n \in ℕ) \to A \subseteq ℝ$
	ovoliun.v	$⊢ (φ \land n \in ℕ) \to {vol}^{*} (A) \in ℝ$
	ovoliun.r	$⊢ φ \to sup (ran T ℝ^{*} <) \in ℝ$
	ovoliun.b	$⊢ φ \to B \in ℝ^{+}$
	ovoliun.s	$⊢ S = seq 1 (+ ((abs \circ -) \circ F (n)))$
	ovoliun.u	$⊢ U = seq 1 (+ ((abs \circ -) \circ H))$
	ovoliun.h	$⊢ H = (k \in ℕ ⟼ F (1^{st} (J (k))) (2^{nd} (J (k))))$
	ovoliun.j	$⊢ φ \to J : ℕ \underset{1-1 onto}{⟶} ℕ \times ℕ$
	ovoliun.f	$⊢ φ \to F : ℕ ⟶ {(\leq \cap ℝ^{2})}^{ℕ}$
	ovoliun.x1	$⊢ (φ \land n \in ℕ) \to A \subseteq ⋃ ran ((.) \circ F (n))$
	ovoliun.x2	$⊢ (φ \land n \in ℕ) \to sup (ran S ℝ^{} <) \leq {vol}^{} (A) + (\frac{B}{2^{n}})$
	ovoliun.k	$⊢ φ \to K \in ℕ$
	ovoliun.l1	$⊢ φ \to L \in ℤ$
	ovoliun.l2	$⊢ φ \to \forall w \in (1 \dots K) 1^{st} (J (w)) \leq L$
Assertion	ovoliunlem1	$⊢ φ \to U (K) \leq sup (ran T ℝ^{*} <) + B$

Proof

Step	Hyp	Ref	Expression
1		ovoliun.t	$⊢ T = seq 1 (+ G)$
2		ovoliun.g	$⊢ G = (n \in ℕ ⟼ {vol}^{*} (A))$
3		ovoliun.a	$⊢ (φ \land n \in ℕ) \to A \subseteq ℝ$
4		ovoliun.v	$⊢ (φ \land n \in ℕ) \to {vol}^{*} (A) \in ℝ$
5		ovoliun.r	$⊢ φ \to sup (ran T ℝ^{*} <) \in ℝ$
6		ovoliun.b	$⊢ φ \to B \in ℝ^{+}$
7		ovoliun.s	$⊢ S = seq 1 (+ ((abs \circ -) \circ F (n)))$
8		ovoliun.u	$⊢ U = seq 1 (+ ((abs \circ -) \circ H))$
9		ovoliun.h	$⊢ H = (k \in ℕ ⟼ F (1^{st} (J (k))) (2^{nd} (J (k))))$
10		ovoliun.j	$⊢ φ \to J : ℕ \underset{1-1 onto}{⟶} ℕ \times ℕ$
11		ovoliun.f	$⊢ φ \to F : ℕ ⟶ {(\leq \cap ℝ^{2})}^{ℕ}$
12		ovoliun.x1	$⊢ (φ \land n \in ℕ) \to A \subseteq ⋃ ran ((.) \circ F (n))$
13		ovoliun.x2	$⊢ (φ \land n \in ℕ) \to sup (ran S ℝ^{} <) \leq {vol}^{} (A) + (\frac{B}{2^{n}})$
14		ovoliun.k	$⊢ φ \to K \in ℕ$
15		ovoliun.l1	$⊢ φ \to L \in ℤ$
16		ovoliun.l2	$⊢ φ \to \forall w \in (1 \dots K) 1^{st} (J (w)) \leq L$
17		2fveq3	$⊢ j = J (m) \to F (1^{st} (j)) = F (1^{st} (J (m)))$
18		fveq2	$⊢ j = J (m) \to 2^{nd} (j) = 2^{nd} (J (m))$
19	17 18	fveq12d	$⊢ j = J (m) \to F (1^{st} (j)) (2^{nd} (j)) = F (1^{st} (J (m))) (2^{nd} (J (m)))$
20	19	fveq2d	$⊢ j = J (m) \to 2^{nd} (F (1^{st} (j)) (2^{nd} (j))) = 2^{nd} (F (1^{st} (J (m))) (2^{nd} (J (m))))$
21	19	fveq2d	$⊢ j = J (m) \to 1^{st} (F (1^{st} (j)) (2^{nd} (j))) = 1^{st} (F (1^{st} (J (m))) (2^{nd} (J (m))))$
22	20 21	oveq12d	$⊢ j = J (m) \to 2^{nd} (F (1^{st} (j)) (2^{nd} (j))) - 1^{st} (F (1^{st} (j)) (2^{nd} (j))) = 2^{nd} (F (1^{st} (J (m))) (2^{nd} (J (m)))) - 1^{st} (F (1^{st} (J (m))) (2^{nd} (J (m))))$
23		fzfid	$⊢ φ \to (1 \dots K) \in Fin$
24		f1of1	$⊢ J : ℕ \underset{1-1 onto}{⟶} ℕ \times ℕ \to J : ℕ \underset{1-1}{⟶} ℕ \times ℕ$
25	10 24	syl	$⊢ φ \to J : ℕ \underset{1-1}{⟶} ℕ \times ℕ$
26		fz1ssnn	$⊢ (1 \dots K) \subseteq ℕ$
27		f1ores	$⊢ (J : ℕ \underset{1-1}{⟶} ℕ \times ℕ \land (1 \dots K) \subseteq ℕ) \to ({J ↾}_{(1 \dots K)}) : (1 \dots K) \underset{1-1 onto}{⟶} J [(1 \dots K)]$
28	25 26 27	sylancl	$⊢ φ \to ({J ↾}_{(1 \dots K)}) : (1 \dots K) \underset{1-1 onto}{⟶} J [(1 \dots K)]$
29		fvres	$⊢ m \in (1 \dots K) \to ({J ↾}_{(1 \dots K)}) (m) = J (m)$
30	29	adantl	$⊢ (φ \land m \in (1 \dots K)) \to ({J ↾}_{(1 \dots K)}) (m) = J (m)$
31	11	adantr	$⊢ (φ \land j \in J [(1 \dots K)]) \to F : ℕ ⟶ {(\leq \cap ℝ^{2})}^{ℕ}$
32		imassrn	$⊢ J [(1 \dots K)] \subseteq ran J$
33		f1of	$⊢ J : ℕ \underset{1-1 onto}{⟶} ℕ \times ℕ \to J : ℕ ⟶ ℕ \times ℕ$
34	10 33	syl	$⊢ φ \to J : ℕ ⟶ ℕ \times ℕ$
35	34	frnd	$⊢ φ \to ran J \subseteq ℕ \times ℕ$
36	32 35	sstrid	$⊢ φ \to J [(1 \dots K)] \subseteq ℕ \times ℕ$
37	36	sselda	$⊢ (φ \land j \in J [(1 \dots K)]) \to j \in (ℕ \times ℕ)$
38		xp1st	$⊢ j \in (ℕ \times ℕ) \to 1^{st} (j) \in ℕ$
39	37 38	syl	$⊢ (φ \land j \in J [(1 \dots K)]) \to 1^{st} (j) \in ℕ$
40	31 39	ffvelcdmd	$⊢ (φ \land j \in J [(1 \dots K)]) \to F (1^{st} (j)) \in ({(\leq \cap ℝ^{2})}^{ℕ})$
41		elovolmlem	$⊢ F (1^{st} (j)) \in ({(\leq \cap ℝ^{2})}^{ℕ}) \leftrightarrow F (1^{st} (j)) : ℕ ⟶ \leq \cap ℝ^{2}$
42	40 41	sylib	$⊢ (φ \land j \in J [(1 \dots K)]) \to F (1^{st} (j)) : ℕ ⟶ \leq \cap ℝ^{2}$
43		xp2nd	$⊢ j \in (ℕ \times ℕ) \to 2^{nd} (j) \in ℕ$
44	37 43	syl	$⊢ (φ \land j \in J [(1 \dots K)]) \to 2^{nd} (j) \in ℕ$
45	42 44	ffvelcdmd	$⊢ (φ \land j \in J [(1 \dots K)]) \to F (1^{st} (j)) (2^{nd} (j)) \in (\leq \cap ℝ^{2})$
46	45	elin2d	$⊢ (φ \land j \in J [(1 \dots K)]) \to F (1^{st} (j)) (2^{nd} (j)) \in ℝ^{2}$
47		xp2nd	$⊢ F (1^{st} (j)) (2^{nd} (j)) \in ℝ^{2} \to 2^{nd} (F (1^{st} (j)) (2^{nd} (j))) \in ℝ$
48	46 47	syl	$⊢ (φ \land j \in J [(1 \dots K)]) \to 2^{nd} (F (1^{st} (j)) (2^{nd} (j))) \in ℝ$
49		xp1st	$⊢ F (1^{st} (j)) (2^{nd} (j)) \in ℝ^{2} \to 1^{st} (F (1^{st} (j)) (2^{nd} (j))) \in ℝ$
50	46 49	syl	$⊢ (φ \land j \in J [(1 \dots K)]) \to 1^{st} (F (1^{st} (j)) (2^{nd} (j))) \in ℝ$
51	48 50	resubcld	$⊢ (φ \land j \in J [(1 \dots K)]) \to 2^{nd} (F (1^{st} (j)) (2^{nd} (j))) - 1^{st} (F (1^{st} (j)) (2^{nd} (j))) \in ℝ$
52	51	recnd	$⊢ (φ \land j \in J [(1 \dots K)]) \to 2^{nd} (F (1^{st} (j)) (2^{nd} (j))) - 1^{st} (F (1^{st} (j)) (2^{nd} (j))) \in ℂ$
53	22 23 28 30 52	fsumf1o	$⊢ φ \to \sum_{j \in J [(1 \dots K)]} (2^{nd} (F (1^{st} (j)) (2^{nd} (j))) - 1^{st} (F (1^{st} (j)) (2^{nd} (j)))) = \sum_{m = 1}^{K} (2^{nd} (F (1^{st} (J (m))) (2^{nd} (J (m)))) - 1^{st} (F (1^{st} (J (m))) (2^{nd} (J (m)))))$
54	11	adantr	$⊢ (φ \land k \in ℕ) \to F : ℕ ⟶ {(\leq \cap ℝ^{2})}^{ℕ}$
55	34	ffvelcdmda	$⊢ (φ \land k \in ℕ) \to J (k) \in (ℕ \times ℕ)$
56		xp1st	$⊢ J (k) \in (ℕ \times ℕ) \to 1^{st} (J (k)) \in ℕ$
57	55 56	syl	$⊢ (φ \land k \in ℕ) \to 1^{st} (J (k)) \in ℕ$
58	54 57	ffvelcdmd	$⊢ (φ \land k \in ℕ) \to F (1^{st} (J (k))) \in ({(\leq \cap ℝ^{2})}^{ℕ})$
59		elovolmlem	$⊢ F (1^{st} (J (k))) \in ({(\leq \cap ℝ^{2})}^{ℕ}) \leftrightarrow F (1^{st} (J (k))) : ℕ ⟶ \leq \cap ℝ^{2}$
60	58 59	sylib	$⊢ (φ \land k \in ℕ) \to F (1^{st} (J (k))) : ℕ ⟶ \leq \cap ℝ^{2}$
61		xp2nd	$⊢ J (k) \in (ℕ \times ℕ) \to 2^{nd} (J (k)) \in ℕ$
62	55 61	syl	$⊢ (φ \land k \in ℕ) \to 2^{nd} (J (k)) \in ℕ$
63	60 62	ffvelcdmd	$⊢ (φ \land k \in ℕ) \to F (1^{st} (J (k))) (2^{nd} (J (k))) \in (\leq \cap ℝ^{2})$
64	63 9	fmptd	$⊢ φ \to H : ℕ ⟶ \leq \cap ℝ^{2}$
65		elfznn	$⊢ m \in (1 \dots K) \to m \in ℕ$
66		eqid	$⊢ (abs \circ -) \circ H = (abs \circ -) \circ H$
67	66	ovolfsval	$⊢ (H : ℕ ⟶ \leq \cap ℝ^{2} \land m \in ℕ) \to ((abs \circ -) \circ H) (m) = 2^{nd} (H (m)) - 1^{st} (H (m))$
68	64 65 67	syl2an	$⊢ (φ \land m \in (1 \dots K)) \to ((abs \circ -) \circ H) (m) = 2^{nd} (H (m)) - 1^{st} (H (m))$
69	65	adantl	$⊢ (φ \land m \in (1 \dots K)) \to m \in ℕ$
70		2fveq3	$⊢ k = m \to 1^{st} (J (k)) = 1^{st} (J (m))$
71	70	fveq2d	$⊢ k = m \to F (1^{st} (J (k))) = F (1^{st} (J (m)))$
72		2fveq3	$⊢ k = m \to 2^{nd} (J (k)) = 2^{nd} (J (m))$
73	71 72	fveq12d	$⊢ k = m \to F (1^{st} (J (k))) (2^{nd} (J (k))) = F (1^{st} (J (m))) (2^{nd} (J (m)))$
74		fvex	$⊢ F (1^{st} (J (m))) (2^{nd} (J (m))) \in V$
75	73 9 74	fvmpt	$⊢ m \in ℕ \to H (m) = F (1^{st} (J (m))) (2^{nd} (J (m)))$
76	69 75	syl	$⊢ (φ \land m \in (1 \dots K)) \to H (m) = F (1^{st} (J (m))) (2^{nd} (J (m)))$
77	76	fveq2d	$⊢ (φ \land m \in (1 \dots K)) \to 2^{nd} (H (m)) = 2^{nd} (F (1^{st} (J (m))) (2^{nd} (J (m))))$
78	76	fveq2d	$⊢ (φ \land m \in (1 \dots K)) \to 1^{st} (H (m)) = 1^{st} (F (1^{st} (J (m))) (2^{nd} (J (m))))$
79	77 78	oveq12d	$⊢ (φ \land m \in (1 \dots K)) \to 2^{nd} (H (m)) - 1^{st} (H (m)) = 2^{nd} (F (1^{st} (J (m))) (2^{nd} (J (m)))) - 1^{st} (F (1^{st} (J (m))) (2^{nd} (J (m))))$
80	68 79	eqtrd	$⊢ (φ \land m \in (1 \dots K)) \to ((abs \circ -) \circ H) (m) = 2^{nd} (F (1^{st} (J (m))) (2^{nd} (J (m)))) - 1^{st} (F (1^{st} (J (m))) (2^{nd} (J (m))))$
81		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
82	14 81	eleqtrdi	$⊢ φ \to K \in ℤ_{\geq 1}$
83		ffvelcdm	$⊢ (H : ℕ ⟶ \leq \cap ℝ^{2} \land m \in ℕ) \to H (m) \in (\leq \cap ℝ^{2})$
84	64 65 83	syl2an	$⊢ (φ \land m \in (1 \dots K)) \to H (m) \in (\leq \cap ℝ^{2})$
85	84	elin2d	$⊢ (φ \land m \in (1 \dots K)) \to H (m) \in ℝ^{2}$
86		xp2nd	$⊢ H (m) \in ℝ^{2} \to 2^{nd} (H (m)) \in ℝ$
87	85 86	syl	$⊢ (φ \land m \in (1 \dots K)) \to 2^{nd} (H (m)) \in ℝ$
88		xp1st	$⊢ H (m) \in ℝ^{2} \to 1^{st} (H (m)) \in ℝ$
89	85 88	syl	$⊢ (φ \land m \in (1 \dots K)) \to 1^{st} (H (m)) \in ℝ$
90	87 89	resubcld	$⊢ (φ \land m \in (1 \dots K)) \to 2^{nd} (H (m)) - 1^{st} (H (m)) \in ℝ$
91	90	recnd	$⊢ (φ \land m \in (1 \dots K)) \to 2^{nd} (H (m)) - 1^{st} (H (m)) \in ℂ$
92	79 91	eqeltrrd	$⊢ (φ \land m \in (1 \dots K)) \to 2^{nd} (F (1^{st} (J (m))) (2^{nd} (J (m)))) - 1^{st} (F (1^{st} (J (m))) (2^{nd} (J (m)))) \in ℂ$
93	80 82 92	fsumser	$⊢ φ \to \sum_{m = 1}^{K} (2^{nd} (F (1^{st} (J (m))) (2^{nd} (J (m)))) - 1^{st} (F (1^{st} (J (m))) (2^{nd} (J (m))))) = seq 1 (+ ((abs \circ -) \circ H)) (K)$
94	53 93	eqtrd	$⊢ φ \to \sum_{j \in J [(1 \dots K)]} (2^{nd} (F (1^{st} (j)) (2^{nd} (j))) - 1^{st} (F (1^{st} (j)) (2^{nd} (j)))) = seq 1 (+ ((abs \circ -) \circ H)) (K)$
95	8	fveq1i	$⊢ U (K) = seq 1 (+ ((abs \circ -) \circ H)) (K)$
96	94 95	eqtr4di	$⊢ φ \to \sum_{j \in J [(1 \dots K)]} (2^{nd} (F (1^{st} (j)) (2^{nd} (j))) - 1^{st} (F (1^{st} (j)) (2^{nd} (j)))) = U (K)$
97		f1oeng	$⊢ ((1 \dots K) \in Fin \land ({J ↾}_{(1 \dots K)}) : (1 \dots K) \underset{1-1 onto}{⟶} J [(1 \dots K)]) \to (1 \dots K) \approx J [(1 \dots K)]$
98	23 28 97	syl2anc	$⊢ φ \to (1 \dots K) \approx J [(1 \dots K)]$
99	98	ensymd	$⊢ φ \to J [(1 \dots K)] \approx (1 \dots K)$
100		enfii	$⊢ ((1 \dots K) \in Fin \land J [(1 \dots K)] \approx (1 \dots K)) \to J [(1 \dots K)] \in Fin$
101	23 99 100	syl2anc	$⊢ φ \to J [(1 \dots K)] \in Fin$
102	101 51	fsumrecl	$⊢ φ \to \sum_{j \in J [(1 \dots K)]} (2^{nd} (F (1^{st} (j)) (2^{nd} (j))) - 1^{st} (F (1^{st} (j)) (2^{nd} (j)))) \in ℝ$
103		fzfid	$⊢ φ \to (1 \dots L) \in Fin$
104		elfznn	$⊢ n \in (1 \dots L) \to n \in ℕ$
105	104 4	sylan2	$⊢ (φ \land n \in (1 \dots L)) \to {vol}^{*} (A) \in ℝ$
106	103 105	fsumrecl	$⊢ φ \to \sum_{n = 1}^{L} {vol}^{*} (A) \in ℝ$
107	6	rpred	$⊢ φ \to B \in ℝ$
108		2nn	$⊢ 2 \in ℕ$
109		nnnn0	$⊢ n \in ℕ \to n \in ℕ_{0}$
110		nnexpcl	$⊢ (2 \in ℕ \land n \in ℕ_{0}) \to 2^{n} \in ℕ$
111	108 109 110	sylancr	$⊢ n \in ℕ \to 2^{n} \in ℕ$
112	104 111	syl	$⊢ n \in (1 \dots L) \to 2^{n} \in ℕ$
113		nndivre	$⊢ (B \in ℝ \land 2^{n} \in ℕ) \to \frac{B}{2^{n}} \in ℝ$
114	107 112 113	syl2an	$⊢ (φ \land n \in (1 \dots L)) \to \frac{B}{2^{n}} \in ℝ$
115	103 114	fsumrecl	$⊢ φ \to \sum_{n = 1}^{L} (\frac{B}{2^{n}}) \in ℝ$
116	106 115	readdcld	$⊢ φ \to \sum_{n = 1}^{L} {vol}^{*} (A) + \sum_{n = 1}^{L} (\frac{B}{2^{n}}) \in ℝ$
117	5 107	readdcld	$⊢ φ \to sup (ran T ℝ^{*} <) + B \in ℝ$
118		relxp	$⊢ Rel (\{n\} \times J [(1 \dots K)] [\{n\}])$
119		relres	$⊢ Rel ({J [(1 \dots K)] ↾}_{\{n\}})$
120		elsni	$⊢ x \in \{n\} \to x = n$
121	120	opeq1d	$⊢ x \in \{n\} \to ⟨x, y⟩ = ⟨n, y⟩$
122	121	eleq1d	$⊢ x \in \{n\} \to (⟨x, y⟩ \in J [(1 \dots K)] \leftrightarrow ⟨n, y⟩ \in J [(1 \dots K)])$
123		vex	$⊢ n \in V$
124		vex	$⊢ y \in V$
125	123 124	elimasn	$⊢ y \in J [(1 \dots K)] [\{n\}] \leftrightarrow ⟨n, y⟩ \in J [(1 \dots K)]$
126	122 125	bitr4di	$⊢ x \in \{n\} \to (⟨x, y⟩ \in J [(1 \dots K)] \leftrightarrow y \in J [(1 \dots K)] [\{n\}])$
127	126	pm5.32i	$⊢ (x \in \{n\} \land ⟨x, y⟩ \in J [(1 \dots K)]) \leftrightarrow (x \in \{n\} \land y \in J [(1 \dots K)] [\{n\}])$
128	124	opelresi	$⊢ ⟨x, y⟩ \in ({J [(1 \dots K)] ↾}_{\{n\}}) \leftrightarrow (x \in \{n\} \land ⟨x, y⟩ \in J [(1 \dots K)])$
129		opelxp	$⊢ ⟨x, y⟩ \in (\{n\} \times J [(1 \dots K)] [\{n\}]) \leftrightarrow (x \in \{n\} \land y \in J [(1 \dots K)] [\{n\}])$
130	127 128 129	3bitr4ri	$⊢ ⟨x, y⟩ \in (\{n\} \times J [(1 \dots K)] [\{n\}]) \leftrightarrow ⟨x, y⟩ \in ({J [(1 \dots K)] ↾}_{\{n\}})$
131	118 119 130	eqrelriiv	$⊢ \{n\} \times J [(1 \dots K)] [\{n\}] = {J [(1 \dots K)] ↾}_{\{n\}}$
132		df-res	$⊢ {J [(1 \dots K)] ↾}_{\{n\}} = J [(1 \dots K)] \cap (\{n\} \times V)$
133	131 132	eqtri	$⊢ \{n\} \times J [(1 \dots K)] [\{n\}] = J [(1 \dots K)] \cap (\{n\} \times V)$
134	133	a1i	$⊢ (φ \land n \in (1 \dots L)) \to \{n\} \times J [(1 \dots K)] [\{n\}] = J [(1 \dots K)] \cap (\{n\} \times V)$
135	134	iuneq2dv	$⊢ φ \to ⋃_{n = 1}^{L} (\{n\} \times J [(1 \dots K)] [\{n\}]) = ⋃_{n = 1}^{L} (J [(1 \dots K)] \cap (\{n\} \times V))$
136		iunin2	$⊢ ⋃_{n = 1}^{L} (J [(1 \dots K)] \cap (\{n\} \times V)) = J [(1 \dots K)] \cap ⋃_{n = 1}^{L} (\{n\} \times V)$
137	135 136	eqtrdi	$⊢ φ \to ⋃_{n = 1}^{L} (\{n\} \times J [(1 \dots K)] [\{n\}]) = J [(1 \dots K)] \cap ⋃_{n = 1}^{L} (\{n\} \times V)$
138		relxp	$⊢ Rel (ℕ \times ℕ)$
139		relss	$⊢ J [(1 \dots K)] \subseteq ℕ \times ℕ \to (Rel (ℕ \times ℕ) \to Rel J [(1 \dots K)])$
140	36 138 139	mpisyl	$⊢ φ \to Rel J [(1 \dots K)]$
141	34	ffnd	$⊢ φ \to J Fn ℕ$
142		fveq2	$⊢ j = J (w) \to 1^{st} (j) = 1^{st} (J (w))$
143	142	breq1d	$⊢ j = J (w) \to (1^{st} (j) \leq L \leftrightarrow 1^{st} (J (w)) \leq L)$
144	143	ralima	$⊢ (J Fn ℕ \land (1 \dots K) \subseteq ℕ) \to (\forall j \in J [(1 \dots K)] 1^{st} (j) \leq L \leftrightarrow \forall w \in (1 \dots K) 1^{st} (J (w)) \leq L)$
145	141 26 144	sylancl	$⊢ φ \to (\forall j \in J [(1 \dots K)] 1^{st} (j) \leq L \leftrightarrow \forall w \in (1 \dots K) 1^{st} (J (w)) \leq L)$
146	16 145	mpbird	$⊢ φ \to \forall j \in J [(1 \dots K)] 1^{st} (j) \leq L$
147	146	r19.21bi	$⊢ (φ \land j \in J [(1 \dots K)]) \to 1^{st} (j) \leq L$
148	39 81	eleqtrdi	$⊢ (φ \land j \in J [(1 \dots K)]) \to 1^{st} (j) \in ℤ_{\geq 1}$
149	15	adantr	$⊢ (φ \land j \in J [(1 \dots K)]) \to L \in ℤ$
150		elfz5	$⊢ (1^{st} (j) \in ℤ_{\geq 1} \land L \in ℤ) \to (1^{st} (j) \in (1 \dots L) \leftrightarrow 1^{st} (j) \leq L)$
151	148 149 150	syl2anc	$⊢ (φ \land j \in J [(1 \dots K)]) \to (1^{st} (j) \in (1 \dots L) \leftrightarrow 1^{st} (j) \leq L)$
152	147 151	mpbird	$⊢ (φ \land j \in J [(1 \dots K)]) \to 1^{st} (j) \in (1 \dots L)$
153	152	ralrimiva	$⊢ φ \to \forall j \in J [(1 \dots K)] 1^{st} (j) \in (1 \dots L)$
154		vex	$⊢ x \in V$
155	154 124	op1std	$⊢ j = ⟨x, y⟩ \to 1^{st} (j) = x$
156	155	eleq1d	$⊢ j = ⟨x, y⟩ \to (1^{st} (j) \in (1 \dots L) \leftrightarrow x \in (1 \dots L))$
157	156	rspccv	$⊢ \forall j \in J [(1 \dots K)] 1^{st} (j) \in (1 \dots L) \to (⟨x, y⟩ \in J [(1 \dots K)] \to x \in (1 \dots L))$
158	153 157	syl	$⊢ φ \to (⟨x, y⟩ \in J [(1 \dots K)] \to x \in (1 \dots L))$
159		opelxp	$⊢ ⟨x, y⟩ \in (⋃_{n = 1}^{L} \{n\} \times V) \leftrightarrow (x \in ⋃_{n = 1}^{L} \{n\} \land y \in V)$
160	124	biantru	$⊢ x \in ⋃_{n = 1}^{L} \{n\} \leftrightarrow (x \in ⋃_{n = 1}^{L} \{n\} \land y \in V)$
161		iunid	$⊢ ⋃_{n = 1}^{L} \{n\} = (1 \dots L)$
162	161	eleq2i	$⊢ x \in ⋃_{n = 1}^{L} \{n\} \leftrightarrow x \in (1 \dots L)$
163	159 160 162	3bitr2i	$⊢ ⟨x, y⟩ \in (⋃_{n = 1}^{L} \{n\} \times V) \leftrightarrow x \in (1 \dots L)$
164	158 163	syl6ibr	$⊢ φ \to (⟨x, y⟩ \in J [(1 \dots K)] \to ⟨x, y⟩ \in (⋃_{n = 1}^{L} \{n\} \times V))$
165	140 164	relssdv	$⊢ φ \to J [(1 \dots K)] \subseteq ⋃_{n = 1}^{L} \{n\} \times V$
166		xpiundir	$⊢ ⋃_{n = 1}^{L} \{n\} \times V = ⋃_{n = 1}^{L} (\{n\} \times V)$
167	165 166	sseqtrdi	$⊢ φ \to J [(1 \dots K)] \subseteq ⋃_{n = 1}^{L} (\{n\} \times V)$
168		df-ss	$⊢ J [(1 \dots K)] \subseteq ⋃_{n = 1}^{L} (\{n\} \times V) \leftrightarrow J [(1 \dots K)] \cap ⋃_{n = 1}^{L} (\{n\} \times V) = J [(1 \dots K)]$
169	167 168	sylib	$⊢ φ \to J [(1 \dots K)] \cap ⋃_{n = 1}^{L} (\{n\} \times V) = J [(1 \dots K)]$
170	137 169	eqtrd	$⊢ φ \to ⋃_{n = 1}^{L} (\{n\} \times J [(1 \dots K)] [\{n\}]) = J [(1 \dots K)]$
171	170 101	eqeltrd	$⊢ φ \to ⋃_{n = 1}^{L} (\{n\} \times J [(1 \dots K)] [\{n\}]) \in Fin$
172		ssiun2	$⊢ n \in (1 \dots L) \to \{n\} \times J [(1 \dots K)] [\{n\}] \subseteq ⋃_{n = 1}^{L} (\{n\} \times J [(1 \dots K)] [\{n\}])$
173		ssfi	$⊢ (⋃_{n = 1}^{L} (\{n\} \times J [(1 \dots K)] [\{n\}]) \in Fin \land \{n\} \times J [(1 \dots K)] [\{n\}] \subseteq ⋃_{n = 1}^{L} (\{n\} \times J [(1 \dots K)] [\{n\}])) \to \{n\} \times J [(1 \dots K)] [\{n\}] \in Fin$
174	171 172 173	syl2an	$⊢ (φ \land n \in (1 \dots L)) \to \{n\} \times J [(1 \dots K)] [\{n\}] \in Fin$
175		2ndconst	$⊢ n \in V \to ({2^{nd} ↾}_{(\{n\} \times J [(1 \dots K)] [\{n\}])}) : \{n\} \times J [(1 \dots K)] [\{n\}] \underset{1-1 onto}{⟶} J [(1 \dots K)] [\{n\}]$
176	175	elv	$⊢ ({2^{nd} ↾}_{(\{n\} \times J [(1 \dots K)] [\{n\}])}) : \{n\} \times J [(1 \dots K)] [\{n\}] \underset{1-1 onto}{⟶} J [(1 \dots K)] [\{n\}]$
177		f1oeng	$⊢ (\{n\} \times J [(1 \dots K)] [\{n\}] \in Fin \land ({2^{nd} ↾}_{(\{n\} \times J [(1 \dots K)] [\{n\}])}) : \{n\} \times J [(1 \dots K)] [\{n\}] \underset{1-1 onto}{⟶} J [(1 \dots K)] [\{n\}]) \to (\{n\} \times J [(1 \dots K)] [\{n\}]) \approx J [(1 \dots K)] [\{n\}]$
178	174 176 177	sylancl	$⊢ (φ \land n \in (1 \dots L)) \to (\{n\} \times J [(1 \dots K)] [\{n\}]) \approx J [(1 \dots K)] [\{n\}]$
179	178	ensymd	$⊢ (φ \land n \in (1 \dots L)) \to J [(1 \dots K)] [\{n\}] \approx (\{n\} \times J [(1 \dots K)] [\{n\}])$
180		enfii	$⊢ (\{n\} \times J [(1 \dots K)] [\{n\}] \in Fin \land J [(1 \dots K)] [\{n\}] \approx (\{n\} \times J [(1 \dots K)] [\{n\}])) \to J [(1 \dots K)] [\{n\}] \in Fin$
181	174 179 180	syl2anc	$⊢ (φ \land n \in (1 \dots L)) \to J [(1 \dots K)] [\{n\}] \in Fin$
182		ffvelcdm	$⊢ (F : ℕ ⟶ {(\leq \cap ℝ^{2})}^{ℕ} \land n \in ℕ) \to F (n) \in ({(\leq \cap ℝ^{2})}^{ℕ})$
183	11 104 182	syl2an	$⊢ (φ \land n \in (1 \dots L)) \to F (n) \in ({(\leq \cap ℝ^{2})}^{ℕ})$
184		elovolmlem	$⊢ F (n) \in ({(\leq \cap ℝ^{2})}^{ℕ}) \leftrightarrow F (n) : ℕ ⟶ \leq \cap ℝ^{2}$
185	183 184	sylib	$⊢ (φ \land n \in (1 \dots L)) \to F (n) : ℕ ⟶ \leq \cap ℝ^{2}$
186	185	adantrr	$⊢ (φ \land (n \in (1 \dots L) \land i \in J [(1 \dots K)] [\{n\}])) \to F (n) : ℕ ⟶ \leq \cap ℝ^{2}$
187		imassrn	$⊢ J [(1 \dots K)] [\{n\}] \subseteq ran J [(1 \dots K)]$
188	36	adantr	$⊢ (φ \land n \in (1 \dots L)) \to J [(1 \dots K)] \subseteq ℕ \times ℕ$
189		rnss	$⊢ J [(1 \dots K)] \subseteq ℕ \times ℕ \to ran J [(1 \dots K)] \subseteq ran (ℕ \times ℕ)$
190	188 189	syl	$⊢ (φ \land n \in (1 \dots L)) \to ran J [(1 \dots K)] \subseteq ran (ℕ \times ℕ)$
191		rnxpid	$⊢ ran (ℕ \times ℕ) = ℕ$
192	190 191	sseqtrdi	$⊢ (φ \land n \in (1 \dots L)) \to ran J [(1 \dots K)] \subseteq ℕ$
193	187 192	sstrid	$⊢ (φ \land n \in (1 \dots L)) \to J [(1 \dots K)] [\{n\}] \subseteq ℕ$
194	193	sseld	$⊢ (φ \land n \in (1 \dots L)) \to (i \in J [(1 \dots K)] [\{n\}] \to i \in ℕ)$
195	194	impr	$⊢ (φ \land (n \in (1 \dots L) \land i \in J [(1 \dots K)] [\{n\}])) \to i \in ℕ$
196	186 195	ffvelcdmd	$⊢ (φ \land (n \in (1 \dots L) \land i \in J [(1 \dots K)] [\{n\}])) \to F (n) (i) \in (\leq \cap ℝ^{2})$
197	196	elin2d	$⊢ (φ \land (n \in (1 \dots L) \land i \in J [(1 \dots K)] [\{n\}])) \to F (n) (i) \in ℝ^{2}$
198		xp2nd	$⊢ F (n) (i) \in ℝ^{2} \to 2^{nd} (F (n) (i)) \in ℝ$
199	197 198	syl	$⊢ (φ \land (n \in (1 \dots L) \land i \in J [(1 \dots K)] [\{n\}])) \to 2^{nd} (F (n) (i)) \in ℝ$
200		xp1st	$⊢ F (n) (i) \in ℝ^{2} \to 1^{st} (F (n) (i)) \in ℝ$
201	197 200	syl	$⊢ (φ \land (n \in (1 \dots L) \land i \in J [(1 \dots K)] [\{n\}])) \to 1^{st} (F (n) (i)) \in ℝ$
202	199 201	resubcld	$⊢ (φ \land (n \in (1 \dots L) \land i \in J [(1 \dots K)] [\{n\}])) \to 2^{nd} (F (n) (i)) - 1^{st} (F (n) (i)) \in ℝ$
203	202	anassrs	$⊢ ((φ \land n \in (1 \dots L)) \land i \in J [(1 \dots K)] [\{n\}]) \to 2^{nd} (F (n) (i)) - 1^{st} (F (n) (i)) \in ℝ$
204	181 203	fsumrecl	$⊢ (φ \land n \in (1 \dots L)) \to \sum_{i \in J [(1 \dots K)] [\{n\}]} (2^{nd} (F (n) (i)) - 1^{st} (F (n) (i))) \in ℝ$
205	107 111 113	syl2an	$⊢ (φ \land n \in ℕ) \to \frac{B}{2^{n}} \in ℝ$
206	4 205	readdcld	$⊢ (φ \land n \in ℕ) \to {vol}^{*} (A) + (\frac{B}{2^{n}}) \in ℝ$
207	104 206	sylan2	$⊢ (φ \land n \in (1 \dots L)) \to {vol}^{*} (A) + (\frac{B}{2^{n}}) \in ℝ$
208		eqid	$⊢ (abs \circ -) \circ F (n) = (abs \circ -) \circ F (n)$
209	208 7	ovolsf	$⊢ F (n) : ℕ ⟶ \leq \cap ℝ^{2} \to S : ℕ ⟶ [0, +∞)$
210	185 209	syl	$⊢ (φ \land n \in (1 \dots L)) \to S : ℕ ⟶ [0, +∞)$
211	210	frnd	$⊢ (φ \land n \in (1 \dots L)) \to ran S \subseteq [0, +∞)$
212		icossxr	$⊢ [0, +∞) \subseteq ℝ^{*}$
213	211 212	sstrdi	$⊢ (φ \land n \in (1 \dots L)) \to ran S \subseteq ℝ^{*}$
214		supxrcl	$⊢ ran S \subseteq ℝ^{} \to sup (ran S ℝ^{} <) \in ℝ^{*}$
215	213 214	syl	$⊢ (φ \land n \in (1 \dots L)) \to sup (ran S ℝ^{} <) \in ℝ^{}$
216		mnfxr	$⊢ −∞ \in ℝ^{*}$
217	216	a1i	$⊢ (φ \land n \in (1 \dots L)) \to −∞ \in ℝ^{*}$
218	105	rexrd	$⊢ (φ \land n \in (1 \dots L)) \to {vol}^{} (A) \in ℝ^{}$
219	105	mnfltd	$⊢ (φ \land n \in (1 \dots L)) \to −∞ < {vol}^{*} (A)$
220	104 12	sylan2	$⊢ (φ \land n \in (1 \dots L)) \to A \subseteq ⋃ ran ((.) \circ F (n))$
221	7	ovollb	$⊢ (F (n) : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ((.) \circ F (n))) \to {vol}^{} (A) \leq sup (ran S ℝ^{} <)$
222	185 220 221	syl2anc	$⊢ (φ \land n \in (1 \dots L)) \to {vol}^{} (A) \leq sup (ran S ℝ^{} <)$
223	217 218 215 219 222	xrltletrd	$⊢ (φ \land n \in (1 \dots L)) \to −∞ < sup (ran S ℝ^{*} <)$
224	104 13	sylan2	$⊢ (φ \land n \in (1 \dots L)) \to sup (ran S ℝ^{} <) \leq {vol}^{} (A) + (\frac{B}{2^{n}})$
225		xrre	$⊢ ((sup (ran S ℝ^{} <) \in ℝ^{} \land {vol}^{} (A) + (\frac{B}{2^{n}}) \in ℝ) \land (−∞ < sup (ran S ℝ^{} <) \land sup (ran S ℝ^{} <) \leq {vol}^{} (A) + (\frac{B}{2^{n}}))) \to sup (ran S ℝ^{*} <) \in ℝ$
226	215 207 223 224 225	syl22anc	$⊢ (φ \land n \in (1 \dots L)) \to sup (ran S ℝ^{*} <) \in ℝ$
227		1zzd	$⊢ (φ \land n \in (1 \dots L)) \to 1 \in ℤ$
228	208	ovolfsval	$⊢ (F (n) : ℕ ⟶ \leq \cap ℝ^{2} \land i \in ℕ) \to ((abs \circ -) \circ F (n)) (i) = 2^{nd} (F (n) (i)) - 1^{st} (F (n) (i))$
229	185 228	sylan	$⊢ ((φ \land n \in (1 \dots L)) \land i \in ℕ) \to ((abs \circ -) \circ F (n)) (i) = 2^{nd} (F (n) (i)) - 1^{st} (F (n) (i))$
230	208	ovolfsf	$⊢ F (n) : ℕ ⟶ \leq \cap ℝ^{2} \to ((abs \circ -) \circ F (n)) : ℕ ⟶ [0, +∞)$
231	185 230	syl	$⊢ (φ \land n \in (1 \dots L)) \to ((abs \circ -) \circ F (n)) : ℕ ⟶ [0, +∞)$
232	231	ffvelcdmda	$⊢ ((φ \land n \in (1 \dots L)) \land i \in ℕ) \to ((abs \circ -) \circ F (n)) (i) \in [0, +∞)$
233	229 232	eqeltrrd	$⊢ ((φ \land n \in (1 \dots L)) \land i \in ℕ) \to 2^{nd} (F (n) (i)) - 1^{st} (F (n) (i)) \in [0, +∞)$
234		elrege0	$⊢ 2^{nd} (F (n) (i)) - 1^{st} (F (n) (i)) \in [0, +∞) \leftrightarrow (2^{nd} (F (n) (i)) - 1^{st} (F (n) (i)) \in ℝ \land 0 \leq 2^{nd} (F (n) (i)) - 1^{st} (F (n) (i)))$
235	233 234	sylib	$⊢ ((φ \land n \in (1 \dots L)) \land i \in ℕ) \to (2^{nd} (F (n) (i)) - 1^{st} (F (n) (i)) \in ℝ \land 0 \leq 2^{nd} (F (n) (i)) - 1^{st} (F (n) (i)))$
236	235	simpld	$⊢ ((φ \land n \in (1 \dots L)) \land i \in ℕ) \to 2^{nd} (F (n) (i)) - 1^{st} (F (n) (i)) \in ℝ$
237	235	simprd	$⊢ ((φ \land n \in (1 \dots L)) \land i \in ℕ) \to 0 \leq 2^{nd} (F (n) (i)) - 1^{st} (F (n) (i))$
238		supxrub	$⊢ (ran S \subseteq ℝ^{} \land z \in ran S) \to z \leq sup (ran S ℝ^{} <)$
239	213 238	sylan	$⊢ ((φ \land n \in (1 \dots L)) \land z \in ran S) \to z \leq sup (ran S ℝ^{*} <)$
240	239	ralrimiva	$⊢ (φ \land n \in (1 \dots L)) \to \forall z \in ran S z \leq sup (ran S ℝ^{*} <)$
241		brralrspcev	$⊢ (sup (ran S ℝ^{} <) \in ℝ \land \forall z \in ran S z \leq sup (ran S ℝ^{} <)) \to \exists x \in ℝ \forall z \in ran S z \leq x$
242	226 240 241	syl2anc	$⊢ (φ \land n \in (1 \dots L)) \to \exists x \in ℝ \forall z \in ran S z \leq x$
243	210	ffnd	$⊢ (φ \land n \in (1 \dots L)) \to S Fn ℕ$
244		breq1	$⊢ z = S (k) \to (z \leq x \leftrightarrow S (k) \leq x)$
245	244	ralrn	$⊢ S Fn ℕ \to (\forall z \in ran S z \leq x \leftrightarrow \forall k \in ℕ S (k) \leq x)$
246	243 245	syl	$⊢ (φ \land n \in (1 \dots L)) \to (\forall z \in ran S z \leq x \leftrightarrow \forall k \in ℕ S (k) \leq x)$
247	246	rexbidv	$⊢ (φ \land n \in (1 \dots L)) \to (\exists x \in ℝ \forall z \in ran S z \leq x \leftrightarrow \exists x \in ℝ \forall k \in ℕ S (k) \leq x)$
248	242 247	mpbid	$⊢ (φ \land n \in (1 \dots L)) \to \exists x \in ℝ \forall k \in ℕ S (k) \leq x$
249	81 7 227 229 236 237 248	isumsup2	$⊢ (φ \land n \in (1 \dots L)) \to S ⇝ sup (ran S ℝ <)$
250	7 249	eqbrtrrid	$⊢ (φ \land n \in (1 \dots L)) \to seq 1 (+ ((abs \circ -) \circ F (n))) ⇝ sup (ran S ℝ <)$
251		climrel	$⊢ Rel ⇝$
252	251	releldmi	$⊢ seq 1 (+ ((abs \circ -) \circ F (n))) ⇝ sup (ran S ℝ <) \to seq 1 (+ ((abs \circ -) \circ F (n))) \in dom ⇝$
253	250 252	syl	$⊢ (φ \land n \in (1 \dots L)) \to seq 1 (+ ((abs \circ -) \circ F (n))) \in dom ⇝$
254	81 227 181 193 229 236 237 253	isumless	$⊢ (φ \land n \in (1 \dots L)) \to \sum_{i \in J [(1 \dots K)] [\{n\}]} (2^{nd} (F (n) (i)) - 1^{st} (F (n) (i))) \leq \sum_{i \in ℕ} (2^{nd} (F (n) (i)) - 1^{st} (F (n) (i)))$
255	81 7 227 229 236 237 248	isumsup	$⊢ (φ \land n \in (1 \dots L)) \to \sum_{i \in ℕ} (2^{nd} (F (n) (i)) - 1^{st} (F (n) (i))) = sup (ran S ℝ <)$
256		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
257	211 256	sstrdi	$⊢ (φ \land n \in (1 \dots L)) \to ran S \subseteq ℝ$
258		1nn	$⊢ 1 \in ℕ$
259	210	fdmd	$⊢ (φ \land n \in (1 \dots L)) \to dom S = ℕ$
260	258 259	eleqtrrid	$⊢ (φ \land n \in (1 \dots L)) \to 1 \in dom S$
261	260	ne0d	$⊢ (φ \land n \in (1 \dots L)) \to dom S \neq \emptyset$
262		dm0rn0	$⊢ dom S = \emptyset \leftrightarrow ran S = \emptyset$
263	262	necon3bii	$⊢ dom S \neq \emptyset \leftrightarrow ran S \neq \emptyset$
264	261 263	sylib	$⊢ (φ \land n \in (1 \dots L)) \to ran S \neq \emptyset$
265		supxrre	$⊢ (ran S \subseteq ℝ \land ran S \neq \emptyset \land \exists x \in ℝ \forall z \in ran S z \leq x) \to sup (ran S ℝ^{*} <) = sup (ran S ℝ <)$
266	257 264 242 265	syl3anc	$⊢ (φ \land n \in (1 \dots L)) \to sup (ran S ℝ^{*} <) = sup (ran S ℝ <)$
267	255 266	eqtr4d	$⊢ (φ \land n \in (1 \dots L)) \to \sum_{i \in ℕ} (2^{nd} (F (n) (i)) - 1^{st} (F (n) (i))) = sup (ran S ℝ^{*} <)$
268	254 267	breqtrd	$⊢ (φ \land n \in (1 \dots L)) \to \sum_{i \in J [(1 \dots K)] [\{n\}]} (2^{nd} (F (n) (i)) - 1^{st} (F (n) (i))) \leq sup (ran S ℝ^{*} <)$
269	204 226 207 268 224	letrd	$⊢ (φ \land n \in (1 \dots L)) \to \sum_{i \in J [(1 \dots K)] [\{n\}]} (2^{nd} (F (n) (i)) - 1^{st} (F (n) (i))) \leq {vol}^{*} (A) + (\frac{B}{2^{n}})$
270	103 204 207 269	fsumle	$⊢ φ \to \sum_{n = 1}^{L} \sum_{i \in J [(1 \dots K)] [\{n\}]} (2^{nd} (F (n) (i)) - 1^{st} (F (n) (i))) \leq \sum_{n = 1}^{L} ({vol}^{*} (A) + (\frac{B}{2^{n}}))$
271		vex	$⊢ i \in V$
272	123 271	op1std	$⊢ j = ⟨n, i⟩ \to 1^{st} (j) = n$
273	272	fveq2d	$⊢ j = ⟨n, i⟩ \to F (1^{st} (j)) = F (n)$
274	123 271	op2ndd	$⊢ j = ⟨n, i⟩ \to 2^{nd} (j) = i$
275	273 274	fveq12d	$⊢ j = ⟨n, i⟩ \to F (1^{st} (j)) (2^{nd} (j)) = F (n) (i)$
276	275	fveq2d	$⊢ j = ⟨n, i⟩ \to 2^{nd} (F (1^{st} (j)) (2^{nd} (j))) = 2^{nd} (F (n) (i))$
277	275	fveq2d	$⊢ j = ⟨n, i⟩ \to 1^{st} (F (1^{st} (j)) (2^{nd} (j))) = 1^{st} (F (n) (i))$
278	276 277	oveq12d	$⊢ j = ⟨n, i⟩ \to 2^{nd} (F (1^{st} (j)) (2^{nd} (j))) - 1^{st} (F (1^{st} (j)) (2^{nd} (j))) = 2^{nd} (F (n) (i)) - 1^{st} (F (n) (i))$
279	202	recnd	$⊢ (φ \land (n \in (1 \dots L) \land i \in J [(1 \dots K)] [\{n\}])) \to 2^{nd} (F (n) (i)) - 1^{st} (F (n) (i)) \in ℂ$
280	278 103 181 279	fsum2d	$⊢ φ \to \sum_{n = 1}^{L} \sum_{i \in J [(1 \dots K)] [\{n\}]} (2^{nd} (F (n) (i)) - 1^{st} (F (n) (i))) = \sum_{j \in ⋃_{n = 1}^{L} (\{n\} \times J [(1 \dots K)] [\{n\}])} (2^{nd} (F (1^{st} (j)) (2^{nd} (j))) - 1^{st} (F (1^{st} (j)) (2^{nd} (j))))$
281	170	sumeq1d	$⊢ φ \to \sum_{j \in ⋃_{n = 1}^{L} (\{n\} \times J [(1 \dots K)] [\{n\}])} (2^{nd} (F (1^{st} (j)) (2^{nd} (j))) - 1^{st} (F (1^{st} (j)) (2^{nd} (j)))) = \sum_{j \in J [(1 \dots K)]} (2^{nd} (F (1^{st} (j)) (2^{nd} (j))) - 1^{st} (F (1^{st} (j)) (2^{nd} (j))))$
282	280 281	eqtrd	$⊢ φ \to \sum_{n = 1}^{L} \sum_{i \in J [(1 \dots K)] [\{n\}]} (2^{nd} (F (n) (i)) - 1^{st} (F (n) (i))) = \sum_{j \in J [(1 \dots K)]} (2^{nd} (F (1^{st} (j)) (2^{nd} (j))) - 1^{st} (F (1^{st} (j)) (2^{nd} (j))))$
283	105	recnd	$⊢ (φ \land n \in (1 \dots L)) \to {vol}^{*} (A) \in ℂ$
284	114	recnd	$⊢ (φ \land n \in (1 \dots L)) \to \frac{B}{2^{n}} \in ℂ$
285	103 283 284	fsumadd	$⊢ φ \to \sum_{n = 1}^{L} ({vol}^{} (A) + (\frac{B}{2^{n}})) = \sum_{n = 1}^{L} {vol}^{} (A) + \sum_{n = 1}^{L} (\frac{B}{2^{n}})$
286	270 282 285	3brtr3d	$⊢ φ \to \sum_{j \in J [(1 \dots K)]} (2^{nd} (F (1^{st} (j)) (2^{nd} (j))) - 1^{st} (F (1^{st} (j)) (2^{nd} (j)))) \leq \sum_{n = 1}^{L} {vol}^{*} (A) + \sum_{n = 1}^{L} (\frac{B}{2^{n}})$
287		1zzd	$⊢ φ \to 1 \in ℤ$
288		simpr	$⊢ (φ \land n \in ℕ) \to n \in ℕ$
289	2	fvmpt2	$⊢ (n \in ℕ \land {vol}^{} (A) \in ℝ) \to G (n) = {vol}^{} (A)$
290	288 4 289	syl2anc	$⊢ (φ \land n \in ℕ) \to G (n) = {vol}^{*} (A)$
291	290 4	eqeltrd	$⊢ (φ \land n \in ℕ) \to G (n) \in ℝ$
292	81 287 291	serfre	$⊢ φ \to seq 1 (+ G) : ℕ ⟶ ℝ$
293	1	feq1i	$⊢ T : ℕ ⟶ ℝ \leftrightarrow seq 1 (+ G) : ℕ ⟶ ℝ$
294	292 293	sylibr	$⊢ φ \to T : ℕ ⟶ ℝ$
295	294	frnd	$⊢ φ \to ran T \subseteq ℝ$
296		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
297	295 296	sstrdi	$⊢ φ \to ran T \subseteq ℝ^{*}$
298	104 290	sylan2	$⊢ (φ \land n \in (1 \dots L)) \to G (n) = {vol}^{*} (A)$
299		1red	$⊢ φ \to 1 \in ℝ$
300		ffvelcdm	$⊢ (J : ℕ ⟶ ℕ \times ℕ \land 1 \in ℕ) \to J (1) \in (ℕ \times ℕ)$
301	34 258 300	sylancl	$⊢ φ \to J (1) \in (ℕ \times ℕ)$
302		xp1st	$⊢ J (1) \in (ℕ \times ℕ) \to 1^{st} (J (1)) \in ℕ$
303	301 302	syl	$⊢ φ \to 1^{st} (J (1)) \in ℕ$
304	303	nnred	$⊢ φ \to 1^{st} (J (1)) \in ℝ$
305	15	zred	$⊢ φ \to L \in ℝ$
306	303	nnge1d	$⊢ φ \to 1 \leq 1^{st} (J (1))$
307		2fveq3	$⊢ w = 1 \to 1^{st} (J (w)) = 1^{st} (J (1))$
308	307	breq1d	$⊢ w = 1 \to (1^{st} (J (w)) \leq L \leftrightarrow 1^{st} (J (1)) \leq L)$
309		eluzfz1	$⊢ K \in ℤ_{\geq 1} \to 1 \in (1 \dots K)$
310	82 309	syl	$⊢ φ \to 1 \in (1 \dots K)$
311	308 16 310	rspcdva	$⊢ φ \to 1^{st} (J (1)) \leq L$
312	299 304 305 306 311	letrd	$⊢ φ \to 1 \leq L$
313		elnnz1	$⊢ L \in ℕ \leftrightarrow (L \in ℤ \land 1 \leq L)$
314	15 312 313	sylanbrc	$⊢ φ \to L \in ℕ$
315	314 81	eleqtrdi	$⊢ φ \to L \in ℤ_{\geq 1}$
316	298 315 283	fsumser	$⊢ φ \to \sum_{n = 1}^{L} {vol}^{*} (A) = seq 1 (+ G) (L)$
317		seqfn	$⊢ 1 \in ℤ \to seq 1 (+ G) Fn ℤ_{\geq 1}$
318	287 317	syl	$⊢ φ \to seq 1 (+ G) Fn ℤ_{\geq 1}$
319		fnfvelrn	$⊢ (seq 1 (+ G) Fn ℤ_{\geq 1} \land L \in ℤ_{\geq 1}) \to seq 1 (+ G) (L) \in ran seq 1 (+ G)$
320	318 315 319	syl2anc	$⊢ φ \to seq 1 (+ G) (L) \in ran seq 1 (+ G)$
321	1	rneqi	$⊢ ran T = ran seq 1 (+ G)$
322	320 321	eleqtrrdi	$⊢ φ \to seq 1 (+ G) (L) \in ran T$
323	316 322	eqeltrd	$⊢ φ \to \sum_{n = 1}^{L} {vol}^{*} (A) \in ran T$
324		supxrub	$⊢ (ran T \subseteq ℝ^{} \land \sum_{n = 1}^{L} {vol}^{} (A) \in ran T) \to \sum_{n = 1}^{L} {vol}^{} (A) \leq sup (ran T ℝ^{} <)$
325	297 323 324	syl2anc	$⊢ φ \to \sum_{n = 1}^{L} {vol}^{} (A) \leq sup (ran T ℝ^{} <)$
326	107	recnd	$⊢ φ \to B \in ℂ$
327		geo2sum	$⊢ (L \in ℕ \land B \in ℂ) \to \sum_{n = 1}^{L} (\frac{B}{2^{n}}) = B - (\frac{B}{2^{L}})$
328	314 326 327	syl2anc	$⊢ φ \to \sum_{n = 1}^{L} (\frac{B}{2^{n}}) = B - (\frac{B}{2^{L}})$
329	314	nnnn0d	$⊢ φ \to L \in ℕ_{0}$
330		nnexpcl	$⊢ (2 \in ℕ \land L \in ℕ_{0}) \to 2^{L} \in ℕ$
331	108 329 330	sylancr	$⊢ φ \to 2^{L} \in ℕ$
332	331	nnrpd	$⊢ φ \to 2^{L} \in ℝ^{+}$
333	6 332	rpdivcld	$⊢ φ \to \frac{B}{2^{L}} \in ℝ^{+}$
334	333	rpge0d	$⊢ φ \to 0 \leq \frac{B}{2^{L}}$
335	107 331	nndivred	$⊢ φ \to \frac{B}{2^{L}} \in ℝ$
336	107 335	subge02d	$⊢ φ \to (0 \leq \frac{B}{2^{L}} \leftrightarrow B - (\frac{B}{2^{L}}) \leq B)$
337	334 336	mpbid	$⊢ φ \to B - (\frac{B}{2^{L}}) \leq B$
338	328 337	eqbrtrd	$⊢ φ \to \sum_{n = 1}^{L} (\frac{B}{2^{n}}) \leq B$
339	106 115 5 107 325 338	le2addd	$⊢ φ \to \sum_{n = 1}^{L} {vol}^{} (A) + \sum_{n = 1}^{L} (\frac{B}{2^{n}}) \leq sup (ran T ℝ^{} <) + B$
340	102 116 117 286 339	letrd	$⊢ φ \to \sum_{j \in J [(1 \dots K)]} (2^{nd} (F (1^{st} (j)) (2^{nd} (j))) - 1^{st} (F (1^{st} (j)) (2^{nd} (j)))) \leq sup (ran T ℝ^{*} <) + B$
341	96 340	eqbrtrrd	$⊢ φ \to U (K) \leq sup (ran T ℝ^{*} <) + B$

Metamath Proof Explorer

Theorem ovoliunlem1

Proof