ovolval5lem1

Description: |- ( ph -> ( sum^( n e. NN |-> ( vol( ( A - ( W / ( 2 ^ n ) ) ) (,) B ) ) ) ) <_ ( ( sum^( n e. NN |-> ( vol( A [,) B ) ) ) ) +e W ) ) . (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	ovolval5lem1.a	$⊢ (φ \land n \in ℕ) \to A \in ℝ$
	ovolval5lem1.b	$⊢ (φ \land n \in ℕ) \to B \in ℝ$
	ovolval5lem1.w	$⊢ φ \to W \in ℝ^{+}$
	ovolval5lem1.c	$⊢ C = \{n \in ℕ \| A < B\}$
Assertion	ovolval5lem1	$⊢ φ \to sum^((n \in ℕ ⟼ vol ((A - (\frac{W}{2^{n}}), B)))) \leq sum^((n \in ℕ ⟼ vol ([A, B)))) +_{𝑒} W$

Proof

Step	Hyp	Ref	Expression
1		ovolval5lem1.a	$⊢ (φ \land n \in ℕ) \to A \in ℝ$
2		ovolval5lem1.b	$⊢ (φ \land n \in ℕ) \to B \in ℝ$
3		ovolval5lem1.w	$⊢ φ \to W \in ℝ^{+}$
4		ovolval5lem1.c	$⊢ C = \{n \in ℕ \| A < B\}$
5		nfv	$⊢ Ⅎ n φ$
6		nnex	$⊢ ℕ \in V$
7	6	a1i	$⊢ φ \to ℕ \in V$
8		volf	$⊢ vol : dom vol ⟶ [0, +∞]$
9	8	a1i	$⊢ (φ \land n \in ℕ) \to vol : dom vol ⟶ [0, +∞]$
10		ioombl	$⊢ (A - (\frac{W}{2^{n}}), B) \in dom vol$
11	10	a1i	$⊢ (φ \land n \in ℕ) \to (A - (\frac{W}{2^{n}}), B) \in dom vol$
12	9 11	ffvelcdmd	$⊢ (φ \land n \in ℕ) \to vol ((A - (\frac{W}{2^{n}}), B)) \in [0, +∞]$
13	5 7 12	sge0xrclmpt	$⊢ φ \to sum^((n \in ℕ ⟼ vol ((A - (\frac{W}{2^{n}}), B)))) \in ℝ^{*}$
14		0xr	$⊢ 0 \in ℝ^{*}$
15	14	a1i	$⊢ (φ \land n \in ℕ) \to 0 \in ℝ^{*}$
16		pnfxr	$⊢ +∞ \in ℝ^{*}$
17	16	a1i	$⊢ (φ \land n \in ℕ) \to +∞ \in ℝ^{*}$
18		volicore	$⊢ (A \in ℝ \land B \in ℝ) \to vol ([A, B)) \in ℝ$
19	1 2 18	syl2anc	$⊢ (φ \land n \in ℕ) \to vol ([A, B)) \in ℝ$
20	3	rpred	$⊢ φ \to W \in ℝ$
21	20	adantr	$⊢ (φ \land n \in ℕ) \to W \in ℝ$
22		2nn	$⊢ 2 \in ℕ$
23	22	a1i	$⊢ n \in ℕ \to 2 \in ℕ$
24		nnnn0	$⊢ n \in ℕ \to n \in ℕ_{0}$
25		nnexpcl	$⊢ (2 \in ℕ \land n \in ℕ_{0}) \to 2^{n} \in ℕ$
26	23 24 25	syl2anc	$⊢ n \in ℕ \to 2^{n} \in ℕ$
27	26	nnred	$⊢ n \in ℕ \to 2^{n} \in ℝ$
28	27	adantl	$⊢ (φ \land n \in ℕ) \to 2^{n} \in ℝ$
29	26	nnne0d	$⊢ n \in ℕ \to 2^{n} \neq 0$
30	29	adantl	$⊢ (φ \land n \in ℕ) \to 2^{n} \neq 0$
31	21 28 30	redivcld	$⊢ (φ \land n \in ℕ) \to \frac{W}{2^{n}} \in ℝ$
32	19 31	readdcld	$⊢ (φ \land n \in ℕ) \to vol ([A, B)) + (\frac{W}{2^{n}}) \in ℝ$
33	32	rexrd	$⊢ (φ \land n \in ℕ) \to vol ([A, B)) + (\frac{W}{2^{n}}) \in ℝ^{*}$
34	2	rexrd	$⊢ (φ \land n \in ℕ) \to B \in ℝ^{*}$
35		icombl	$⊢ (A \in ℝ \land B \in ℝ^{*}) \to [A, B) \in dom vol$
36	1 34 35	syl2anc	$⊢ (φ \land n \in ℕ) \to [A, B) \in dom vol$
37		volge0	$⊢ [A, B) \in dom vol \to 0 \leq vol ([A, B))$
38	36 37	syl	$⊢ (φ \land n \in ℕ) \to 0 \leq vol ([A, B))$
39	3	adantr	$⊢ (φ \land n \in ℕ) \to W \in ℝ^{+}$
40	26	nnrpd	$⊢ n \in ℕ \to 2^{n} \in ℝ^{+}$
41	40	adantl	$⊢ (φ \land n \in ℕ) \to 2^{n} \in ℝ^{+}$
42	39 41	rpdivcld	$⊢ (φ \land n \in ℕ) \to \frac{W}{2^{n}} \in ℝ^{+}$
43	42	rpge0d	$⊢ (φ \land n \in ℕ) \to 0 \leq \frac{W}{2^{n}}$
44	19 31 38 43	addge0d	$⊢ (φ \land n \in ℕ) \to 0 \leq vol ([A, B)) + (\frac{W}{2^{n}})$
45		rexr	$⊢ vol ([A, B)) + (\frac{W}{2^{n}}) \in ℝ \to vol ([A, B)) + (\frac{W}{2^{n}}) \in ℝ^{*}$
46	16	a1i	$⊢ vol ([A, B)) + (\frac{W}{2^{n}}) \in ℝ \to +∞ \in ℝ^{*}$
47		ltpnf	$⊢ vol ([A, B)) + (\frac{W}{2^{n}}) \in ℝ \to vol ([A, B)) + (\frac{W}{2^{n}}) < +∞$
48	45 46 47	xrltled	$⊢ vol ([A, B)) + (\frac{W}{2^{n}}) \in ℝ \to vol ([A, B)) + (\frac{W}{2^{n}}) \leq +∞$
49	32 48	syl	$⊢ (φ \land n \in ℕ) \to vol ([A, B)) + (\frac{W}{2^{n}}) \leq +∞$
50	15 17 33 44 49	eliccxrd	$⊢ (φ \land n \in ℕ) \to vol ([A, B)) + (\frac{W}{2^{n}}) \in [0, +∞]$
51	5 7 50	sge0xrclmpt	$⊢ φ \to sum^((n \in ℕ ⟼ vol ([A, B)) + (\frac{W}{2^{n}}))) \in ℝ^{*}$
52	9 36	ffvelcdmd	$⊢ (φ \land n \in ℕ) \to vol ([A, B)) \in [0, +∞]$
53	5 7 52	sge0xrclmpt	$⊢ φ \to sum^((n \in ℕ ⟼ vol ([A, B)))) \in ℝ^{*}$
54	20	rexrd	$⊢ φ \to W \in ℝ^{*}$
55	53 54	xaddcld	$⊢ φ \to sum^((n \in ℕ ⟼ vol ([A, B)))) +_{𝑒} W \in ℝ^{*}$
56	1 31	resubcld	$⊢ (φ \land n \in ℕ) \to A - (\frac{W}{2^{n}}) \in ℝ$
57		volioore	$⊢ (A - (\frac{W}{2^{n}}) \in ℝ \land B \in ℝ) \to vol ((A - (\frac{W}{2^{n}}), B)) = if (A - (\frac{W}{2^{n}}) \leq B, B - (A - (\frac{W}{2^{n}})), 0)$
58	56 2 57	syl2anc	$⊢ (φ \land n \in ℕ) \to vol ((A - (\frac{W}{2^{n}}), B)) = if (A - (\frac{W}{2^{n}}) \leq B, B - (A - (\frac{W}{2^{n}})), 0)$
59	58	adantr	$⊢ ((φ \land n \in ℕ) \land A - (\frac{W}{2^{n}}) \leq B) \to vol ((A - (\frac{W}{2^{n}}), B)) = if (A - (\frac{W}{2^{n}}) \leq B, B - (A - (\frac{W}{2^{n}})), 0)$
60		iftrue	$⊢ A - (\frac{W}{2^{n}}) \leq B \to if (A - (\frac{W}{2^{n}}) \leq B, B - (A - (\frac{W}{2^{n}})), 0) = B - (A - (\frac{W}{2^{n}}))$
61	60	adantl	$⊢ ((φ \land n \in ℕ) \land A - (\frac{W}{2^{n}}) \leq B) \to if (A - (\frac{W}{2^{n}}) \leq B, B - (A - (\frac{W}{2^{n}})), 0) = B - (A - (\frac{W}{2^{n}}))$
62	2	recnd	$⊢ (φ \land n \in ℕ) \to B \in ℂ$
63	1	recnd	$⊢ (φ \land n \in ℕ) \to A \in ℂ$
64	31	recnd	$⊢ (φ \land n \in ℕ) \to \frac{W}{2^{n}} \in ℂ$
65	62 63 64	subsubd	$⊢ (φ \land n \in ℕ) \to B - (A - (\frac{W}{2^{n}})) = B - A + (\frac{W}{2^{n}})$
66	65	adantr	$⊢ ((φ \land n \in ℕ) \land A - (\frac{W}{2^{n}}) \leq B) \to B - (A - (\frac{W}{2^{n}})) = B - A + (\frac{W}{2^{n}})$
67	59 61 66	3eqtrd	$⊢ ((φ \land n \in ℕ) \land A - (\frac{W}{2^{n}}) \leq B) \to vol ((A - (\frac{W}{2^{n}}), B)) = B - A + (\frac{W}{2^{n}})$
68	2 1	resubcld	$⊢ (φ \land n \in ℕ) \to B - A \in ℝ$
69	1 2	sublevolico	$⊢ (φ \land n \in ℕ) \to B - A \leq vol ([A, B))$
70	68 19 31 69	leadd1dd	$⊢ (φ \land n \in ℕ) \to B - A + (\frac{W}{2^{n}}) \leq vol ([A, B)) + (\frac{W}{2^{n}})$
71	70	adantr	$⊢ ((φ \land n \in ℕ) \land A - (\frac{W}{2^{n}}) \leq B) \to B - A + (\frac{W}{2^{n}}) \leq vol ([A, B)) + (\frac{W}{2^{n}})$
72	67 71	eqbrtrd	$⊢ ((φ \land n \in ℕ) \land A - (\frac{W}{2^{n}}) \leq B) \to vol ((A - (\frac{W}{2^{n}}), B)) \leq vol ([A, B)) + (\frac{W}{2^{n}})$
73	58	adantr	$⊢ ((φ \land n \in ℕ) \land \neg A - (\frac{W}{2^{n}}) \leq B) \to vol ((A - (\frac{W}{2^{n}}), B)) = if (A - (\frac{W}{2^{n}}) \leq B, B - (A - (\frac{W}{2^{n}})), 0)$
74		iffalse	$⊢ \neg A - (\frac{W}{2^{n}}) \leq B \to if (A - (\frac{W}{2^{n}}) \leq B, B - (A - (\frac{W}{2^{n}})), 0) = 0$
75	74	adantl	$⊢ ((φ \land n \in ℕ) \land \neg A - (\frac{W}{2^{n}}) \leq B) \to if (A - (\frac{W}{2^{n}}) \leq B, B - (A - (\frac{W}{2^{n}})), 0) = 0$
76	73 75	eqtrd	$⊢ ((φ \land n \in ℕ) \land \neg A - (\frac{W}{2^{n}}) \leq B) \to vol ((A - (\frac{W}{2^{n}}), B)) = 0$
77	44	adantr	$⊢ ((φ \land n \in ℕ) \land \neg A - (\frac{W}{2^{n}}) \leq B) \to 0 \leq vol ([A, B)) + (\frac{W}{2^{n}})$
78	76 77	eqbrtrd	$⊢ ((φ \land n \in ℕ) \land \neg A - (\frac{W}{2^{n}}) \leq B) \to vol ((A - (\frac{W}{2^{n}}), B)) \leq vol ([A, B)) + (\frac{W}{2^{n}})$
79	72 78	pm2.61dan	$⊢ (φ \land n \in ℕ) \to vol ((A - (\frac{W}{2^{n}}), B)) \leq vol ([A, B)) + (\frac{W}{2^{n}})$
80	5 7 12 50 79	sge0lempt	$⊢ φ \to sum^((n \in ℕ ⟼ vol ((A - (\frac{W}{2^{n}}), B)))) \leq sum^((n \in ℕ ⟼ vol ([A, B)) + (\frac{W}{2^{n}})))$
81	19 31	rexaddd	$⊢ (φ \land n \in ℕ) \to vol ([A, B)) +_{𝑒} (\frac{W}{2^{n}}) = vol ([A, B)) + (\frac{W}{2^{n}})$
82	81	eqcomd	$⊢ (φ \land n \in ℕ) \to vol ([A, B)) + (\frac{W}{2^{n}}) = vol ([A, B)) +_{𝑒} (\frac{W}{2^{n}})$
83	82	mpteq2dva	$⊢ φ \to (n \in ℕ ⟼ vol ([A, B)) + (\frac{W}{2^{n}})) = (n \in ℕ ⟼ vol ([A, B)) +_{𝑒} (\frac{W}{2^{n}}))$
84	83	fveq2d	$⊢ φ \to sum^((n \in ℕ ⟼ vol ([A, B)) + (\frac{W}{2^{n}}))) = sum^((n \in ℕ ⟼ vol ([A, B)) +_{𝑒} (\frac{W}{2^{n}})))$
85	31	rexrd	$⊢ (φ \land n \in ℕ) \to \frac{W}{2^{n}} \in ℝ^{*}$
86		rexr	$⊢ \frac{W}{2^{n}} \in ℝ \to \frac{W}{2^{n}} \in ℝ^{*}$
87	16	a1i	$⊢ \frac{W}{2^{n}} \in ℝ \to +∞ \in ℝ^{*}$
88		ltpnf	$⊢ \frac{W}{2^{n}} \in ℝ \to \frac{W}{2^{n}} < +∞$
89	86 87 88	xrltled	$⊢ \frac{W}{2^{n}} \in ℝ \to \frac{W}{2^{n}} \leq +∞$
90	31 89	syl	$⊢ (φ \land n \in ℕ) \to \frac{W}{2^{n}} \leq +∞$
91	15 17 85 43 90	eliccxrd	$⊢ (φ \land n \in ℕ) \to \frac{W}{2^{n}} \in [0, +∞]$
92	5 7 52 91	sge0xadd	$⊢ φ \to sum^((n \in ℕ ⟼ vol ([A, B)) +_{𝑒} (\frac{W}{2^{n}}))) = sum^((n \in ℕ ⟼ vol ([A, B)))) +_{𝑒} sum^((n \in ℕ ⟼ \frac{W}{2^{n}}))$
93	14	a1i	$⊢ φ \to 0 \in ℝ^{*}$
94	16	a1i	$⊢ φ \to +∞ \in ℝ^{*}$
95	3	rpge0d	$⊢ φ \to 0 \leq W$
96	20	ltpnfd	$⊢ φ \to W < +∞$
97	93 94 54 95 96	elicod	$⊢ φ \to W \in [0, +∞)$
98	97	sge0ad2en	$⊢ φ \to sum^((n \in ℕ ⟼ \frac{W}{2^{n}})) = W$
99	98	oveq2d	$⊢ φ \to sum^((n \in ℕ ⟼ vol ([A, B)))) +_{𝑒} sum^((n \in ℕ ⟼ \frac{W}{2^{n}})) = sum^((n \in ℕ ⟼ vol ([A, B)))) +_{𝑒} W$
100	84 92 99	3eqtrd	$⊢ φ \to sum^((n \in ℕ ⟼ vol ([A, B)) + (\frac{W}{2^{n}}))) = sum^((n \in ℕ ⟼ vol ([A, B)))) +_{𝑒} W$
101	51 100	xreqled	$⊢ φ \to sum^((n \in ℕ ⟼ vol ([A, B)) + (\frac{W}{2^{n}}))) \leq sum^((n \in ℕ ⟼ vol ([A, B)))) +_{𝑒} W$
102	13 51 55 80 101	xrletrd	$⊢ φ \to sum^((n \in ℕ ⟼ vol ((A - (\frac{W}{2^{n}}), B)))) \leq sum^((n \in ℕ ⟼ vol ([A, B)))) +_{𝑒} W$

Metamath Proof Explorer

Theorem ovolval5lem1

Proof