Metamath Proof Explorer

Theorem ovollb2lem

Description: Lemma for ovollb2 . (Contributed by Mario Carneiro, 24-Mar-2015)

Ref Expression
Hypotheses ovollb2.1 
|- S = seq 1 ( + , ( ( abs o. - ) o. F ) )
ovollb2.2 
|- G = ( n e. NN |-> <. ( ( 1st ` ( F ` n ) ) - ( ( B / 2 ) / ( 2 ^ n ) ) ) , ( ( 2nd ` ( F ` n ) ) + ( ( B / 2 ) / ( 2 ^ n ) ) ) >. )
ovollb2.3 
|- T = seq 1 ( + , ( ( abs o. - ) o. G ) )
ovollb2.4 
|- ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
ovollb2.5 
|- ( ph -> A C_ U. ran ( [,] o. F ) )
ovollb2.6 
|- ( ph -> B e. RR+ )
ovollb2.7 
|- ( ph -> sup ( ran S , RR* , < ) e. RR )
Assertion ovollb2lem 
|- ( ph -> ( vol* ` A ) <_ ( sup ( ran S , RR* , < ) + B ) )

Proof

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