MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ovolunlem1a Unicode version

Theorem ovolunlem1a 18855
Description: Lemma for ovolun 18858. (Contributed by Mario Carneiro, 7-May-2015.)
Hypotheses
Ref Expression
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
Ref Expression
ovolunlem1a  |-  ( (
ph  /\  k  e.  NN )  ->  ( U `
 k )  <_ 
( ( ( vol
* `  A )  +  ( vol * `  B ) )  +  C ) )
Distinct variable groups:    k, n, C    k, F, n    k, H    A, k, n    B, k, n    S, k    T, k    k, G, n    ph, k, n    U, k
Allowed substitution hints:    S( n)    T( n)    U( n)    H( n)

Proof of Theorem ovolunlem1a
Dummy variables  z 
j are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ovolun.g1 . . . . . . . . . 10  |-  ( ph  ->  G  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) )
2 reex 8828 . . . . . . . . . . . . 13  |-  RR  e.  _V
32, 2xpex 4801 . . . . . . . . . . . 12  |-  ( RR 
X.  RR )  e. 
_V
43inex2 4156 . . . . . . . . . . 11  |-  (  <_  i^i  ( RR  X.  RR ) )  e.  _V
5 nnex 9752 . . . . . . . . . . 11  |-  NN  e.  _V
64, 5elmap 6796 . . . . . . . . . 10  |-  ( G  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) 
<->  G : NN --> (  <_  i^i  ( RR  X.  RR ) ) )
71, 6sylib 188 . . . . . . . . 9  |-  ( ph  ->  G : NN --> (  <_  i^i  ( RR  X.  RR ) ) )
87adantr 451 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  G : NN
--> (  <_  i^i  ( RR  X.  RR ) ) )
9 ffvelrn 5663 . . . . . . . 8  |-  ( ( G : NN --> (  <_  i^i  ( RR  X.  RR ) )  /\  (
n  /  2 )  e.  NN )  -> 
( G `  (
n  /  2 ) )  e.  (  <_  i^i  ( RR  X.  RR ) ) )
108, 9sylan 457 . . . . . . 7  |-  ( ( ( ph  /\  n  e.  NN )  /\  (
n  /  2 )  e.  NN )  -> 
( G `  (
n  /  2 ) )  e.  (  <_  i^i  ( RR  X.  RR ) ) )
11 nneo 10095 . . . . . . . . . . 11  |-  ( n  e.  NN  ->  (
( n  /  2
)  e.  NN  <->  -.  (
( n  +  1 )  /  2 )  e.  NN ) )
1211adantl 452 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( n  /  2 )  e.  NN  <->  -.  (
( n  +  1 )  /  2 )  e.  NN ) )
1312con2bid 319 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( n  +  1 )  /  2 )  e.  NN  <->  -.  (
n  /  2 )  e.  NN ) )
1413biimpar 471 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  NN )  /\  -.  ( n  /  2
)  e.  NN )  ->  ( ( n  +  1 )  / 
2 )  e.  NN )
15 ovolun.f1 . . . . . . . . . . 11  |-  ( ph  ->  F  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) )
164, 5elmap 6796 . . . . . . . . . . 11  |-  ( F  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) 
<->  F : NN --> (  <_  i^i  ( RR  X.  RR ) ) )
1715, 16sylib 188 . . . . . . . . . 10  |-  ( ph  ->  F : NN --> (  <_  i^i  ( RR  X.  RR ) ) )
1817adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN )  ->  F : NN
--> (  <_  i^i  ( RR  X.  RR ) ) )
19 ffvelrn 5663 . . . . . . . . 9  |-  ( ( F : NN --> (  <_  i^i  ( RR  X.  RR ) )  /\  (
( n  +  1 )  /  2 )  e.  NN )  -> 
( F `  (
( n  +  1 )  /  2 ) )  e.  (  <_  i^i  ( RR  X.  RR ) ) )
2018, 19sylan 457 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  NN )  /\  (
( n  +  1 )  /  2 )  e.  NN )  -> 
( F `  (
( n  +  1 )  /  2 ) )  e.  (  <_  i^i  ( RR  X.  RR ) ) )
2114, 20syldan 456 . . . . . . 7  |-  ( ( ( ph  /\  n  e.  NN )  /\  -.  ( n  /  2
)  e.  NN )  ->  ( F `  ( ( n  + 
1 )  /  2
) )  e.  (  <_  i^i  ( RR  X.  RR ) ) )
2210, 21ifclda 3592 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  if ( ( n  /  2
)  e.  NN , 
( G `  (
n  /  2 ) ) ,  ( F `
 ( ( n  +  1 )  / 
2 ) ) )  e.  (  <_  i^i  ( RR  X.  RR ) ) )
23 ovolun.h . . . . . 6  |-  H  =  ( n  e.  NN  |->  if ( ( n  / 
2 )  e.  NN ,  ( G `  ( n  /  2
) ) ,  ( F `  ( ( n  +  1 )  /  2 ) ) ) )
2422, 23fmptd 5684 . . . . 5  |-  ( ph  ->  H : NN --> (  <_  i^i  ( RR  X.  RR ) ) )
25 eqid 2283 . . . . . 6  |-  ( ( abs  o.  -  )  o.  H )  =  ( ( abs  o.  -  )  o.  H )
26 ovolun.u . . . . . 6  |-  U  =  seq  1 (  +  ,  ( ( abs 
o.  -  )  o.  H ) )
2725, 26ovolsf 18832 . . . . 5  |-  ( H : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  U : NN --> ( 0 [,) 
+oo ) )
2824, 27syl 15 . . . 4  |-  ( ph  ->  U : NN --> ( 0 [,)  +oo ) )
29 0re 8838 . . . . 5  |-  0  e.  RR
30 pnfxr 10455 . . . . 5  |-  +oo  e.  RR*
31 icossre 10730 . . . . 5  |-  ( ( 0  e.  RR  /\  +oo 
e.  RR* )  ->  (
0 [,)  +oo )  C_  RR )
3229, 30, 31mp2an 653 . . . 4  |-  ( 0 [,)  +oo )  C_  RR
33 fss 5397 . . . 4  |-  ( ( U : NN --> ( 0 [,)  +oo )  /\  (
0 [,)  +oo )  C_  RR )  ->  U : NN
--> RR )
3428, 32, 33sylancl 643 . . 3  |-  ( ph  ->  U : NN --> RR )
35 ffvelrn 5663 . . 3  |-  ( ( U : NN --> RR  /\  k  e.  NN )  ->  ( U `  k
)  e.  RR )
3634, 35sylan 457 . 2  |-  ( (
ph  /\  k  e.  NN )  ->  ( U `
 k )  e.  RR )
37 2nn 9877 . . . 4  |-  2  e.  NN
38 peano2nn 9758 . . . . . . . . 9  |-  ( k  e.  NN  ->  (
k  +  1 )  e.  NN )
3938adantl 452 . . . . . . . 8  |-  ( (
ph  /\  k  e.  NN )  ->  ( k  +  1 )  e.  NN )
4039nnred 9761 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN )  ->  ( k  +  1 )  e.  RR )
4140rehalfcld 9958 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( k  +  1 )  /  2 )  e.  RR )
4241flcld 10930 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  ( |_
`  ( ( k  +  1 )  / 
2 ) )  e.  ZZ )
43 ax-1cn 8795 . . . . . . . . 9  |-  1  e.  CC
44432timesi 9845 . . . . . . . 8  |-  ( 2  x.  1 )  =  ( 1  +  1 )
45 nnge1 9772 . . . . . . . . . 10  |-  ( k  e.  NN  ->  1  <_  k )
4645adantl 452 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN )  ->  1  <_ 
k )
47 nnre 9753 . . . . . . . . . . 11  |-  ( k  e.  NN  ->  k  e.  RR )
4847adantl 452 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  RR )
49 1re 8837 . . . . . . . . . . 11  |-  1  e.  RR
50 leadd1 9242 . . . . . . . . . . 11  |-  ( ( 1  e.  RR  /\  k  e.  RR  /\  1  e.  RR )  ->  (
1  <_  k  <->  ( 1  +  1 )  <_ 
( k  +  1 ) ) )
5149, 49, 50mp3an13 1268 . . . . . . . . . 10  |-  ( k  e.  RR  ->  (
1  <_  k  <->  ( 1  +  1 )  <_ 
( k  +  1 ) ) )
5248, 51syl 15 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN )  ->  ( 1  <_  k  <->  ( 1  +  1 )  <_ 
( k  +  1 ) ) )
5346, 52mpbid 201 . . . . . . . 8  |-  ( (
ph  /\  k  e.  NN )  ->  ( 1  +  1 )  <_ 
( k  +  1 ) )
5444, 53syl5eqbr 4056 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN )  ->  ( 2  x.  1 )  <_ 
( k  +  1 ) )
55 2re 9815 . . . . . . . . . 10  |-  2  e.  RR
56 2pos 9828 . . . . . . . . . 10  |-  0  <  2
5755, 56pm3.2i 441 . . . . . . . . 9  |-  ( 2  e.  RR  /\  0  <  2 )
58 lemuldiv2 9636 . . . . . . . . 9  |-  ( ( 1  e.  RR  /\  ( k  +  1 )  e.  RR  /\  ( 2  e.  RR  /\  0  <  2 ) )  ->  ( (
2  x.  1 )  <_  ( k  +  1 )  <->  1  <_  ( ( k  +  1 )  /  2 ) ) )
5949, 57, 58mp3an13 1268 . . . . . . . 8  |-  ( ( k  +  1 )  e.  RR  ->  (
( 2  x.  1 )  <_  ( k  +  1 )  <->  1  <_  ( ( k  +  1 )  /  2 ) ) )
6040, 59syl 15 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( 2  x.  1 )  <_  ( k  +  1 )  <->  1  <_  ( ( k  +  1 )  /  2 ) ) )
6154, 60mpbid 201 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  1  <_ 
( ( k  +  1 )  /  2
) )
62 1z 10053 . . . . . . 7  |-  1  e.  ZZ
63 flge 10937 . . . . . . 7  |-  ( ( ( ( k  +  1 )  /  2
)  e.  RR  /\  1  e.  ZZ )  ->  ( 1  <_  (
( k  +  1 )  /  2 )  <->  1  <_  ( |_ `  ( ( k  +  1 )  /  2
) ) ) )
6441, 62, 63sylancl 643 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  ( 1  <_  ( ( k  +  1 )  / 
2 )  <->  1  <_  ( |_ `  ( ( k  +  1 )  /  2 ) ) ) )
6561, 64mpbid 201 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  1  <_ 
( |_ `  (
( k  +  1 )  /  2 ) ) )
66 elnnz1 10049 . . . . 5  |-  ( ( |_ `  ( ( k  +  1 )  /  2 ) )  e.  NN  <->  ( ( |_ `  ( ( k  +  1 )  / 
2 ) )  e.  ZZ  /\  1  <_ 
( |_ `  (
( k  +  1 )  /  2 ) ) ) )
6742, 65, 66sylanbrc 645 . . . 4  |-  ( (
ph  /\  k  e.  NN )  ->  ( |_
`  ( ( k  +  1 )  / 
2 ) )  e.  NN )
68 nnmulcl 9769 . . . 4  |-  ( ( 2  e.  NN  /\  ( |_ `  ( ( k  +  1 )  /  2 ) )  e.  NN )  -> 
( 2  x.  ( |_ `  ( ( k  +  1 )  / 
2 ) ) )  e.  NN )
6937, 67, 68sylancr 644 . . 3  |-  ( (
ph  /\  k  e.  NN )  ->  ( 2  x.  ( |_ `  ( ( k  +  1 )  /  2
) ) )  e.  NN )
70 ffvelrn 5663 . . . 4  |-  ( ( U : NN --> RR  /\  ( 2  x.  ( |_ `  ( ( k  +  1 )  / 
2 ) ) )  e.  NN )  -> 
( U `  (
2  x.  ( |_
`  ( ( k  +  1 )  / 
2 ) ) ) )  e.  RR )
7134, 70sylan 457 . . 3  |-  ( (
ph  /\  ( 2  x.  ( |_ `  ( ( k  +  1 )  /  2
) ) )  e.  NN )  ->  ( U `  ( 2  x.  ( |_ `  (
( k  +  1 )  /  2 ) ) ) )  e.  RR )
7269, 71syldan 456 . 2  |-  ( (
ph  /\  k  e.  NN )  ->  ( U `
 ( 2  x.  ( |_ `  (
( k  +  1 )  /  2 ) ) ) )  e.  RR )
73 ovolun.a . . . . . 6  |-  ( ph  ->  ( A  C_  RR  /\  ( vol * `  A )  e.  RR ) )
7473simprd 449 . . . . 5  |-  ( ph  ->  ( vol * `  A )  e.  RR )
75 ovolun.b . . . . . 6  |-  ( ph  ->  ( B  C_  RR  /\  ( vol * `  B )  e.  RR ) )
7675simprd 449 . . . . 5  |-  ( ph  ->  ( vol * `  B )  e.  RR )
7774, 76readdcld 8862 . . . 4  |-  ( ph  ->  ( ( vol * `  A )  +  ( vol * `  B
) )  e.  RR )
78 ovolun.c . . . . 5  |-  ( ph  ->  C  e.  RR+ )
7978rpred 10390 . . . 4  |-  ( ph  ->  C  e.  RR )
8077, 79readdcld 8862 . . 3  |-  ( ph  ->  ( ( ( vol
* `  A )  +  ( vol * `  B ) )  +  C )  e.  RR )
8180adantr 451 . 2  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( ( vol * `  A )  +  ( vol * `  B
) )  +  C
)  e.  RR )
82 simpr 447 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  NN )
83 nnuz 10263 . . . . 5  |-  NN  =  ( ZZ>= `  1 )
8482, 83syl6eleq 2373 . . . 4  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  ( ZZ>= `  1 )
)
85 nnz 10045 . . . . . . 7  |-  ( k  e.  NN  ->  k  e.  ZZ )
8685adantl 452 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  ZZ )
87 flhalf 10954 . . . . . 6  |-  ( k  e.  ZZ  ->  k  <_  ( 2  x.  ( |_ `  ( ( k  +  1 )  / 
2 ) ) ) )
8886, 87syl 15 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  k  <_ 
( 2  x.  ( |_ `  ( ( k  +  1 )  / 
2 ) ) ) )
89 nnz 10045 . . . . . . 7  |-  ( ( 2  x.  ( |_
`  ( ( k  +  1 )  / 
2 ) ) )  e.  NN  ->  (
2  x.  ( |_
`  ( ( k  +  1 )  / 
2 ) ) )  e.  ZZ )
90 eluz 10241 . . . . . . 7  |-  ( ( k  e.  ZZ  /\  ( 2  x.  ( |_ `  ( ( k  +  1 )  / 
2 ) ) )  e.  ZZ )  -> 
( ( 2  x.  ( |_ `  (
( k  +  1 )  /  2 ) ) )  e.  (
ZZ>= `  k )  <->  k  <_  ( 2  x.  ( |_
`  ( ( k  +  1 )  / 
2 ) ) ) ) )
9185, 89, 90syl2an 463 . . . . . 6  |-  ( ( k  e.  NN  /\  ( 2  x.  ( |_ `  ( ( k  +  1 )  / 
2 ) ) )  e.  NN )  -> 
( ( 2  x.  ( |_ `  (
( k  +  1 )  /  2 ) ) )  e.  (
ZZ>= `  k )  <->  k  <_  ( 2  x.  ( |_
`  ( ( k  +  1 )  / 
2 ) ) ) ) )
9282, 69, 91syl2anc 642 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( 2  x.  ( |_
`  ( ( k  +  1 )  / 
2 ) ) )  e.  ( ZZ>= `  k
)  <->  k  <_  (
2  x.  ( |_
`  ( ( k  +  1 )  / 
2 ) ) ) ) )
9388, 92mpbird 223 . . . 4  |-  ( (
ph  /\  k  e.  NN )  ->  ( 2  x.  ( |_ `  ( ( k  +  1 )  /  2
) ) )  e.  ( ZZ>= `  k )
)
94 elfznn 10819 . . . . 5  |-  ( j  e.  ( 1 ... ( 2  x.  ( |_ `  ( ( k  +  1 )  / 
2 ) ) ) )  ->  j  e.  NN )
9525ovolfsf 18831 . . . . . . . . . 10  |-  ( H : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  (
( abs  o.  -  )  o.  H ) : NN --> ( 0 [,)  +oo ) )
9624, 95syl 15 . . . . . . . . 9  |-  ( ph  ->  ( ( abs  o.  -  )  o.  H
) : NN --> ( 0 [,)  +oo ) )
9796adantr 451 . . . . . . . 8  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( abs  o.  -  )  o.  H ) : NN --> ( 0 [,)  +oo ) )
98 ffvelrn 5663 . . . . . . . 8  |-  ( ( ( ( abs  o.  -  )  o.  H
) : NN --> ( 0 [,)  +oo )  /\  j  e.  NN )  ->  (
( ( abs  o.  -  )  o.  H
) `  j )  e.  ( 0 [,)  +oo ) )
9997, 98sylan 457 . . . . . . 7  |-  ( ( ( ph  /\  k  e.  NN )  /\  j  e.  NN )  ->  (
( ( abs  o.  -  )  o.  H
) `  j )  e.  ( 0 [,)  +oo ) )
100 elrege0 10746 . . . . . . 7  |-  ( ( ( ( abs  o.  -  )  o.  H
) `  j )  e.  ( 0 [,)  +oo ) 
<->  ( ( ( ( abs  o.  -  )  o.  H ) `  j
)  e.  RR  /\  0  <_  ( ( ( abs  o.  -  )  o.  H ) `  j
) ) )
10199, 100sylib 188 . . . . . 6  |-  ( ( ( ph  /\  k  e.  NN )  /\  j  e.  NN )  ->  (
( ( ( abs 
o.  -  )  o.  H ) `  j
)  e.  RR  /\  0  <_  ( ( ( abs  o.  -  )  o.  H ) `  j
) ) )
102101simpld 445 . . . . 5  |-  ( ( ( ph  /\  k  e.  NN )  /\  j  e.  NN )  ->  (
( ( abs  o.  -  )  o.  H
) `  j )  e.  RR )
10394, 102sylan2 460 . . . 4  |-  ( ( ( ph  /\  k  e.  NN )  /\  j  e.  ( 1 ... (
2  x.  ( |_
`  ( ( k  +  1 )  / 
2 ) ) ) ) )  ->  (
( ( abs  o.  -  )  o.  H
) `  j )  e.  RR )
104 elfzuz 10794 . . . . . 6  |-  ( j  e.  ( ( k  +  1 ) ... ( 2  x.  ( |_ `  ( ( k  +  1 )  / 
2 ) ) ) )  ->  j  e.  ( ZZ>= `  ( k  +  1 ) ) )
10583uztrn2 10245 . . . . . 6  |-  ( ( ( k  +  1 )  e.  NN  /\  j  e.  ( ZZ>= `  ( k  +  1 ) ) )  -> 
j  e.  NN )
10639, 104, 105syl2an 463 . . . . 5  |-  ( ( ( ph  /\  k  e.  NN )  /\  j  e.  ( ( k  +  1 ) ... (
2  x.  ( |_
`  ( ( k  +  1 )  / 
2 ) ) ) ) )  ->  j  e.  NN )
107101simprd 449 . . . . 5  |-  ( ( ( ph  /\  k  e.  NN )  /\  j  e.  NN )  ->  0  <_  ( ( ( abs 
o.  -  )  o.  H ) `  j
) )
108106, 107syldan 456 . . . 4  |-  ( ( ( ph  /\  k  e.  NN )  /\  j  e.  ( ( k  +  1 ) ... (
2  x.  ( |_
`  ( ( k  +  1 )  / 
2 ) ) ) ) )  ->  0  <_  ( ( ( abs 
o.  -  )  o.  H ) `  j
) )
10984, 93, 103, 108sermono 11078 . . 3  |-  ( (
ph  /\  k  e.  NN )  ->  (  seq  1 (  +  , 
( ( abs  o.  -  )  o.  H
) ) `  k
)  <_  (  seq  1 (  +  , 
( ( abs  o.  -  )  o.  H
) ) `  (
2  x.  ( |_
`  ( ( k  +  1 )  / 
2 ) ) ) ) )
11026fveq1i 5526 . . 3  |-  ( U `
 k )  =  (  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  H ) ) `  k )
11126fveq1i 5526 . . 3  |-  ( U `
 ( 2  x.  ( |_ `  (
( k  +  1 )  /  2 ) ) ) )  =  (  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  H ) ) `  ( 2  x.  ( |_ `  ( ( k  +  1 )  / 
2 ) ) ) )
112109, 110, 1113brtr4g 4055 . 2  |-  ( (
ph  /\  k  e.  NN )  ->  ( U `
 k )  <_ 
( U `  (
2  x.  ( |_
`  ( ( k  +  1 )  / 
2 ) ) ) ) )
113 eqid 2283 . . . . . . . . . 10  |-  ( ( abs  o.  -  )  o.  F )  =  ( ( abs  o.  -  )  o.  F )
114 ovolun.s . . . . . . . . . 10  |-  S  =  seq  1 (  +  ,  ( ( abs 
o.  -  )  o.  F ) )
115113, 114ovolsf 18832 . . . . . . . . 9  |-  ( F : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  S : NN --> ( 0 [,) 
+oo ) )
11617, 115syl 15 . . . . . . . 8  |-  ( ph  ->  S : NN --> ( 0 [,)  +oo ) )
117 frn 5395 . . . . . . . 8  |-  ( S : NN --> ( 0 [,)  +oo )  ->  ran  S 
C_  ( 0 [,) 
+oo ) )
118116, 117syl 15 . . . . . . 7  |-  ( ph  ->  ran  S  C_  (
0 [,)  +oo ) )
119118, 32syl6ss 3191 . . . . . 6  |-  ( ph  ->  ran  S  C_  RR )
120119adantr 451 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  ran  S  C_  RR )
121 ffn 5389 . . . . . . . 8  |-  ( S : NN --> ( 0 [,)  +oo )  ->  S  Fn  NN )
122116, 121syl 15 . . . . . . 7  |-  ( ph  ->  S  Fn  NN )
123122adantr 451 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  S  Fn  NN )
124 fnfvelrn 5662 . . . . . 6  |-  ( ( S  Fn  NN  /\  ( |_ `  ( ( k  +  1 )  /  2 ) )  e.  NN )  -> 
( S `  ( |_ `  ( ( k  +  1 )  / 
2 ) ) )  e.  ran  S )
125123, 67, 124syl2anc 642 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  ( S `
 ( |_ `  ( ( k  +  1 )  /  2
) ) )  e. 
ran  S )
126120, 125sseldd 3181 . . . 4  |-  ( (
ph  /\  k  e.  NN )  ->  ( S `
 ( |_ `  ( ( k  +  1 )  /  2
) ) )  e.  RR )
127 eqid 2283 . . . . . . . . . 10  |-  ( ( abs  o.  -  )  o.  G )  =  ( ( abs  o.  -  )  o.  G )
128 ovolun.t . . . . . . . . . 10  |-  T  =  seq  1 (  +  ,  ( ( abs 
o.  -  )  o.  G ) )
129127, 128ovolsf 18832 . . . . . . . . 9  |-  ( G : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  T : NN --> ( 0 [,) 
+oo ) )
1307, 129syl 15 . . . . . . . 8  |-  ( ph  ->  T : NN --> ( 0 [,)  +oo ) )
131 frn 5395 . . . . . . . 8  |-  ( T : NN --> ( 0 [,)  +oo )  ->  ran  T 
C_  ( 0 [,) 
+oo ) )
132130, 131syl 15 . . . . . . 7  |-  ( ph  ->  ran  T  C_  (
0 [,)  +oo ) )
133132, 32syl6ss 3191 . . . . . 6  |-  ( ph  ->  ran  T  C_  RR )
134133adantr 451 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  ran  T  C_  RR )
135 ffn 5389 . . . . . . . 8  |-  ( T : NN --> ( 0 [,)  +oo )  ->  T  Fn  NN )
136130, 135syl 15 . . . . . . 7  |-  ( ph  ->  T  Fn  NN )
137136adantr 451 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  T  Fn  NN )
138 fnfvelrn 5662 . . . . . 6  |-  ( ( T  Fn  NN  /\  ( |_ `  ( ( k  +  1 )  /  2 ) )  e.  NN )  -> 
( T `  ( |_ `  ( ( k  +  1 )  / 
2 ) ) )  e.  ran  T )
139137, 67, 138syl2anc 642 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  ( T `
 ( |_ `  ( ( k  +  1 )  /  2
) ) )  e. 
ran  T )
140134, 139sseldd 3181 . . . 4  |-  ( (
ph  /\  k  e.  NN )  ->  ( T `
 ( |_ `  ( ( k  +  1 )  /  2
) ) )  e.  RR )
14179rehalfcld 9958 . . . . . 6  |-  ( ph  ->  ( C  /  2
)  e.  RR )
14274, 141readdcld 8862 . . . . 5  |-  ( ph  ->  ( ( vol * `  A )  +  ( C  /  2 ) )  e.  RR )
143142adantr 451 . . . 4  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( vol * `  A
)  +  ( C  /  2 ) )  e.  RR )
14476, 141readdcld 8862 . . . . 5  |-  ( ph  ->  ( ( vol * `  B )  +  ( C  /  2 ) )  e.  RR )
145144adantr 451 . . . 4  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( vol * `  B
)  +  ( C  /  2 ) )  e.  RR )
146 ressxr 8876 . . . . . . . . 9  |-  RR  C_  RR*
147119, 146syl6ss 3191 . . . . . . . 8  |-  ( ph  ->  ran  S  C_  RR* )
148 supxrcl 10633 . . . . . . . 8  |-  ( ran 
S  C_  RR*  ->  sup ( ran  S ,  RR* ,  <  )  e.  RR* )
149147, 148syl 15 . . . . . . 7  |-  ( ph  ->  sup ( ran  S ,  RR* ,  <  )  e.  RR* )
150 1nn 9757 . . . . . . . . . . 11  |-  1  e.  NN
151 fdm 5393 . . . . . . . . . . . 12  |-  ( S : NN --> ( 0 [,)  +oo )  ->  dom  S  =  NN )
152116, 151syl 15 . . . . . . . . . . 11  |-  ( ph  ->  dom  S  =  NN )
153150, 152syl5eleqr 2370 . . . . . . . . . 10  |-  ( ph  ->  1  e.  dom  S
)
154 ne0i 3461 . . . . . . . . . 10  |-  ( 1  e.  dom  S  ->  dom  S  =/=  (/) )
155153, 154syl 15 . . . . . . . . 9  |-  ( ph  ->  dom  S  =/=  (/) )
156 dm0rn0 4895 . . . . . . . . . 10  |-  ( dom 
S  =  (/)  <->  ran  S  =  (/) )
157156necon3bii 2478 . . . . . . . . 9  |-  ( dom 
S  =/=  (/)  <->  ran  S  =/=  (/) )
158155, 157sylib 188 . . . . . . . 8  |-  ( ph  ->  ran  S  =/=  (/) )
159 supxrgtmnf 10648 . . . . . . . 8  |-  ( ( ran  S  C_  RR  /\ 
ran  S  =/=  (/) )  ->  -oo  <  sup ( ran  S ,  RR* ,  <  )
)
160119, 158, 159syl2anc 642 . . . . . . 7  |-  ( ph  ->  -oo  <  sup ( ran  S ,  RR* ,  <  ) )
161 ovolun.f3 . . . . . . 7  |-  ( ph  ->  sup ( ran  S ,  RR* ,  <  )  <_  ( ( vol * `  A )  +  ( C  /  2 ) ) )
162 xrre 10498 . . . . . . 7  |-  ( ( ( 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 )
163149, 142, 160, 161, 162syl22anc 1183 . . . . . 6  |-  ( ph  ->  sup ( ran  S ,  RR* ,  <  )  e.  RR )
164163adantr 451 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  sup ( ran  S ,  RR* ,  <  )  e.  RR )
165147adantr 451 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  ran  S  C_ 
RR* )
166 supxrub 10643 . . . . . 6  |-  ( ( ran  S  C_  RR*  /\  ( S `  ( |_ `  ( ( k  +  1 )  /  2
) ) )  e. 
ran  S )  -> 
( S `  ( |_ `  ( ( k  +  1 )  / 
2 ) ) )  <_  sup ( ran  S ,  RR* ,  <  )
)
167165, 125, 166syl2anc 642 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  ( S `
 ( |_ `  ( ( k  +  1 )  /  2
) ) )  <_  sup ( ran  S ,  RR* ,  <  ) )
168161adantr 451 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  sup ( ran  S ,  RR* ,  <  )  <_  ( ( vol
* `  A )  +  ( C  / 
2 ) ) )
169126, 164, 143, 167, 168letrd 8973 . . . 4  |-  ( (
ph  /\  k  e.  NN )  ->  ( S `
 ( |_ `  ( ( k  +  1 )  /  2
) ) )  <_ 
( ( vol * `  A )  +  ( C  /  2 ) ) )
170133, 146syl6ss 3191 . . . . . . . 8  |-  ( ph  ->  ran  T  C_  RR* )
171 supxrcl 10633 . . . . . . . 8  |-  ( ran 
T  C_  RR*  ->  sup ( ran  T ,  RR* ,  <  )  e.  RR* )
172170, 171syl 15 . . . . . . 7  |-  ( ph  ->  sup ( ran  T ,  RR* ,  <  )  e.  RR* )
173 fdm 5393 . . . . . . . . . . . 12  |-  ( T : NN --> ( 0 [,)  +oo )  ->  dom  T  =  NN )
174130, 173syl 15 . . . . . . . . . . 11  |-  ( ph  ->  dom  T  =  NN )
175150, 174syl5eleqr 2370 . . . . . . . . . 10  |-  ( ph  ->  1  e.  dom  T
)
176 ne0i 3461 . . . . . . . . . 10  |-  ( 1  e.  dom  T  ->  dom  T  =/=  (/) )
177175, 176syl 15 . . . . . . . . 9  |-  ( ph  ->  dom  T  =/=  (/) )
178 dm0rn0 4895 . . . . . . . . . 10  |-  ( dom 
T  =  (/)  <->  ran  T  =  (/) )
179178necon3bii 2478 . . . . . . . . 9  |-  ( dom 
T  =/=  (/)  <->  ran  T  =/=  (/) )
180177, 179sylib 188 . . . . . . . 8  |-  ( ph  ->  ran  T  =/=  (/) )
181 supxrgtmnf 10648 . . . . . . . 8  |-  ( ( ran  T  C_  RR  /\ 
ran  T  =/=  (/) )  ->  -oo  <  sup ( ran  T ,  RR* ,  <  )
)
182133, 180, 181syl2anc 642 . . . . . . 7  |-  ( ph  ->  -oo  <  sup ( ran  T ,  RR* ,  <  ) )
183 ovolun.g3 . . . . . . 7  |-  ( ph  ->  sup ( ran  T ,  RR* ,  <  )  <_  ( ( vol * `  B )  +  ( C  /  2 ) ) )
184 xrre 10498 . . . . . . 7  |-  ( ( ( 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 )
185172, 144, 182, 183, 184syl22anc 1183 . . . . . 6  |-  ( ph  ->  sup ( ran  T ,  RR* ,  <  )  e.  RR )
186185adantr 451 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  sup ( ran  T ,  RR* ,  <  )  e.  RR )
187170adantr 451 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  ran  T  C_ 
RR* )
188 supxrub 10643 . . . . . 6  |-  ( ( ran  T  C_  RR*  /\  ( T `  ( |_ `  ( ( k  +  1 )  /  2
) ) )  e. 
ran  T )  -> 
( T `  ( |_ `  ( ( k  +  1 )  / 
2 ) ) )  <_  sup ( ran  T ,  RR* ,  <  )
)
189187, 139, 188syl2anc 642 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  ( T `
 ( |_ `  ( ( k  +  1 )  /  2
) ) )  <_  sup ( ran  T ,  RR* ,  <  ) )
190183adantr 451 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  sup ( ran  T ,  RR* ,  <  )  <_  ( ( vol
* `  B )  +  ( C  / 
2 ) ) )
191140, 186, 145, 189, 190letrd 8973 . . . 4  |-  ( (
ph  /\  k  e.  NN )  ->  ( T `
 ( |_ `  ( ( k  +  1 )  /  2
) ) )  <_ 
( ( vol * `  B )  +  ( C  /  2 ) ) )
192126, 140, 143, 145, 169, 191le2addd 9390 . . 3  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( S `  ( |_
`  ( ( k  +  1 )  / 
2 ) ) )  +  ( T `  ( |_ `  ( ( k  +  1 )  /  2 ) ) ) )  <_  (
( ( vol * `  A )  +  ( C  /  2 ) )  +  ( ( vol * `  B
)  +  ( C  /  2 ) ) ) )
193 oveq2 5866 . . . . . . . . 9  |-  ( z  =  1  ->  (
2  x.  z )  =  ( 2  x.  1 ) )
194193fveq2d 5529 . . . . . . . 8  |-  ( z  =  1  ->  ( U `  ( 2  x.  z ) )  =  ( U `  (
2  x.  1 ) ) )
195 fveq2 5525 . . . . . . . . 9  |-  ( z  =  1  ->  ( S `  z )  =  ( S ` 
1 ) )
196 fveq2 5525 . . . . . . . . 9  |-  ( z  =  1  ->  ( T `  z )  =  ( T ` 
1 ) )
197195, 196oveq12d 5876 . . . . . . . 8  |-  ( z  =  1  ->  (
( S `  z
)  +  ( T `
 z ) )  =  ( ( S `
 1 )  +  ( T `  1
) ) )
198194, 197eqeq12d 2297 . . . . . . 7  |-  ( z  =  1  ->  (
( U `  (
2  x.  z ) )  =  ( ( S `  z )  +  ( T `  z ) )  <->  ( U `  ( 2  x.  1 ) )  =  ( ( S `  1
)  +  ( T `
 1 ) ) ) )
199198imbi2d 307 . . . . . 6  |-  ( z  =  1  ->  (
( ph  ->  ( U `
 ( 2  x.  z ) )  =  ( ( S `  z )  +  ( T `  z ) ) )  <->  ( ph  ->  ( U `  (
2  x.  1 ) )  =  ( ( S `  1 )  +  ( T ` 
1 ) ) ) ) )
200 oveq2 5866 . . . . . . . . 9  |-  ( z  =  k  ->  (
2  x.  z )  =  ( 2  x.  k ) )
201200fveq2d 5529 . . . . . . . 8  |-  ( z  =  k  ->  ( U `  ( 2  x.  z ) )  =  ( U `  (
2  x.  k ) ) )
202 fveq2 5525 . . . . . . . . 9  |-  ( z  =  k  ->  ( S `  z )  =  ( S `  k ) )
203 fveq2 5525 . . . . . . . . 9  |-  ( z  =  k  ->  ( T `  z )  =  ( T `  k ) )
204202, 203oveq12d 5876 . . . . . . . 8  |-  ( z  =  k  ->  (
( S `  z
)  +  ( T `
 z ) )  =  ( ( S `
 k )  +  ( T `  k
) ) )
205201, 204eqeq12d 2297 . . . . . . 7  |-  ( z  =  k  ->  (
( U `  (
2  x.  z ) )  =  ( ( S `  z )  +  ( T `  z ) )  <->  ( U `  ( 2  x.  k
) )  =  ( ( S `  k
)  +  ( T `
 k ) ) ) )
206205imbi2d 307 . . . . . 6  |-  ( z  =  k  ->  (
( ph  ->  ( U `
 ( 2  x.  z ) )  =  ( ( S `  z )  +  ( T `  z ) ) )  <->  ( ph  ->  ( U `  (
2  x.  k ) )  =  ( ( S `  k )  +  ( T `  k ) ) ) ) )
207 oveq2 5866 . . . . . . . . 9  |-  ( z  =  ( k  +  1 )  ->  (
2  x.  z )  =  ( 2  x.  ( k  +  1 ) ) )
208207fveq2d 5529 . . . . . . . 8  |-  ( z  =  ( k  +  1 )  ->  ( U `  ( 2  x.  z ) )  =  ( U `  (
2  x.  ( k  +  1 ) ) ) )
209 fveq2 5525 . . . . . . . . 9  |-  ( z  =  ( k  +  1 )  ->  ( S `  z )  =  ( S `  ( k  +  1 ) ) )
210 fveq2 5525 . . . . . . . . 9  |-  ( z  =  ( k  +  1 )  ->  ( T `  z )  =  ( T `  ( k  +  1 ) ) )
211209, 210oveq12d 5876 . . . . . . . 8  |-  ( z  =  ( k  +  1 )  ->  (
( S `  z
)  +  ( T `
 z ) )  =  ( ( S `
 ( k  +  1 ) )  +  ( T `  (
k  +  1 ) ) ) )
212208, 211eqeq12d 2297 . . . . . . 7  |-  ( z  =  ( k  +  1 )  ->  (
( U `  (
2  x.  z ) )  =  ( ( S `  z )  +  ( T `  z ) )  <->  ( U `  ( 2  x.  (
k  +  1 ) ) )  =  ( ( S `  (
k  +  1 ) )  +  ( T `
 ( k  +  1 ) ) ) ) )
213212imbi2d 307 . . . . . 6  |-  ( z  =  ( k  +  1 )  ->  (
( ph  ->  ( U `
 ( 2  x.  z ) )  =  ( ( S `  z )  +  ( T `  z ) ) )  <->  ( ph  ->  ( U `  (
2  x.  ( k  +  1 ) ) )  =  ( ( S `  ( k  +  1 ) )  +  ( T `  ( k  +  1 ) ) ) ) ) )
214 oveq2 5866 . . . . . . . . 9  |-  ( z  =  ( |_ `  ( ( k  +  1 )  /  2
) )  ->  (
2  x.  z )  =  ( 2  x.  ( |_ `  (
( k  +  1 )  /  2 ) ) ) )
215214fveq2d 5529 . . . . . . . 8  |-  ( z  =  ( |_ `  ( ( k  +  1 )  /  2
) )  ->  ( U `  ( 2  x.  z ) )  =  ( U `  (
2  x.  ( |_
`  ( ( k  +  1 )  / 
2 ) ) ) ) )
216 fveq2 5525 . . . . . . . . 9  |-  ( z  =  ( |_ `  ( ( k  +  1 )  /  2
) )  ->  ( S `  z )  =  ( S `  ( |_ `  ( ( k  +  1 )  /  2 ) ) ) )
217 fveq2 5525 . . . . . . . . 9  |-  ( z  =  ( |_ `  ( ( k  +  1 )  /  2
) )  ->  ( T `  z )  =  ( T `  ( |_ `  ( ( k  +  1 )  /  2 ) ) ) )
218216, 217oveq12d 5876 . . . . . . . 8  |-  ( z  =  ( |_ `  ( ( k  +  1 )  /  2
) )  ->  (
( S `  z
)  +  ( T `
 z ) )  =  ( ( S `
 ( |_ `  ( ( k  +  1 )  /  2
) ) )  +  ( T `  ( |_ `  ( ( k  +  1 )  / 
2 ) ) ) ) )
219215, 218eqeq12d 2297 . . . . . . 7  |-  ( 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 ) ) ) ) ) )
220219imbi2d 307 . . . . . 6  |-  ( 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 ) ) ) ) ) ) )
22126fveq1i 5526 . . . . . . . 8  |-  ( U `
 ( 2  x.  1 ) )  =  (  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  H ) ) `  ( 2  x.  1 ) )
22225ovolfsval 18830 . . . . . . . . . . . 12  |-  ( ( H : NN --> (  <_  i^i  ( RR  X.  RR ) )  /\  1  e.  NN )  ->  (
( ( abs  o.  -  )  o.  H
) `  1 )  =  ( ( 2nd `  ( H `  1
) )  -  ( 1st `  ( H ` 
1 ) ) ) )
22324, 150, 222sylancl 643 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( abs 
o.  -  )  o.  H ) `  1
)  =  ( ( 2nd `  ( H `
 1 ) )  -  ( 1st `  ( H `  1 )
) ) )
224 halfnz 10090 . . . . . . . . . . . . . . . . . 18  |-  -.  (
1  /  2 )  e.  ZZ
225 nnz 10045 . . . . . . . . . . . . . . . . . . 19  |-  ( ( n  /  2 )  e.  NN  ->  (
n  /  2 )  e.  ZZ )
226 oveq1 5865 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  1  ->  (
n  /  2 )  =  ( 1  / 
2 ) )
227226eleq1d 2349 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  1  ->  (
( n  /  2
)  e.  ZZ  <->  ( 1  /  2 )  e.  ZZ ) )
228225, 227syl5ib 210 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  1  ->  (
( n  /  2
)  e.  NN  ->  ( 1  /  2 )  e.  ZZ ) )
229224, 228mtoi 169 . . . . . . . . . . . . . . . . 17  |-  ( n  =  1  ->  -.  ( n  /  2
)  e.  NN )
230 iffalse 3572 . . . . . . . . . . . . . . . . 17  |-  ( -.  ( n  /  2
)  e.  NN  ->  if ( ( n  / 
2 )  e.  NN ,  ( G `  ( n  /  2
) ) ,  ( F `  ( ( n  +  1 )  /  2 ) ) )  =  ( F `
 ( ( n  +  1 )  / 
2 ) ) )
231229, 230syl 15 . . . . . . . . . . . . . . . 16  |-  ( n  =  1  ->  if ( ( n  / 
2 )  e.  NN ,  ( G `  ( n  /  2
) ) ,  ( F `  ( ( n  +  1 )  /  2 ) ) )  =  ( F `
 ( ( n  +  1 )  / 
2 ) ) )
232 oveq1 5865 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  1  ->  (
n  +  1 )  =  ( 1  +  1 ) )
233 df-2 9804 . . . . . . . . . . . . . . . . . . . 20  |-  2  =  ( 1  +  1 )
234232, 233syl6eqr 2333 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  1  ->  (
n  +  1 )  =  2 )
235234oveq1d 5873 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  1  ->  (
( n  +  1 )  /  2 )  =  ( 2  / 
2 ) )
236 2cn 9816 . . . . . . . . . . . . . . . . . . 19  |-  2  e.  CC
237 2ne0 9829 . . . . . . . . . . . . . . . . . . 19  |-  2  =/=  0
238236, 237dividi 9493 . . . . . . . . . . . . . . . . . 18  |-  ( 2  /  2 )  =  1
239235, 238syl6eq 2331 . . . . . . . . . . . . . . . . 17  |-  ( n  =  1  ->  (
( n  +  1 )  /  2 )  =  1 )
240239fveq2d 5529 . . . . . . . . . . . . . . . 16  |-  ( n  =  1  ->  ( F `  ( (
n  +  1 )  /  2 ) )  =  ( F ` 
1 ) )
241231, 240eqtrd 2315 . . . . . . . . . . . . . . 15  |-  ( n  =  1  ->  if ( ( n  / 
2 )  e.  NN ,  ( G `  ( n  /  2
) ) ,  ( F `  ( ( n  +  1 )  /  2 ) ) )  =  ( F `
 1 ) )
242 fvex 5539 . . . . . . . . . . . . . . 15  |-  ( F `
 1 )  e. 
_V
243241, 23, 242fvmpt 5602 . . . . . . . . . . . . . 14  |-  ( 1  e.  NN  ->  ( H `  1 )  =  ( F ` 
1 ) )
244150, 243ax-mp 8 . . . . . . . . . . . . 13  |-  ( H `
 1 )  =  ( F `  1
)
245244fveq2i 5528 . . . . . . . . . . . 12  |-  ( 2nd `  ( H `  1
) )  =  ( 2nd `  ( F `
 1 ) )
246244fveq2i 5528 . . . . . . . . . . . 12  |-  ( 1st `  ( H `  1
) )  =  ( 1st `  ( F `
 1 ) )
247245, 246oveq12i 5870 . . . . . . . . . . 11  |-  ( ( 2nd `  ( H `
 1 ) )  -  ( 1st `  ( H `  1 )
) )  =  ( ( 2nd `  ( F `  1 )
)  -  ( 1st `  ( F `  1
) ) )
248223, 247syl6eq 2331 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( abs 
o.  -  )  o.  H ) `  1
)  =  ( ( 2nd `  ( F `
 1 ) )  -  ( 1st `  ( F `  1 )
) ) )
24962, 248seq1i 11060 . . . . . . . . 9  |-  ( ph  ->  (  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  H ) ) ` 
1 )  =  ( ( 2nd `  ( F `  1 )
)  -  ( 1st `  ( F `  1
) ) ) )
250236mulid1i 8839 . . . . . . . . . . 11  |-  ( 2  x.  1 )  =  2
251250fveq2i 5528 . . . . . . . . . 10  |-  ( ( ( abs  o.  -  )  o.  H ) `  ( 2  x.  1 ) )  =  ( ( ( abs  o.  -  )  o.  H
) `  2 )
25225ovolfsval 18830 . . . . . . . . . . . 12  |-  ( ( H : NN --> (  <_  i^i  ( RR  X.  RR ) )  /\  2  e.  NN )  ->  (
( ( abs  o.  -  )  o.  H
) `  2 )  =  ( ( 2nd `  ( H `  2
) )  -  ( 1st `  ( H ` 
2 ) ) ) )
25324, 37, 252sylancl 643 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( abs 
o.  -  )  o.  H ) `  2
)  =  ( ( 2nd `  ( H `
 2 ) )  -  ( 1st `  ( H `  2 )
) ) )
254 oveq1 5865 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  2  ->  (
n  /  2 )  =  ( 2  / 
2 ) )
255254, 238syl6eq 2331 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  2  ->  (
n  /  2 )  =  1 )
256255, 150syl6eqel 2371 . . . . . . . . . . . . . . . . 17  |-  ( n  =  2  ->  (
n  /  2 )  e.  NN )
257 iftrue 3571 . . . . . . . . . . . . . . . . 17  |-  ( ( n  /  2 )  e.  NN  ->  if ( ( n  / 
2 )  e.  NN ,  ( G `  ( n  /  2
) ) ,  ( F `  ( ( n  +  1 )  /  2 ) ) )  =  ( G `
 ( n  / 
2 ) ) )
258256, 257syl 15 . . . . . . . . . . . . . . . 16  |-  ( n  =  2  ->  if ( ( n  / 
2 )  e.  NN ,  ( G `  ( n  /  2
) ) ,  ( F `  ( ( n  +  1 )  /  2 ) ) )  =  ( G `
 ( n  / 
2 ) ) )
259255fveq2d 5529 . . . . . . . . . . . . . . . 16  |-  ( n  =  2  ->  ( G `  ( n  /  2 ) )  =  ( G ` 
1 ) )
260258, 259eqtrd 2315 . . . . . . . . . . . . . . 15  |-  ( n  =  2  ->  if ( ( n  / 
2 )  e.  NN ,  ( G `  ( n  /  2
) ) ,  ( F `  ( ( n  +  1 )  /  2 ) ) )  =  ( G `
 1 ) )
261 fvex 5539 . . . . . . . . . . . . . . 15  |-  ( G `
 1 )  e. 
_V
262260, 23, 261fvmpt 5602 . . . . . . . . . . . . . 14  |-  ( 2  e.  NN  ->  ( H `  2 )  =  ( G ` 
1 ) )
26337, 262ax-mp 8 . . . . . . . . . . . . 13  |-  ( H `
 2 )  =  ( G `  1
)
264263fveq2i 5528 . . . . . . . . . . . 12  |-  ( 2nd `  ( H `  2
) )  =  ( 2nd `  ( G `
 1 ) )
265263fveq2i 5528 . . . . . . . . . . . 12  |-  ( 1st `  ( H `  2
) )  =  ( 1st `  ( G `
 1 ) )
266264, 265oveq12i 5870 . . . . . . . . . . 11  |-  ( ( 2nd `  ( H `
 2 ) )  -  ( 1st `  ( H `  2 )
) )  =  ( ( 2nd `  ( G `  1 )
)  -  ( 1st `  ( G `  1
) ) )
267253, 266syl6eq 2331 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( abs 
o.  -  )  o.  H ) `  2
)  =  ( ( 2nd `  ( G `
 1 ) )  -  ( 1st `  ( G `  1 )
) ) )
268251, 267syl5eq 2327 . . . . . . . . 9  |-  ( ph  ->  ( ( ( abs 
o.  -  )  o.  H ) `  (
2  x.  1 ) )  =  ( ( 2nd `  ( G `
 1 ) )  -  ( 1st `  ( G `  1 )
) ) )
26983, 150, 44, 249, 268seqp1i 11062 . . . . . . . 8  |-  ( ph  ->  (  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  H ) ) `  ( 2  x.  1 ) )  =  ( ( ( 2nd `  ( F `  1 )
)  -  ( 1st `  ( F `  1
) ) )  +  ( ( 2nd `  ( G `  1 )
)  -  ( 1st `  ( G `  1
) ) ) ) )
270221, 269syl5eq 2327 . . . . . . 7  |-  ( ph  ->  ( U `  (
2  x.  1 ) )  =  ( ( ( 2nd `  ( F `  1 )
)  -  ( 1st `  ( F `  1
) ) )  +  ( ( 2nd `  ( G `  1 )
)  -  ( 1st `  ( G `  1
) ) ) ) )
271114fveq1i 5526 . . . . . . . . 9  |-  ( S `
 1 )  =  (  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  F ) ) ` 
1 )
272113ovolfsval 18830 . . . . . . . . . . 11  |-  ( ( F : NN --> (  <_  i^i  ( RR  X.  RR ) )  /\  1  e.  NN )  ->  (
( ( abs  o.  -  )  o.  F
) `  1 )  =  ( ( 2nd `  ( F `  1
) )  -  ( 1st `  ( F ` 
1 ) ) ) )
27317, 150, 272sylancl 643 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( abs 
o.  -  )  o.  F ) `  1
)  =  ( ( 2nd `  ( F `
 1 ) )  -  ( 1st `  ( F `  1 )
) ) )
27462, 273seq1i 11060 . . . . . . . . 9  |-  ( ph  ->  (  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  F ) ) ` 
1 )  =  ( ( 2nd `  ( F `  1 )
)  -  ( 1st `  ( F `  1
) ) ) )
275271, 274syl5eq 2327 . . . . . . . 8  |-  ( ph  ->  ( S `  1
)  =  ( ( 2nd `  ( F `
 1 ) )  -  ( 1st `  ( F `  1 )
) ) )
276128fveq1i 5526 . . . . . . . . 9  |-  ( T `
 1 )  =  (  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  G ) ) ` 
1 )
277127ovolfsval 18830 . . . . . . . . . . 11  |-  ( ( G : NN --> (  <_  i^i  ( RR  X.  RR ) )  /\  1  e.  NN )  ->  (
( ( abs  o.  -  )  o.  G
) `  1 )  =  ( ( 2nd `  ( G `  1
) )  -  ( 1st `  ( G ` 
1 ) ) ) )
2787, 150, 277sylancl 643 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( abs 
o.  -  )  o.  G ) `  1
)  =  ( ( 2nd `  ( G `
 1 ) )  -  ( 1st `  ( G `  1 )
) ) )
27962, 278seq1i 11060 . . . . . . . . 9  |-  ( ph  ->  (  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  G ) ) ` 
1 )  =  ( ( 2nd `  ( G `  1 )
)  -  ( 1st `  ( G `  1
) ) ) )
280276, 279syl5eq 2327 . . . . . . . 8  |-  ( ph  ->  ( T `  1
)  =  ( ( 2nd `  ( G `
 1 ) )  -  ( 1st `  ( G `  1 )
) ) )
281275, 280oveq12d 5876 . . . . . . 7  |-  ( ph  ->  ( ( S ` 
1 )  +  ( T `  1 ) )  =  ( ( ( 2nd `  ( F `  1 )
)  -  ( 1st `  ( F `  1
) ) )  +  ( ( 2nd `  ( G `  1 )
)  -  ( 1st `  ( G `  1
) ) ) ) )
282270, 281eqtr4d 2318 . . . . . 6  |-  ( ph  ->  ( U `  (
2  x.  1 ) )  =  ( ( S `  1 )  +  ( T ` 
1 ) ) )
283 oveq1 5865 . . . . . . . . 9  |-  ( ( 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 ) ) ) ) )
28444oveq2i 5869 . . . . . . . . . . . . 13  |-  ( ( 2  x.  k )  +  ( 2  x.  1 ) )  =  ( ( 2  x.  k )  +  ( 1  +  1 ) )
285236a1i 10 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN )  ->  2  e.  CC )
28648recnd 8861 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  CC )
28743a1i 10 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN )  ->  1  e.  CC )
288285, 286, 287adddid 8859 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN )  ->  ( 2  x.  ( k  +  1 ) )  =  ( ( 2  x.  k )  +  ( 2  x.  1 ) ) )
289 nnmulcl 9769 . . . . . . . . . . . . . . . . 17  |-  ( ( 2  e.  NN  /\  k  e.  NN )  ->  ( 2  x.  k
)  e.  NN )
29037, 289mpan 651 . . . . . . . . . . . . . . . 16  |-  ( k  e.  NN  ->  (
2  x.  k )  e.  NN )
291290adantl 452 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  NN )  ->  ( 2  x.  k )  e.  NN )
292291nncnd 9762 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN )  ->  ( 2  x.  k )  e.  CC )
293292, 287, 287addassd 8857 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( ( 2  x.  k
)  +  1 )  +  1 )  =  ( ( 2  x.  k )  +  ( 1  +  1 ) ) )
294284, 288, 2933eqtr4a 2341 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN )  ->  ( 2  x.  ( k  +  1 ) )  =  ( ( ( 2  x.  k )  +  1 )  +  1 ) )
295294fveq2d 5529 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN )  ->  ( U `
 ( 2  x.  ( k  +  1 ) ) )  =  ( U `  (
( ( 2  x.  k )  +  1 )  +  1 ) ) )
29626fveq1i 5526 . . . . . . . . . . . 12  |-  ( U `
 ( ( ( 2  x.  k )  +  1 )  +  1 ) )  =  (  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  H ) ) `  ( ( ( 2  x.  k )  +  1 )  +  1 ) )
297291peano2nnd 9763 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( 2  x.  k )  +  1 )  e.  NN )
298297, 83syl6eleq 2373 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( 2  x.  k )  +  1 )  e.  ( ZZ>= `  1 )
)
299 seqp1 11061 . . . . . . . . . . . . . 14  |-  ( ( ( 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 ) ) ) )
300298, 299syl 15 . . . . . . . . . . . . 13  |-  ( (
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 ) ) ) )
301291, 83syl6eleq 2373 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  NN )  ->  ( 2  x.  k )  e.  ( ZZ>= `  1 )
)
302 seqp1 11061 . . . . . . . . . . . . . . . 16  |-  ( ( 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 ) ) ) )
303301, 302syl 15 . . . . . . . . . . . . . . 15  |-  ( (
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 ) ) ) )
30426fveq1i 5526 . . . . . . . . . . . . . . . . 17  |-  ( U `
 ( 2  x.  k ) )  =  (  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  H ) ) `  ( 2  x.  k
) )
305304a1i 10 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  NN )  ->  ( U `
 ( 2  x.  k ) )  =  (  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  H ) ) `  ( 2  x.  k
) ) )
306 oveq1 5865 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  =  ( ( 2  x.  k )  +  1 )  ->  (
n  /  2 )  =  ( ( ( 2  x.  k )  +  1 )  / 
2 ) )
307306eleq1d 2349 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  =  ( ( 2  x.  k )  +  1 )  ->  (
( n  /  2
)  e.  NN  <->  ( (
( 2  x.  k
)  +  1 )  /  2 )  e.  NN ) )
308306fveq2d 5529 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  =  ( ( 2  x.  k )  +  1 )  ->  ( G `  ( n  /  2 ) )  =  ( G `  ( ( ( 2  x.  k )  +  1 )  /  2
) ) )
309 oveq1 5865 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( n  =  ( ( 2  x.  k )  +  1 )  ->  (
n  +  1 )  =  ( ( ( 2  x.  k )  +  1 )  +  1 ) )
310309oveq1d 5873 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  =  ( ( 2  x.  k )  +  1 )  ->  (
( n  +  1 )  /  2 )  =  ( ( ( ( 2  x.  k
)  +  1 )  +  1 )  / 
2 ) )
311310fveq2d 5529 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  =  ( ( 2  x.  k )  +  1 )  ->  ( F `  ( (
n  +  1 )  /  2 ) )  =  ( F `  ( ( ( ( 2  x.  k )  +  1 )  +  1 )  /  2
) ) )
312307, 308, 311ifbieq12d 3587 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 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 ) ) ) )
313 fvex 5539 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( G `
 ( ( ( 2  x.  k )  +  1 )  / 
2 ) )  e. 
_V
314 fvex 5539 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( F `
 ( ( ( ( 2  x.  k
)  +  1 )  +  1 )  / 
2 ) )  e. 
_V
315313, 314ifex 3623 . . . . . . . . . . . . . . . . . . . . . 22  |-  if ( ( ( ( 2  x.  k )  +  1 )  /  2
)  e.  NN , 
( G `  (
( ( 2  x.  k )  +  1 )  /  2 ) ) ,  ( F `
 ( ( ( ( 2  x.  k
)  +  1 )  +  1 )  / 
2 ) ) )  e.  _V
316312, 23, 315fvmpt 5602 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( 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
) ) ) )
317297, 316syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
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 ) ) ) )
318237a1i 10 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  k  e.  NN )  ->  2  =/=  0 )
319286, 285, 318divcan3d 9541 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( 2  x.  k )  /  2 )  =  k )
320319, 82eqeltrd 2357 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( 2  x.  k )  /  2 )  e.  NN )
321 nneo 10095 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 2  x.  k )  e.  NN  ->  (
( ( 2  x.  k )  /  2
)  e.  NN  <->  -.  (
( ( 2  x.  k )  +  1 )  /  2 )  e.  NN ) )
322291, 321syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( ( 2  x.  k
)  /  2 )  e.  NN  <->  -.  (
( ( 2  x.  k )  +  1 )  /  2 )  e.  NN ) )
323320, 322mpbid 201 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  k  e.  NN )  ->  -.  (
( ( 2  x.  k )  +  1 )  /  2 )  e.  NN )
324 iffalse 3572 . . . . . . . . . . . . . . . . . . . . 21  |-  ( -.  ( ( ( 2  x.  k )  +  1 )  /  2
)  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 ) ) )
325323, 324syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
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
) ) )
326294oveq1d 5873 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( 2  x.  ( k  +  1 ) )  /  2 )  =  ( ( ( ( 2  x.  k )  +  1 )  +  1 )  /  2
) )
32739nncnd 9762 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  k  e.  NN )  ->  ( k  +  1 )  e.  CC )
328 divcan3 9448 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( k  +  1 )  e.  CC  /\  2  e.  CC  /\  2  =/=  0 )  ->  (
( 2  x.  (
k  +  1 ) )  /  2 )  =  ( k  +  1 ) )
329236, 237, 328mp3an23 1269 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( k  +  1 )  e.  CC  ->  (
( 2  x.  (
k  +  1 ) )  /  2 )  =  ( k  +  1 ) )
330327, 329syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( 2  x.  ( k  +  1 ) )  /  2 )  =  ( k  +  1 ) )
331326, 330eqtr3d 2317 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( ( ( 2  x.  k )  +  1 )  +  1 )  /  2 )  =  ( k  +  1 ) )
332331fveq2d 5529 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  k  e.  NN )  ->  ( F `
 ( ( ( ( 2  x.  k
)  +  1 )  +  1 )  / 
2 ) )  =  ( F `  (
k  +  1 ) ) )
333317, 325, 3323eqtrd 2319 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  k  e.  NN )  ->  ( H `
 ( ( 2  x.  k )  +  1 ) )  =  ( F `  (
k  +  1 ) ) )
334333fveq2d 5529 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  NN )  ->  ( 2nd `  ( H `  (
( 2  x.  k
)  +  1 ) ) )  =  ( 2nd `  ( F `
 ( k  +  1 ) ) ) )
335333fveq2d 5529 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  NN )  ->  ( 1st `  ( H `  (
( 2  x.  k
)  +  1 ) ) )  =  ( 1st `  ( F `
 ( k  +  1 ) ) ) )
336334, 335oveq12d 5876 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( 2nd `  ( H `
 ( ( 2  x.  k )  +  1 ) ) )  -  ( 1st `  ( H `  ( (
2  x.  k )  +  1 ) ) ) )  =  ( ( 2nd `  ( F `  ( k  +  1 ) ) )  -  ( 1st `  ( F `  (
k  +  1 ) ) ) ) )
33724adantr 451 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  NN )  ->  H : NN
--> (  <_  i^i  ( RR  X.  RR ) ) )
33825ovolfsval 18830 . . . . . . . . . . . . . . . . . 18  |-  ( ( 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 ) ) ) ) )
339337, 297, 338syl2anc 642 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  H ) `  ( ( 2  x.  k )  +  1 ) )  =  ( ( 2nd `  ( H `  ( (
2  x.  k )  +  1 ) ) )  -  ( 1st `  ( H `  (
( 2  x.  k
)  +  1 ) ) ) ) )
340113ovolfsval 18830 . . . . . . . . . . . . . . . . . 18  |-  ( ( 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 ) ) ) ) )
34117, 38, 340syl2an 463 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  F ) `  ( k  +  1 ) )  =  ( ( 2nd `  ( F `  ( k  +  1 ) ) )  -  ( 1st `  ( F `  (
k  +  1 ) ) ) ) )
342336, 339, 3413eqtr4rd 2326 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  F ) `  ( k  +  1 ) )  =  ( ( ( abs  o.  -  )  o.  H
) `  ( (
2  x.  k )  +  1 ) ) )
343305, 342oveq12d 5876 . . . . . . . . . . . . . . 15  |-  ( (
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 ) ) ) )
344303, 343eqtr4d 2318 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN )  ->  (  seq  1 (  +  , 
( ( abs  o.  -  )  o.  H
) ) `  (
( 2  x.  k
)  +  1 ) )  =  ( ( U `  ( 2  x.  k ) )  +  ( ( ( abs  o.  -  )  o.  F ) `  (
k  +  1 ) ) ) )
345294fveq2d 5529 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  NN )  ->  ( H `
 ( 2  x.  ( k  +  1 ) ) )  =  ( H `  (
( ( 2  x.  k )  +  1 )  +  1 ) ) )
346297peano2nnd 9763 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( ( 2  x.  k
)  +  1 )  +  1 )  e.  NN )
347294, 346eqeltrd 2357 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  k  e.  NN )  ->  ( 2  x.  ( k  +  1 ) )  e.  NN )
348 oveq1 5865 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  =  ( 2  x.  ( k  +  1 ) )  ->  (
n  /  2 )  =  ( ( 2  x.  ( k  +  1 ) )  / 
2 ) )
349348eleq1d 2349 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  =  ( 2  x.  ( k  +  1 ) )  ->  (
( n  /  2
)  e.  NN  <->  ( (
2  x.  ( k  +  1 ) )  /  2 )  e.  NN ) )
350348fveq2d 5529 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  =  ( 2  x.  ( k  +  1 ) )  ->  ( G `  ( n  /  2 ) )  =  ( G `  ( ( 2  x.  ( k  +  1 ) )  /  2
) ) )
351 oveq1 5865 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  =  ( 2  x.  ( k  +  1 ) )  ->  (
n  +  1 )  =  ( ( 2  x.  ( k  +  1 ) )  +  1 ) )
352351oveq1d 5873 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  =  ( 2  x.  ( k  +  1 ) )  ->  (
( n  +  1 )  /  2 )  =  ( ( ( 2  x.  ( k  +  1 ) )  +  1 )  / 
2 ) )
353352fveq2d 5529 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  =  ( 2  x.  ( k  +  1 ) )  ->  ( F `  ( (
n  +  1 )  /  2 ) )  =  ( F `  ( ( ( 2  x.  ( k  +  1 ) )  +  1 )  /  2
) ) )
354349, 350, 353ifbieq12d 3587 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 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 ) ) ) )
355 fvex 5539 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( G `
 ( ( 2  x.  ( k  +  1 ) )  / 
2 ) )  e. 
_V
356 fvex 5539 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( F `
 ( ( ( 2  x.  ( k  +  1 ) )  +  1 )  / 
2 ) )  e. 
_V
357355, 356ifex 3623 . . . . . . . . . . . . . . . . . . . . 21  |-  if ( ( ( 2  x.  ( k  +  1 ) )  /  2
)  e.  NN , 
( G `  (
( 2  x.  (
k  +  1 ) )  /  2 ) ) ,  ( F `
 ( ( ( 2  x.  ( k  +  1 ) )  +  1 )  / 
2 ) ) )  e.  _V
358354, 23, 357fvmpt 5602 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 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 ) ) ) )
359347, 358syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( (
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 ) ) ) )
360330, 39eqeltrd 2357 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( 2  x.  ( k  +  1 ) )  /  2 )  e.  NN )
361 iftrue 3571 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 2  x.  (
k  +  1 ) )  /  2 )  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 ) ) )
362360, 361syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( (
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
) ) )
363330fveq2d 5529 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  k  e.  NN )  ->  ( G `
 ( ( 2  x.  ( k  +  1 ) )  / 
2 ) )  =  ( G `  (
k  +  1 ) ) )
364359, 362, 3633eqtrd 2319 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  NN )  ->  ( H `
 ( 2  x.  ( k  +  1 ) ) )  =  ( G `  (
k  +  1 ) ) )
365345, 364eqtr3d 2317 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  NN )  ->  ( H `
 ( ( ( 2  x.  k )  +  1 )  +  1 ) )  =  ( G `  (
k  +  1 ) ) )
366365fveq2d 5529 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  NN )  ->  ( 2nd `  ( H `  (
( ( 2  x.  k )  +  1 )  +  1 ) ) )  =  ( 2nd `  ( G `
 ( k  +  1 ) ) ) )
367365fveq2d 5529 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  NN )  ->  ( 1st `  ( H `  (
( ( 2  x.  k )  +  1 )  +  1 ) ) )  =  ( 1st `  ( G `
 ( k  +  1 ) ) ) )
368366, 367oveq12d 5876 . . . . . . . . . . . . . . 15  |-  ( (
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 ) ) ) ) )
36925ovolfsval 18830 . . . . . . . . . . . . . . . 16  |-  ( ( 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 ) ) ) ) )
370337, 346, 369syl2anc 642 . . . . . . . . . . . . . . 15  |-  ( (
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 ) ) ) ) )
371127ovolfsval 18830 . . . . . . . . . . . . . . . 16  |-  ( ( 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 ) ) ) ) )
3727, 38, 371syl2an 463 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  G ) `  ( k  +  1 ) )  =  ( ( 2nd `  ( G `  ( k  +  1 ) ) )  -  ( 1st `  ( G `  (
k  +  1 ) ) ) ) )
373368, 370, 3723eqtr4d 2325 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  H ) `  ( ( ( 2  x.  k )  +  1 )  +  1 ) )  =  ( ( ( abs  o.  -  )  o.  G
) `  ( k  +  1 ) ) )
374344, 373oveq12d 5876 . . . . . . . . . . . . 13  |-  ( (
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 ) ) ) )
375300, 374eqtrd 2315 . . . . . . . . . . . 12  |-  ( (
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 ) ) ) )
376296, 375syl5eq 2327 . . . . . . . . . . 11  |-  ( (
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 ) ) ) )
377 ffvelrn 5663 . . . . . . . . . . . . . . 15  |-  ( ( U : NN --> ( 0 [,)  +oo )  /\  (
2  x.  k )  e.  NN )  -> 
( U `  (
2  x.  k ) )  e.  ( 0 [,)  +oo ) )
37828, 290, 377syl2an 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN )  ->  ( U `
 ( 2  x.  k ) )  e.  ( 0 [,)  +oo ) )
37932, 378sseldi 3178 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN )  ->  ( U `
 ( 2  x.  k ) )  e.  RR )
380379recnd 8861 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN )  ->  ( U `
 ( 2  x.  k ) )  e.  CC )
381113ovolfsf 18831 . . . . . . . . . . . . . . . 16  |-  ( F : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  (
( abs  o.  -  )  o.  F ) : NN --> ( 0 [,)  +oo ) )
38217, 381syl 15 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( abs  o.  -  )  o.  F
) : NN --> ( 0 [,)  +oo ) )
383 ffvelrn 5663 . . . . . . . . . . . . . . 15  |-  ( ( ( ( abs  o.  -  )  o.  F
) : NN --> ( 0 [,)  +oo )  /\  (
k  +  1 )  e.  NN )  -> 
( ( ( abs 
o.  -  )  o.  F ) `  (
k  +  1 ) )  e.  ( 0 [,)  +oo ) )
384382, 38, 383syl2an 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  F ) `  ( k  +  1 ) )  e.  ( 0 [,)  +oo )
)
38532, 384sseldi 3178 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  F ) `  ( k  +  1 ) )  e.  RR )
386385recnd 8861 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  F ) `  ( k  +  1 ) )  e.  CC )
387127ovolfsf 18831 . . . . . . . . . . . . . . . 16  |-  ( G : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  (
( abs  o.  -  )  o.  G ) : NN --> ( 0 [,)  +oo ) )
3887, 387syl 15 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( abs  o.  -  )  o.  G
) : NN --> ( 0 [,)  +oo ) )
389 ffvelrn 5663 . . . . . . . . . . . . . . 15  |-  ( ( ( ( abs  o.  -  )  o.  G
) : NN --> ( 0 [,)  +oo )  /\  (
k  +  1 )  e.  NN )  -> 
( ( ( abs 
o.  -  )  o.  G ) `  (
k  +  1 ) )  e.  ( 0 [,)  +oo ) )
390388, 38, 389syl2an 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  G ) `  ( k  +  1 ) )  e.  ( 0 [,)  +oo )
)
39132, 390sseldi 3178 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  G ) `  ( k  +  1 ) )  e.  RR )
392391recnd 8861 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  G ) `  ( k  +  1 ) )  e.  CC )
393380, 386, 392addassd 8857 . . . . . . . . . . 11  |-  ( (
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 ) ) ) ) )
394295, 376, 3933eqtrd 2319 . . . . . . . . . 10  |-  ( (
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 ) ) ) ) )
395 seqp1 11061 . . . . . . . . . . . . . 14  |-  ( 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 ) ) ) )
39684, 395syl 15 . . . . . . . . . . . . 13  |-  ( (
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 ) ) ) )
397114fveq1i 5526 . . . . . . . . . . . . 13  |-  ( S `
 ( k  +  1 ) )  =  (  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  F ) ) `  ( k  +  1 ) )
398114fveq1i 5526 . . . . . . . . . . . . . 14  |-  ( S `
 k )  =  (  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  F ) ) `  k )
399398oveq1i 5868 . . . . . . . . . . . . 13  |-  ( ( S `  k )  +  ( ( ( abs  o.  -  )  o.  F ) `  (
k  +  1 ) ) )  =  ( (  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  F ) ) `  k )  +  ( ( ( abs  o.  -  )  o.  F
) `  ( k  +  1 ) ) )
400396, 397, 3993eqtr4g 2340 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN )  ->  ( S `
 ( k  +  1 ) )  =  ( ( S `  k )  +  ( ( ( abs  o.  -  )  o.  F
) `  ( k  +  1 ) ) ) )
401 seqp1 11061 . . . . . . . . . . . . . 14  |-  ( 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 ) ) ) )
40284, 401syl 15 . . . . . . . . . . . . 13  |-  ( (
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 ) ) ) )
403128fveq1i 5526 . . . . . . . . . . . . 13  |-  ( T `
 ( k  +  1 ) )  =  (  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  G ) ) `  ( k  +  1 ) )
404128fveq1i 5526 . . . . . . . . . . . . . 14  |-  ( T `
 k )  =  (  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  G ) ) `  k )
405404oveq1i 5868 . . . . . . . . . . . . 13  |-  ( ( T `  k )  +  ( ( ( abs  o.  -  )  o.  G ) `  (
k  +  1 ) ) )  =  ( (  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  G ) ) `  k )  +  ( ( ( abs  o.  -  )  o.  G
) `  ( k  +  1 ) ) )
406402, 403, 4053eqtr4g 2340 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN )  ->  ( T `
 ( k  +  1 ) )  =  ( ( T `  k )  +  ( ( ( abs  o.  -  )  o.  G
) `  ( k  +  1 ) ) ) )
407400, 406oveq12d 5876 . . . . . . . . . . 11  |-  ( (
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 ) ) ) ) )
408 ffvelrn 5663 . . . . . . . . . . . . . . 15  |-  ( ( S : NN --> ( 0 [,)  +oo )  /\  k  e.  NN )  ->  ( S `  k )  e.  ( 0 [,)  +oo ) )
409116, 408sylan 457 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN )  ->  ( S `
 k )  e.  ( 0 [,)  +oo ) )
41032, 409sseldi 3178 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN )  ->  ( S `
 k )  e.  RR )
411410recnd 8861 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN )  ->  ( S `
 k )  e.  CC )
412 ffvelrn 5663 . . . . . . . . . . . . . . 15  |-  ( ( T : NN --> ( 0 [,)  +oo )  /\  k  e.  NN )  ->  ( T `  k )  e.  ( 0 [,)  +oo ) )
413130, 412sylan 457 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN )  ->  ( T `
 k )  e.  ( 0 [,)  +oo ) )
41432, 413sseldi 3178 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN )  ->  ( T `
 k )  e.  RR )
415414recnd 8861 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN )  ->  ( T `
 k )  e.  CC )
416411, 386, 415, 392add4d 9035 . . . . . . . . . . 11  |-  ( (
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 ) ) ) ) )
417407, 416eqtrd 2315 . . . . . . . . . 10  |-  ( (
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 ) ) ) ) )
418394, 417eqeq12d 2297 . . . . . . . . 9  |-  ( (
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 ) ) ) ) ) )
419283, 418syl5ibr 212 . . . . . . . 8  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( U `  ( 2  x.  k ) )  =  ( ( S `
 k )  +  ( T `  k
) )  ->  ( U `  ( 2  x.  ( k  +  1 ) ) )  =  ( ( S `  ( k  +  1 ) )  +  ( T `  ( k  +  1 ) ) ) ) )
420419expcom 424 . . . . . . 7  |-  ( k  e.  NN  ->  ( ph  ->  ( ( U `
 ( 2  x.  k ) )  =  ( ( S `  k )  +  ( T `  k ) )  ->  ( U `  ( 2  x.  (
k  +  1 ) ) )  =  ( ( S `  (
k  +  1 ) )  +  ( T `
 ( k  +  1 ) ) ) ) ) )
421420a2d 23 . . . . . 6  |-  ( k  e.  NN  ->  (
( ph  ->  ( U `
 ( 2  x.  k ) )  =  ( ( S `  k )  +  ( T `  k ) ) )  ->  ( ph  ->  ( U `  ( 2  x.  (
k  +  1 ) ) )  =  ( ( S `  (
k  +  1 ) )  +  ( T `
 ( k  +  1 ) ) ) ) ) )
422199, 206, 213, 220, 282, 421nnind 9764 . . . . 5  |-  ( ( |_ `  ( ( k  +  1 )  /  2 ) )  e.  NN  ->  ( ph  ->  ( U `  ( 2  x.  ( |_ `  ( ( k  +  1 )  / 
2 ) ) ) )  =  ( ( S `  ( |_
`  ( ( k  +  1 )  / 
2 ) ) )  +  ( T `  ( |_ `  ( ( k  +  1 )  /  2 ) ) ) ) ) )
423422impcom 419 . . . 4  |-  ( (
ph  /\  ( |_ `  ( ( k  +  1 )  /  2
) )  e.  NN )  ->  ( U `  ( 2  x.  ( |_ `  ( ( k  +  1 )  / 
2 ) ) ) )  =  ( ( S `  ( |_
`  ( ( k  +  1 )  / 
2 ) ) )  +  ( T `  ( |_ `  ( ( k  +  1 )  /  2 ) ) ) ) )
42467, 423syldan 456 . . 3  |-  ( (
ph  /\  k  e.  NN )  ->  ( U `
 ( 2  x.  ( |_ `  (
( k  +  1 )  /  2 ) ) ) )  =  ( ( S `  ( |_ `  ( ( k  +  1 )  /  2 ) ) )  +  ( T `
 ( |_ `  ( ( k  +  1 )  /  2
) ) ) ) )
42574adantr 451 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  ( vol
* `  A )  e.  RR )
426425recnd 8861 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  ( vol
* `  A )  e.  CC )
42779adantr 451 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN )  ->  C  e.  RR )
428427