Theorem 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	|- ( ( ph /\ n e. NN ) -> A e. RR )
	ovolval5lem1.b	|- ( ( ph /\ n e. NN ) -> B e. RR )
	ovolval5lem1.w	|- ( ph -> W e. RR+ )
	ovolval5lem1.c	|- C = { n e. NN | A < B }
Assertion	ovolval5lem1	|- ( ph -> ( sum^ ` ( n e. NN |-> ( vol ` ( ( A - ( W / ( 2 ^ n ) ) ) (,) B ) ) ) ) <_ ( ( sum^ ` ( n e. NN |-> ( vol ` ( A [,) B ) ) ) ) +e W ) )

Proof

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