Metamath Proof Explorer

Theorem ovolunlem1a

Description: Lemma for ovolun . (Contributed by Mario Carneiro, 7-May-2015)

Ref Expression
Hypotheses ovolun.a 
|- ( ph -> ( A C_ RR /\ ( vol* ` A ) e. RR ) )
ovolun.b 
|- ( ph -> ( B C_ RR /\ ( vol* ` B ) e. RR ) )
ovolun.c 
|- ( ph -> C e. RR+ )
ovolun.s 
|- S = seq 1 ( + , ( ( abs o. - ) o. F ) )
ovolun.t 
|- T = seq 1 ( + , ( ( abs o. - ) o. G ) )
ovolun.u 
|- U = seq 1 ( + , ( ( abs o. - ) o. H ) )
ovolun.f1 
|- ( ph -> F e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) )
ovolun.f2 
|- ( ph -> A C_ U. ran ( (,) o. F ) )
ovolun.f3 
|- ( ph -> sup ( ran S , RR* , < ) <_ ( ( vol* ` A ) + ( C / 2 ) ) )
ovolun.g1 
|- ( ph -> G e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) )
ovolun.g2 
|- ( ph -> B C_ U. ran ( (,) o. G ) )
ovolun.g3 
|- ( ph -> sup ( ran T , RR* , < ) <_ ( ( vol* ` B ) + ( C / 2 ) ) )
ovolun.h 
|- H = ( n e. NN |-> if ( ( n / 2 ) e. NN , ( G ` ( n / 2 ) ) , ( F ` ( ( n + 1 ) / 2 ) ) ) )
Assertion ovolunlem1a 
|- ( ( ph /\ k e. NN ) -> ( U ` k ) <_ ( ( ( vol* ` A ) + ( vol* ` B ) ) + C ) )

Proof

Step Hyp Ref Expression
1 ovolun.a 
 |-  ( ph -> ( A C_ RR /\ ( vol* ` A ) e. RR ) )
2 ovolun.b 
 |-  ( ph -> ( B C_ RR /\ ( vol* ` B ) e. RR ) )
3 ovolun.c 
 |-  ( ph -> C e. RR+ )
4 ovolun.s 
 |-  S = seq 1 ( + , ( ( abs o. - ) o. F ) )
5 ovolun.t 
 |-  T = seq 1 ( + , ( ( abs o. - ) o. G ) )
6 ovolun.u 
 |-  U = seq 1 ( + , ( ( abs o. - ) o. H ) )
7 ovolun.f1 
 |-  ( ph -> F e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) )
8 ovolun.f2 
 |-  ( ph -> A C_ U. ran ( (,) o. F ) )
9 ovolun.f3 
 |-  ( ph -> sup ( ran S , RR* , < ) <_ ( ( vol* ` A ) + ( C / 2 ) ) )
10 ovolun.g1 
 |-  ( ph -> G e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) )
11 ovolun.g2 
 |-  ( ph -> B C_ U. ran ( (,) o. G ) )
12 ovolun.g3 
 |-  ( ph -> sup ( ran T , RR* , < ) <_ ( ( vol* ` B ) + ( C / 2 ) ) )
13 ovolun.h 
 |-  H = ( n e. NN |-> if ( ( n / 2 ) e. NN , ( G ` ( n / 2 ) ) , ( F ` ( ( n + 1 ) / 2 ) ) ) )
14 elovolmlem 
 |-  ( G e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) <-> G : NN --> ( <_ i^i ( RR X. RR ) ) )
15 10 14 sylib 
 |-  ( ph -> G : NN --> ( <_ i^i ( RR X. RR ) ) )
16 15 adantr 
 |-  ( ( ph /\ n e. NN ) -> G : NN --> ( <_ i^i ( RR X. RR ) ) )
17 16 ffvelcdmda 
 |-  ( ( ( ph /\ n e. NN ) /\ ( n / 2 ) e. NN ) -> ( G ` ( n / 2 ) ) e. ( <_ i^i ( RR X. RR ) ) )
18 nneo 
 |-  ( n e. NN -> ( ( n / 2 ) e. NN <-> -. ( ( n + 1 ) / 2 ) e. NN ) )
19 18 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( ( n / 2 ) e. NN <-> -. ( ( n + 1 ) / 2 ) e. NN ) )
20 19 con2bid 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( n + 1 ) / 2 ) e. NN <-> -. ( n / 2 ) e. NN ) )
21 20 biimpar 
 |-  ( ( ( ph /\ n e. NN ) /\ -. ( n / 2 ) e. NN ) -> ( ( n + 1 ) / 2 ) e. NN )
22 elovolmlem 
 |-  ( F e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) <-> F : NN --> ( <_ i^i ( RR X. RR ) ) )
23 7 22 sylib 
 |-  ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
24 23 adantr 
 |-  ( ( ph /\ n e. NN ) -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
25 24 ffvelcdmda 
 |-  ( ( ( ph /\ n e. NN ) /\ ( ( n + 1 ) / 2 ) e. NN ) -> ( F ` ( ( n + 1 ) / 2 ) ) e. ( <_ i^i ( RR X. RR ) ) )
26 21 25 syldan 
 |-  ( ( ( ph /\ n e. NN ) /\ -. ( n / 2 ) e. NN ) -> ( F ` ( ( n + 1 ) / 2 ) ) e. ( <_ i^i ( RR X. RR ) ) )
27 17 26 ifclda 
 |-  ( ( ph /\ n e. NN ) -> if ( ( n / 2 ) e. NN , ( G ` ( n / 2 ) ) , ( F ` ( ( n + 1 ) / 2 ) ) ) e. ( <_ i^i ( RR X. RR ) ) )
28 27 13 fmptd 
 |-  ( ph -> H : NN --> ( <_ i^i ( RR X. RR ) ) )
29 eqid 
 |-  ( ( abs o. - ) o. H ) = ( ( abs o. - ) o. H )
30 29 6 ovolsf 
 |-  ( H : NN --> ( <_ i^i ( RR X. RR ) ) -> U : NN --> ( 0 [,) +oo ) )
31 28 30 syl 
 |-  ( ph -> U : NN --> ( 0 [,) +oo ) )
32 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
33 fss 
 |-  ( ( U : NN --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ RR ) -> U : NN --> RR )
34 31 32 33 sylancl 
 |-  ( ph -> U : NN --> RR )
35 34 ffvelcdmda 
 |-  ( ( ph /\ k e. NN ) -> ( U ` k ) e. RR )
36 2nn 
 |-  2 e. NN
37 peano2nn 
 |-  ( k e. NN -> ( k + 1 ) e. NN )
38 37 adantl 
 |-  ( ( ph /\ k e. NN ) -> ( k + 1 ) e. NN )
39 38 nnred 
 |-  ( ( ph /\ k e. NN ) -> ( k + 1 ) e. RR )
40 39 rehalfcld 
 |-  ( ( ph /\ k e. NN ) -> ( ( k + 1 ) / 2 ) e. RR )
41 40 flcld 
 |-  ( ( ph /\ k e. NN ) -> ( |_ ` ( ( k + 1 ) / 2 ) ) e. ZZ )
42 ax-1cn 
 |-  1 e. CC
43 42 2timesi 
 |-  ( 2 x. 1 ) = ( 1 + 1 )
44 nnge1 
 |-  ( k e. NN -> 1 <_ k )
45 44 adantl 
 |-  ( ( ph /\ k e. NN ) -> 1 <_ k )
46 nnre 
 |-  ( k e. NN -> k e. RR )
47 46 adantl 
 |-  ( ( ph /\ k e. NN ) -> k e. RR )
48 1re 
 |-  1 e. RR
49 leadd1 
 |-  ( ( 1 e. RR /\ k e. RR /\ 1 e. RR ) -> ( 1 <_ k <-> ( 1 + 1 ) <_ ( k + 1 ) ) )
50 48 48 49 mp3an13 
 |-  ( k e. RR -> ( 1 <_ k <-> ( 1 + 1 ) <_ ( k + 1 ) ) )
51 47 50 syl 
 |-  ( ( ph /\ k e. NN ) -> ( 1 <_ k <-> ( 1 + 1 ) <_ ( k + 1 ) ) )
52 45 51 mpbid 
 |-  ( ( ph /\ k e. NN ) -> ( 1 + 1 ) <_ ( k + 1 ) )
53 43 52 eqbrtrid 
 |-  ( ( ph /\ k e. NN ) -> ( 2 x. 1 ) <_ ( k + 1 ) )
54 2re 
 |-  2 e. RR
55 2pos 
 |-  0 < 2
56 54 55 pm3.2i 
 |-  ( 2 e. RR /\ 0 < 2 )
57 lemuldiv2 
 |-  ( ( 1 e. RR /\ ( k + 1 ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( 2 x. 1 ) <_ ( k + 1 ) <-> 1 <_ ( ( k + 1 ) / 2 ) ) )
58 48 56 57 mp3an13 
 |-  ( ( k + 1 ) e. RR -> ( ( 2 x. 1 ) <_ ( k + 1 ) <-> 1 <_ ( ( k + 1 ) / 2 ) ) )
59 39 58 syl 
 |-  ( ( ph /\ k e. NN ) -> ( ( 2 x. 1 ) <_ ( k + 1 ) <-> 1 <_ ( ( k + 1 ) / 2 ) ) )
60 53 59 mpbid 
 |-  ( ( ph /\ k e. NN ) -> 1 <_ ( ( k + 1 ) / 2 ) )
61 1z 
 |-  1 e. ZZ
62 flge 
 |-  ( ( ( ( k + 1 ) / 2 ) e. RR /\ 1 e. ZZ ) -> ( 1 <_ ( ( k + 1 ) / 2 ) <-> 1 <_ ( |_ ` ( ( k + 1 ) / 2 ) ) ) )
63 40 61 62 sylancl 
 |-  ( ( ph /\ k e. NN ) -> ( 1 <_ ( ( k + 1 ) / 2 ) <-> 1 <_ ( |_ ` ( ( k + 1 ) / 2 ) ) ) )
64 60 63 mpbid 
 |-  ( ( ph /\ k e. NN ) -> 1 <_ ( |_ ` ( ( k + 1 ) / 2 ) ) )
65 elnnz1 
 |-  ( ( |_ ` ( ( k + 1 ) / 2 ) ) e. NN <-> ( ( |_ ` ( ( k + 1 ) / 2 ) ) e. ZZ /\ 1 <_ ( |_ ` ( ( k + 1 ) / 2 ) ) ) )
66 41 64 65 sylanbrc 
 |-  ( ( ph /\ k e. NN ) -> ( |_ ` ( ( k + 1 ) / 2 ) ) e. NN )
67 nnmulcl 
 |-  ( ( 2 e. NN /\ ( |_ ` ( ( k + 1 ) / 2 ) ) e. NN ) -> ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) e. NN )
68 36 66 67 sylancr 
 |-  ( ( ph /\ k e. NN ) -> ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) e. NN )
69 34 ffvelcdmda 
 |-  ( ( ph /\ ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) e. NN ) -> ( U ` ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) e. RR )
70 68 69 syldan 
 |-  ( ( ph /\ k e. NN ) -> ( U ` ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) e. RR )
71 1 simprd 
 |-  ( ph -> ( vol* ` A ) e. RR )
72 2 simprd 
 |-  ( ph -> ( vol* ` B ) e. RR )
73 71 72 readdcld 
 |-  ( ph -> ( ( vol* ` A ) + ( vol* ` B ) ) e. RR )
74 3 rpred 
 |-  ( ph -> C e. RR )
75 73 74 readdcld 
 |-  ( ph -> ( ( ( vol* ` A ) + ( vol* ` B ) ) + C ) e. RR )
76 75 adantr 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( vol* ` A ) + ( vol* ` B ) ) + C ) e. RR )
77 simpr 
 |-  ( ( ph /\ k e. NN ) -> k e. NN )
78 nnuz 
 |-  NN = ( ZZ>= ` 1 )
79 77 78 eleqtrdi 
 |-  ( ( ph /\ k e. NN ) -> k e. ( ZZ>= ` 1 ) )
80 nnz 
 |-  ( k e. NN -> k e. ZZ )
81 80 adantl 
 |-  ( ( ph /\ k e. NN ) -> k e. ZZ )
82 flhalf 
 |-  ( k e. ZZ -> k <_ ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) )
83 81 82 syl 
 |-  ( ( ph /\ k e. NN ) -> k <_ ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) )
84 nnz 
 |-  ( ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) e. NN -> ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) e. ZZ )
85 eluz 
 |-  ( ( k e. ZZ /\ ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) e. ZZ ) -> ( ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) e. ( ZZ>= ` k ) <-> k <_ ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) )
86 80 84 85 syl2an 
 |-  ( ( k e. NN /\ ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) e. NN ) -> ( ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) e. ( ZZ>= ` k ) <-> k <_ ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) )
87 77 68 86 syl2anc 
 |-  ( ( ph /\ k e. NN ) -> ( ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) e. ( ZZ>= ` k ) <-> k <_ ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) )
88 83 87 mpbird 
 |-  ( ( ph /\ k e. NN ) -> ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) e. ( ZZ>= ` k ) )
89 elfznn 
 |-  ( j e. ( 1 ... ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) -> j e. NN )
90 29 ovolfsf 
 |-  ( H : NN --> ( <_ i^i ( RR X. RR ) ) -> ( ( abs o. - ) o. H ) : NN --> ( 0 [,) +oo ) )
91 28 90 syl 
 |-  ( ph -> ( ( abs o. - ) o. H ) : NN --> ( 0 [,) +oo ) )
92 91 adantr 
 |-  ( ( ph /\ k e. NN ) -> ( ( abs o. - ) o. H ) : NN --> ( 0 [,) +oo ) )
93 92 ffvelcdmda 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. NN ) -> ( ( ( abs o. - ) o. H ) ` j ) e. ( 0 [,) +oo ) )
94 elrege0 
 |-  ( ( ( ( abs o. - ) o. H ) ` j ) e. ( 0 [,) +oo ) <-> ( ( ( ( abs o. - ) o. H ) ` j ) e. RR /\ 0 <_ ( ( ( abs o. - ) o. H ) ` j ) ) )
95 93 94 sylib 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. NN ) -> ( ( ( ( abs o. - ) o. H ) ` j ) e. RR /\ 0 <_ ( ( ( abs o. - ) o. H ) ` j ) ) )
96 95 simpld 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. NN ) -> ( ( ( abs o. - ) o. H ) ` j ) e. RR )
97 89 96 sylan2 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( 1 ... ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) ) -> ( ( ( abs o. - ) o. H ) ` j ) e. RR )
98 elfzuz 
 |-  ( j e. ( ( k + 1 ) ... ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) -> j e. ( ZZ>= ` ( k + 1 ) ) )
99 eluznn 
 |-  ( ( ( k + 1 ) e. NN /\ j e. ( ZZ>= ` ( k + 1 ) ) ) -> j e. NN )
100 38 98 99 syl2an 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( ( k + 1 ) ... ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) ) -> j e. NN )
101 95 simprd 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. NN ) -> 0 <_ ( ( ( abs o. - ) o. H ) ` j ) )
102 100 101 syldan 
 |-  ( ( ( ph /\ k e. NN ) /\ j e. ( ( k + 1 ) ... ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) ) -> 0 <_ ( ( ( abs o. - ) o. H ) ` j ) )
103 79 88 97 102 sermono 
 |-  ( ( ph /\ k e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` k ) <_ ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) )
104 6 fveq1i 
 |-  ( U ` k ) = ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` k )
105 6 fveq1i 
 |-  ( U ` ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) = ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) )
106 103 104 105 3brtr4g 
 |-  ( ( ph /\ k e. NN ) -> ( U ` k ) <_ ( U ` ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) )
107 eqid 
 |-  ( ( abs o. - ) o. F ) = ( ( abs o. - ) o. F )
108 107 4 ovolsf 
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> S : NN --> ( 0 [,) +oo ) )
109 23 108 syl 
 |-  ( ph -> S : NN --> ( 0 [,) +oo ) )
110 109 frnd 
 |-  ( ph -> ran S C_ ( 0 [,) +oo ) )
111 110 32 sstrdi 
 |-  ( ph -> ran S C_ RR )
112 111 adantr 
 |-  ( ( ph /\ k e. NN ) -> ran S C_ RR )
113 109 ffnd 
 |-  ( ph -> S Fn NN )
114 fnfvelrn 
 |-  ( ( S Fn NN /\ ( |_ ` ( ( k + 1 ) / 2 ) ) e. NN ) -> ( S ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) e. ran S )
115 113 66 114 syl2an2r 
 |-  ( ( ph /\ k e. NN ) -> ( S ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) e. ran S )
116 112 115 sseldd 
 |-  ( ( ph /\ k e. NN ) -> ( S ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) e. RR )
117 eqid 
 |-  ( ( abs o. - ) o. G ) = ( ( abs o. - ) o. G )
118 117 5 ovolsf 
 |-  ( G : NN --> ( <_ i^i ( RR X. RR ) ) -> T : NN --> ( 0 [,) +oo ) )
119 15 118 syl 
 |-  ( ph -> T : NN --> ( 0 [,) +oo ) )
120 119 frnd 
 |-  ( ph -> ran T C_ ( 0 [,) +oo ) )
121 120 32 sstrdi 
 |-  ( ph -> ran T C_ RR )
122 121 adantr 
 |-  ( ( ph /\ k e. NN ) -> ran T C_ RR )
123 119 ffnd 
 |-  ( ph -> T Fn NN )
124 fnfvelrn 
 |-  ( ( T Fn NN /\ ( |_ ` ( ( k + 1 ) / 2 ) ) e. NN ) -> ( T ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) e. ran T )
125 123 66 124 syl2an2r 
 |-  ( ( ph /\ k e. NN ) -> ( T ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) e. ran T )
126 122 125 sseldd 
 |-  ( ( ph /\ k e. NN ) -> ( T ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) e. RR )
127 74 rehalfcld 
 |-  ( ph -> ( C / 2 ) e. RR )
128 71 127 readdcld 
 |-  ( ph -> ( ( vol* ` A ) + ( C / 2 ) ) e. RR )
129 128 adantr 
 |-  ( ( ph /\ k e. NN ) -> ( ( vol* ` A ) + ( C / 2 ) ) e. RR )
130 72 127 readdcld 
 |-  ( ph -> ( ( vol* ` B ) + ( C / 2 ) ) e. RR )
131 130 adantr 
 |-  ( ( ph /\ k e. NN ) -> ( ( vol* ` B ) + ( C / 2 ) ) e. RR )
132 ressxr 
 |-  RR C_ RR*
133 111 132 sstrdi 
 |-  ( ph -> ran S C_ RR* )
134 supxrcl 
 |-  ( ran S C_ RR* -> sup ( ran S , RR* , < ) e. RR* )
135 133 134 syl 
 |-  ( ph -> sup ( ran S , RR* , < ) e. RR* )
136 1nn 
 |-  1 e. NN
137 109 fdmd 
 |-  ( ph -> dom S = NN )
138 136 137 eleqtrrid 
 |-  ( ph -> 1 e. dom S )
139 138 ne0d 
 |-  ( ph -> dom S =/= (/) )
140 dm0rn0 
 |-  ( dom S = (/) <-> ran S = (/) )
141 140 necon3bii 
 |-  ( dom S =/= (/) <-> ran S =/= (/) )
142 139 141 sylib 
 |-  ( ph -> ran S =/= (/) )
143 supxrgtmnf 
 |-  ( ( ran S C_ RR /\ ran S =/= (/) ) -> -oo < sup ( ran S , RR* , < ) )
144 111 142 143 syl2anc 
 |-  ( ph -> -oo < sup ( ran S , RR* , < ) )
145 xrre 
 |-  ( ( ( sup ( ran S , RR* , < ) e. RR* /\ ( ( vol* ` A ) + ( C / 2 ) ) e. RR ) /\ ( -oo < sup ( ran S , RR* , < ) /\ sup ( ran S , RR* , < ) <_ ( ( vol* ` A ) + ( C / 2 ) ) ) ) -> sup ( ran S , RR* , < ) e. RR )
146 135 128 144 9 145 syl22anc 
 |-  ( ph -> sup ( ran S , RR* , < ) e. RR )
147 146 adantr 
 |-  ( ( ph /\ k e. NN ) -> sup ( ran S , RR* , < ) e. RR )
148 supxrub 
 |-  ( ( ran S C_ RR* /\ ( S ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) e. ran S ) -> ( S ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) <_ sup ( ran S , RR* , < ) )
149 133 115 148 syl2an2r 
 |-  ( ( ph /\ k e. NN ) -> ( S ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) <_ sup ( ran S , RR* , < ) )
150 9 adantr 
 |-  ( ( ph /\ k e. NN ) -> sup ( ran S , RR* , < ) <_ ( ( vol* ` A ) + ( C / 2 ) ) )
151 116 147 129 149 150 letrd 
 |-  ( ( ph /\ k e. NN ) -> ( S ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) <_ ( ( vol* ` A ) + ( C / 2 ) ) )
152 121 132 sstrdi 
 |-  ( ph -> ran T C_ RR* )
153 supxrcl 
 |-  ( ran T C_ RR* -> sup ( ran T , RR* , < ) e. RR* )
154 152 153 syl 
 |-  ( ph -> sup ( ran T , RR* , < ) e. RR* )
155 119 fdmd 
 |-  ( ph -> dom T = NN )
156 136 155 eleqtrrid 
 |-  ( ph -> 1 e. dom T )
157 156 ne0d 
 |-  ( ph -> dom T =/= (/) )
158 dm0rn0 
 |-  ( dom T = (/) <-> ran T = (/) )
159 158 necon3bii 
 |-  ( dom T =/= (/) <-> ran T =/= (/) )
160 157 159 sylib 
 |-  ( ph -> ran T =/= (/) )
161 supxrgtmnf 
 |-  ( ( ran T C_ RR /\ ran T =/= (/) ) -> -oo < sup ( ran T , RR* , < ) )
162 121 160 161 syl2anc 
 |-  ( ph -> -oo < sup ( ran T , RR* , < ) )
163 xrre 
 |-  ( ( ( sup ( ran T , RR* , < ) e. RR* /\ ( ( vol* ` B ) + ( C / 2 ) ) e. RR ) /\ ( -oo < sup ( ran T , RR* , < ) /\ sup ( ran T , RR* , < ) <_ ( ( vol* ` B ) + ( C / 2 ) ) ) ) -> sup ( ran T , RR* , < ) e. RR )
164 154 130 162 12 163 syl22anc 
 |-  ( ph -> sup ( ran T , RR* , < ) e. RR )
165 164 adantr 
 |-  ( ( ph /\ k e. NN ) -> sup ( ran T , RR* , < ) e. RR )
166 supxrub 
 |-  ( ( ran T C_ RR* /\ ( T ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) e. ran T ) -> ( T ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) <_ sup ( ran T , RR* , < ) )
167 152 125 166 syl2an2r 
 |-  ( ( ph /\ k e. NN ) -> ( T ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) <_ sup ( ran T , RR* , < ) )
168 12 adantr 
 |-  ( ( ph /\ k e. NN ) -> sup ( ran T , RR* , < ) <_ ( ( vol* ` B ) + ( C / 2 ) ) )
169 126 165 131 167 168 letrd 
 |-  ( ( ph /\ k e. NN ) -> ( T ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) <_ ( ( vol* ` B ) + ( C / 2 ) ) )
170 116 126 129 131 151 169 le2addd 
 |-  ( ( ph /\ k e. NN ) -> ( ( S ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) + ( T ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) <_ ( ( ( vol* ` A ) + ( C / 2 ) ) + ( ( vol* ` B ) + ( C / 2 ) ) ) )
171 oveq2 
 |-  ( z = 1 -> ( 2 x. z ) = ( 2 x. 1 ) )
172 171 fveq2d 
 |-  ( z = 1 -> ( U ` ( 2 x. z ) ) = ( U ` ( 2 x. 1 ) ) )
173 fveq2 
 |-  ( z = 1 -> ( S ` z ) = ( S ` 1 ) )
174 fveq2 
 |-  ( z = 1 -> ( T ` z ) = ( T ` 1 ) )
175 173 174 oveq12d 
 |-  ( z = 1 -> ( ( S ` z ) + ( T ` z ) ) = ( ( S ` 1 ) + ( T ` 1 ) ) )
176 172 175 eqeq12d 
 |-  ( z = 1 -> ( ( U ` ( 2 x. z ) ) = ( ( S ` z ) + ( T ` z ) ) <-> ( U ` ( 2 x. 1 ) ) = ( ( S ` 1 ) + ( T ` 1 ) ) ) )
177 176 imbi2d 
 |-  ( z = 1 -> ( ( ph -> ( U ` ( 2 x. z ) ) = ( ( S ` z ) + ( T ` z ) ) ) <-> ( ph -> ( U ` ( 2 x. 1 ) ) = ( ( S ` 1 ) + ( T ` 1 ) ) ) ) )
178 oveq2 
 |-  ( z = k -> ( 2 x. z ) = ( 2 x. k ) )
179 178 fveq2d 
 |-  ( z = k -> ( U ` ( 2 x. z ) ) = ( U ` ( 2 x. k ) ) )
180 fveq2 
 |-  ( z = k -> ( S ` z ) = ( S ` k ) )
181 fveq2 
 |-  ( z = k -> ( T ` z ) = ( T ` k ) )
182 180 181 oveq12d 
 |-  ( z = k -> ( ( S ` z ) + ( T ` z ) ) = ( ( S ` k ) + ( T ` k ) ) )
183 179 182 eqeq12d 
 |-  ( z = k -> ( ( U ` ( 2 x. z ) ) = ( ( S ` z ) + ( T ` z ) ) <-> ( U ` ( 2 x. k ) ) = ( ( S ` k ) + ( T ` k ) ) ) )
184 183 imbi2d 
 |-  ( z = k -> ( ( ph -> ( U ` ( 2 x. z ) ) = ( ( S ` z ) + ( T ` z ) ) ) <-> ( ph -> ( U ` ( 2 x. k ) ) = ( ( S ` k ) + ( T ` k ) ) ) ) )
185 oveq2 
 |-  ( z = ( k + 1 ) -> ( 2 x. z ) = ( 2 x. ( k + 1 ) ) )
186 185 fveq2d 
 |-  ( z = ( k + 1 ) -> ( U ` ( 2 x. z ) ) = ( U ` ( 2 x. ( k + 1 ) ) ) )
187 fveq2 
 |-  ( z = ( k + 1 ) -> ( S ` z ) = ( S ` ( k + 1 ) ) )
188 fveq2 
 |-  ( z = ( k + 1 ) -> ( T ` z ) = ( T ` ( k + 1 ) ) )
189 187 188 oveq12d 
 |-  ( z = ( k + 1 ) -> ( ( S ` z ) + ( T ` z ) ) = ( ( S ` ( k + 1 ) ) + ( T ` ( k + 1 ) ) ) )
190 186 189 eqeq12d 
 |-  ( z = ( k + 1 ) -> ( ( U ` ( 2 x. z ) ) = ( ( S ` z ) + ( T ` z ) ) <-> ( U ` ( 2 x. ( k + 1 ) ) ) = ( ( S ` ( k + 1 ) ) + ( T ` ( k + 1 ) ) ) ) )
191 190 imbi2d 
 |-  ( z = ( k + 1 ) -> ( ( ph -> ( U ` ( 2 x. z ) ) = ( ( S ` z ) + ( T ` z ) ) ) <-> ( ph -> ( U ` ( 2 x. ( k + 1 ) ) ) = ( ( S ` ( k + 1 ) ) + ( T ` ( k + 1 ) ) ) ) ) )
192 oveq2 
 |-  ( z = ( |_ ` ( ( k + 1 ) / 2 ) ) -> ( 2 x. z ) = ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) )
193 192 fveq2d 
 |-  ( z = ( |_ ` ( ( k + 1 ) / 2 ) ) -> ( U ` ( 2 x. z ) ) = ( U ` ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) )
194 fveq2 
 |-  ( z = ( |_ ` ( ( k + 1 ) / 2 ) ) -> ( S ` z ) = ( S ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) )
195 fveq2 
 |-  ( z = ( |_ ` ( ( k + 1 ) / 2 ) ) -> ( T ` z ) = ( T ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) )
196 194 195 oveq12d 
 |-  ( z = ( |_ ` ( ( k + 1 ) / 2 ) ) -> ( ( S ` z ) + ( T ` z ) ) = ( ( S ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) + ( T ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) )
197 193 196 eqeq12d 
 |-  ( z = ( |_ ` ( ( k + 1 ) / 2 ) ) -> ( ( U ` ( 2 x. z ) ) = ( ( S ` z ) + ( T ` z ) ) <-> ( U ` ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) = ( ( S ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) + ( T ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) ) )
198 197 imbi2d 
 |-  ( z = ( |_ ` ( ( k + 1 ) / 2 ) ) -> ( ( ph -> ( U ` ( 2 x. z ) ) = ( ( S ` z ) + ( T ` z ) ) ) <-> ( ph -> ( U ` ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) = ( ( S ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) + ( T ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) ) ) )
199 6 fveq1i 
 |-  ( U ` ( 2 x. 1 ) ) = ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` ( 2 x. 1 ) )
200 136 a1i 
 |-  ( ph -> 1 e. NN )
201 29 ovolfsval 
 |-  ( ( H : NN --> ( <_ i^i ( RR X. RR ) ) /\ 1 e. NN ) -> ( ( ( abs o. - ) o. H ) ` 1 ) = ( ( 2nd ` ( H ` 1 ) ) - ( 1st ` ( H ` 1 ) ) ) )
202 28 136 201 sylancl 
 |-  ( ph -> ( ( ( abs o. - ) o. H ) ` 1 ) = ( ( 2nd ` ( H ` 1 ) ) - ( 1st ` ( H ` 1 ) ) ) )
203 halfnz 
 |-  -. ( 1 / 2 ) e. ZZ
204 nnz 
 |-  ( ( n / 2 ) e. NN -> ( n / 2 ) e. ZZ )
205 oveq1 
 |-  ( n = 1 -> ( n / 2 ) = ( 1 / 2 ) )
206 205 eleq1d 
 |-  ( n = 1 -> ( ( n / 2 ) e. ZZ <-> ( 1 / 2 ) e. ZZ ) )
207 204 206 imbitrid 
 |-  ( n = 1 -> ( ( n / 2 ) e. NN -> ( 1 / 2 ) e. ZZ ) )
208 203 207 mtoi 
 |-  ( n = 1 -> -. ( n / 2 ) e. NN )
209 208 iffalsed 
 |-  ( n = 1 -> if ( ( n / 2 ) e. NN , ( G ` ( n / 2 ) ) , ( F ` ( ( n + 1 ) / 2 ) ) ) = ( F ` ( ( n + 1 ) / 2 ) ) )
210 oveq1 
 |-  ( n = 1 -> ( n + 1 ) = ( 1 + 1 ) )
211 df-2 
 |-  2 = ( 1 + 1 )
212 210 211 eqtr4di 
 |-  ( n = 1 -> ( n + 1 ) = 2 )
213 212 oveq1d 
 |-  ( n = 1 -> ( ( n + 1 ) / 2 ) = ( 2 / 2 ) )
214 2div2e1 
 |-  ( 2 / 2 ) = 1
215 213 214 eqtrdi 
 |-  ( n = 1 -> ( ( n + 1 ) / 2 ) = 1 )
216 215 fveq2d 
 |-  ( n = 1 -> ( F ` ( ( n + 1 ) / 2 ) ) = ( F ` 1 ) )
217 209 216 eqtrd 
 |-  ( n = 1 -> if ( ( n / 2 ) e. NN , ( G ` ( n / 2 ) ) , ( F ` ( ( n + 1 ) / 2 ) ) ) = ( F ` 1 ) )
218 fvex 
 |-  ( F ` 1 ) e. _V
219 217 13 218 fvmpt 
 |-  ( 1 e. NN -> ( H ` 1 ) = ( F ` 1 ) )
220 136 219 ax-mp 
 |-  ( H ` 1 ) = ( F ` 1 )
221 220 fveq2i 
 |-  ( 2nd ` ( H ` 1 ) ) = ( 2nd ` ( F ` 1 ) )
222 220 fveq2i 
 |-  ( 1st ` ( H ` 1 ) ) = ( 1st ` ( F ` 1 ) )
223 221 222 oveq12i 
 |-  ( ( 2nd ` ( H ` 1 ) ) - ( 1st ` ( H ` 1 ) ) ) = ( ( 2nd ` ( F ` 1 ) ) - ( 1st ` ( F ` 1 ) ) )
224 202 223 eqtrdi 
 |-  ( ph -> ( ( ( abs o. - ) o. H ) ` 1 ) = ( ( 2nd ` ( F ` 1 ) ) - ( 1st ` ( F ` 1 ) ) ) )
225 61 224 seq1i 
 |-  ( ph -> ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` 1 ) = ( ( 2nd ` ( F ` 1 ) ) - ( 1st ` ( F ` 1 ) ) ) )
226 2t1e2 
 |-  ( 2 x. 1 ) = 2
227 226 fveq2i 
 |-  ( ( ( abs o. - ) o. H ) ` ( 2 x. 1 ) ) = ( ( ( abs o. - ) o. H ) ` 2 )
228 29 ovolfsval 
 |-  ( ( H : NN --> ( <_ i^i ( RR X. RR ) ) /\ 2 e. NN ) -> ( ( ( abs o. - ) o. H ) ` 2 ) = ( ( 2nd ` ( H ` 2 ) ) - ( 1st ` ( H ` 2 ) ) ) )
229 28 36 228 sylancl 
 |-  ( ph -> ( ( ( abs o. - ) o. H ) ` 2 ) = ( ( 2nd ` ( H ` 2 ) ) - ( 1st ` ( H ` 2 ) ) ) )
230 oveq1 
 |-  ( n = 2 -> ( n / 2 ) = ( 2 / 2 ) )
231 230 214 eqtrdi 
 |-  ( n = 2 -> ( n / 2 ) = 1 )
232 231 136 eqeltrdi 
 |-  ( n = 2 -> ( n / 2 ) e. NN )
233 232 iftrued 
 |-  ( n = 2 -> if ( ( n / 2 ) e. NN , ( G ` ( n / 2 ) ) , ( F ` ( ( n + 1 ) / 2 ) ) ) = ( G ` ( n / 2 ) ) )
234 231 fveq2d 
 |-  ( n = 2 -> ( G ` ( n / 2 ) ) = ( G ` 1 ) )
235 233 234 eqtrd 
 |-  ( n = 2 -> if ( ( n / 2 ) e. NN , ( G ` ( n / 2 ) ) , ( F ` ( ( n + 1 ) / 2 ) ) ) = ( G ` 1 ) )
236 fvex 
 |-  ( G ` 1 ) e. _V
237 235 13 236 fvmpt 
 |-  ( 2 e. NN -> ( H ` 2 ) = ( G ` 1 ) )
238 36 237 ax-mp 
 |-  ( H ` 2 ) = ( G ` 1 )
239 238 fveq2i 
 |-  ( 2nd ` ( H ` 2 ) ) = ( 2nd ` ( G ` 1 ) )
240 238 fveq2i 
 |-  ( 1st ` ( H ` 2 ) ) = ( 1st ` ( G ` 1 ) )
241 239 240 oveq12i 
 |-  ( ( 2nd ` ( H ` 2 ) ) - ( 1st ` ( H ` 2 ) ) ) = ( ( 2nd ` ( G ` 1 ) ) - ( 1st ` ( G ` 1 ) ) )
242 229 241 eqtrdi 
 |-  ( ph -> ( ( ( abs o. - ) o. H ) ` 2 ) = ( ( 2nd ` ( G ` 1 ) ) - ( 1st ` ( G ` 1 ) ) ) )
243 227 242 eqtrid 
 |-  ( ph -> ( ( ( abs o. - ) o. H ) ` ( 2 x. 1 ) ) = ( ( 2nd ` ( G ` 1 ) ) - ( 1st ` ( G ` 1 ) ) ) )
244 78 200 43 225 243 seqp1d 
 |-  ( ph -> ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` ( 2 x. 1 ) ) = ( ( ( 2nd ` ( F ` 1 ) ) - ( 1st ` ( F ` 1 ) ) ) + ( ( 2nd ` ( G ` 1 ) ) - ( 1st ` ( G ` 1 ) ) ) ) )
245 199 244 eqtrid 
 |-  ( ph -> ( U ` ( 2 x. 1 ) ) = ( ( ( 2nd ` ( F ` 1 ) ) - ( 1st ` ( F ` 1 ) ) ) + ( ( 2nd ` ( G ` 1 ) ) - ( 1st ` ( G ` 1 ) ) ) ) )
246 4 fveq1i 
 |-  ( S ` 1 ) = ( seq 1 ( + , ( ( abs o. - ) o. F ) ) ` 1 )
247 107 ovolfsval 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ 1 e. NN ) -> ( ( ( abs o. - ) o. F ) ` 1 ) = ( ( 2nd ` ( F ` 1 ) ) - ( 1st ` ( F ` 1 ) ) ) )
248 23 136 247 sylancl 
 |-  ( ph -> ( ( ( abs o. - ) o. F ) ` 1 ) = ( ( 2nd ` ( F ` 1 ) ) - ( 1st ` ( F ` 1 ) ) ) )
249 61 248 seq1i 
 |-  ( ph -> ( seq 1 ( + , ( ( abs o. - ) o. F ) ) ` 1 ) = ( ( 2nd ` ( F ` 1 ) ) - ( 1st ` ( F ` 1 ) ) ) )
250 246 249 eqtrid 
 |-  ( ph -> ( S ` 1 ) = ( ( 2nd ` ( F ` 1 ) ) - ( 1st ` ( F ` 1 ) ) ) )
251 5 fveq1i 
 |-  ( T ` 1 ) = ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` 1 )
252 117 ovolfsval 
 |-  ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ 1 e. NN ) -> ( ( ( abs o. - ) o. G ) ` 1 ) = ( ( 2nd ` ( G ` 1 ) ) - ( 1st ` ( G ` 1 ) ) ) )
253 15 136 252 sylancl 
 |-  ( ph -> ( ( ( abs o. - ) o. G ) ` 1 ) = ( ( 2nd ` ( G ` 1 ) ) - ( 1st ` ( G ` 1 ) ) ) )
254 61 253 seq1i 
 |-  ( ph -> ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` 1 ) = ( ( 2nd ` ( G ` 1 ) ) - ( 1st ` ( G ` 1 ) ) ) )
255 251 254 eqtrid 
 |-  ( ph -> ( T ` 1 ) = ( ( 2nd ` ( G ` 1 ) ) - ( 1st ` ( G ` 1 ) ) ) )
256 250 255 oveq12d 
 |-  ( ph -> ( ( S ` 1 ) + ( T ` 1 ) ) = ( ( ( 2nd ` ( F ` 1 ) ) - ( 1st ` ( F ` 1 ) ) ) + ( ( 2nd ` ( G ` 1 ) ) - ( 1st ` ( G ` 1 ) ) ) ) )
257 245 256 eqtr4d 
 |-  ( ph -> ( U ` ( 2 x. 1 ) ) = ( ( S ` 1 ) + ( T ` 1 ) ) )
258 oveq1 
 |-  ( ( U ` ( 2 x. k ) ) = ( ( S ` k ) + ( T ` k ) ) -> ( ( U ` ( 2 x. k ) ) + ( ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) + ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) ) ) = ( ( ( S ` k ) + ( T ` k ) ) + ( ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) + ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) ) ) )
259 43 oveq2i 
 |-  ( ( 2 x. k ) + ( 2 x. 1 ) ) = ( ( 2 x. k ) + ( 1 + 1 ) )
260 2cnd 
 |-  ( ( ph /\ k e. NN ) -> 2 e. CC )
261 47 recnd 
 |-  ( ( ph /\ k e. NN ) -> k e. CC )
262 1cnd 
 |-  ( ( ph /\ k e. NN ) -> 1 e. CC )
263 260 261 262 adddid 
 |-  ( ( ph /\ k e. NN ) -> ( 2 x. ( k + 1 ) ) = ( ( 2 x. k ) + ( 2 x. 1 ) ) )
264 nnmulcl 
 |-  ( ( 2 e. NN /\ k e. NN ) -> ( 2 x. k ) e. NN )
265 36 264 mpan 
 |-  ( k e. NN -> ( 2 x. k ) e. NN )
266 265 adantl 
 |-  ( ( ph /\ k e. NN ) -> ( 2 x. k ) e. NN )
267 266 nncnd 
 |-  ( ( ph /\ k e. NN ) -> ( 2 x. k ) e. CC )
268 267 262 262 addassd 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( 2 x. k ) + 1 ) + 1 ) = ( ( 2 x. k ) + ( 1 + 1 ) ) )
269 259 263 268 3eqtr4a 
 |-  ( ( ph /\ k e. NN ) -> ( 2 x. ( k + 1 ) ) = ( ( ( 2 x. k ) + 1 ) + 1 ) )
270 269 fveq2d 
 |-  ( ( ph /\ k e. NN ) -> ( U ` ( 2 x. ( k + 1 ) ) ) = ( U ` ( ( ( 2 x. k ) + 1 ) + 1 ) ) )
271 6 fveq1i 
 |-  ( U ` ( ( ( 2 x. k ) + 1 ) + 1 ) ) = ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` ( ( ( 2 x. k ) + 1 ) + 1 ) )
272 266 peano2nnd 
 |-  ( ( ph /\ k e. NN ) -> ( ( 2 x. k ) + 1 ) e. NN )
273 272 78 eleqtrdi 
 |-  ( ( ph /\ k e. NN ) -> ( ( 2 x. k ) + 1 ) e. ( ZZ>= ` 1 ) )
274 seqp1 
 |-  ( ( ( 2 x. k ) + 1 ) e. ( ZZ>= ` 1 ) -> ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` ( ( ( 2 x. k ) + 1 ) + 1 ) ) = ( ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` ( ( 2 x. k ) + 1 ) ) + ( ( ( abs o. - ) o. H ) ` ( ( ( 2 x. k ) + 1 ) + 1 ) ) ) )
275 273 274 syl 
 |-  ( ( ph /\ k e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` ( ( ( 2 x. k ) + 1 ) + 1 ) ) = ( ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` ( ( 2 x. k ) + 1 ) ) + ( ( ( abs o. - ) o. H ) ` ( ( ( 2 x. k ) + 1 ) + 1 ) ) ) )
276 266 78 eleqtrdi 
 |-  ( ( ph /\ k e. NN ) -> ( 2 x. k ) e. ( ZZ>= ` 1 ) )
277 seqp1 
 |-  ( ( 2 x. k ) e. ( ZZ>= ` 1 ) -> ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` ( ( 2 x. k ) + 1 ) ) = ( ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` ( 2 x. k ) ) + ( ( ( abs o. - ) o. H ) ` ( ( 2 x. k ) + 1 ) ) ) )
278 276 277 syl 
 |-  ( ( ph /\ k e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` ( ( 2 x. k ) + 1 ) ) = ( ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` ( 2 x. k ) ) + ( ( ( abs o. - ) o. H ) ` ( ( 2 x. k ) + 1 ) ) ) )
279 6 fveq1i 
 |-  ( U ` ( 2 x. k ) ) = ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` ( 2 x. k ) )
280 279 a1i 
 |-  ( ( ph /\ k e. NN ) -> ( U ` ( 2 x. k ) ) = ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` ( 2 x. k ) ) )
281 oveq1 
 |-  ( n = ( ( 2 x. k ) + 1 ) -> ( n / 2 ) = ( ( ( 2 x. k ) + 1 ) / 2 ) )
282 281 eleq1d 
 |-  ( n = ( ( 2 x. k ) + 1 ) -> ( ( n / 2 ) e. NN <-> ( ( ( 2 x. k ) + 1 ) / 2 ) e. NN ) )
283 281 fveq2d 
 |-  ( n = ( ( 2 x. k ) + 1 ) -> ( G ` ( n / 2 ) ) = ( G ` ( ( ( 2 x. k ) + 1 ) / 2 ) ) )
284 oveq1 
 |-  ( n = ( ( 2 x. k ) + 1 ) -> ( n + 1 ) = ( ( ( 2 x. k ) + 1 ) + 1 ) )
285 284 fvoveq1d 
 |-  ( n = ( ( 2 x. k ) + 1 ) -> ( F ` ( ( n + 1 ) / 2 ) ) = ( F ` ( ( ( ( 2 x. k ) + 1 ) + 1 ) / 2 ) ) )
286 282 283 285 ifbieq12d 
 |-  ( n = ( ( 2 x. k ) + 1 ) -> if ( ( n / 2 ) e. NN , ( G ` ( n / 2 ) ) , ( F ` ( ( n + 1 ) / 2 ) ) ) = if ( ( ( ( 2 x. k ) + 1 ) / 2 ) e. NN , ( G ` ( ( ( 2 x. k ) + 1 ) / 2 ) ) , ( F ` ( ( ( ( 2 x. k ) + 1 ) + 1 ) / 2 ) ) ) )
287 fvex 
 |-  ( G ` ( ( ( 2 x. k ) + 1 ) / 2 ) ) e. _V
288 fvex 
 |-  ( F ` ( ( ( ( 2 x. k ) + 1 ) + 1 ) / 2 ) ) e. _V
289 287 288 ifex 
 |-  if ( ( ( ( 2 x. k ) + 1 ) / 2 ) e. NN , ( G ` ( ( ( 2 x. k ) + 1 ) / 2 ) ) , ( F ` ( ( ( ( 2 x. k ) + 1 ) + 1 ) / 2 ) ) ) e. _V
290 286 13 289 fvmpt 
 |-  ( ( ( 2 x. k ) + 1 ) e. NN -> ( H ` ( ( 2 x. k ) + 1 ) ) = if ( ( ( ( 2 x. k ) + 1 ) / 2 ) e. NN , ( G ` ( ( ( 2 x. k ) + 1 ) / 2 ) ) , ( F ` ( ( ( ( 2 x. k ) + 1 ) + 1 ) / 2 ) ) ) )
291 272 290 syl 
 |-  ( ( ph /\ k e. NN ) -> ( H ` ( ( 2 x. k ) + 1 ) ) = if ( ( ( ( 2 x. k ) + 1 ) / 2 ) e. NN , ( G ` ( ( ( 2 x. k ) + 1 ) / 2 ) ) , ( F ` ( ( ( ( 2 x. k ) + 1 ) + 1 ) / 2 ) ) ) )
292 2ne0 
 |-  2 =/= 0
293 292 a1i 
 |-  ( ( ph /\ k e. NN ) -> 2 =/= 0 )
294 261 260 293 divcan3d 
 |-  ( ( ph /\ k e. NN ) -> ( ( 2 x. k ) / 2 ) = k )
295 294 77 eqeltrd 
 |-  ( ( ph /\ k e. NN ) -> ( ( 2 x. k ) / 2 ) e. NN )
296 nneo 
 |-  ( ( 2 x. k ) e. NN -> ( ( ( 2 x. k ) / 2 ) e. NN <-> -. ( ( ( 2 x. k ) + 1 ) / 2 ) e. NN ) )
297 266 296 syl 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( 2 x. k ) / 2 ) e. NN <-> -. ( ( ( 2 x. k ) + 1 ) / 2 ) e. NN ) )
298 295 297 mpbid 
 |-  ( ( ph /\ k e. NN ) -> -. ( ( ( 2 x. k ) + 1 ) / 2 ) e. NN )
299 298 iffalsed 
 |-  ( ( ph /\ k e. NN ) -> if ( ( ( ( 2 x. k ) + 1 ) / 2 ) e. NN , ( G ` ( ( ( 2 x. k ) + 1 ) / 2 ) ) , ( F ` ( ( ( ( 2 x. k ) + 1 ) + 1 ) / 2 ) ) ) = ( F ` ( ( ( ( 2 x. k ) + 1 ) + 1 ) / 2 ) ) )
300 269 oveq1d 
 |-  ( ( ph /\ k e. NN ) -> ( ( 2 x. ( k + 1 ) ) / 2 ) = ( ( ( ( 2 x. k ) + 1 ) + 1 ) / 2 ) )
301 38 nncnd 
 |-  ( ( ph /\ k e. NN ) -> ( k + 1 ) e. CC )
302 2cn 
 |-  2 e. CC
303 divcan3 
 |-  ( ( ( k + 1 ) e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( ( 2 x. ( k + 1 ) ) / 2 ) = ( k + 1 ) )
304 302 292 303 mp3an23 
 |-  ( ( k + 1 ) e. CC -> ( ( 2 x. ( k + 1 ) ) / 2 ) = ( k + 1 ) )
305 301 304 syl 
 |-  ( ( ph /\ k e. NN ) -> ( ( 2 x. ( k + 1 ) ) / 2 ) = ( k + 1 ) )
306 300 305 eqtr3d 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( ( 2 x. k ) + 1 ) + 1 ) / 2 ) = ( k + 1 ) )
307 306 fveq2d 
 |-  ( ( ph /\ k e. NN ) -> ( F ` ( ( ( ( 2 x. k ) + 1 ) + 1 ) / 2 ) ) = ( F ` ( k + 1 ) ) )
308 291 299 307 3eqtrd 
 |-  ( ( ph /\ k e. NN ) -> ( H ` ( ( 2 x. k ) + 1 ) ) = ( F ` ( k + 1 ) ) )
309 308 fveq2d 
 |-  ( ( ph /\ k e. NN ) -> ( 2nd ` ( H ` ( ( 2 x. k ) + 1 ) ) ) = ( 2nd ` ( F ` ( k + 1 ) ) ) )
310 308 fveq2d 
 |-  ( ( ph /\ k e. NN ) -> ( 1st ` ( H ` ( ( 2 x. k ) + 1 ) ) ) = ( 1st ` ( F ` ( k + 1 ) ) ) )
311 309 310 oveq12d 
 |-  ( ( ph /\ k e. NN ) -> ( ( 2nd ` ( H ` ( ( 2 x. k ) + 1 ) ) ) - ( 1st ` ( H ` ( ( 2 x. k ) + 1 ) ) ) ) = ( ( 2nd ` ( F ` ( k + 1 ) ) ) - ( 1st ` ( F ` ( k + 1 ) ) ) ) )
312 29 ovolfsval 
 |-  ( ( H : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( ( 2 x. k ) + 1 ) e. NN ) -> ( ( ( abs o. - ) o. H ) ` ( ( 2 x. k ) + 1 ) ) = ( ( 2nd ` ( H ` ( ( 2 x. k ) + 1 ) ) ) - ( 1st ` ( H ` ( ( 2 x. k ) + 1 ) ) ) ) )
313 28 272 312 syl2an2r 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( abs o. - ) o. H ) ` ( ( 2 x. k ) + 1 ) ) = ( ( 2nd ` ( H ` ( ( 2 x. k ) + 1 ) ) ) - ( 1st ` ( H ` ( ( 2 x. k ) + 1 ) ) ) ) )
314 107 ovolfsval 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( k + 1 ) e. NN ) -> ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) = ( ( 2nd ` ( F ` ( k + 1 ) ) ) - ( 1st ` ( F ` ( k + 1 ) ) ) ) )
315 23 37 314 syl2an 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) = ( ( 2nd ` ( F ` ( k + 1 ) ) ) - ( 1st ` ( F ` ( k + 1 ) ) ) ) )
316 311 313 315 3eqtr4rd 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) = ( ( ( abs o. - ) o. H ) ` ( ( 2 x. k ) + 1 ) ) )
317 280 316 oveq12d 
 |-  ( ( ph /\ k e. NN ) -> ( ( U ` ( 2 x. k ) ) + ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) ) = ( ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` ( 2 x. k ) ) + ( ( ( abs o. - ) o. H ) ` ( ( 2 x. k ) + 1 ) ) ) )
318 278 317 eqtr4d 
 |-  ( ( ph /\ k e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` ( ( 2 x. k ) + 1 ) ) = ( ( U ` ( 2 x. k ) ) + ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) ) )
319 269 fveq2d 
 |-  ( ( ph /\ k e. NN ) -> ( H ` ( 2 x. ( k + 1 ) ) ) = ( H ` ( ( ( 2 x. k ) + 1 ) + 1 ) ) )
320 272 peano2nnd 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( 2 x. k ) + 1 ) + 1 ) e. NN )
321 269 320 eqeltrd 
 |-  ( ( ph /\ k e. NN ) -> ( 2 x. ( k + 1 ) ) e. NN )
322 oveq1 
 |-  ( n = ( 2 x. ( k + 1 ) ) -> ( n / 2 ) = ( ( 2 x. ( k + 1 ) ) / 2 ) )
323 322 eleq1d 
 |-  ( n = ( 2 x. ( k + 1 ) ) -> ( ( n / 2 ) e. NN <-> ( ( 2 x. ( k + 1 ) ) / 2 ) e. NN ) )
324 322 fveq2d 
 |-  ( n = ( 2 x. ( k + 1 ) ) -> ( G ` ( n / 2 ) ) = ( G ` ( ( 2 x. ( k + 1 ) ) / 2 ) ) )
325 oveq1 
 |-  ( n = ( 2 x. ( k + 1 ) ) -> ( n + 1 ) = ( ( 2 x. ( k + 1 ) ) + 1 ) )
326 325 fvoveq1d 
 |-  ( n = ( 2 x. ( k + 1 ) ) -> ( F ` ( ( n + 1 ) / 2 ) ) = ( F ` ( ( ( 2 x. ( k + 1 ) ) + 1 ) / 2 ) ) )
327 323 324 326 ifbieq12d 
 |-  ( n = ( 2 x. ( k + 1 ) ) -> if ( ( n / 2 ) e. NN , ( G ` ( n / 2 ) ) , ( F ` ( ( n + 1 ) / 2 ) ) ) = if ( ( ( 2 x. ( k + 1 ) ) / 2 ) e. NN , ( G ` ( ( 2 x. ( k + 1 ) ) / 2 ) ) , ( F ` ( ( ( 2 x. ( k + 1 ) ) + 1 ) / 2 ) ) ) )
328 fvex 
 |-  ( G ` ( ( 2 x. ( k + 1 ) ) / 2 ) ) e. _V
329 fvex 
 |-  ( F ` ( ( ( 2 x. ( k + 1 ) ) + 1 ) / 2 ) ) e. _V
330 328 329 ifex 
 |-  if ( ( ( 2 x. ( k + 1 ) ) / 2 ) e. NN , ( G ` ( ( 2 x. ( k + 1 ) ) / 2 ) ) , ( F ` ( ( ( 2 x. ( k + 1 ) ) + 1 ) / 2 ) ) ) e. _V
331 327 13 330 fvmpt 
 |-  ( ( 2 x. ( k + 1 ) ) e. NN -> ( H ` ( 2 x. ( k + 1 ) ) ) = if ( ( ( 2 x. ( k + 1 ) ) / 2 ) e. NN , ( G ` ( ( 2 x. ( k + 1 ) ) / 2 ) ) , ( F ` ( ( ( 2 x. ( k + 1 ) ) + 1 ) / 2 ) ) ) )
332 321 331 syl 
 |-  ( ( ph /\ k e. NN ) -> ( H ` ( 2 x. ( k + 1 ) ) ) = if ( ( ( 2 x. ( k + 1 ) ) / 2 ) e. NN , ( G ` ( ( 2 x. ( k + 1 ) ) / 2 ) ) , ( F ` ( ( ( 2 x. ( k + 1 ) ) + 1 ) / 2 ) ) ) )
333 305 38 eqeltrd 
 |-  ( ( ph /\ k e. NN ) -> ( ( 2 x. ( k + 1 ) ) / 2 ) e. NN )
334 333 iftrued 
 |-  ( ( ph /\ k e. NN ) -> if ( ( ( 2 x. ( k + 1 ) ) / 2 ) e. NN , ( G ` ( ( 2 x. ( k + 1 ) ) / 2 ) ) , ( F ` ( ( ( 2 x. ( k + 1 ) ) + 1 ) / 2 ) ) ) = ( G ` ( ( 2 x. ( k + 1 ) ) / 2 ) ) )
335 305 fveq2d 
 |-  ( ( ph /\ k e. NN ) -> ( G ` ( ( 2 x. ( k + 1 ) ) / 2 ) ) = ( G ` ( k + 1 ) ) )
336 332 334 335 3eqtrd 
 |-  ( ( ph /\ k e. NN ) -> ( H ` ( 2 x. ( k + 1 ) ) ) = ( G ` ( k + 1 ) ) )
337 319 336 eqtr3d 
 |-  ( ( ph /\ k e. NN ) -> ( H ` ( ( ( 2 x. k ) + 1 ) + 1 ) ) = ( G ` ( k + 1 ) ) )
338 337 fveq2d 
 |-  ( ( ph /\ k e. NN ) -> ( 2nd ` ( H ` ( ( ( 2 x. k ) + 1 ) + 1 ) ) ) = ( 2nd ` ( G ` ( k + 1 ) ) ) )
339 337 fveq2d 
 |-  ( ( ph /\ k e. NN ) -> ( 1st ` ( H ` ( ( ( 2 x. k ) + 1 ) + 1 ) ) ) = ( 1st ` ( G ` ( k + 1 ) ) ) )
340 338 339 oveq12d 
 |-  ( ( ph /\ k e. NN ) -> ( ( 2nd ` ( H ` ( ( ( 2 x. k ) + 1 ) + 1 ) ) ) - ( 1st ` ( H ` ( ( ( 2 x. k ) + 1 ) + 1 ) ) ) ) = ( ( 2nd ` ( G ` ( k + 1 ) ) ) - ( 1st ` ( G ` ( k + 1 ) ) ) ) )
341 29 ovolfsval 
 |-  ( ( H : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( ( ( 2 x. k ) + 1 ) + 1 ) e. NN ) -> ( ( ( abs o. - ) o. H ) ` ( ( ( 2 x. k ) + 1 ) + 1 ) ) = ( ( 2nd ` ( H ` ( ( ( 2 x. k ) + 1 ) + 1 ) ) ) - ( 1st ` ( H ` ( ( ( 2 x. k ) + 1 ) + 1 ) ) ) ) )
342 28 320 341 syl2an2r 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( abs o. - ) o. H ) ` ( ( ( 2 x. k ) + 1 ) + 1 ) ) = ( ( 2nd ` ( H ` ( ( ( 2 x. k ) + 1 ) + 1 ) ) ) - ( 1st ` ( H ` ( ( ( 2 x. k ) + 1 ) + 1 ) ) ) ) )
343 117 ovolfsval 
 |-  ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( k + 1 ) e. NN ) -> ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) = ( ( 2nd ` ( G ` ( k + 1 ) ) ) - ( 1st ` ( G ` ( k + 1 ) ) ) ) )
344 15 37 343 syl2an 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) = ( ( 2nd ` ( G ` ( k + 1 ) ) ) - ( 1st ` ( G ` ( k + 1 ) ) ) ) )
345 340 342 344 3eqtr4d 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( abs o. - ) o. H ) ` ( ( ( 2 x. k ) + 1 ) + 1 ) ) = ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) )
346 318 345 oveq12d 
 |-  ( ( ph /\ k e. NN ) -> ( ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` ( ( 2 x. k ) + 1 ) ) + ( ( ( abs o. - ) o. H ) ` ( ( ( 2 x. k ) + 1 ) + 1 ) ) ) = ( ( ( U ` ( 2 x. k ) ) + ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) ) + ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) ) )
347 275 346 eqtrd 
 |-  ( ( ph /\ k e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. H ) ) ` ( ( ( 2 x. k ) + 1 ) + 1 ) ) = ( ( ( U ` ( 2 x. k ) ) + ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) ) + ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) ) )
348 271 347 eqtrid 
 |-  ( ( ph /\ k e. NN ) -> ( U ` ( ( ( 2 x. k ) + 1 ) + 1 ) ) = ( ( ( U ` ( 2 x. k ) ) + ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) ) + ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) ) )
349 ffvelcdm 
 |-  ( ( U : NN --> ( 0 [,) +oo ) /\ ( 2 x. k ) e. NN ) -> ( U ` ( 2 x. k ) ) e. ( 0 [,) +oo ) )
350 31 265 349 syl2an 
 |-  ( ( ph /\ k e. NN ) -> ( U ` ( 2 x. k ) ) e. ( 0 [,) +oo ) )
351 32 350 sselid 
 |-  ( ( ph /\ k e. NN ) -> ( U ` ( 2 x. k ) ) e. RR )
352 351 recnd 
 |-  ( ( ph /\ k e. NN ) -> ( U ` ( 2 x. k ) ) e. CC )
353 107 ovolfsf 
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> ( ( abs o. - ) o. F ) : NN --> ( 0 [,) +oo ) )
354 23 353 syl 
 |-  ( ph -> ( ( abs o. - ) o. F ) : NN --> ( 0 [,) +oo ) )
355 ffvelcdm 
 |-  ( ( ( ( abs o. - ) o. F ) : NN --> ( 0 [,) +oo ) /\ ( k + 1 ) e. NN ) -> ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) e. ( 0 [,) +oo ) )
356 354 37 355 syl2an 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) e. ( 0 [,) +oo ) )
357 32 356 sselid 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) e. RR )
358 357 recnd 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) e. CC )
359 117 ovolfsf 
 |-  ( G : NN --> ( <_ i^i ( RR X. RR ) ) -> ( ( abs o. - ) o. G ) : NN --> ( 0 [,) +oo ) )
360 15 359 syl 
 |-  ( ph -> ( ( abs o. - ) o. G ) : NN --> ( 0 [,) +oo ) )
361 ffvelcdm 
 |-  ( ( ( ( abs o. - ) o. G ) : NN --> ( 0 [,) +oo ) /\ ( k + 1 ) e. NN ) -> ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) e. ( 0 [,) +oo ) )
362 360 37 361 syl2an 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) e. ( 0 [,) +oo ) )
363 32 362 sselid 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) e. RR )
364 363 recnd 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) e. CC )
365 352 358 364 addassd 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( U ` ( 2 x. k ) ) + ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) ) + ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) ) = ( ( U ` ( 2 x. k ) ) + ( ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) + ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) ) ) )
366 270 348 365 3eqtrd 
 |-  ( ( ph /\ k e. NN ) -> ( U ` ( 2 x. ( k + 1 ) ) ) = ( ( U ` ( 2 x. k ) ) + ( ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) + ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) ) ) )
367 seqp1 
 |-  ( k e. ( ZZ>= ` 1 ) -> ( seq 1 ( + , ( ( abs o. - ) o. F ) ) ` ( k + 1 ) ) = ( ( seq 1 ( + , ( ( abs o. - ) o. F ) ) ` k ) + ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) ) )
368 79 367 syl 
 |-  ( ( ph /\ k e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. F ) ) ` ( k + 1 ) ) = ( ( seq 1 ( + , ( ( abs o. - ) o. F ) ) ` k ) + ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) ) )
369 4 fveq1i 
 |-  ( S ` ( k + 1 ) ) = ( seq 1 ( + , ( ( abs o. - ) o. F ) ) ` ( k + 1 ) )
370 4 fveq1i 
 |-  ( S ` k ) = ( seq 1 ( + , ( ( abs o. - ) o. F ) ) ` k )
371 370 oveq1i 
 |-  ( ( S ` k ) + ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) ) = ( ( seq 1 ( + , ( ( abs o. - ) o. F ) ) ` k ) + ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) )
372 368 369 371 3eqtr4g 
 |-  ( ( ph /\ k e. NN ) -> ( S ` ( k + 1 ) ) = ( ( S ` k ) + ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) ) )
373 seqp1 
 |-  ( k e. ( ZZ>= ` 1 ) -> ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` ( k + 1 ) ) = ( ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` k ) + ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) ) )
374 79 373 syl 
 |-  ( ( ph /\ k e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` ( k + 1 ) ) = ( ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` k ) + ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) ) )
375 5 fveq1i 
 |-  ( T ` ( k + 1 ) ) = ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` ( k + 1 ) )
376 5 fveq1i 
 |-  ( T ` k ) = ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` k )
377 376 oveq1i 
 |-  ( ( T ` k ) + ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) ) = ( ( seq 1 ( + , ( ( abs o. - ) o. G ) ) ` k ) + ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) )
378 374 375 377 3eqtr4g 
 |-  ( ( ph /\ k e. NN ) -> ( T ` ( k + 1 ) ) = ( ( T ` k ) + ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) ) )
379 372 378 oveq12d 
 |-  ( ( ph /\ k e. NN ) -> ( ( S ` ( k + 1 ) ) + ( T ` ( k + 1 ) ) ) = ( ( ( S ` k ) + ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) ) + ( ( T ` k ) + ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) ) ) )
380 109 ffvelcdmda 
 |-  ( ( ph /\ k e. NN ) -> ( S ` k ) e. ( 0 [,) +oo ) )
381 32 380 sselid 
 |-  ( ( ph /\ k e. NN ) -> ( S ` k ) e. RR )
382 381 recnd 
 |-  ( ( ph /\ k e. NN ) -> ( S ` k ) e. CC )
383 119 ffvelcdmda 
 |-  ( ( ph /\ k e. NN ) -> ( T ` k ) e. ( 0 [,) +oo ) )
384 32 383 sselid 
 |-  ( ( ph /\ k e. NN ) -> ( T ` k ) e. RR )
385 384 recnd 
 |-  ( ( ph /\ k e. NN ) -> ( T ` k ) e. CC )
386 382 358 385 364 add4d 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( S ` k ) + ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) ) + ( ( T ` k ) + ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) ) ) = ( ( ( S ` k ) + ( T ` k ) ) + ( ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) + ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) ) ) )
387 379 386 eqtrd 
 |-  ( ( ph /\ k e. NN ) -> ( ( S ` ( k + 1 ) ) + ( T ` ( k + 1 ) ) ) = ( ( ( S ` k ) + ( T ` k ) ) + ( ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) + ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) ) ) )
388 366 387 eqeq12d 
 |-  ( ( ph /\ k e. NN ) -> ( ( U ` ( 2 x. ( k + 1 ) ) ) = ( ( S ` ( k + 1 ) ) + ( T ` ( k + 1 ) ) ) <-> ( ( U ` ( 2 x. k ) ) + ( ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) + ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) ) ) = ( ( ( S ` k ) + ( T ` k ) ) + ( ( ( ( abs o. - ) o. F ) ` ( k + 1 ) ) + ( ( ( abs o. - ) o. G ) ` ( k + 1 ) ) ) ) ) )
389 258 388 imbitrrid 
 |-  ( ( ph /\ k e. NN ) -> ( ( U ` ( 2 x. k ) ) = ( ( S ` k ) + ( T ` k ) ) -> ( U ` ( 2 x. ( k + 1 ) ) ) = ( ( S ` ( k + 1 ) ) + ( T ` ( k + 1 ) ) ) ) )
390 389 expcom 
 |-  ( k e. NN -> ( ph -> ( ( U ` ( 2 x. k ) ) = ( ( S ` k ) + ( T ` k ) ) -> ( U ` ( 2 x. ( k + 1 ) ) ) = ( ( S ` ( k + 1 ) ) + ( T ` ( k + 1 ) ) ) ) ) )
391 390 a2d 
 |-  ( k e. NN -> ( ( ph -> ( U ` ( 2 x. k ) ) = ( ( S ` k ) + ( T ` k ) ) ) -> ( ph -> ( U ` ( 2 x. ( k + 1 ) ) ) = ( ( S ` ( k + 1 ) ) + ( T ` ( k + 1 ) ) ) ) ) )
392 177 184 191 198 257 391 nnind 
 |-  ( ( |_ ` ( ( k + 1 ) / 2 ) ) e. NN -> ( ph -> ( U ` ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) = ( ( S ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) + ( T ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) ) )
393 392 impcom 
 |-  ( ( ph /\ ( |_ ` ( ( k + 1 ) / 2 ) ) e. NN ) -> ( U ` ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) = ( ( S ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) + ( T ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) )
394 66 393 syldan 
 |-  ( ( ph /\ k e. NN ) -> ( U ` ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) = ( ( S ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) + ( T ` ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) )
395 71 adantr 
 |-  ( ( ph /\ k e. NN ) -> ( vol* ` A ) e. RR )
396 395 recnd 
 |-  ( ( ph /\ k e. NN ) -> ( vol* ` A ) e. CC )
397 74 adantr 
 |-  ( ( ph /\ k e. NN ) -> C e. RR )
398 397 rehalfcld 
 |-  ( ( ph /\ k e. NN ) -> ( C / 2 ) e. RR )
399 398 recnd 
 |-  ( ( ph /\ k e. NN ) -> ( C / 2 ) e. CC )
400 72 adantr 
 |-  ( ( ph /\ k e. NN ) -> ( vol* ` B ) e. RR )
401 400 recnd 
 |-  ( ( ph /\ k e. NN ) -> ( vol* ` B ) e. CC )
402 396 399 401 399 add4d 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( vol* ` A ) + ( C / 2 ) ) + ( ( vol* ` B ) + ( C / 2 ) ) ) = ( ( ( vol* ` A ) + ( vol* ` B ) ) + ( ( C / 2 ) + ( C / 2 ) ) ) )
403 397 recnd 
 |-  ( ( ph /\ k e. NN ) -> C e. CC )
404 403 2halvesd 
 |-  ( ( ph /\ k e. NN ) -> ( ( C / 2 ) + ( C / 2 ) ) = C )
405 404 oveq2d 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( vol* ` A ) + ( vol* ` B ) ) + ( ( C / 2 ) + ( C / 2 ) ) ) = ( ( ( vol* ` A ) + ( vol* ` B ) ) + C ) )
406 402 405 eqtr2d 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( vol* ` A ) + ( vol* ` B ) ) + C ) = ( ( ( vol* ` A ) + ( C / 2 ) ) + ( ( vol* ` B ) + ( C / 2 ) ) ) )
407 170 394 406 3brtr4d 
 |-  ( ( ph /\ k e. NN ) -> ( U ` ( 2 x. ( |_ ` ( ( k + 1 ) / 2 ) ) ) ) <_ ( ( ( vol* ` A ) + ( vol* ` B ) ) + C ) )
408 35 70 76 106 407 letrd 
 |-  ( ( ph /\ k e. NN ) -> ( U ` k ) <_ ( ( ( vol* ` A ) + ( vol* ` B ) ) + C ) )