ovollb2lem

	Ref	Expression
Hypotheses	ovollb2.1	$⊢ S = seq 1 (+ ((abs \circ -) \circ F))$
	ovollb2.2	$⊢ G = (n \in ℕ ⟼ ⟨1^{st} (F (n)) - (\frac{\frac{B}{2}}{2^{n}}), 2^{nd} (F (n)) + (\frac{\frac{B}{2}}{2^{n}})⟩)$
	ovollb2.3	$⊢ T = seq 1 (+ ((abs \circ -) \circ G))$
	ovollb2.4	$⊢ φ \to F : ℕ ⟶ \leq \cap ℝ^{2}$
	ovollb2.5	$⊢ φ \to A \subseteq ⋃ ran ([.] \circ F)$
	ovollb2.6	$⊢ φ \to B \in ℝ^{+}$
	ovollb2.7	$⊢ φ \to sup (ran S ℝ^{*} <) \in ℝ$
Assertion	ovollb2lem	$⊢ φ \to {vol}^{} (A) \leq sup (ran S ℝ^{} <) + B$

Proof

Step	Hyp	Ref	Expression
1		ovollb2.1	$⊢ S = seq 1 (+ ((abs \circ -) \circ F))$
2		ovollb2.2	$⊢ G = (n \in ℕ ⟼ ⟨1^{st} (F (n)) - (\frac{\frac{B}{2}}{2^{n}}), 2^{nd} (F (n)) + (\frac{\frac{B}{2}}{2^{n}})⟩)$
3		ovollb2.3	$⊢ T = seq 1 (+ ((abs \circ -) \circ G))$
4		ovollb2.4	$⊢ φ \to F : ℕ ⟶ \leq \cap ℝ^{2}$
5		ovollb2.5	$⊢ φ \to A \subseteq ⋃ ran ([.] \circ F)$
6		ovollb2.6	$⊢ φ \to B \in ℝ^{+}$
7		ovollb2.7	$⊢ φ \to sup (ran S ℝ^{*} <) \in ℝ$
8		ovolficcss	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to ⋃ ran ([.] \circ F) \subseteq ℝ$
9	4 8	syl	$⊢ φ \to ⋃ ran ([.] \circ F) \subseteq ℝ$
10	5 9	sstrd	$⊢ φ \to A \subseteq ℝ$
11		ovolcl	$⊢ A \subseteq ℝ \to {vol}^{} (A) \in ℝ^{}$
12	10 11	syl	$⊢ φ \to {vol}^{} (A) \in ℝ^{}$
13		ovolfcl	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land n \in ℕ) \to (1^{st} (F (n)) \in ℝ \land 2^{nd} (F (n)) \in ℝ \land 1^{st} (F (n)) \leq 2^{nd} (F (n)))$
14	4 13	sylan	$⊢ (φ \land n \in ℕ) \to (1^{st} (F (n)) \in ℝ \land 2^{nd} (F (n)) \in ℝ \land 1^{st} (F (n)) \leq 2^{nd} (F (n)))$
15	14	simp1d	$⊢ (φ \land n \in ℕ) \to 1^{st} (F (n)) \in ℝ$
16	6	rphalfcld	$⊢ φ \to \frac{B}{2} \in ℝ^{+}$
17	16	adantr	$⊢ (φ \land n \in ℕ) \to \frac{B}{2} \in ℝ^{+}$
18		2nn	$⊢ 2 \in ℕ$
19		nnnn0	$⊢ n \in ℕ \to n \in ℕ_{0}$
20	19	adantl	$⊢ (φ \land n \in ℕ) \to n \in ℕ_{0}$
21		nnexpcl	$⊢ (2 \in ℕ \land n \in ℕ_{0}) \to 2^{n} \in ℕ$
22	18 20 21	sylancr	$⊢ (φ \land n \in ℕ) \to 2^{n} \in ℕ$
23	22	nnrpd	$⊢ (φ \land n \in ℕ) \to 2^{n} \in ℝ^{+}$
24	17 23	rpdivcld	$⊢ (φ \land n \in ℕ) \to \frac{\frac{B}{2}}{2^{n}} \in ℝ^{+}$
25	24	rpred	$⊢ (φ \land n \in ℕ) \to \frac{\frac{B}{2}}{2^{n}} \in ℝ$
26	15 25	resubcld	$⊢ (φ \land n \in ℕ) \to 1^{st} (F (n)) - (\frac{\frac{B}{2}}{2^{n}}) \in ℝ$
27	14	simp2d	$⊢ (φ \land n \in ℕ) \to 2^{nd} (F (n)) \in ℝ$
28	27 25	readdcld	$⊢ (φ \land n \in ℕ) \to 2^{nd} (F (n)) + (\frac{\frac{B}{2}}{2^{n}}) \in ℝ$
29	15 24	ltsubrpd	$⊢ (φ \land n \in ℕ) \to 1^{st} (F (n)) - (\frac{\frac{B}{2}}{2^{n}}) < 1^{st} (F (n))$
30	14	simp3d	$⊢ (φ \land n \in ℕ) \to 1^{st} (F (n)) \leq 2^{nd} (F (n))$
31	27 24	ltaddrpd	$⊢ (φ \land n \in ℕ) \to 2^{nd} (F (n)) < 2^{nd} (F (n)) + (\frac{\frac{B}{2}}{2^{n}})$
32	15 27 28 30 31	lelttrd	$⊢ (φ \land n \in ℕ) \to 1^{st} (F (n)) < 2^{nd} (F (n)) + (\frac{\frac{B}{2}}{2^{n}})$
33	26 15 28 29 32	lttrd	$⊢ (φ \land n \in ℕ) \to 1^{st} (F (n)) - (\frac{\frac{B}{2}}{2^{n}}) < 2^{nd} (F (n)) + (\frac{\frac{B}{2}}{2^{n}})$
34	26 28 33	ltled	$⊢ (φ \land n \in ℕ) \to 1^{st} (F (n)) - (\frac{\frac{B}{2}}{2^{n}}) \leq 2^{nd} (F (n)) + (\frac{\frac{B}{2}}{2^{n}})$
35		df-br	$⊢ 1^{st} (F (n)) - (\frac{\frac{B}{2}}{2^{n}}) \leq 2^{nd} (F (n)) + (\frac{\frac{B}{2}}{2^{n}}) \leftrightarrow ⟨1^{st} (F (n)) - (\frac{\frac{B}{2}}{2^{n}}), 2^{nd} (F (n)) + (\frac{\frac{B}{2}}{2^{n}})⟩ \in \leq$
36	34 35	sylib	$⊢ (φ \land n \in ℕ) \to ⟨1^{st} (F (n)) - (\frac{\frac{B}{2}}{2^{n}}), 2^{nd} (F (n)) + (\frac{\frac{B}{2}}{2^{n}})⟩ \in \leq$
37	26 28	opelxpd	$⊢ (φ \land n \in ℕ) \to ⟨1^{st} (F (n)) - (\frac{\frac{B}{2}}{2^{n}}), 2^{nd} (F (n)) + (\frac{\frac{B}{2}}{2^{n}})⟩ \in ℝ^{2}$
38	36 37	elind	$⊢ (φ \land n \in ℕ) \to ⟨1^{st} (F (n)) - (\frac{\frac{B}{2}}{2^{n}}), 2^{nd} (F (n)) + (\frac{\frac{B}{2}}{2^{n}})⟩ \in (\leq \cap ℝ^{2})$
39	38 2	fmptd	$⊢ φ \to G : ℕ ⟶ \leq \cap ℝ^{2}$
40		eqid	$⊢ (abs \circ -) \circ G = (abs \circ -) \circ G$
41	40 3	ovolsf	$⊢ G : ℕ ⟶ \leq \cap ℝ^{2} \to T : ℕ ⟶ [0, +∞)$
42	39 41	syl	$⊢ φ \to T : ℕ ⟶ [0, +∞)$
43	42	frnd	$⊢ φ \to ran T \subseteq [0, +∞)$
44		icossxr	$⊢ [0, +∞) \subseteq ℝ^{*}$
45	43 44	sstrdi	$⊢ φ \to ran T \subseteq ℝ^{*}$
46		supxrcl	$⊢ ran T \subseteq ℝ^{} \to sup (ran T ℝ^{} <) \in ℝ^{*}$
47	45 46	syl	$⊢ φ \to sup (ran T ℝ^{} <) \in ℝ^{}$
48	6	rpred	$⊢ φ \to B \in ℝ$
49	7 48	readdcld	$⊢ φ \to sup (ran S ℝ^{*} <) + B \in ℝ$
50	49	rexrd	$⊢ φ \to sup (ran S ℝ^{} <) + B \in ℝ^{}$
51		2fveq3	$⊢ n = m \to 1^{st} (F (n)) = 1^{st} (F (m))$
52		oveq2	$⊢ n = m \to 2^{n} = 2^{m}$
53	52	oveq2d	$⊢ n = m \to \frac{\frac{B}{2}}{2^{n}} = \frac{\frac{B}{2}}{2^{m}}$
54	51 53	oveq12d	$⊢ n = m \to 1^{st} (F (n)) - (\frac{\frac{B}{2}}{2^{n}}) = 1^{st} (F (m)) - (\frac{\frac{B}{2}}{2^{m}})$
55		2fveq3	$⊢ n = m \to 2^{nd} (F (n)) = 2^{nd} (F (m))$
56	55 53	oveq12d	$⊢ n = m \to 2^{nd} (F (n)) + (\frac{\frac{B}{2}}{2^{n}}) = 2^{nd} (F (m)) + (\frac{\frac{B}{2}}{2^{m}})$
57	54 56	opeq12d	$⊢ n = m \to ⟨1^{st} (F (n)) - (\frac{\frac{B}{2}}{2^{n}}), 2^{nd} (F (n)) + (\frac{\frac{B}{2}}{2^{n}})⟩ = ⟨1^{st} (F (m)) - (\frac{\frac{B}{2}}{2^{m}}), 2^{nd} (F (m)) + (\frac{\frac{B}{2}}{2^{m}})⟩$
58		opex	$⊢ ⟨1^{st} (F (m)) - (\frac{\frac{B}{2}}{2^{m}}), 2^{nd} (F (m)) + (\frac{\frac{B}{2}}{2^{m}})⟩ \in V$
59	57 2 58	fvmpt	$⊢ m \in ℕ \to G (m) = ⟨1^{st} (F (m)) - (\frac{\frac{B}{2}}{2^{m}}), 2^{nd} (F (m)) + (\frac{\frac{B}{2}}{2^{m}})⟩$
60	59	adantl	$⊢ (φ \land m \in ℕ) \to G (m) = ⟨1^{st} (F (m)) - (\frac{\frac{B}{2}}{2^{m}}), 2^{nd} (F (m)) + (\frac{\frac{B}{2}}{2^{m}})⟩$
61	60	fveq2d	$⊢ (φ \land m \in ℕ) \to 1^{st} (G (m)) = 1^{st} (⟨1^{st} (F (m)) - (\frac{\frac{B}{2}}{2^{m}}), 2^{nd} (F (m)) + (\frac{\frac{B}{2}}{2^{m}})⟩)$
62		ovex	$⊢ 1^{st} (F (m)) - (\frac{\frac{B}{2}}{2^{m}}) \in V$
63		ovex	$⊢ 2^{nd} (F (m)) + (\frac{\frac{B}{2}}{2^{m}}) \in V$
64	62 63	op1st	$⊢ 1^{st} (⟨1^{st} (F (m)) - (\frac{\frac{B}{2}}{2^{m}}), 2^{nd} (F (m)) + (\frac{\frac{B}{2}}{2^{m}})⟩) = 1^{st} (F (m)) - (\frac{\frac{B}{2}}{2^{m}})$
65	61 64	eqtrdi	$⊢ (φ \land m \in ℕ) \to 1^{st} (G (m)) = 1^{st} (F (m)) - (\frac{\frac{B}{2}}{2^{m}})$
66		ovolfcl	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land m \in ℕ) \to (1^{st} (F (m)) \in ℝ \land 2^{nd} (F (m)) \in ℝ \land 1^{st} (F (m)) \leq 2^{nd} (F (m)))$
67	4 66	sylan	$⊢ (φ \land m \in ℕ) \to (1^{st} (F (m)) \in ℝ \land 2^{nd} (F (m)) \in ℝ \land 1^{st} (F (m)) \leq 2^{nd} (F (m)))$
68	67	simp1d	$⊢ (φ \land m \in ℕ) \to 1^{st} (F (m)) \in ℝ$
69	16	adantr	$⊢ (φ \land m \in ℕ) \to \frac{B}{2} \in ℝ^{+}$
70		nnnn0	$⊢ m \in ℕ \to m \in ℕ_{0}$
71	70	adantl	$⊢ (φ \land m \in ℕ) \to m \in ℕ_{0}$
72		nnexpcl	$⊢ (2 \in ℕ \land m \in ℕ_{0}) \to 2^{m} \in ℕ$
73	18 71 72	sylancr	$⊢ (φ \land m \in ℕ) \to 2^{m} \in ℕ$
74	73	nnrpd	$⊢ (φ \land m \in ℕ) \to 2^{m} \in ℝ^{+}$
75	69 74	rpdivcld	$⊢ (φ \land m \in ℕ) \to \frac{\frac{B}{2}}{2^{m}} \in ℝ^{+}$
76	68 75	ltsubrpd	$⊢ (φ \land m \in ℕ) \to 1^{st} (F (m)) - (\frac{\frac{B}{2}}{2^{m}}) < 1^{st} (F (m))$
77	65 76	eqbrtrd	$⊢ (φ \land m \in ℕ) \to 1^{st} (G (m)) < 1^{st} (F (m))$
78	77	adantlr	$⊢ ((φ \land z \in A) \land m \in ℕ) \to 1^{st} (G (m)) < 1^{st} (F (m))$
79		ovolfcl	$⊢ (G : ℕ ⟶ \leq \cap ℝ^{2} \land m \in ℕ) \to (1^{st} (G (m)) \in ℝ \land 2^{nd} (G (m)) \in ℝ \land 1^{st} (G (m)) \leq 2^{nd} (G (m)))$
80	39 79	sylan	$⊢ (φ \land m \in ℕ) \to (1^{st} (G (m)) \in ℝ \land 2^{nd} (G (m)) \in ℝ \land 1^{st} (G (m)) \leq 2^{nd} (G (m)))$
81	80	simp1d	$⊢ (φ \land m \in ℕ) \to 1^{st} (G (m)) \in ℝ$
82	81	adantlr	$⊢ ((φ \land z \in A) \land m \in ℕ) \to 1^{st} (G (m)) \in ℝ$
83	68	adantlr	$⊢ ((φ \land z \in A) \land m \in ℕ) \to 1^{st} (F (m)) \in ℝ$
84	10	sselda	$⊢ (φ \land z \in A) \to z \in ℝ$
85	84	adantr	$⊢ ((φ \land z \in A) \land m \in ℕ) \to z \in ℝ$
86		ltletr	$⊢ (1^{st} (G (m)) \in ℝ \land 1^{st} (F (m)) \in ℝ \land z \in ℝ) \to ((1^{st} (G (m)) < 1^{st} (F (m)) \land 1^{st} (F (m)) \leq z) \to 1^{st} (G (m)) < z)$
87	82 83 85 86	syl3anc	$⊢ ((φ \land z \in A) \land m \in ℕ) \to ((1^{st} (G (m)) < 1^{st} (F (m)) \land 1^{st} (F (m)) \leq z) \to 1^{st} (G (m)) < z)$
88	78 87	mpand	$⊢ ((φ \land z \in A) \land m \in ℕ) \to (1^{st} (F (m)) \leq z \to 1^{st} (G (m)) < z)$
89	67	simp2d	$⊢ (φ \land m \in ℕ) \to 2^{nd} (F (m)) \in ℝ$
90	89 75	ltaddrpd	$⊢ (φ \land m \in ℕ) \to 2^{nd} (F (m)) < 2^{nd} (F (m)) + (\frac{\frac{B}{2}}{2^{m}})$
91	60	fveq2d	$⊢ (φ \land m \in ℕ) \to 2^{nd} (G (m)) = 2^{nd} (⟨1^{st} (F (m)) - (\frac{\frac{B}{2}}{2^{m}}), 2^{nd} (F (m)) + (\frac{\frac{B}{2}}{2^{m}})⟩)$
92	62 63	op2nd	$⊢ 2^{nd} (⟨1^{st} (F (m)) - (\frac{\frac{B}{2}}{2^{m}}), 2^{nd} (F (m)) + (\frac{\frac{B}{2}}{2^{m}})⟩) = 2^{nd} (F (m)) + (\frac{\frac{B}{2}}{2^{m}})$
93	91 92	eqtrdi	$⊢ (φ \land m \in ℕ) \to 2^{nd} (G (m)) = 2^{nd} (F (m)) + (\frac{\frac{B}{2}}{2^{m}})$
94	90 93	breqtrrd	$⊢ (φ \land m \in ℕ) \to 2^{nd} (F (m)) < 2^{nd} (G (m))$
95	94	adantlr	$⊢ ((φ \land z \in A) \land m \in ℕ) \to 2^{nd} (F (m)) < 2^{nd} (G (m))$
96	89	adantlr	$⊢ ((φ \land z \in A) \land m \in ℕ) \to 2^{nd} (F (m)) \in ℝ$
97	80	simp2d	$⊢ (φ \land m \in ℕ) \to 2^{nd} (G (m)) \in ℝ$
98	97	adantlr	$⊢ ((φ \land z \in A) \land m \in ℕ) \to 2^{nd} (G (m)) \in ℝ$
99		lelttr	$⊢ (z \in ℝ \land 2^{nd} (F (m)) \in ℝ \land 2^{nd} (G (m)) \in ℝ) \to ((z \leq 2^{nd} (F (m)) \land 2^{nd} (F (m)) < 2^{nd} (G (m))) \to z < 2^{nd} (G (m)))$
100	85 96 98 99	syl3anc	$⊢ ((φ \land z \in A) \land m \in ℕ) \to ((z \leq 2^{nd} (F (m)) \land 2^{nd} (F (m)) < 2^{nd} (G (m))) \to z < 2^{nd} (G (m)))$
101	95 100	mpan2d	$⊢ ((φ \land z \in A) \land m \in ℕ) \to (z \leq 2^{nd} (F (m)) \to z < 2^{nd} (G (m)))$
102	88 101	anim12d	$⊢ ((φ \land z \in A) \land m \in ℕ) \to ((1^{st} (F (m)) \leq z \land z \leq 2^{nd} (F (m))) \to (1^{st} (G (m)) < z \land z < 2^{nd} (G (m))))$
103	102	reximdva	$⊢ (φ \land z \in A) \to (\exists m \in ℕ (1^{st} (F (m)) \leq z \land z \leq 2^{nd} (F (m))) \to \exists m \in ℕ (1^{st} (G (m)) < z \land z < 2^{nd} (G (m))))$
104	103	ralimdva	$⊢ φ \to (\forall z \in A \exists m \in ℕ (1^{st} (F (m)) \leq z \land z \leq 2^{nd} (F (m))) \to \forall z \in A \exists m \in ℕ (1^{st} (G (m)) < z \land z < 2^{nd} (G (m))))$
105		ovolficc	$⊢ (A \subseteq ℝ \land F : ℕ ⟶ \leq \cap ℝ^{2}) \to (A \subseteq ⋃ ran ([.] \circ F) \leftrightarrow \forall z \in A \exists m \in ℕ (1^{st} (F (m)) \leq z \land z \leq 2^{nd} (F (m))))$
106	10 4 105	syl2anc	$⊢ φ \to (A \subseteq ⋃ ran ([.] \circ F) \leftrightarrow \forall z \in A \exists m \in ℕ (1^{st} (F (m)) \leq z \land z \leq 2^{nd} (F (m))))$
107		ovolfioo	$⊢ (A \subseteq ℝ \land G : ℕ ⟶ \leq \cap ℝ^{2}) \to (A \subseteq ⋃ ran ((.) \circ G) \leftrightarrow \forall z \in A \exists m \in ℕ (1^{st} (G (m)) < z \land z < 2^{nd} (G (m))))$
108	10 39 107	syl2anc	$⊢ φ \to (A \subseteq ⋃ ran ((.) \circ G) \leftrightarrow \forall z \in A \exists m \in ℕ (1^{st} (G (m)) < z \land z < 2^{nd} (G (m))))$
109	104 106 108	3imtr4d	$⊢ φ \to (A \subseteq ⋃ ran ([.] \circ F) \to A \subseteq ⋃ ran ((.) \circ G))$
110	5 109	mpd	$⊢ φ \to A \subseteq ⋃ ran ((.) \circ G)$
111	3	ovollb	$⊢ (G : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ((.) \circ G)) \to {vol}^{} (A) \leq sup (ran T ℝ^{} <)$
112	39 110 111	syl2anc	$⊢ φ \to {vol}^{} (A) \leq sup (ran T ℝ^{} <)$
113	3	fveq1i	$⊢ T (k) = seq 1 (+ ((abs \circ -) \circ G)) (k)$
114		fzfid	$⊢ (φ \land k \in ℕ) \to (1 \dots k) \in Fin$
115		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
116		eqid	$⊢ (abs \circ -) \circ F = (abs \circ -) \circ F$
117	116	ovolfsf	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to ((abs \circ -) \circ F) : ℕ ⟶ [0, +∞)$
118	4 117	syl	$⊢ φ \to ((abs \circ -) \circ F) : ℕ ⟶ [0, +∞)$
119	118	adantr	$⊢ (φ \land k \in ℕ) \to ((abs \circ -) \circ F) : ℕ ⟶ [0, +∞)$
120		elfznn	$⊢ m \in (1 \dots k) \to m \in ℕ$
121		ffvelcdm	$⊢ (((abs \circ -) \circ F) : ℕ ⟶ [0, +∞) \land m \in ℕ) \to ((abs \circ -) \circ F) (m) \in [0, +∞)$
122	119 120 121	syl2an	$⊢ ((φ \land k \in ℕ) \land m \in (1 \dots k)) \to ((abs \circ -) \circ F) (m) \in [0, +∞)$
123	115 122	sselid	$⊢ ((φ \land k \in ℕ) \land m \in (1 \dots k)) \to ((abs \circ -) \circ F) (m) \in ℝ$
124	123	recnd	$⊢ ((φ \land k \in ℕ) \land m \in (1 \dots k)) \to ((abs \circ -) \circ F) (m) \in ℂ$
125	6	adantr	$⊢ (φ \land m \in ℕ) \to B \in ℝ^{+}$
126	125 74	rpdivcld	$⊢ (φ \land m \in ℕ) \to \frac{B}{2^{m}} \in ℝ^{+}$
127	126	rpcnd	$⊢ (φ \land m \in ℕ) \to \frac{B}{2^{m}} \in ℂ$
128	120 127	sylan2	$⊢ (φ \land m \in (1 \dots k)) \to \frac{B}{2^{m}} \in ℂ$
129	128	adantlr	$⊢ ((φ \land k \in ℕ) \land m \in (1 \dots k)) \to \frac{B}{2^{m}} \in ℂ$
130	114 124 129	fsumadd	$⊢ (φ \land k \in ℕ) \to \sum_{m = 1}^{k} (((abs \circ -) \circ F) (m) + (\frac{B}{2^{m}})) = \sum_{m = 1}^{k} ((abs \circ -) \circ F) (m) + \sum_{m = 1}^{k} (\frac{B}{2^{m}})$
131	40	ovolfsval	$⊢ (G : ℕ ⟶ \leq \cap ℝ^{2} \land m \in ℕ) \to ((abs \circ -) \circ G) (m) = 2^{nd} (G (m)) - 1^{st} (G (m))$
132	39 131	sylan	$⊢ (φ \land m \in ℕ) \to ((abs \circ -) \circ G) (m) = 2^{nd} (G (m)) - 1^{st} (G (m))$
133	89	recnd	$⊢ (φ \land m \in ℕ) \to 2^{nd} (F (m)) \in ℂ$
134	75	rpcnd	$⊢ (φ \land m \in ℕ) \to \frac{\frac{B}{2}}{2^{m}} \in ℂ$
135	68	recnd	$⊢ (φ \land m \in ℕ) \to 1^{st} (F (m)) \in ℂ$
136	135 134	subcld	$⊢ (φ \land m \in ℕ) \to 1^{st} (F (m)) - (\frac{\frac{B}{2}}{2^{m}}) \in ℂ$
137	133 134 136	addsubassd	$⊢ (φ \land m \in ℕ) \to 2^{nd} (F (m)) + (\frac{\frac{B}{2}}{2^{m}}) - (1^{st} (F (m)) - (\frac{\frac{B}{2}}{2^{m}})) = 2^{nd} (F (m)) + (\frac{\frac{B}{2}}{2^{m}}) - (1^{st} (F (m)) - (\frac{\frac{B}{2}}{2^{m}}))$
138	93 65	oveq12d	$⊢ (φ \land m \in ℕ) \to 2^{nd} (G (m)) - 1^{st} (G (m)) = 2^{nd} (F (m)) + (\frac{\frac{B}{2}}{2^{m}}) - (1^{st} (F (m)) - (\frac{\frac{B}{2}}{2^{m}}))$
139	133 135 127	subadd23d	$⊢ (φ \land m \in ℕ) \to 2^{nd} (F (m)) - 1^{st} (F (m)) + (\frac{B}{2^{m}}) = 2^{nd} (F (m)) + (\frac{B}{2^{m}}) - 1^{st} (F (m))$
140	116	ovolfsval	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land m \in ℕ) \to ((abs \circ -) \circ F) (m) = 2^{nd} (F (m)) - 1^{st} (F (m))$
141	4 140	sylan	$⊢ (φ \land m \in ℕ) \to ((abs \circ -) \circ F) (m) = 2^{nd} (F (m)) - 1^{st} (F (m))$
142	141	oveq1d	$⊢ (φ \land m \in ℕ) \to ((abs \circ -) \circ F) (m) + (\frac{B}{2^{m}}) = 2^{nd} (F (m)) - 1^{st} (F (m)) + (\frac{B}{2^{m}})$
143	134 135 134	subsub3d	$⊢ (φ \land m \in ℕ) \to (\frac{\frac{B}{2}}{2^{m}}) - (1^{st} (F (m)) - (\frac{\frac{B}{2}}{2^{m}})) = (\frac{\frac{B}{2}}{2^{m}}) + (\frac{\frac{B}{2}}{2^{m}}) - 1^{st} (F (m))$
144	69	rpcnd	$⊢ (φ \land m \in ℕ) \to \frac{B}{2} \in ℂ$
145	73	nncnd	$⊢ (φ \land m \in ℕ) \to 2^{m} \in ℂ$
146	73	nnne0d	$⊢ (φ \land m \in ℕ) \to 2^{m} \neq 0$
147	144 144 145 146	divdird	$⊢ (φ \land m \in ℕ) \to \frac{(\frac{B}{2}) + (\frac{B}{2})}{2^{m}} = (\frac{\frac{B}{2}}{2^{m}}) + (\frac{\frac{B}{2}}{2^{m}})$
148	125	rpcnd	$⊢ (φ \land m \in ℕ) \to B \in ℂ$
149	148	2halvesd	$⊢ (φ \land m \in ℕ) \to (\frac{B}{2}) + (\frac{B}{2}) = B$
150	149	oveq1d	$⊢ (φ \land m \in ℕ) \to \frac{(\frac{B}{2}) + (\frac{B}{2})}{2^{m}} = \frac{B}{2^{m}}$
151	147 150	eqtr3d	$⊢ (φ \land m \in ℕ) \to (\frac{\frac{B}{2}}{2^{m}}) + (\frac{\frac{B}{2}}{2^{m}}) = \frac{B}{2^{m}}$
152	151	oveq1d	$⊢ (φ \land m \in ℕ) \to (\frac{\frac{B}{2}}{2^{m}}) + (\frac{\frac{B}{2}}{2^{m}}) - 1^{st} (F (m)) = (\frac{B}{2^{m}}) - 1^{st} (F (m))$
153	143 152	eqtrd	$⊢ (φ \land m \in ℕ) \to (\frac{\frac{B}{2}}{2^{m}}) - (1^{st} (F (m)) - (\frac{\frac{B}{2}}{2^{m}})) = (\frac{B}{2^{m}}) - 1^{st} (F (m))$
154	153	oveq2d	$⊢ (φ \land m \in ℕ) \to 2^{nd} (F (m)) + (\frac{\frac{B}{2}}{2^{m}}) - (1^{st} (F (m)) - (\frac{\frac{B}{2}}{2^{m}})) = 2^{nd} (F (m)) + (\frac{B}{2^{m}}) - 1^{st} (F (m))$
155	139 142 154	3eqtr4d	$⊢ (φ \land m \in ℕ) \to ((abs \circ -) \circ F) (m) + (\frac{B}{2^{m}}) = 2^{nd} (F (m)) + (\frac{\frac{B}{2}}{2^{m}}) - (1^{st} (F (m)) - (\frac{\frac{B}{2}}{2^{m}}))$
156	137 138 155	3eqtr4d	$⊢ (φ \land m \in ℕ) \to 2^{nd} (G (m)) - 1^{st} (G (m)) = ((abs \circ -) \circ F) (m) + (\frac{B}{2^{m}})$
157	132 156	eqtrd	$⊢ (φ \land m \in ℕ) \to ((abs \circ -) \circ G) (m) = ((abs \circ -) \circ F) (m) + (\frac{B}{2^{m}})$
158	120 157	sylan2	$⊢ (φ \land m \in (1 \dots k)) \to ((abs \circ -) \circ G) (m) = ((abs \circ -) \circ F) (m) + (\frac{B}{2^{m}})$
159	158	adantlr	$⊢ ((φ \land k \in ℕ) \land m \in (1 \dots k)) \to ((abs \circ -) \circ G) (m) = ((abs \circ -) \circ F) (m) + (\frac{B}{2^{m}})$
160		simpr	$⊢ (φ \land k \in ℕ) \to k \in ℕ$
161		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
162	160 161	eleqtrdi	$⊢ (φ \land k \in ℕ) \to k \in ℤ_{\geq 1}$
163	124 129	addcld	$⊢ ((φ \land k \in ℕ) \land m \in (1 \dots k)) \to ((abs \circ -) \circ F) (m) + (\frac{B}{2^{m}}) \in ℂ$
164	159 162 163	fsumser	$⊢ (φ \land k \in ℕ) \to \sum_{m = 1}^{k} (((abs \circ -) \circ F) (m) + (\frac{B}{2^{m}})) = seq 1 (+ ((abs \circ -) \circ G)) (k)$
165		eqidd	$⊢ ((φ \land k \in ℕ) \land m \in (1 \dots k)) \to ((abs \circ -) \circ F) (m) = ((abs \circ -) \circ F) (m)$
166	165 162 124	fsumser	$⊢ (φ \land k \in ℕ) \to \sum_{m = 1}^{k} ((abs \circ -) \circ F) (m) = seq 1 (+ ((abs \circ -) \circ F)) (k)$
167	1	fveq1i	$⊢ S (k) = seq 1 (+ ((abs \circ -) \circ F)) (k)$
168	166 167	eqtr4di	$⊢ (φ \land k \in ℕ) \to \sum_{m = 1}^{k} ((abs \circ -) \circ F) (m) = S (k)$
169	6	adantr	$⊢ (φ \land k \in ℕ) \to B \in ℝ^{+}$
170	169	rpcnd	$⊢ (φ \land k \in ℕ) \to B \in ℂ$
171		geo2sum	$⊢ (k \in ℕ \land B \in ℂ) \to \sum_{m = 1}^{k} (\frac{B}{2^{m}}) = B - (\frac{B}{2^{k}})$
172	160 170 171	syl2anc	$⊢ (φ \land k \in ℕ) \to \sum_{m = 1}^{k} (\frac{B}{2^{m}}) = B - (\frac{B}{2^{k}})$
173	168 172	oveq12d	$⊢ (φ \land k \in ℕ) \to \sum_{m = 1}^{k} ((abs \circ -) \circ F) (m) + \sum_{m = 1}^{k} (\frac{B}{2^{m}}) = S (k) + B - (\frac{B}{2^{k}})$
174	130 164 173	3eqtr3d	$⊢ (φ \land k \in ℕ) \to seq 1 (+ ((abs \circ -) \circ G)) (k) = S (k) + B - (\frac{B}{2^{k}})$
175	113 174	eqtrid	$⊢ (φ \land k \in ℕ) \to T (k) = S (k) + B - (\frac{B}{2^{k}})$
176	116 1	ovolsf	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to S : ℕ ⟶ [0, +∞)$
177	4 176	syl	$⊢ φ \to S : ℕ ⟶ [0, +∞)$
178	177	ffvelcdmda	$⊢ (φ \land k \in ℕ) \to S (k) \in [0, +∞)$
179	115 178	sselid	$⊢ (φ \land k \in ℕ) \to S (k) \in ℝ$
180	169	rpred	$⊢ (φ \land k \in ℕ) \to B \in ℝ$
181		nnnn0	$⊢ k \in ℕ \to k \in ℕ_{0}$
182	181	adantl	$⊢ (φ \land k \in ℕ) \to k \in ℕ_{0}$
183		nnexpcl	$⊢ (2 \in ℕ \land k \in ℕ_{0}) \to 2^{k} \in ℕ$
184	18 182 183	sylancr	$⊢ (φ \land k \in ℕ) \to 2^{k} \in ℕ$
185	184	nnrpd	$⊢ (φ \land k \in ℕ) \to 2^{k} \in ℝ^{+}$
186	169 185	rpdivcld	$⊢ (φ \land k \in ℕ) \to \frac{B}{2^{k}} \in ℝ^{+}$
187	186	rpred	$⊢ (φ \land k \in ℕ) \to \frac{B}{2^{k}} \in ℝ$
188	180 187	resubcld	$⊢ (φ \land k \in ℕ) \to B - (\frac{B}{2^{k}}) \in ℝ$
189	7	adantr	$⊢ (φ \land k \in ℕ) \to sup (ran S ℝ^{*} <) \in ℝ$
190	177	frnd	$⊢ φ \to ran S \subseteq [0, +∞)$
191	190 44	sstrdi	$⊢ φ \to ran S \subseteq ℝ^{*}$
192	191	adantr	$⊢ (φ \land k \in ℕ) \to ran S \subseteq ℝ^{*}$
193	177	ffnd	$⊢ φ \to S Fn ℕ$
194		fnfvelrn	$⊢ (S Fn ℕ \land k \in ℕ) \to S (k) \in ran S$
195	193 194	sylan	$⊢ (φ \land k \in ℕ) \to S (k) \in ran S$
196		supxrub	$⊢ (ran S \subseteq ℝ^{} \land S (k) \in ran S) \to S (k) \leq sup (ran S ℝ^{} <)$
197	192 195 196	syl2anc	$⊢ (φ \land k \in ℕ) \to S (k) \leq sup (ran S ℝ^{*} <)$
198	180 186	ltsubrpd	$⊢ (φ \land k \in ℕ) \to B - (\frac{B}{2^{k}}) < B$
199	188 180 198	ltled	$⊢ (φ \land k \in ℕ) \to B - (\frac{B}{2^{k}}) \leq B$
200	179 188 189 180 197 199	le2addd	$⊢ (φ \land k \in ℕ) \to S (k) + B - (\frac{B}{2^{k}}) \leq sup (ran S ℝ^{*} <) + B$
201	175 200	eqbrtrd	$⊢ (φ \land k \in ℕ) \to T (k) \leq sup (ran S ℝ^{*} <) + B$
202	201	ralrimiva	$⊢ φ \to \forall k \in ℕ T (k) \leq sup (ran S ℝ^{*} <) + B$
203		ffn	$⊢ T : ℕ ⟶ [0, +∞) \to T Fn ℕ$
204		breq1	$⊢ y = T (k) \to (y \leq sup (ran S ℝ^{} <) + B \leftrightarrow T (k) \leq sup (ran S ℝ^{} <) + B)$
205	204	ralrn	$⊢ T Fn ℕ \to (\forall y \in ran T y \leq sup (ran S ℝ^{} <) + B \leftrightarrow \forall k \in ℕ T (k) \leq sup (ran S ℝ^{} <) + B)$
206	42 203 205	3syl	$⊢ φ \to (\forall y \in ran T y \leq sup (ran S ℝ^{} <) + B \leftrightarrow \forall k \in ℕ T (k) \leq sup (ran S ℝ^{} <) + B)$
207	202 206	mpbird	$⊢ φ \to \forall y \in ran T y \leq sup (ran S ℝ^{*} <) + B$
208		supxrleub	$⊢ (ran T \subseteq ℝ^{} \land sup (ran S ℝ^{} <) + B \in ℝ^{}) \to (sup (ran T ℝ^{} <) \leq sup (ran S ℝ^{} <) + B \leftrightarrow \forall y \in ran T y \leq sup (ran S ℝ^{} <) + B)$
209	45 50 208	syl2anc	$⊢ φ \to (sup (ran T ℝ^{} <) \leq sup (ran S ℝ^{} <) + B \leftrightarrow \forall y \in ran T y \leq sup (ran S ℝ^{*} <) + B)$
210	207 209	mpbird	$⊢ φ \to sup (ran T ℝ^{} <) \leq sup (ran S ℝ^{} <) + B$
211	12 47 50 112 210	xrletrd	$⊢ φ \to {vol}^{} (A) \leq sup (ran S ℝ^{} <) + B$

Metamath Proof Explorer

Theorem ovollb2lem

Proof