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 sselid
 |-  ( ( ( 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 sselid
 |-  ( ( 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 ) )