Metamath Proof Explorer


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 φ n A
ovolval5lem1.b φ n B
ovolval5lem1.w φ W +
ovolval5lem1.c C = n | A < B
Assertion ovolval5lem1 φ sum^ n vol A W 2 n B sum^ n vol A B + 𝑒 W

Proof

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