ovolval5lem2

Description: |- ( ( ph /\ n e. NN ) -> <. ( ( 1st( Fn ) ) - ( W / ( 2 ^ n ) ) ) , ( 2nd( Fn ) ) >. e. ( RR X. RR ) ) . (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	ovolval5lem2.q	$⊢ Q = \{z \in ℝ^{*} \| \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land z = sum^((vol \circ (.)) \circ f))\}$
	ovolval5lem2.y	$⊢ φ \to Y = sum^((vol \circ [.)) \circ F)$
	ovolval5lem2.z	$⊢ Z = sum^((vol \circ (.)) \circ G)$
	ovolval5lem2.f	$⊢ φ \to F : ℕ ⟶ ℝ^{2}$
	ovolval5lem2.s	$⊢ φ \to A \subseteq ⋃ ran ([.) \circ F)$
	ovolval5lem2.w	$⊢ φ \to W \in ℝ^{+}$
	ovolval5lem2.g	$⊢ G = (n \in ℕ ⟼ ⟨1^{st} (F (n)) - (\frac{W}{2^{n}}), 2^{nd} (F (n))⟩)$
Assertion	ovolval5lem2	$⊢ φ \to \exists z \in Q z \leq Y +_{𝑒} W$

Proof

Step	Hyp	Ref	Expression
1		ovolval5lem2.q	$⊢ Q = \{z \in ℝ^{*} \| \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land z = sum^((vol \circ (.)) \circ f))\}$
2		ovolval5lem2.y	$⊢ φ \to Y = sum^((vol \circ [.)) \circ F)$
3		ovolval5lem2.z	$⊢ Z = sum^((vol \circ (.)) \circ G)$
4		ovolval5lem2.f	$⊢ φ \to F : ℕ ⟶ ℝ^{2}$
5		ovolval5lem2.s	$⊢ φ \to A \subseteq ⋃ ran ([.) \circ F)$
6		ovolval5lem2.w	$⊢ φ \to W \in ℝ^{+}$
7		ovolval5lem2.g	$⊢ G = (n \in ℕ ⟼ ⟨1^{st} (F (n)) - (\frac{W}{2^{n}}), 2^{nd} (F (n))⟩)$
8	3	a1i	$⊢ φ \to Z = sum^((vol \circ (.)) \circ G)$
9		nnex	$⊢ ℕ \in V$
10	9	a1i	$⊢ φ \to ℕ \in V$
11		volioof	$⊢ (vol \circ (.)) : ℝ^{} \times ℝ^{} ⟶ [0, +∞]$
12	11	a1i	$⊢ φ \to (vol \circ (.)) : ℝ^{} \times ℝ^{} ⟶ [0, +∞]$
13		rexpssxrxp	$⊢ ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
14	13	a1i	$⊢ φ \to ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
15	4	ffvelrnda	$⊢ (φ \land n \in ℕ) \to F (n) \in ℝ^{2}$
16		xp1st	$⊢ F (n) \in ℝ^{2} \to 1^{st} (F (n)) \in ℝ$
17	15 16	syl	$⊢ (φ \land n \in ℕ) \to 1^{st} (F (n)) \in ℝ$
18	6	rpred	$⊢ φ \to W \in ℝ$
19	18	adantr	$⊢ (φ \land n \in ℕ) \to W \in ℝ$
20		2nn	$⊢ 2 \in ℕ$
21	20	a1i	$⊢ n \in ℕ \to 2 \in ℕ$
22		nnnn0	$⊢ n \in ℕ \to n \in ℕ_{0}$
23	21 22	nnexpcld	$⊢ n \in ℕ \to 2^{n} \in ℕ$
24	23	nnred	$⊢ n \in ℕ \to 2^{n} \in ℝ$
25	24	adantl	$⊢ (φ \land n \in ℕ) \to 2^{n} \in ℝ$
26	23	nnne0d	$⊢ n \in ℕ \to 2^{n} \neq 0$
27	26	adantl	$⊢ (φ \land n \in ℕ) \to 2^{n} \neq 0$
28	19 25 27	redivcld	$⊢ (φ \land n \in ℕ) \to \frac{W}{2^{n}} \in ℝ$
29	17 28	resubcld	$⊢ (φ \land n \in ℕ) \to 1^{st} (F (n)) - (\frac{W}{2^{n}}) \in ℝ$
30		xp2nd	$⊢ F (n) \in ℝ^{2} \to 2^{nd} (F (n)) \in ℝ$
31	15 30	syl	$⊢ (φ \land n \in ℕ) \to 2^{nd} (F (n)) \in ℝ$
32	29 31	opelxpd	$⊢ (φ \land n \in ℕ) \to ⟨1^{st} (F (n)) - (\frac{W}{2^{n}}), 2^{nd} (F (n))⟩ \in ℝ^{2}$
33	32 7	fmptd	$⊢ φ \to G : ℕ ⟶ ℝ^{2}$
34	12 14 33	fcoss	$⊢ φ \to ((vol \circ (.)) \circ G) : ℕ ⟶ [0, +∞]$
35	10 34	sge0xrcl	$⊢ φ \to sum^((vol \circ (.)) \circ G) \in ℝ^{*}$
36	8 35	eqeltrd	$⊢ φ \to Z \in ℝ^{*}$
37		reex	$⊢ ℝ \in V$
38	37 37	xpex	$⊢ ℝ^{2} \in V$
39	38	a1i	$⊢ φ \to ℝ^{2} \in V$
40	39 10	elmapd	$⊢ φ \to (G \in ({ℝ^{2}}^{ℕ}) \leftrightarrow G : ℕ ⟶ ℝ^{2})$
41	33 40	mpbird	$⊢ φ \to G \in ({ℝ^{2}}^{ℕ})$
42	33	ffvelrnda	$⊢ (φ \land n \in ℕ) \to G (n) \in ℝ^{2}$
43		xp1st	$⊢ G (n) \in ℝ^{2} \to 1^{st} (G (n)) \in ℝ$
44	42 43	syl	$⊢ (φ \land n \in ℕ) \to 1^{st} (G (n)) \in ℝ$
45	44	rexrd	$⊢ (φ \land n \in ℕ) \to 1^{st} (G (n)) \in ℝ^{*}$
46		xp2nd	$⊢ G (n) \in ℝ^{2} \to 2^{nd} (G (n)) \in ℝ$
47	42 46	syl	$⊢ (φ \land n \in ℕ) \to 2^{nd} (G (n)) \in ℝ$
48	47	rexrd	$⊢ (φ \land n \in ℕ) \to 2^{nd} (G (n)) \in ℝ^{*}$
49	6	adantr	$⊢ (φ \land n \in ℕ) \to W \in ℝ^{+}$
50	23	nnrpd	$⊢ n \in ℕ \to 2^{n} \in ℝ^{+}$
51	50	adantl	$⊢ (φ \land n \in ℕ) \to 2^{n} \in ℝ^{+}$
52	49 51	rpdivcld	$⊢ (φ \land n \in ℕ) \to \frac{W}{2^{n}} \in ℝ^{+}$
53	17 52	ltsubrpd	$⊢ (φ \land n \in ℕ) \to 1^{st} (F (n)) - (\frac{W}{2^{n}}) < 1^{st} (F (n))$
54		id	$⊢ n \in ℕ \to n \in ℕ$
55		opex	$⊢ ⟨1^{st} (F (n)) - (\frac{W}{2^{n}}), 2^{nd} (F (n))⟩ \in V$
56	55	a1i	$⊢ n \in ℕ \to ⟨1^{st} (F (n)) - (\frac{W}{2^{n}}), 2^{nd} (F (n))⟩ \in V$
57	7	fvmpt2	$⊢ (n \in ℕ \land ⟨1^{st} (F (n)) - (\frac{W}{2^{n}}), 2^{nd} (F (n))⟩ \in V) \to G (n) = ⟨1^{st} (F (n)) - (\frac{W}{2^{n}}), 2^{nd} (F (n))⟩$
58	54 56 57	syl2anc	$⊢ n \in ℕ \to G (n) = ⟨1^{st} (F (n)) - (\frac{W}{2^{n}}), 2^{nd} (F (n))⟩$
59	58	fveq2d	$⊢ n \in ℕ \to 1^{st} (G (n)) = 1^{st} (⟨1^{st} (F (n)) - (\frac{W}{2^{n}}), 2^{nd} (F (n))⟩)$
60		ovex	$⊢ 1^{st} (F (n)) - (\frac{W}{2^{n}}) \in V$
61		fvex	$⊢ 2^{nd} (F (n)) \in V$
62		op1stg	$⊢ (1^{st} (F (n)) - (\frac{W}{2^{n}}) \in V \land 2^{nd} (F (n)) \in V) \to 1^{st} (⟨1^{st} (F (n)) - (\frac{W}{2^{n}}), 2^{nd} (F (n))⟩) = 1^{st} (F (n)) - (\frac{W}{2^{n}})$
63	60 61 62	mp2an	$⊢ 1^{st} (⟨1^{st} (F (n)) - (\frac{W}{2^{n}}), 2^{nd} (F (n))⟩) = 1^{st} (F (n)) - (\frac{W}{2^{n}})$
64	63	a1i	$⊢ n \in ℕ \to 1^{st} (⟨1^{st} (F (n)) - (\frac{W}{2^{n}}), 2^{nd} (F (n))⟩) = 1^{st} (F (n)) - (\frac{W}{2^{n}})$
65	59 64	eqtrd	$⊢ n \in ℕ \to 1^{st} (G (n)) = 1^{st} (F (n)) - (\frac{W}{2^{n}})$
66	65	adantl	$⊢ (φ \land n \in ℕ) \to 1^{st} (G (n)) = 1^{st} (F (n)) - (\frac{W}{2^{n}})$
67	66	breq1d	$⊢ (φ \land n \in ℕ) \to (1^{st} (G (n)) < 1^{st} (F (n)) \leftrightarrow 1^{st} (F (n)) - (\frac{W}{2^{n}}) < 1^{st} (F (n)))$
68	53 67	mpbird	$⊢ (φ \land n \in ℕ) \to 1^{st} (G (n)) < 1^{st} (F (n))$
69	58	fveq2d	$⊢ n \in ℕ \to 2^{nd} (G (n)) = 2^{nd} (⟨1^{st} (F (n)) - (\frac{W}{2^{n}}), 2^{nd} (F (n))⟩)$
70	60 61	op2nd	$⊢ 2^{nd} (⟨1^{st} (F (n)) - (\frac{W}{2^{n}}), 2^{nd} (F (n))⟩) = 2^{nd} (F (n))$
71	70	a1i	$⊢ n \in ℕ \to 2^{nd} (⟨1^{st} (F (n)) - (\frac{W}{2^{n}}), 2^{nd} (F (n))⟩) = 2^{nd} (F (n))$
72	69 71	eqtrd	$⊢ n \in ℕ \to 2^{nd} (G (n)) = 2^{nd} (F (n))$
73	72	adantl	$⊢ (φ \land n \in ℕ) \to 2^{nd} (G (n)) = 2^{nd} (F (n))$
74	73	eqcomd	$⊢ (φ \land n \in ℕ) \to 2^{nd} (F (n)) = 2^{nd} (G (n))$
75	31 74	eqled	$⊢ (φ \land n \in ℕ) \to 2^{nd} (F (n)) \leq 2^{nd} (G (n))$
76		icossioo	$⊢ ((1^{st} (G (n)) \in ℝ^{} \land 2^{nd} (G (n)) \in ℝ^{}) \land (1^{st} (G (n)) < 1^{st} (F (n)) \land 2^{nd} (F (n)) \leq 2^{nd} (G (n)))) \to [1^{st} (F (n)), 2^{nd} (F (n))) \subseteq (1^{st} (G (n)), 2^{nd} (G (n)))$
77	45 48 68 75 76	syl22anc	$⊢ (φ \land n \in ℕ) \to [1^{st} (F (n)), 2^{nd} (F (n))) \subseteq (1^{st} (G (n)), 2^{nd} (G (n)))$
78		1st2nd2	$⊢ F (n) \in ℝ^{2} \to F (n) = ⟨1^{st} (F (n)), 2^{nd} (F (n))⟩$
79	15 78	syl	$⊢ (φ \land n \in ℕ) \to F (n) = ⟨1^{st} (F (n)), 2^{nd} (F (n))⟩$
80	79	fveq2d	$⊢ (φ \land n \in ℕ) \to [.) (F (n)) = [.) (⟨1^{st} (F (n)), 2^{nd} (F (n))⟩)$
81		df-ov	$⊢ [1^{st} (F (n)), 2^{nd} (F (n))) = [.) (⟨1^{st} (F (n)), 2^{nd} (F (n))⟩)$
82	81	a1i	$⊢ (φ \land n \in ℕ) \to [1^{st} (F (n)), 2^{nd} (F (n))) = [.) (⟨1^{st} (F (n)), 2^{nd} (F (n))⟩)$
83	80 82	eqtr4d	$⊢ (φ \land n \in ℕ) \to [.) (F (n)) = [1^{st} (F (n)), 2^{nd} (F (n)))$
84		1st2nd2	$⊢ G (n) \in ℝ^{2} \to G (n) = ⟨1^{st} (G (n)), 2^{nd} (G (n))⟩$
85	42 84	syl	$⊢ (φ \land n \in ℕ) \to G (n) = ⟨1^{st} (G (n)), 2^{nd} (G (n))⟩$
86	85	fveq2d	$⊢ (φ \land n \in ℕ) \to (.) (G (n)) = (.) (⟨1^{st} (G (n)), 2^{nd} (G (n))⟩)$
87		df-ov	$⊢ (1^{st} (G (n)), 2^{nd} (G (n))) = (.) (⟨1^{st} (G (n)), 2^{nd} (G (n))⟩)$
88	87	a1i	$⊢ (φ \land n \in ℕ) \to (1^{st} (G (n)), 2^{nd} (G (n))) = (.) (⟨1^{st} (G (n)), 2^{nd} (G (n))⟩)$
89	86 88	eqtr4d	$⊢ (φ \land n \in ℕ) \to (.) (G (n)) = (1^{st} (G (n)), 2^{nd} (G (n)))$
90	83 89	sseq12d	$⊢ (φ \land n \in ℕ) \to ([.) (F (n)) \subseteq (.) (G (n)) \leftrightarrow [1^{st} (F (n)), 2^{nd} (F (n))) \subseteq (1^{st} (G (n)), 2^{nd} (G (n))))$
91	77 90	mpbird	$⊢ (φ \land n \in ℕ) \to [.) (F (n)) \subseteq (.) (G (n))$
92	91	ralrimiva	$⊢ φ \to \forall n \in ℕ [.) (F (n)) \subseteq (.) (G (n))$
93		ss2iun	$⊢ \forall n \in ℕ [.) (F (n)) \subseteq (.) (G (n)) \to ⋃_{n \in ℕ} [.) (F (n)) \subseteq ⋃_{n \in ℕ} (.) (G (n))$
94	92 93	syl	$⊢ φ \to ⋃_{n \in ℕ} [.) (F (n)) \subseteq ⋃_{n \in ℕ} (.) (G (n))$
95		fvex	$⊢ [.) (F (n)) \in V$
96	95	rgenw	$⊢ \forall n \in ℕ [.) (F (n)) \in V$
97	96	a1i	$⊢ φ \to \forall n \in ℕ [.) (F (n)) \in V$
98		dfiun3g	$⊢ \forall n \in ℕ [.) (F (n)) \in V \to ⋃_{n \in ℕ} [.) (F (n)) = ⋃ ran (n \in ℕ ⟼ [.) (F (n)))$
99	97 98	syl	$⊢ φ \to ⋃_{n \in ℕ} [.) (F (n)) = ⋃ ran (n \in ℕ ⟼ [.) (F (n)))$
100		icof	$⊢ [.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{*}$
101	100	a1i	$⊢ φ \to [.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{*}$
102	4 14 101	fcomptss	$⊢ φ \to [.) \circ F = (n \in ℕ ⟼ [.) (F (n)))$
103	102	eqcomd	$⊢ φ \to (n \in ℕ ⟼ [.) (F (n))) = [.) \circ F$
104	103	rneqd	$⊢ φ \to ran (n \in ℕ ⟼ [.) (F (n))) = ran ([.) \circ F)$
105	104	unieqd	$⊢ φ \to ⋃ ran (n \in ℕ ⟼ [.) (F (n))) = ⋃ ran ([.) \circ F)$
106	99 105	eqtr2d	$⊢ φ \to ⋃ ran ([.) \circ F) = ⋃_{n \in ℕ} [.) (F (n))$
107		fvex	$⊢ (.) (G (n)) \in V$
108	107	rgenw	$⊢ \forall n \in ℕ (.) (G (n)) \in V$
109	108	a1i	$⊢ φ \to \forall n \in ℕ (.) (G (n)) \in V$
110		dfiun3g	$⊢ \forall n \in ℕ (.) (G (n)) \in V \to ⋃_{n \in ℕ} (.) (G (n)) = ⋃ ran (n \in ℕ ⟼ (.) (G (n)))$
111	109 110	syl	$⊢ φ \to ⋃_{n \in ℕ} (.) (G (n)) = ⋃ ran (n \in ℕ ⟼ (.) (G (n)))$
112		ioof	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
113	112	a1i	$⊢ φ \to (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
114	33 14 113	fcomptss	$⊢ φ \to (.) \circ G = (n \in ℕ ⟼ (.) (G (n)))$
115	114	eqcomd	$⊢ φ \to (n \in ℕ ⟼ (.) (G (n))) = (.) \circ G$
116	115	rneqd	$⊢ φ \to ran (n \in ℕ ⟼ (.) (G (n))) = ran ((.) \circ G)$
117	116	unieqd	$⊢ φ \to ⋃ ran (n \in ℕ ⟼ (.) (G (n))) = ⋃ ran ((.) \circ G)$
118	111 117	eqtr2d	$⊢ φ \to ⋃ ran ((.) \circ G) = ⋃_{n \in ℕ} (.) (G (n))$
119	106 118	sseq12d	$⊢ φ \to (⋃ ran ([.) \circ F) \subseteq ⋃ ran ((.) \circ G) \leftrightarrow ⋃_{n \in ℕ} [.) (F (n)) \subseteq ⋃_{n \in ℕ} (.) (G (n)))$
120	94 119	mpbird	$⊢ φ \to ⋃ ran ([.) \circ F) \subseteq ⋃ ran ((.) \circ G)$
121	5 120	sstrd	$⊢ φ \to A \subseteq ⋃ ran ((.) \circ G)$
122	121 8	jca	$⊢ φ \to (A \subseteq ⋃ ran ((.) \circ G) \land Z = sum^((vol \circ (.)) \circ G))$
123		coeq2	$⊢ f = G \to (.) \circ f = (.) \circ G$
124	123	rneqd	$⊢ f = G \to ran ((.) \circ f) = ran ((.) \circ G)$
125	124	unieqd	$⊢ f = G \to ⋃ ran ((.) \circ f) = ⋃ ran ((.) \circ G)$
126	125	sseq2d	$⊢ f = G \to (A \subseteq ⋃ ran ((.) \circ f) \leftrightarrow A \subseteq ⋃ ran ((.) \circ G))$
127		coeq2	$⊢ f = G \to (vol \circ (.)) \circ f = (vol \circ (.)) \circ G$
128	127	fveq2d	$⊢ f = G \to sum^((vol \circ (.)) \circ f) = sum^((vol \circ (.)) \circ G)$
129	128	eqeq2d	$⊢ f = G \to (Z = sum^((vol \circ (.)) \circ f) \leftrightarrow Z = sum^((vol \circ (.)) \circ G))$
130	126 129	anbi12d	$⊢ f = G \to ((A \subseteq ⋃ ran ((.) \circ f) \land Z = sum^((vol \circ (.)) \circ f)) \leftrightarrow (A \subseteq ⋃ ran ((.) \circ G) \land Z = sum^((vol \circ (.)) \circ G)))$
131	130	rspcev	$⊢ (G \in ({ℝ^{2}}^{ℕ}) \land (A \subseteq ⋃ ran ((.) \circ G) \land Z = sum^((vol \circ (.)) \circ G))) \to \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land Z = sum^((vol \circ (.)) \circ f))$
132	41 122 131	syl2anc	$⊢ φ \to \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land Z = sum^((vol \circ (.)) \circ f))$
133	36 132	jca	$⊢ φ \to (Z \in ℝ^{*} \land \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land Z = sum^((vol \circ (.)) \circ f)))$
134		eqeq1	$⊢ z = Z \to (z = sum^((vol \circ (.)) \circ f) \leftrightarrow Z = sum^((vol \circ (.)) \circ f))$
135	134	anbi2d	$⊢ z = Z \to ((A \subseteq ⋃ ran ((.) \circ f) \land z = sum^((vol \circ (.)) \circ f)) \leftrightarrow (A \subseteq ⋃ ran ((.) \circ f) \land Z = sum^((vol \circ (.)) \circ f)))$
136	135	rexbidv	$⊢ z = Z \to (\exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land z = sum^((vol \circ (.)) \circ f)) \leftrightarrow \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land Z = sum^((vol \circ (.)) \circ f)))$
137	136 1	elrab2	$⊢ Z \in Q \leftrightarrow (Z \in ℝ^{*} \land \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land Z = sum^((vol \circ (.)) \circ f)))$
138	133 137	sylibr	$⊢ φ \to Z \in Q$
139		2fveq3	$⊢ m = n \to 1^{st} (F (m)) = 1^{st} (F (n))$
140		2fveq3	$⊢ m = n \to 2^{nd} (F (m)) = 2^{nd} (F (n))$
141	139 140	breq12d	$⊢ m = n \to (1^{st} (F (m)) < 2^{nd} (F (m)) \leftrightarrow 1^{st} (F (n)) < 2^{nd} (F (n)))$
142	141	cbvrabv	$⊢ \{m \in ℕ \| 1^{st} (F (m)) < 2^{nd} (F (m))\} = \{n \in ℕ \| 1^{st} (F (n)) < 2^{nd} (F (n))\}$
143	17 31 6 142	ovolval5lem1	$⊢ φ \to sum^((n \in ℕ ⟼ vol ((1^{st} (F (n)) - (\frac{W}{2^{n}}), 2^{nd} (F (n)))))) \leq sum^((n \in ℕ ⟼ vol ([1^{st} (F (n)), 2^{nd} (F (n)))))) +_{𝑒} W$
144		nfcv	$⊢ \underline{Ⅎ} n G$
145	33 14	fssd	$⊢ φ \to G : ℕ ⟶ ℝ^{} \times ℝ^{}$
146	144 145	volioofmpt	$⊢ φ \to (vol \circ (.)) \circ G = (n \in ℕ ⟼ vol ((1^{st} (G (n)), 2^{nd} (G (n)))))$
147	66 73	oveq12d	$⊢ (φ \land n \in ℕ) \to (1^{st} (G (n)), 2^{nd} (G (n))) = (1^{st} (F (n)) - (\frac{W}{2^{n}}), 2^{nd} (F (n)))$
148	147	fveq2d	$⊢ (φ \land n \in ℕ) \to vol ((1^{st} (G (n)), 2^{nd} (G (n)))) = vol ((1^{st} (F (n)) - (\frac{W}{2^{n}}), 2^{nd} (F (n))))$
149	148	mpteq2dva	$⊢ φ \to (n \in ℕ ⟼ vol ((1^{st} (G (n)), 2^{nd} (G (n))))) = (n \in ℕ ⟼ vol ((1^{st} (F (n)) - (\frac{W}{2^{n}}), 2^{nd} (F (n)))))$
150	146 149	eqtrd	$⊢ φ \to (vol \circ (.)) \circ G = (n \in ℕ ⟼ vol ((1^{st} (F (n)) - (\frac{W}{2^{n}}), 2^{nd} (F (n)))))$
151	150	fveq2d	$⊢ φ \to sum^((vol \circ (.)) \circ G) = sum^((n \in ℕ ⟼ vol ((1^{st} (F (n)) - (\frac{W}{2^{n}}), 2^{nd} (F (n))))))$
152	8 151	eqtrd	$⊢ φ \to Z = sum^((n \in ℕ ⟼ vol ((1^{st} (F (n)) - (\frac{W}{2^{n}}), 2^{nd} (F (n))))))$
153		nfcv	$⊢ \underline{Ⅎ} n F$
154		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
155		xpss2	$⊢ ℝ \subseteq ℝ^{} \to ℝ^{2} \subseteq ℝ \times ℝ^{}$
156	154 155	ax-mp	$⊢ ℝ^{2} \subseteq ℝ \times ℝ^{*}$
157	156	a1i	$⊢ φ \to ℝ^{2} \subseteq ℝ \times ℝ^{*}$
158	4 157	fssd	$⊢ φ \to F : ℕ ⟶ ℝ \times ℝ^{*}$
159	153 158	volicofmpt	$⊢ φ \to (vol \circ [.)) \circ F = (n \in ℕ ⟼ vol ([1^{st} (F (n)), 2^{nd} (F (n)))))$
160	159	fveq2d	$⊢ φ \to sum^((vol \circ [.)) \circ F) = sum^((n \in ℕ ⟼ vol ([1^{st} (F (n)), 2^{nd} (F (n))))))$
161	2 160	eqtrd	$⊢ φ \to Y = sum^((n \in ℕ ⟼ vol ([1^{st} (F (n)), 2^{nd} (F (n))))))$
162	161	oveq1d	$⊢ φ \to Y +_{𝑒} W = sum^((n \in ℕ ⟼ vol ([1^{st} (F (n)), 2^{nd} (F (n)))))) +_{𝑒} W$
163	152 162	breq12d	$⊢ φ \to (Z \leq Y +_{𝑒} W \leftrightarrow sum^((n \in ℕ ⟼ vol ((1^{st} (F (n)) - (\frac{W}{2^{n}}), 2^{nd} (F (n)))))) \leq sum^((n \in ℕ ⟼ vol ([1^{st} (F (n)), 2^{nd} (F (n)))))) +_{𝑒} W)$
164	143 163	mpbird	$⊢ φ \to Z \leq Y +_{𝑒} W$
165		breq1	$⊢ z = Z \to (z \leq Y +_{𝑒} W \leftrightarrow Z \leq Y +_{𝑒} W)$
166	165	rspcev	$⊢ (Z \in Q \land Z \leq Y +_{𝑒} W) \to \exists z \in Q z \leq Y +_{𝑒} W$
167	138 164 166	syl2anc	$⊢ φ \to \exists z \in Q z \leq Y +_{𝑒} W$

Metamath Proof Explorer

Theorem ovolval5lem2

Proof