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

Theorem ovolunlem1a 19259
Description: Lemma for ovolun 19262. (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 9014 . . . . . . . . . . . . 13  |-  RR  e.  _V
32, 2xpex 4930 . . . . . . . . . . . 12  |-  ( RR 
X.  RR )  e. 
_V
43inex2 4286 . . . . . . . . . . 11  |-  (  <_  i^i  ( RR  X.  RR ) )  e.  _V
5 nnex 9938 . . . . . . . . . . 11  |-  NN  e.  _V
64, 5elmap 6978 . . . . . . . . . 10  |-  ( G  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) 
<->  G : NN --> (  <_  i^i  ( RR  X.  RR ) ) )
71, 6sylib 189 . . . . . . . . 9  |-  ( ph  ->  G : NN --> (  <_  i^i  ( RR  X.  RR ) ) )
87adantr 452 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  G : NN
--> (  <_  i^i  ( RR  X.  RR ) ) )
98ffvelrnda 5809 . . . . . . 7  |-  ( ( ( ph  /\  n  e.  NN )  /\  (
n  /  2 )  e.  NN )  -> 
( G `  (
n  /  2 ) )  e.  (  <_  i^i  ( RR  X.  RR ) ) )
10 nneo 10285 . . . . . . . . . . 11  |-  ( n  e.  NN  ->  (
( n  /  2
)  e.  NN  <->  -.  (
( n  +  1 )  /  2 )  e.  NN ) )
1110adantl 453 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( n  /  2 )  e.  NN  <->  -.  (
( n  +  1 )  /  2 )  e.  NN ) )
1211con2bid 320 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( ( n  +  1 )  /  2 )  e.  NN  <->  -.  (
n  /  2 )  e.  NN ) )
1312biimpar 472 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  NN )  /\  -.  ( n  /  2
)  e.  NN )  ->  ( ( n  +  1 )  / 
2 )  e.  NN )
14 ovolun.f1 . . . . . . . . . . 11  |-  ( ph  ->  F  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) )
154, 5elmap 6978 . . . . . . . . . . 11  |-  ( F  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) 
<->  F : NN --> (  <_  i^i  ( RR  X.  RR ) ) )
1614, 15sylib 189 . . . . . . . . . 10  |-  ( ph  ->  F : NN --> (  <_  i^i  ( RR  X.  RR ) ) )
1716adantr 452 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN )  ->  F : NN
--> (  <_  i^i  ( RR  X.  RR ) ) )
1817ffvelrnda 5809 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  NN )  /\  (
( n  +  1 )  /  2 )  e.  NN )  -> 
( F `  (
( n  +  1 )  /  2 ) )  e.  (  <_  i^i  ( RR  X.  RR ) ) )
1913, 18syldan 457 . . . . . . 7  |-  ( ( ( ph  /\  n  e.  NN )  /\  -.  ( n  /  2
)  e.  NN )  ->  ( F `  ( ( n  + 
1 )  /  2
) )  e.  (  <_  i^i  ( RR  X.  RR ) ) )
209, 19ifclda 3709 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  if ( ( n  /  2
)  e.  NN , 
( G `  (
n  /  2 ) ) ,  ( F `
 ( ( n  +  1 )  / 
2 ) ) )  e.  (  <_  i^i  ( RR  X.  RR ) ) )
21 ovolun.h . . . . . 6  |-  H  =  ( n  e.  NN  |->  if ( ( n  / 
2 )  e.  NN ,  ( G `  ( n  /  2
) ) ,  ( F `  ( ( n  +  1 )  /  2 ) ) ) )
2220, 21fmptd 5832 . . . . 5  |-  ( ph  ->  H : NN --> (  <_  i^i  ( RR  X.  RR ) ) )
23 eqid 2387 . . . . . 6  |-  ( ( abs  o.  -  )  o.  H )  =  ( ( abs  o.  -  )  o.  H )
24 ovolun.u . . . . . 6  |-  U  =  seq  1 (  +  ,  ( ( abs 
o.  -  )  o.  H ) )
2523, 24ovolsf 19236 . . . . 5  |-  ( H : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  U : NN --> ( 0 [,) 
+oo ) )
2622, 25syl 16 . . . 4  |-  ( ph  ->  U : NN --> ( 0 [,)  +oo ) )
27 0re 9024 . . . . 5  |-  0  e.  RR
28 pnfxr 10645 . . . . 5  |-  +oo  e.  RR*
29 icossre 10923 . . . . 5  |-  ( ( 0  e.  RR  /\  +oo 
e.  RR* )  ->  (
0 [,)  +oo )  C_  RR )
3027, 28, 29mp2an 654 . . . 4  |-  ( 0 [,)  +oo )  C_  RR
31 fss 5539 . . . 4  |-  ( ( U : NN --> ( 0 [,)  +oo )  /\  (
0 [,)  +oo )  C_  RR )  ->  U : NN
--> RR )
3226, 30, 31sylancl 644 . . 3  |-  ( ph  ->  U : NN --> RR )
3332ffvelrnda 5809 . 2  |-  ( (
ph  /\  k  e.  NN )  ->  ( U `
 k )  e.  RR )
34 2nn 10065 . . . 4  |-  2  e.  NN
35 peano2nn 9944 . . . . . . . . 9  |-  ( k  e.  NN  ->  (
k  +  1 )  e.  NN )
3635adantl 453 . . . . . . . 8  |-  ( (
ph  /\  k  e.  NN )  ->  ( k  +  1 )  e.  NN )
3736nnred 9947 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN )  ->  ( k  +  1 )  e.  RR )
3837rehalfcld 10146 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( k  +  1 )  /  2 )  e.  RR )
3938flcld 11134 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  ( |_
`  ( ( k  +  1 )  / 
2 ) )  e.  ZZ )
40 ax-1cn 8981 . . . . . . . . 9  |-  1  e.  CC
41402timesi 10033 . . . . . . . 8  |-  ( 2  x.  1 )  =  ( 1  +  1 )
42 nnge1 9958 . . . . . . . . . 10  |-  ( k  e.  NN  ->  1  <_  k )
4342adantl 453 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN )  ->  1  <_ 
k )
44 nnre 9939 . . . . . . . . . . 11  |-  ( k  e.  NN  ->  k  e.  RR )
4544adantl 453 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  RR )
46 1re 9023 . . . . . . . . . . 11  |-  1  e.  RR
47 leadd1 9428 . . . . . . . . . . 11  |-  ( ( 1  e.  RR  /\  k  e.  RR  /\  1  e.  RR )  ->  (
1  <_  k  <->  ( 1  +  1 )  <_ 
( k  +  1 ) ) )
4846, 46, 47mp3an13 1270 . . . . . . . . . 10  |-  ( k  e.  RR  ->  (
1  <_  k  <->  ( 1  +  1 )  <_ 
( k  +  1 ) ) )
4945, 48syl 16 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN )  ->  ( 1  <_  k  <->  ( 1  +  1 )  <_ 
( k  +  1 ) ) )
5043, 49mpbid 202 . . . . . . . 8  |-  ( (
ph  /\  k  e.  NN )  ->  ( 1  +  1 )  <_ 
( k  +  1 ) )
5141, 50syl5eqbr 4186 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN )  ->  ( 2  x.  1 )  <_ 
( k  +  1 ) )
52 2re 10001 . . . . . . . . . 10  |-  2  e.  RR
53 2pos 10014 . . . . . . . . . 10  |-  0  <  2
5452, 53pm3.2i 442 . . . . . . . . 9  |-  ( 2  e.  RR  /\  0  <  2 )
55 lemuldiv2 9822 . . . . . . . . 9  |-  ( ( 1  e.  RR  /\  ( k  +  1 )  e.  RR  /\  ( 2  e.  RR  /\  0  <  2 ) )  ->  ( (
2  x.  1 )  <_  ( k  +  1 )  <->  1  <_  ( ( k  +  1 )  /  2 ) ) )
5646, 54, 55mp3an13 1270 . . . . . . . 8  |-  ( ( k  +  1 )  e.  RR  ->  (
( 2  x.  1 )  <_  ( k  +  1 )  <->  1  <_  ( ( k  +  1 )  /  2 ) ) )
5737, 56syl 16 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( 2  x.  1 )  <_  ( k  +  1 )  <->  1  <_  ( ( k  +  1 )  /  2 ) ) )
5851, 57mpbid 202 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  1  <_ 
( ( k  +  1 )  /  2
) )
59 1z 10243 . . . . . . 7  |-  1  e.  ZZ
60 flge 11141 . . . . . . 7  |-  ( ( ( ( k  +  1 )  /  2
)  e.  RR  /\  1  e.  ZZ )  ->  ( 1  <_  (
( k  +  1 )  /  2 )  <->  1  <_  ( |_ `  ( ( k  +  1 )  /  2
) ) ) )
6138, 59, 60sylancl 644 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  ( 1  <_  ( ( k  +  1 )  / 
2 )  <->  1  <_  ( |_ `  ( ( k  +  1 )  /  2 ) ) ) )
6258, 61mpbid 202 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  1  <_ 
( |_ `  (
( k  +  1 )  /  2 ) ) )
63 elnnz1 10239 . . . . 5  |-  ( ( |_ `  ( ( k  +  1 )  /  2 ) )  e.  NN  <->  ( ( |_ `  ( ( k  +  1 )  / 
2 ) )  e.  ZZ  /\  1  <_ 
( |_ `  (
( k  +  1 )  /  2 ) ) ) )
6439, 62, 63sylanbrc 646 . . . 4  |-  ( (
ph  /\  k  e.  NN )  ->  ( |_
`  ( ( k  +  1 )  / 
2 ) )  e.  NN )
65 nnmulcl 9955 . . . 4  |-  ( ( 2  e.  NN  /\  ( |_ `  ( ( k  +  1 )  /  2 ) )  e.  NN )  -> 
( 2  x.  ( |_ `  ( ( k  +  1 )  / 
2 ) ) )  e.  NN )
6634, 64, 65sylancr 645 . . 3  |-  ( (
ph  /\  k  e.  NN )  ->  ( 2  x.  ( |_ `  ( ( k  +  1 )  /  2
) ) )  e.  NN )
6732ffvelrnda 5809 . . 3  |-  ( (
ph  /\  ( 2  x.  ( |_ `  ( ( k  +  1 )  /  2
) ) )  e.  NN )  ->  ( U `  ( 2  x.  ( |_ `  (
( k  +  1 )  /  2 ) ) ) )  e.  RR )
6866, 67syldan 457 . 2  |-  ( (
ph  /\  k  e.  NN )  ->  ( U `
 ( 2  x.  ( |_ `  (
( k  +  1 )  /  2 ) ) ) )  e.  RR )
69 ovolun.a . . . . . 6  |-  ( ph  ->  ( A  C_  RR  /\  ( vol * `  A )  e.  RR ) )
7069simprd 450 . . . . 5  |-  ( ph  ->  ( vol * `  A )  e.  RR )
71 ovolun.b . . . . . 6  |-  ( ph  ->  ( B  C_  RR  /\  ( vol * `  B )  e.  RR ) )
7271simprd 450 . . . . 5  |-  ( ph  ->  ( vol * `  B )  e.  RR )
7370, 72readdcld 9048 . . . 4  |-  ( ph  ->  ( ( vol * `  A )  +  ( vol * `  B
) )  e.  RR )
74 ovolun.c . . . . 5  |-  ( ph  ->  C  e.  RR+ )
7574rpred 10580 . . . 4  |-  ( ph  ->  C  e.  RR )
7673, 75readdcld 9048 . . 3  |-  ( ph  ->  ( ( ( vol
* `  A )  +  ( vol * `  B ) )  +  C )  e.  RR )
7776adantr 452 . 2  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( ( vol * `  A )  +  ( vol * `  B
) )  +  C
)  e.  RR )
78 simpr 448 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  NN )
79 nnuz 10453 . . . . 5  |-  NN  =  ( ZZ>= `  1 )
8078, 79syl6eleq 2477 . . . 4  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  ( ZZ>= `  1 )
)
81 nnz 10235 . . . . . . 7  |-  ( k  e.  NN  ->  k  e.  ZZ )
8281adantl 453 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  ZZ )
83 flhalf 11158 . . . . . 6  |-  ( k  e.  ZZ  ->  k  <_  ( 2  x.  ( |_ `  ( ( k  +  1 )  / 
2 ) ) ) )
8482, 83syl 16 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  k  <_ 
( 2  x.  ( |_ `  ( ( k  +  1 )  / 
2 ) ) ) )
85 nnz 10235 . . . . . . 7  |-  ( ( 2  x.  ( |_
`  ( ( k  +  1 )  / 
2 ) ) )  e.  NN  ->  (
2  x.  ( |_
`  ( ( k  +  1 )  / 
2 ) ) )  e.  ZZ )
86 eluz 10431 . . . . . . 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 ) ) ) ) )
8781, 85, 86syl2an 464 . . . . . 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 ) ) ) ) )
8878, 66, 87syl2anc 643 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( 2  x.  ( |_
`  ( ( k  +  1 )  / 
2 ) ) )  e.  ( ZZ>= `  k
)  <->  k  <_  (
2  x.  ( |_
`  ( ( k  +  1 )  / 
2 ) ) ) ) )
8984, 88mpbird 224 . . . 4  |-  ( (
ph  /\  k  e.  NN )  ->  ( 2  x.  ( |_ `  ( ( k  +  1 )  /  2
) ) )  e.  ( ZZ>= `  k )
)
90 elfznn 11012 . . . . 5  |-  ( j  e.  ( 1 ... ( 2  x.  ( |_ `  ( ( k  +  1 )  / 
2 ) ) ) )  ->  j  e.  NN )
9123ovolfsf 19235 . . . . . . . . . 10  |-  ( H : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  (
( abs  o.  -  )  o.  H ) : NN --> ( 0 [,)  +oo ) )
9222, 91syl 16 . . . . . . . . 9  |-  ( ph  ->  ( ( abs  o.  -  )  o.  H
) : NN --> ( 0 [,)  +oo ) )
9392adantr 452 . . . . . . . 8  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( abs  o.  -  )  o.  H ) : NN --> ( 0 [,)  +oo ) )
9493ffvelrnda 5809 . . . . . . 7  |-  ( ( ( ph  /\  k  e.  NN )  /\  j  e.  NN )  ->  (
( ( abs  o.  -  )  o.  H
) `  j )  e.  ( 0 [,)  +oo ) )
95 elrege0 10939 . . . . . . 7  |-  ( ( ( ( abs  o.  -  )  o.  H
) `  j )  e.  ( 0 [,)  +oo ) 
<->  ( ( ( ( abs  o.  -  )  o.  H ) `  j
)  e.  RR  /\  0  <_  ( ( ( abs  o.  -  )  o.  H ) `  j
) ) )
9694, 95sylib 189 . . . . . 6  |-  ( ( ( ph  /\  k  e.  NN )  /\  j  e.  NN )  ->  (
( ( ( abs 
o.  -  )  o.  H ) `  j
)  e.  RR  /\  0  <_  ( ( ( abs  o.  -  )  o.  H ) `  j
) ) )
9796simpld 446 . . . . 5  |-  ( ( ( ph  /\  k  e.  NN )  /\  j  e.  NN )  ->  (
( ( abs  o.  -  )  o.  H
) `  j )  e.  RR )
9890, 97sylan2 461 . . . 4  |-  ( ( ( ph  /\  k  e.  NN )  /\  j  e.  ( 1 ... (
2  x.  ( |_
`  ( ( k  +  1 )  / 
2 ) ) ) ) )  ->  (
( ( abs  o.  -  )  o.  H
) `  j )  e.  RR )
99 elfzuz 10987 . . . . . 6  |-  ( j  e.  ( ( k  +  1 ) ... ( 2  x.  ( |_ `  ( ( k  +  1 )  / 
2 ) ) ) )  ->  j  e.  ( ZZ>= `  ( k  +  1 ) ) )
10079uztrn2 10435 . . . . . 6  |-  ( ( ( k  +  1 )  e.  NN  /\  j  e.  ( ZZ>= `  ( k  +  1 ) ) )  -> 
j  e.  NN )
10136, 99, 100syl2an 464 . . . . 5  |-  ( ( ( ph  /\  k  e.  NN )  /\  j  e.  ( ( k  +  1 ) ... (
2  x.  ( |_
`  ( ( k  +  1 )  / 
2 ) ) ) ) )  ->  j  e.  NN )
10296simprd 450 . . . . 5  |-  ( ( ( ph  /\  k  e.  NN )  /\  j  e.  NN )  ->  0  <_  ( ( ( abs 
o.  -  )  o.  H ) `  j
) )
103101, 102syldan 457 . . . 4  |-  ( ( ( ph  /\  k  e.  NN )  /\  j  e.  ( ( k  +  1 ) ... (
2  x.  ( |_
`  ( ( k  +  1 )  / 
2 ) ) ) ) )  ->  0  <_  ( ( ( abs 
o.  -  )  o.  H ) `  j
) )
10480, 89, 98, 103sermono 11282 . . 3  |-  ( (
ph  /\  k  e.  NN )  ->  (  seq  1 (  +  , 
( ( abs  o.  -  )  o.  H
) ) `  k
)  <_  (  seq  1 (  +  , 
( ( abs  o.  -  )  o.  H
) ) `  (
2  x.  ( |_
`  ( ( k  +  1 )  / 
2 ) ) ) ) )
10524fveq1i 5669 . . 3  |-  ( U `
 k )  =  (  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  H ) ) `  k )
10624fveq1i 5669 . . 3  |-  ( U `
 ( 2  x.  ( |_ `  (
( k  +  1 )  /  2 ) ) ) )  =  (  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  H ) ) `  ( 2  x.  ( |_ `  ( ( k  +  1 )  / 
2 ) ) ) )
107104, 105, 1063brtr4g 4185 . 2  |-  ( (
ph  /\  k  e.  NN )  ->  ( U `
 k )  <_ 
( U `  (
2  x.  ( |_
`  ( ( k  +  1 )  / 
2 ) ) ) ) )
108 eqid 2387 . . . . . . . . . 10  |-  ( ( abs  o.  -  )  o.  F )  =  ( ( abs  o.  -  )  o.  F )
109 ovolun.s . . . . . . . . . 10  |-  S  =  seq  1 (  +  ,  ( ( abs 
o.  -  )  o.  F ) )
110108, 109ovolsf 19236 . . . . . . . . 9  |-  ( F : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  S : NN --> ( 0 [,) 
+oo ) )
11116, 110syl 16 . . . . . . . 8  |-  ( ph  ->  S : NN --> ( 0 [,)  +oo ) )
112 frn 5537 . . . . . . . 8  |-  ( S : NN --> ( 0 [,)  +oo )  ->  ran  S 
C_  ( 0 [,) 
+oo ) )
113111, 112syl 16 . . . . . . 7  |-  ( ph  ->  ran  S  C_  (
0 [,)  +oo ) )
114113, 30syl6ss 3303 . . . . . 6  |-  ( ph  ->  ran  S  C_  RR )
115114adantr 452 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  ran  S  C_  RR )
116 ffn 5531 . . . . . . . 8  |-  ( S : NN --> ( 0 [,)  +oo )  ->  S  Fn  NN )
117111, 116syl 16 . . . . . . 7  |-  ( ph  ->  S  Fn  NN )
118117adantr 452 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  S  Fn  NN )
119 fnfvelrn 5806 . . . . . 6  |-  ( ( S  Fn  NN  /\  ( |_ `  ( ( k  +  1 )  /  2 ) )  e.  NN )  -> 
( S `  ( |_ `  ( ( k  +  1 )  / 
2 ) ) )  e.  ran  S )
120118, 64, 119syl2anc 643 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  ( S `
 ( |_ `  ( ( k  +  1 )  /  2
) ) )  e. 
ran  S )
121115, 120sseldd 3292 . . . 4  |-  ( (
ph  /\  k  e.  NN )  ->  ( S `
 ( |_ `  ( ( k  +  1 )  /  2
) ) )  e.  RR )
122 eqid 2387 . . . . . . . . . 10  |-  ( ( abs  o.  -  )  o.  G )  =  ( ( abs  o.  -  )  o.  G )
123 ovolun.t . . . . . . . . . 10  |-  T  =  seq  1 (  +  ,  ( ( abs 
o.  -  )  o.  G ) )
124122, 123ovolsf 19236 . . . . . . . . 9  |-  ( G : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  T : NN --> ( 0 [,) 
+oo ) )
1257, 124syl 16 . . . . . . . 8  |-  ( ph  ->  T : NN --> ( 0 [,)  +oo ) )
126 frn 5537 . . . . . . . 8  |-  ( T : NN --> ( 0 [,)  +oo )  ->  ran  T 
C_  ( 0 [,) 
+oo ) )
127125, 126syl 16 . . . . . . 7  |-  ( ph  ->  ran  T  C_  (
0 [,)  +oo ) )
128127, 30syl6ss 3303 . . . . . 6  |-  ( ph  ->  ran  T  C_  RR )
129128adantr 452 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  ran  T  C_  RR )
130 ffn 5531 . . . . . . . 8  |-  ( T : NN --> ( 0 [,)  +oo )  ->  T  Fn  NN )
131125, 130syl 16 . . . . . . 7  |-  ( ph  ->  T  Fn  NN )
132131adantr 452 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  T  Fn  NN )
133 fnfvelrn 5806 . . . . . 6  |-  ( ( T  Fn  NN  /\  ( |_ `  ( ( k  +  1 )  /  2 ) )  e.  NN )  -> 
( T `  ( |_ `  ( ( k  +  1 )  / 
2 ) ) )  e.  ran  T )
134132, 64, 133syl2anc 643 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  ( T `
 ( |_ `  ( ( k  +  1 )  /  2
) ) )  e. 
ran  T )
135129, 134sseldd 3292 . . . 4  |-  ( (
ph  /\  k  e.  NN )  ->  ( T `
 ( |_ `  ( ( k  +  1 )  /  2
) ) )  e.  RR )
13675rehalfcld 10146 . . . . . 6  |-  ( ph  ->  ( C  /  2
)  e.  RR )
13770, 136readdcld 9048 . . . . 5  |-  ( ph  ->  ( ( vol * `  A )  +  ( C  /  2 ) )  e.  RR )
138137adantr 452 . . . 4  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( vol * `  A
)  +  ( C  /  2 ) )  e.  RR )
13972, 136readdcld 9048 . . . . 5  |-  ( ph  ->  ( ( vol * `  B )  +  ( C  /  2 ) )  e.  RR )
140139adantr 452 . . . 4  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( vol * `  B
)  +  ( C  /  2 ) )  e.  RR )
141 ressxr 9062 . . . . . . . . 9  |-  RR  C_  RR*
142114, 141syl6ss 3303 . . . . . . . 8  |-  ( ph  ->  ran  S  C_  RR* )
143 supxrcl 10825 . . . . . . . 8  |-  ( ran 
S  C_  RR*  ->  sup ( ran  S ,  RR* ,  <  )  e.  RR* )
144142, 143syl 16 . . . . . . 7  |-  ( ph  ->  sup ( ran  S ,  RR* ,  <  )  e.  RR* )
145 1nn 9943 . . . . . . . . . . 11  |-  1  e.  NN
146 fdm 5535 . . . . . . . . . . . 12  |-  ( S : NN --> ( 0 [,)  +oo )  ->  dom  S  =  NN )
147111, 146syl 16 . . . . . . . . . . 11  |-  ( ph  ->  dom  S  =  NN )
148145, 147syl5eleqr 2474 . . . . . . . . . 10  |-  ( ph  ->  1  e.  dom  S
)
149 ne0i 3577 . . . . . . . . . 10  |-  ( 1  e.  dom  S  ->  dom  S  =/=  (/) )
150148, 149syl 16 . . . . . . . . 9  |-  ( ph  ->  dom  S  =/=  (/) )
151 dm0rn0 5026 . . . . . . . . . 10  |-  ( dom 
S  =  (/)  <->  ran  S  =  (/) )
152151necon3bii 2582 . . . . . . . . 9  |-  ( dom 
S  =/=  (/)  <->  ran  S  =/=  (/) )
153150, 152sylib 189 . . . . . . . 8  |-  ( ph  ->  ran  S  =/=  (/) )
154 supxrgtmnf 10840 . . . . . . . 8  |-  ( ( ran  S  C_  RR  /\ 
ran  S  =/=  (/) )  ->  -oo  <  sup ( ran  S ,  RR* ,  <  )
)
155114, 153, 154syl2anc 643 . . . . . . 7  |-  ( ph  ->  -oo  <  sup ( ran  S ,  RR* ,  <  ) )
156 ovolun.f3 . . . . . . 7  |-  ( ph  ->  sup ( ran  S ,  RR* ,  <  )  <_  ( ( vol * `  A )  +  ( C  /  2 ) ) )
157 xrre 10689 . . . . . . 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 )
158144, 137, 155, 156, 157syl22anc 1185 . . . . . 6  |-  ( ph  ->  sup ( ran  S ,  RR* ,  <  )  e.  RR )
159158adantr 452 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  sup ( ran  S ,  RR* ,  <  )  e.  RR )
160142adantr 452 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  ran  S  C_ 
RR* )
161 supxrub 10835 . . . . . 6  |-  ( ( ran  S  C_  RR*  /\  ( S `  ( |_ `  ( ( k  +  1 )  /  2
) ) )  e. 
ran  S )  -> 
( S `  ( |_ `  ( ( k  +  1 )  / 
2 ) ) )  <_  sup ( ran  S ,  RR* ,  <  )
)
162160, 120, 161syl2anc 643 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  ( S `
 ( |_ `  ( ( k  +  1 )  /  2
) ) )  <_  sup ( ran  S ,  RR* ,  <  ) )
163156adantr 452 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  sup ( ran  S ,  RR* ,  <  )  <_  ( ( vol
* `  A )  +  ( C  / 
2 ) ) )
164121, 159, 138, 162, 163letrd 9159 . . . 4  |-  ( (
ph  /\  k  e.  NN )  ->  ( S `
 ( |_ `  ( ( k  +  1 )  /  2
) ) )  <_ 
( ( vol * `  A )  +  ( C  /  2 ) ) )
165128, 141syl6ss 3303 . . . . . . . 8  |-  ( ph  ->  ran  T  C_  RR* )
166 supxrcl 10825 . . . . . . . 8  |-  ( ran 
T  C_  RR*  ->  sup ( ran  T ,  RR* ,  <  )  e.  RR* )
167165, 166syl 16 . . . . . . 7  |-  ( ph  ->  sup ( ran  T ,  RR* ,  <  )  e.  RR* )
168 fdm 5535 . . . . . . . . . . . 12  |-  ( T : NN --> ( 0 [,)  +oo )  ->  dom  T  =  NN )
169125, 168syl 16 . . . . . . . . . . 11  |-  ( ph  ->  dom  T  =  NN )
170145, 169syl5eleqr 2474 . . . . . . . . . 10  |-  ( ph  ->  1  e.  dom  T
)
171 ne0i 3577 . . . . . . . . . 10  |-  ( 1  e.  dom  T  ->  dom  T  =/=  (/) )
172170, 171syl 16 . . . . . . . . 9  |-  ( ph  ->  dom  T  =/=  (/) )
173 dm0rn0 5026 . . . . . . . . . 10  |-  ( dom 
T  =  (/)  <->  ran  T  =  (/) )
174173necon3bii 2582 . . . . . . . . 9  |-  ( dom 
T  =/=  (/)  <->  ran  T  =/=  (/) )
175172, 174sylib 189 . . . . . . . 8  |-  ( ph  ->  ran  T  =/=  (/) )
176 supxrgtmnf 10840 . . . . . . . 8  |-  ( ( ran  T  C_  RR  /\ 
ran  T  =/=  (/) )  ->  -oo  <  sup ( ran  T ,  RR* ,  <  )
)
177128, 175, 176syl2anc 643 . . . . . . 7  |-  ( ph  ->  -oo  <  sup ( ran  T ,  RR* ,  <  ) )
178 ovolun.g3 . . . . . . 7  |-  ( ph  ->  sup ( ran  T ,  RR* ,  <  )  <_  ( ( vol * `  B )  +  ( C  /  2 ) ) )
179 xrre 10689 . . . . . . 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 )
180167, 139, 177, 178, 179syl22anc 1185 . . . . . 6  |-  ( ph  ->  sup ( ran  T ,  RR* ,  <  )  e.  RR )
181180adantr 452 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  sup ( ran  T ,  RR* ,  <  )  e.  RR )
182165adantr 452 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  ran  T  C_ 
RR* )
183 supxrub 10835 . . . . . 6  |-  ( ( ran  T  C_  RR*  /\  ( T `  ( |_ `  ( ( k  +  1 )  /  2
) ) )  e. 
ran  T )  -> 
( T `  ( |_ `  ( ( k  +  1 )  / 
2 ) ) )  <_  sup ( ran  T ,  RR* ,  <  )
)
184182, 134, 183syl2anc 643 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  ( T `
 ( |_ `  ( ( k  +  1 )  /  2
) ) )  <_  sup ( ran  T ,  RR* ,  <  ) )
185178adantr 452 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  sup ( ran  T ,  RR* ,  <  )  <_  ( ( vol
* `  B )  +  ( C  / 
2 ) ) )
186135, 181, 140, 184, 185letrd 9159 . . . 4  |-  ( (
ph  /\  k  e.  NN )  ->  ( T `
 ( |_ `  ( ( k  +  1 )  /  2
) ) )  <_ 
( ( vol * `  B )  +  ( C  /  2 ) ) )
187121, 135, 138, 140, 164, 186le2addd 9576 . . 3  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( S `  ( |_
`  ( ( k  +  1 )  / 
2 ) ) )  +  ( T `  ( |_ `  ( ( k  +  1 )  /  2 ) ) ) )  <_  (
( ( vol * `  A )  +  ( C  /  2 ) )  +  ( ( vol * `  B
)  +  ( C  /  2 ) ) ) )
188 oveq2 6028 . . . . . . . . 9  |-  ( z  =  1  ->  (
2  x.  z )  =  ( 2  x.  1 ) )
189188fveq2d 5672 . . . . . . . 8  |-  ( z  =  1  ->  ( U `  ( 2  x.  z ) )  =  ( U `  (
2  x.  1 ) ) )
190 fveq2 5668 . . . . . . . . 9  |-  ( z  =  1  ->  ( S `  z )  =  ( S ` 
1 ) )
191 fveq2 5668 . . . . . . . . 9  |-  ( z  =  1  ->  ( T `  z )  =  ( T ` 
1 ) )
192190, 191oveq12d 6038 . . . . . . . 8  |-  ( z  =  1  ->  (
( S `  z
)  +  ( T `
 z ) )  =  ( ( S `
 1 )  +  ( T `  1
) ) )
193189, 192eqeq12d 2401 . . . . . . 7  |-  ( z  =  1  ->  (
( U `  (
2  x.  z ) )  =  ( ( S `  z )  +  ( T `  z ) )  <->  ( U `  ( 2  x.  1 ) )  =  ( ( S `  1
)  +  ( T `
 1 ) ) ) )
194193imbi2d 308 . . . . . 6  |-  ( z  =  1  ->  (
( ph  ->  ( U `
 ( 2  x.  z ) )  =  ( ( S `  z )  +  ( T `  z ) ) )  <->  ( ph  ->  ( U `  (
2  x.  1 ) )  =  ( ( S `  1 )  +  ( T ` 
1 ) ) ) ) )
195 oveq2 6028 . . . . . . . . 9  |-  ( z  =  k  ->  (
2  x.  z )  =  ( 2  x.  k ) )
196195fveq2d 5672 . . . . . . . 8  |-  ( z  =  k  ->  ( U `  ( 2  x.  z ) )  =  ( U `  (
2  x.  k ) ) )
197 fveq2 5668 . . . . . . . . 9  |-  ( z  =  k  ->  ( S `  z )  =  ( S `  k ) )
198 fveq2 5668 . . . . . . . . 9  |-  ( z  =  k  ->  ( T `  z )  =  ( T `  k ) )
199197, 198oveq12d 6038 . . . . . . . 8  |-  ( z  =  k  ->  (
( S `  z
)  +  ( T `
 z ) )  =  ( ( S `
 k )  +  ( T `  k
) ) )
200196, 199eqeq12d 2401 . . . . . . 7  |-  ( z  =  k  ->  (
( U `  (
2  x.  z ) )  =  ( ( S `  z )  +  ( T `  z ) )  <->  ( U `  ( 2  x.  k
) )  =  ( ( S `  k
)  +  ( T `
 k ) ) ) )
201200imbi2d 308 . . . . . 6  |-  ( z  =  k  ->  (
( ph  ->  ( U `
 ( 2  x.  z ) )  =  ( ( S `  z )  +  ( T `  z ) ) )  <->  ( ph  ->  ( U `  (
2  x.  k ) )  =  ( ( S `  k )  +  ( T `  k ) ) ) ) )
202 oveq2 6028 . . . . . . . . 9  |-  ( z  =  ( k  +  1 )  ->  (
2  x.  z )  =  ( 2  x.  ( k  +  1 ) ) )
203202fveq2d 5672 . . . . . . . 8  |-  ( z  =  ( k  +  1 )  ->  ( U `  ( 2  x.  z ) )  =  ( U `  (
2  x.  ( k  +  1 ) ) ) )
204 fveq2 5668 . . . . . . . . 9  |-  ( z  =  ( k  +  1 )  ->  ( S `  z )  =  ( S `  ( k  +  1 ) ) )
205 fveq2 5668 . . . . . . . . 9  |-  ( z  =  ( k  +  1 )  ->  ( T `  z )  =  ( T `  ( k  +  1 ) ) )
206204, 205oveq12d 6038 . . . . . . . 8  |-  ( z  =  ( k  +  1 )  ->  (
( S `  z
)  +  ( T `
 z ) )  =  ( ( S `
 ( k  +  1 ) )  +  ( T `  (
k  +  1 ) ) ) )
207203, 206eqeq12d 2401 . . . . . . 7  |-  ( z  =  ( k  +  1 )  ->  (
( U `  (
2  x.  z ) )  =  ( ( S `  z )  +  ( T `  z ) )  <->  ( U `  ( 2  x.  (
k  +  1 ) ) )  =  ( ( S `  (
k  +  1 ) )  +  ( T `
 ( k  +  1 ) ) ) ) )
208207imbi2d 308 . . . . . 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 ) ) ) ) ) )
209 oveq2 6028 . . . . . . . . 9  |-  ( z  =  ( |_ `  ( ( k  +  1 )  /  2
) )  ->  (
2  x.  z )  =  ( 2  x.  ( |_ `  (
( k  +  1 )  /  2 ) ) ) )
210209fveq2d 5672 . . . . . . . 8  |-  ( z  =  ( |_ `  ( ( k  +  1 )  /  2
) )  ->  ( U `  ( 2  x.  z ) )  =  ( U `  (
2  x.  ( |_
`  ( ( k  +  1 )  / 
2 ) ) ) ) )
211 fveq2 5668 . . . . . . . . 9  |-  ( z  =  ( |_ `  ( ( k  +  1 )  /  2
) )  ->  ( S `  z )  =  ( S `  ( |_ `  ( ( k  +  1 )  /  2 ) ) ) )
212 fveq2 5668 . . . . . . . . 9  |-  ( z  =  ( |_ `  ( ( k  +  1 )  /  2
) )  ->  ( T `  z )  =  ( T `  ( |_ `  ( ( k  +  1 )  /  2 ) ) ) )
213211, 212oveq12d 6038 . . . . . . . 8  |-  ( z  =  ( |_ `  ( ( k  +  1 )  /  2
) )  ->  (
( S `  z
)  +  ( T `
 z ) )  =  ( ( S `
 ( |_ `  ( ( k  +  1 )  /  2
) ) )  +  ( T `  ( |_ `  ( ( k  +  1 )  / 
2 ) ) ) ) )
214210, 213eqeq12d 2401 . . . . . . 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 ) ) ) ) ) )
215214imbi2d 308 . . . . . 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 ) ) ) ) ) ) )
21624fveq1i 5669 . . . . . . . 8  |-  ( U `
 ( 2  x.  1 ) )  =  (  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  H ) ) `  ( 2  x.  1 ) )
21723ovolfsval 19234 . . . . . . . . . . . 12  |-  ( ( H : NN --> (  <_  i^i  ( RR  X.  RR ) )  /\  1  e.  NN )  ->  (
( ( abs  o.  -  )  o.  H
) `  1 )  =  ( ( 2nd `  ( H `  1
) )  -  ( 1st `  ( H ` 
1 ) ) ) )
21822, 145, 217sylancl 644 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( abs 
o.  -  )  o.  H ) `  1
)  =  ( ( 2nd `  ( H `
 1 ) )  -  ( 1st `  ( H `  1 )
) ) )
219 halfnz 10280 . . . . . . . . . . . . . . . . . 18  |-  -.  (
1  /  2 )  e.  ZZ
220 nnz 10235 . . . . . . . . . . . . . . . . . . 19  |-  ( ( n  /  2 )  e.  NN  ->  (
n  /  2 )  e.  ZZ )
221 oveq1 6027 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  1  ->  (
n  /  2 )  =  ( 1  / 
2 ) )
222221eleq1d 2453 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  1  ->  (
( n  /  2
)  e.  ZZ  <->  ( 1  /  2 )  e.  ZZ ) )
223220, 222syl5ib 211 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  1  ->  (
( n  /  2
)  e.  NN  ->  ( 1  /  2 )  e.  ZZ ) )
224219, 223mtoi 171 . . . . . . . . . . . . . . . . 17  |-  ( n  =  1  ->  -.  ( n  /  2
)  e.  NN )
225 iffalse 3689 . . . . . . . . . . . . . . . . 17  |-  ( -.  ( n  /  2
)  e.  NN  ->  if ( ( n  / 
2 )  e.  NN ,  ( G `  ( n  /  2
) ) ,  ( F `  ( ( n  +  1 )  /  2 ) ) )  =  ( F `
 ( ( n  +  1 )  / 
2 ) ) )
226224, 225syl 16 . . . . . . . . . . . . . . . 16  |-  ( n  =  1  ->  if ( ( n  / 
2 )  e.  NN ,  ( G `  ( n  /  2
) ) ,  ( F `  ( ( n  +  1 )  /  2 ) ) )  =  ( F `
 ( ( n  +  1 )  / 
2 ) ) )
227 oveq1 6027 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  1  ->  (
n  +  1 )  =  ( 1  +  1 ) )
228 df-2 9990 . . . . . . . . . . . . . . . . . . . 20  |-  2  =  ( 1  +  1 )
229227, 228syl6eqr 2437 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  1  ->  (
n  +  1 )  =  2 )
230229oveq1d 6035 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  1  ->  (
( n  +  1 )  /  2 )  =  ( 2  / 
2 ) )
231 2cn 10002 . . . . . . . . . . . . . . . . . . 19  |-  2  e.  CC
232 2ne0 10015 . . . . . . . . . . . . . . . . . . 19  |-  2  =/=  0
233231, 232dividi 9679 . . . . . . . . . . . . . . . . . 18  |-  ( 2  /  2 )  =  1
234230, 233syl6eq 2435 . . . . . . . . . . . . . . . . 17  |-  ( n  =  1  ->  (
( n  +  1 )  /  2 )  =  1 )
235234fveq2d 5672 . . . . . . . . . . . . . . . 16  |-  ( n  =  1  ->  ( F `  ( (
n  +  1 )  /  2 ) )  =  ( F ` 
1 ) )
236226, 235eqtrd 2419 . . . . . . . . . . . . . . 15  |-  ( n  =  1  ->  if ( ( n  / 
2 )  e.  NN ,  ( G `  ( n  /  2
) ) ,  ( F `  ( ( n  +  1 )  /  2 ) ) )  =  ( F `
 1 ) )
237 fvex 5682 . . . . . . . . . . . . . . 15  |-  ( F `
 1 )  e. 
_V
238236, 21, 237fvmpt 5745 . . . . . . . . . . . . . 14  |-  ( 1  e.  NN  ->  ( H `  1 )  =  ( F ` 
1 ) )
239145, 238ax-mp 8 . . . . . . . . . . . . 13  |-  ( H `
 1 )  =  ( F `  1
)
240239fveq2i 5671 . . . . . . . . . . . 12  |-  ( 2nd `  ( H `  1
) )  =  ( 2nd `  ( F `
 1 ) )
241239fveq2i 5671 . . . . . . . . . . . 12  |-  ( 1st `  ( H `  1
) )  =  ( 1st `  ( F `
 1 ) )
242240, 241oveq12i 6032 . . . . . . . . . . 11  |-  ( ( 2nd `  ( H `
 1 ) )  -  ( 1st `  ( H `  1 )
) )  =  ( ( 2nd `  ( F `  1 )
)  -  ( 1st `  ( F `  1
) ) )
243218, 242syl6eq 2435 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( abs 
o.  -  )  o.  H ) `  1
)  =  ( ( 2nd `  ( F `
 1 ) )  -  ( 1st `  ( F `  1 )
) ) )
24459, 243seq1i 11264 . . . . . . . . 9  |-  ( ph  ->  (  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  H ) ) ` 
1 )  =  ( ( 2nd `  ( F `  1 )
)  -  ( 1st `  ( F `  1
) ) ) )
245231mulid1i 9025 . . . . . . . . . . 11  |-  ( 2  x.  1 )  =  2
246245fveq2i 5671 . . . . . . . . . 10  |-  ( ( ( abs  o.  -  )  o.  H ) `  ( 2  x.  1 ) )  =  ( ( ( abs  o.  -  )  o.  H
) `  2 )
24723ovolfsval 19234 . . . . . . . . . . . 12  |-  ( ( H : NN --> (  <_  i^i  ( RR  X.  RR ) )  /\  2  e.  NN )  ->  (
( ( abs  o.  -  )  o.  H
) `  2 )  =  ( ( 2nd `  ( H `  2
) )  -  ( 1st `  ( H ` 
2 ) ) ) )
24822, 34, 247sylancl 644 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( abs 
o.  -  )  o.  H ) `  2
)  =  ( ( 2nd `  ( H `
 2 ) )  -  ( 1st `  ( H `  2 )
) ) )
249 oveq1 6027 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  2  ->  (
n  /  2 )  =  ( 2  / 
2 ) )
250249, 233syl6eq 2435 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  2  ->  (
n  /  2 )  =  1 )
251250, 145syl6eqel 2475 . . . . . . . . . . . . . . . . 17  |-  ( n  =  2  ->  (
n  /  2 )  e.  NN )
252 iftrue 3688 . . . . . . . . . . . . . . . . 17  |-  ( ( n  /  2 )  e.  NN  ->  if ( ( n  / 
2 )  e.  NN ,  ( G `  ( n  /  2
) ) ,  ( F `  ( ( n  +  1 )  /  2 ) ) )  =  ( G `
 ( n  / 
2 ) ) )
253251, 252syl 16 . . . . . . . . . . . . . . . 16  |-  ( n  =  2  ->  if ( ( n  / 
2 )  e.  NN ,  ( G `  ( n  /  2
) ) ,  ( F `  ( ( n  +  1 )  /  2 ) ) )  =  ( G `
 ( n  / 
2 ) ) )
254250fveq2d 5672 . . . . . . . . . . . . . . . 16  |-  ( n  =  2  ->  ( G `  ( n  /  2 ) )  =  ( G ` 
1 ) )
255253, 254eqtrd 2419 . . . . . . . . . . . . . . 15  |-  ( n  =  2  ->  if ( ( n  / 
2 )  e.  NN ,  ( G `  ( n  /  2
) ) ,  ( F `  ( ( n  +  1 )  /  2 ) ) )  =  ( G `
 1 ) )
256 fvex 5682 . . . . . . . . . . . . . . 15  |-  ( G `
 1 )  e. 
_V
257255, 21, 256fvmpt 5745 . . . . . . . . . . . . . 14  |-  ( 2  e.  NN  ->  ( H `  2 )  =  ( G ` 
1 ) )
25834, 257ax-mp 8 . . . . . . . . . . . . 13  |-  ( H `
 2 )  =  ( G `  1
)
259258fveq2i 5671 . . . . . . . . . . . 12  |-  ( 2nd `  ( H `  2
) )  =  ( 2nd `  ( G `
 1 ) )
260258fveq2i 5671 . . . . . . . . . . . 12  |-  ( 1st `  ( H `  2
) )  =  ( 1st `  ( G `
 1 ) )
261259, 260oveq12i 6032 . . . . . . . . . . 11  |-  ( ( 2nd `  ( H `
 2 ) )  -  ( 1st `  ( H `  2 )
) )  =  ( ( 2nd `  ( G `  1 )
)  -  ( 1st `  ( G `  1
) ) )
262248, 261syl6eq 2435 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( abs 
o.  -  )  o.  H ) `  2
)  =  ( ( 2nd `  ( G `
 1 ) )  -  ( 1st `  ( G `  1 )
) ) )
263246, 262syl5eq 2431 . . . . . . . . 9  |-  ( ph  ->  ( ( ( abs 
o.  -  )  o.  H ) `  (
2  x.  1 ) )  =  ( ( 2nd `  ( G `
 1 ) )  -  ( 1st `  ( G `  1 )
) ) )
26479, 145, 41, 244, 263seqp1i 11266 . . . . . . . 8  |-  ( ph  ->  (  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  H ) ) `  ( 2  x.  1 ) )  =  ( ( ( 2nd `  ( F `  1 )
)  -  ( 1st `  ( F `  1
) ) )  +  ( ( 2nd `  ( G `  1 )
)  -  ( 1st `  ( G `  1
) ) ) ) )
265216, 264syl5eq 2431 . . . . . . 7  |-  ( ph  ->  ( U `  (
2  x.  1 ) )  =  ( ( ( 2nd `  ( F `  1 )
)  -  ( 1st `  ( F `  1
) ) )  +  ( ( 2nd `  ( G `  1 )
)  -  ( 1st `  ( G `  1
) ) ) ) )
266109fveq1i 5669 . . . . . . . . 9  |-  ( S `
 1 )  =  (  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  F ) ) ` 
1 )
267108ovolfsval 19234 . . . . . . . . . . 11  |-  ( ( F : NN --> (  <_  i^i  ( RR  X.  RR ) )  /\  1  e.  NN )  ->  (
( ( abs  o.  -  )  o.  F
) `  1 )  =  ( ( 2nd `  ( F `  1
) )  -  ( 1st `  ( F ` 
1 ) ) ) )
26816, 145, 267sylancl 644 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( abs 
o.  -  )  o.  F ) `  1
)  =  ( ( 2nd `  ( F `
 1 ) )  -  ( 1st `  ( F `  1 )
) ) )
26959, 268seq1i 11264 . . . . . . . . 9  |-  ( ph  ->  (  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  F ) ) ` 
1 )  =  ( ( 2nd `  ( F `  1 )
)  -  ( 1st `  ( F `  1
) ) ) )
270266, 269syl5eq 2431 . . . . . . . 8  |-  ( ph  ->  ( S `  1
)  =  ( ( 2nd `  ( F `
 1 ) )  -  ( 1st `  ( F `  1 )
) ) )
271123fveq1i 5669 . . . . . . . . 9  |-  ( T `
 1 )  =  (  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  G ) ) ` 
1 )
272122ovolfsval 19234 . . . . . . . . . . 11  |-  ( ( G : NN --> (  <_  i^i  ( RR  X.  RR ) )  /\  1  e.  NN )  ->  (
( ( abs  o.  -  )  o.  G
) `  1 )  =  ( ( 2nd `  ( G `  1
) )  -  ( 1st `  ( G ` 
1 ) ) ) )
2737, 145, 272sylancl 644 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( abs 
o.  -  )  o.  G ) `  1
)  =  ( ( 2nd `  ( G `
 1 ) )  -  ( 1st `  ( G `  1 )
) ) )
27459, 273seq1i 11264 . . . . . . . . 9  |-  ( ph  ->  (  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  G ) ) ` 
1 )  =  ( ( 2nd `  ( G `  1 )
)  -  ( 1st `  ( G `  1
) ) ) )
275271, 274syl5eq 2431 . . . . . . . 8  |-  ( ph  ->  ( T `  1
)  =  ( ( 2nd `  ( G `
 1 ) )  -  ( 1st `  ( G `  1 )
) ) )
276270, 275oveq12d 6038 . . . . . . 7  |-  ( ph  ->  ( ( S ` 
1 )  +  ( T `  1 ) )  =  ( ( ( 2nd `  ( F `  1 )
)  -  ( 1st `  ( F `  1
) ) )  +  ( ( 2nd `  ( G `  1 )
)  -  ( 1st `  ( G `  1
) ) ) ) )
277265, 276eqtr4d 2422 . . . . . 6  |-  ( ph  ->  ( U `  (
2  x.  1 ) )  =  ( ( S `  1 )  +  ( T ` 
1 ) ) )
278 oveq1 6027 . . . . . . . . 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 ) ) ) ) )
27941oveq2i 6031 . . . . . . . . . . . . 13  |-  ( ( 2  x.  k )  +  ( 2  x.  1 ) )  =  ( ( 2  x.  k )  +  ( 1  +  1 ) )
280231a1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN )  ->  2  e.  CC )
28145recnd 9047 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  CC )
28240a1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN )  ->  1  e.  CC )
283280, 281, 282adddid 9045 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN )  ->  ( 2  x.  ( k  +  1 ) )  =  ( ( 2  x.  k )  +  ( 2  x.  1 ) ) )
284 nnmulcl 9955 . . . . . . . . . . . . . . . . 17  |-  ( ( 2  e.  NN  /\  k  e.  NN )  ->  ( 2  x.  k
)  e.  NN )
28534, 284mpan 652 . . . . . . . . . . . . . . . 16  |-  ( k  e.  NN  ->  (
2  x.  k )  e.  NN )
286285adantl 453 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  NN )  ->  ( 2  x.  k )  e.  NN )
287286nncnd 9948 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN )  ->  ( 2  x.  k )  e.  CC )
288287, 282, 282addassd 9043 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( ( 2  x.  k
)  +  1 )  +  1 )  =  ( ( 2  x.  k )  +  ( 1  +  1 ) ) )
289279, 283, 2883eqtr4a 2445 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN )  ->  ( 2  x.  ( k  +  1 ) )  =  ( ( ( 2  x.  k )  +  1 )  +  1 ) )
290289fveq2d 5672 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN )  ->  ( U `
 ( 2  x.  ( k  +  1 ) ) )  =  ( U `  (
( ( 2  x.  k )  +  1 )  +  1 ) ) )
29124fveq1i 5669 . . . . . . . . . . . 12  |-  ( U `
 ( ( ( 2  x.  k )  +  1 )  +  1 ) )  =  (  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  H ) ) `  ( ( ( 2  x.  k )  +  1 )  +  1 ) )
292286peano2nnd 9949 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( 2  x.  k )  +  1 )  e.  NN )
293292, 79syl6eleq 2477 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( 2  x.  k )  +  1 )  e.  ( ZZ>= `  1 )
)
294 seqp1 11265 . . . . . . . . . . . . . 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 ) ) ) )
295293, 294syl 16 . . . . . . . . . . . . 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 ) ) ) )
296286, 79syl6eleq 2477 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  NN )  ->  ( 2  x.  k )  e.  ( ZZ>= `  1 )
)
297 seqp1 11265 . . . . . . . . . . . . . . . 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 ) ) ) )
298296, 297syl 16 . . . . . . . . . . . . . . 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 ) ) ) )
29924fveq1i 5669 . . . . . . . . . . . . . . . . 17  |-  ( U `
 ( 2  x.  k ) )  =  (  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  H ) ) `  ( 2  x.  k
) )
300299a1i 11 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  NN )  ->  ( U `
 ( 2  x.  k ) )  =  (  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  H ) ) `  ( 2  x.  k
) ) )
301 oveq1 6027 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  =  ( ( 2  x.  k )  +  1 )  ->  (
n  /  2 )  =  ( ( ( 2  x.  k )  +  1 )  / 
2 ) )
302301eleq1d 2453 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  =  ( ( 2  x.  k )  +  1 )  ->  (
( n  /  2
)  e.  NN  <->  ( (
( 2  x.  k
)  +  1 )  /  2 )  e.  NN ) )
303301fveq2d 5672 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  =  ( ( 2  x.  k )  +  1 )  ->  ( G `  ( n  /  2 ) )  =  ( G `  ( ( ( 2  x.  k )  +  1 )  /  2
) ) )
304 oveq1 6027 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( n  =  ( ( 2  x.  k )  +  1 )  ->  (
n  +  1 )  =  ( ( ( 2  x.  k )  +  1 )  +  1 ) )
305304oveq1d 6035 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  =  ( ( 2  x.  k )  +  1 )  ->  (
( n  +  1 )  /  2 )  =  ( ( ( ( 2  x.  k
)  +  1 )  +  1 )  / 
2 ) )
306305fveq2d 5672 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  =  ( ( 2  x.  k )  +  1 )  ->  ( F `  ( (
n  +  1 )  /  2 ) )  =  ( F `  ( ( ( ( 2  x.  k )  +  1 )  +  1 )  /  2
) ) )
307302, 303, 306ifbieq12d 3704 . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
308 fvex 5682 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( G `
 ( ( ( 2  x.  k )  +  1 )  / 
2 ) )  e. 
_V
309 fvex 5682 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( F `
 ( ( ( ( 2  x.  k
)  +  1 )  +  1 )  / 
2 ) )  e. 
_V
310308, 309ifex 3740 . . . . . . . . . . . . . . . . . . . . . 22  |-  if ( ( ( ( 2  x.  k )  +  1 )  /  2
)  e.  NN , 
( G `  (
( ( 2  x.  k )  +  1 )  /  2 ) ) ,  ( F `
 ( ( ( ( 2  x.  k
)  +  1 )  +  1 )  / 
2 ) ) )  e.  _V
311307, 21, 310fvmpt 5745 . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
312292, 311syl 16 . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
313232a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  k  e.  NN )  ->  2  =/=  0 )
314281, 280, 313divcan3d 9727 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( 2  x.  k )  /  2 )  =  k )
315314, 78eqeltrd 2461 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( 2  x.  k )  /  2 )  e.  NN )
316 nneo 10285 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 2  x.  k )  e.  NN  ->  (
( ( 2  x.  k )  /  2
)  e.  NN  <->  -.  (
( ( 2  x.  k )  +  1 )  /  2 )  e.  NN ) )
317286, 316syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( ( 2  x.  k
)  /  2 )  e.  NN  <->  -.  (
( ( 2  x.  k )  +  1 )  /  2 )  e.  NN ) )
318315, 317mpbid 202 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  k  e.  NN )  ->  -.  (
( ( 2  x.  k )  +  1 )  /  2 )  e.  NN )
319 iffalse 3689 . . . . . . . . . . . . . . . . . . . . 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 ) ) )
320318, 319syl 16 . . . . . . . . . . . . . . . . . . . 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
) ) )
321289oveq1d 6035 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( 2  x.  ( k  +  1 ) )  /  2 )  =  ( ( ( ( 2  x.  k )  +  1 )  +  1 )  /  2
) )
32236nncnd 9948 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  k  e.  NN )  ->  ( k  +  1 )  e.  CC )
323 divcan3 9634 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( k  +  1 )  e.  CC  /\  2  e.  CC  /\  2  =/=  0 )  ->  (
( 2  x.  (
k  +  1 ) )  /  2 )  =  ( k  +  1 ) )
324231, 232, 323mp3an23 1271 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( k  +  1 )  e.  CC  ->  (
( 2  x.  (
k  +  1 ) )  /  2 )  =  ( k  +  1 ) )
325322, 324syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( 2  x.  ( k  +  1 ) )  /  2 )  =  ( k  +  1 ) )
326321, 325eqtr3d 2421 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( ( ( 2  x.  k )  +  1 )  +  1 )  /  2 )  =  ( k  +  1 ) )
327326fveq2d 5672 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  k  e.  NN )  ->  ( F `
 ( ( ( ( 2  x.  k
)  +  1 )  +  1 )  / 
2 ) )  =  ( F `  (
k  +  1 ) ) )
328312, 320, 3273eqtrd 2423 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  k  e.  NN )  ->  ( H `
 ( ( 2  x.  k )  +  1 ) )  =  ( F `  (
k  +  1 ) ) )
329328fveq2d 5672 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  NN )  ->  ( 2nd `  ( H `  (
( 2  x.  k
)  +  1 ) ) )  =  ( 2nd `  ( F `
 ( k  +  1 ) ) ) )
330328fveq2d 5672 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  NN )  ->  ( 1st `  ( H `  (
( 2  x.  k
)  +  1 ) ) )  =  ( 1st `  ( F `
 ( k  +  1 ) ) ) )
331329, 330oveq12d 6038 . . . . . . . . . . . . . . . . 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 ) ) ) ) )
33222adantr 452 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  NN )  ->  H : NN
--> (  <_  i^i  ( RR  X.  RR ) ) )
33323ovolfsval 19234 . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
334332, 292, 333syl2anc 643 . . . . . . . . . . . . . . . . 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 ) ) ) ) )
335108ovolfsval 19234 . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
33616, 35, 335syl2an 464 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  F ) `  ( k  +  1 ) )  =  ( ( 2nd `  ( F `  ( k  +  1 ) ) )  -  ( 1st `  ( F `  (
k  +  1 ) ) ) ) )
337331, 334, 3363eqtr4rd 2430 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  F ) `  ( k  +  1 ) )  =  ( ( ( abs  o.  -  )  o.  H
) `  ( (
2  x.  k )  +  1 ) ) )
338300, 337oveq12d 6038 . . . . . . . . . . . . . . 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 ) ) ) )
339298, 338eqtr4d 2422 . . . . . . . . . . . . . 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 ) ) ) )
340289fveq2d 5672 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  NN )  ->  ( H `
 ( 2  x.  ( k  +  1 ) ) )  =  ( H `  (
( ( 2  x.  k )  +  1 )  +  1 ) ) )
341292peano2nnd 9949 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( ( 2  x.  k
)  +  1 )  +  1 )  e.  NN )
342289, 341eqeltrd 2461 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  k  e.  NN )  ->  ( 2  x.  ( k  +  1 ) )  e.  NN )
343 oveq1 6027 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  =  ( 2  x.  ( k  +  1 ) )  ->  (
n  /  2 )  =  ( ( 2  x.  ( k  +  1 ) )  / 
2 ) )
344343eleq1d 2453 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  =  ( 2  x.  ( k  +  1 ) )  ->  (
( n  /  2
)  e.  NN  <->  ( (
2  x.  ( k  +  1 ) )  /  2 )  e.  NN ) )
345343fveq2d 5672 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  =  ( 2  x.  ( k  +  1 ) )  ->  ( G `  ( n  /  2 ) )  =  ( G `  ( ( 2  x.  ( k  +  1 ) )  /  2
) ) )
346 oveq1 6027 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  =  ( 2  x.  ( k  +  1 ) )  ->  (
n  +  1 )  =  ( ( 2  x.  ( k  +  1 ) )  +  1 ) )
347346oveq1d 6035 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  =  ( 2  x.  ( k  +  1 ) )  ->  (
( n  +  1 )  /  2 )  =  ( ( ( 2  x.  ( k  +  1 ) )  +  1 )  / 
2 ) )
348347fveq2d 5672 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  =  ( 2  x.  ( k  +  1 ) )  ->  ( F `  ( (
n  +  1 )  /  2 ) )  =  ( F `  ( ( ( 2  x.  ( k  +  1 ) )  +  1 )  /  2
) ) )
349344, 345, 348ifbieq12d 3704 . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
350 fvex 5682 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( G `
 ( ( 2  x.  ( k  +  1 ) )  / 
2 ) )  e. 
_V
351 fvex 5682 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( F `
 ( ( ( 2  x.  ( k  +  1 ) )  +  1 )  / 
2 ) )  e. 
_V
352350, 351ifex 3740 . . . . . . . . . . . . . . . . . . . . 21  |-  if ( ( ( 2  x.  ( k  +  1 ) )  /  2
)  e.  NN , 
( G `  (
( 2  x.  (
k  +  1 ) )  /  2 ) ) ,  ( F `
 ( ( ( 2  x.  ( k  +  1 ) )  +  1 )  / 
2 ) ) )  e.  _V
353349, 21, 352fvmpt 5745 . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
354342, 353syl 16 . . . . . . . . . . . . . . . . . . 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 ) ) ) )
355325, 36eqeltrd 2461 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( 2  x.  ( k  +  1 ) )  /  2 )  e.  NN )
356 iftrue 3688 . . . . . . . . . . . . . . . . . . . 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 ) ) )
357355, 356syl 16 . . . . . . . . . . . . . . . . . . 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
) ) )
358325fveq2d 5672 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  k  e.  NN )  ->  ( G `
 ( ( 2  x.  ( k  +  1 ) )  / 
2 ) )  =  ( G `  (
k  +  1 ) ) )
359354, 357, 3583eqtrd 2423 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  NN )  ->  ( H `
 ( 2  x.  ( k  +  1 ) ) )  =  ( G `  (
k  +  1 ) ) )
360340, 359eqtr3d 2421 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  NN )  ->  ( H `
 ( ( ( 2  x.  k )  +  1 )  +  1 ) )  =  ( G `  (
k  +  1 ) ) )
361360fveq2d 5672 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  NN )  ->  ( 2nd `  ( H `  (
( ( 2  x.  k )  +  1 )  +  1 ) ) )  =  ( 2nd `  ( G `
 ( k  +  1 ) ) ) )
362360fveq2d 5672 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  NN )  ->  ( 1st `  ( H `  (
( ( 2  x.  k )  +  1 )  +  1 ) ) )  =  ( 1st `  ( G `
 ( k  +  1 ) ) ) )
363361, 362oveq12d 6038 . . . . . . . . . . . . . . 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 ) ) ) ) )
36423ovolfsval 19234 . . . . . . . . . . . . . . . 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 ) ) ) ) )
365332, 341, 364syl2anc 643 . . . . . . . . . . . . . . 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 ) ) ) ) )
366122ovolfsval 19234 . . . . . . . . . . . . . . . 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 ) ) ) ) )
3677, 35, 366syl2an 464 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  G ) `  ( k  +  1 ) )  =  ( ( 2nd `  ( G `  ( k  +  1 ) ) )  -  ( 1st `  ( G `  (
k  +  1 ) ) ) ) )
368363, 365, 3673eqtr4d 2429 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  H ) `  ( ( ( 2  x.  k )  +  1 )  +  1 ) )  =  ( ( ( abs  o.  -  )  o.  G
) `  ( k  +  1 ) ) )
369339, 368oveq12d 6038 . . . . . . . . . . . . 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 ) ) ) )
370295, 369eqtrd 2419 . . . . . . . . . . . 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 ) ) ) )
371291, 370syl5eq 2431 . . . . . . . . . . 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 ) ) ) )
372 ffvelrn 5807 . . . . . . . . . . . . . . 15  |-  ( ( U : NN --> ( 0 [,)  +oo )  /\  (
2  x.  k )  e.  NN )  -> 
( U `  (
2  x.  k ) )  e.  ( 0 [,)  +oo ) )
37326, 285, 372syl2an 464 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN )  ->  ( U `
 ( 2  x.  k ) )  e.  ( 0 [,)  +oo ) )
37430, 373sseldi 3289 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN )  ->  ( U `
 ( 2  x.  k ) )  e.  RR )
375374recnd 9047 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN )  ->  ( U `
 ( 2  x.  k ) )  e.  CC )
376108ovolfsf 19235 . . . . . . . . . . . . . . . 16  |-  ( F : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  (
( abs  o.  -  )  o.  F ) : NN --> ( 0 [,)  +oo ) )
37716, 376syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( abs  o.  -  )  o.  F
) : NN --> ( 0 [,)  +oo ) )
378 ffvelrn 5807 . . . . . . . . . . . . . . 15  |-  ( ( ( ( abs  o.  -  )  o.  F
) : NN --> ( 0 [,)  +oo )  /\  (
k  +  1 )  e.  NN )  -> 
( ( ( abs 
o.  -  )  o.  F ) `  (
k  +  1 ) )  e.  ( 0 [,)  +oo ) )
379377, 35, 378syl2an 464 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  F ) `  ( k  +  1 ) )  e.  ( 0 [,)  +oo )
)
38030, 379sseldi 3289 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  F ) `  ( k  +  1 ) )  e.  RR )
381380recnd 9047 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  F ) `  ( k  +  1 ) )  e.  CC )
382122ovolfsf 19235 . . . . . . . . . . . . . . . 16  |-  ( G : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  (
( abs  o.  -  )  o.  G ) : NN --> ( 0 [,)  +oo ) )
3837, 382syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( abs  o.  -  )  o.  G
) : NN --> ( 0 [,)  +oo ) )
384 ffvelrn 5807 . . . . . . . . . . . . . . 15  |-  ( ( ( ( abs  o.  -  )  o.  G
) : NN --> ( 0 [,)  +oo )  /\  (
k  +  1 )  e.  NN )  -> 
( ( ( abs 
o.  -  )  o.  G ) `  (
k  +  1 ) )  e.  ( 0 [,)  +oo ) )
385383, 35, 384syl2an 464 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  G ) `  ( k  +  1 ) )  e.  ( 0 [,)  +oo )
)
38630, 385sseldi 3289 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  G ) `  ( k  +  1 ) )  e.  RR )
387386recnd 9047 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  G ) `  ( k  +  1 ) )  e.  CC )
388375, 381, 387addassd 9043 . . . . . . . . . . 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 ) ) ) ) )
389290, 371, 3883eqtrd 2423 . . . . . . . . . 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 ) ) ) ) )
390 seqp1 11265 . . . . . . . . . . . . . 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 ) ) ) )
39180, 390syl 16 . . . . . . . . . . . . 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 ) ) ) )
392109fveq1i 5669 . . . . . . . . . . . . 13  |-  ( S `
 ( k  +  1 ) )  =  (  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  F ) ) `  ( k  +  1 ) )
393109fveq1i 5669 . . . . . . . . . . . . . 14  |-  ( S `
 k )  =  (  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  F ) ) `  k )
394393oveq1i 6030 . . . . . . . . . . . . 13  |-  ( ( S `  k )  +  ( ( ( abs  o.  -  )  o.  F ) `  (
k  +  1 ) ) )  =  ( (  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  F ) ) `  k )  +  ( ( ( abs  o.  -  )  o.  F
) `  ( k  +  1 ) ) )
395391, 392, 3943eqtr4g 2444 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN )  ->  ( S `
 ( k  +  1 ) )  =  ( ( S `  k )  +  ( ( ( abs  o.  -  )  o.  F
) `  ( k  +  1 ) ) ) )
396 seqp1 11265 . . . . . . . . . . . . . 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 ) ) ) )
39780, 396syl 16 . . . . . . . . . . . . 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 ) ) ) )
398123fveq1i 5669 . . . . . . . . . . . . 13  |-  ( T `
 ( k  +  1 ) )  =  (  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  G ) ) `  ( k  +  1 ) )
399123fveq1i 5669 . . . . . . . . . . . . . 14  |-  ( T `
 k )  =  (  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  G ) ) `  k )
400399oveq1i 6030 . . . . . . . . . . . . 13  |-  ( ( T `  k )  +  ( ( ( abs  o.  -  )  o.  G ) `  (
k  +  1 ) ) )  =  ( (  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  G ) ) `  k )  +  ( ( ( abs  o.  -  )  o.  G
) `  ( k  +  1 ) ) )
401397, 398, 4003eqtr4g 2444 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN )  ->  ( T `
 ( k  +  1 ) )  =  ( ( T `  k )  +  ( ( ( abs  o.  -  )  o.  G
) `  ( k  +  1 ) ) ) )
402395, 401oveq12d 6038 . . . . . . . . . . 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 ) ) ) ) )
403111ffvelrnda 5809 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN )  ->  ( S `
 k )  e.  ( 0 [,)  +oo ) )
40430, 403sseldi 3289 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN )  ->  ( S `
 k )  e.  RR )
405404recnd 9047 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN )  ->  ( S `
 k )  e.  CC )
406125ffvelrnda 5809 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN )  ->  ( T `
 k )  e.  ( 0 [,)  +oo ) )
40730, 406sseldi 3289 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN )  ->  ( T `
 k )  e.  RR )
408407recnd 9047 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN )  ->  ( T `
 k )  e.  CC )
409405, 381, 408, 387add4d 9221 . . . . . . . . . . 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 ) ) ) ) )
410402, 409eqtrd 2419 . . . . . . . . . 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 ) ) ) ) )
411389, 410eqeq12d 2401 . . . . . . . . 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 ) ) ) ) ) )
412278, 411syl5ibr 213 . . . . . . . 8  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( U `  ( 2  x.  k ) )  =  ( ( S `
 k )  +  ( T `  k
) )  ->  ( U `  ( 2  x.  ( k  +  1 ) ) )  =  ( ( S `  ( k  +  1 ) )  +  ( T `  ( k  +  1 ) ) ) ) )
413412expcom 425 . . . . . . 7  |-  ( k  e.  NN  ->  ( ph  ->  ( ( U `
 ( 2  x.  k ) )  =  ( ( S `  k )  +  ( T `  k ) )  ->  ( U `  ( 2  x.  (
k  +  1 ) ) )  =  ( ( S `  (
k  +  1 ) )  +  ( T `
 ( k  +  1 ) ) ) ) ) )
414413a2d 24 . . . . . 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 ) ) ) ) ) )
415194, 201, 208, 215, 277, 414nnind 9950 . . . . 5  |-  ( ( |_ `  ( ( k  +  1 )  /  2 ) )  e.  NN  ->  ( ph  ->  ( U `  ( 2  x.  ( |_ `  ( ( k  +  1 )  / 
2 ) ) ) )  =  ( ( S `  ( |_
`  ( ( k  +  1 )  / 
2 ) ) )  +  ( T `  ( |_ `  ( ( k  +  1 )  /  2 ) ) ) ) ) )
416415impcom 420 . . . 4  |-  ( (
ph  /\  ( |_ `  ( ( k  +  1 )  /  2
) )  e.  NN )  ->  ( U `  ( 2  x.  ( |_ `  ( ( k  +  1 )  / 
2 ) ) ) )  =  ( ( S `  ( |_
`  ( ( k  +  1 )  / 
2 ) ) )  +  ( T `  ( |_ `  ( ( k  +  1 )  /  2 ) ) ) ) )
41764, 416syldan 457 . . 3  |-  ( (
ph  /\  k  e.  NN )  ->  ( U `
 ( 2  x.  ( |_ `  (
( k  +  1 )  /  2 ) ) ) )  =  ( ( S `  ( |_ `  ( ( k  +  1 )  /  2 ) ) )  +  ( T `
 ( |_ `  ( ( k  +  1 )  /  2
) ) ) ) )
41870adantr 452 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  ( vol
* `  A )  e.  RR )
419418recnd 9047 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  ( vol
* `  A )  e.  CC )
42075adantr 452 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN )  ->  C  e.  RR )
421420rehalfcld 10146 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  ( C  /  2 )  e.  RR )
422421recnd 9047 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  ( C  /  2 )  e.  CC )
42372adantr 452 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  ( vol
* `  B )  e.  RR )
424423recnd 9047 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  ( vol
* `  B )  e.  CC )
425419, 422, 424, 422add4d 9221 . . . 4  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( ( vol * `  A )  +  ( C  /  2 ) )  +  ( ( vol * `  B
)  +  ( C  /  2 ) ) )  =  ( ( ( vol * `  A )  +  ( vol * `  B
) )  +  ( ( C  /  2
)  +  ( C  /  2 ) ) ) )
426420recnd 9047 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  C  e.  CC )
4274262halvesd 10145 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( C  /  2 )  +  ( C  / 
2 ) )  =  C )
428427oveq2d 6036 . . . 4  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( ( vol * `  A )  +  ( vol * `  B
) )  +  ( ( C  /  2
)  +  ( C  /  2 ) ) )  =  ( ( ( vol * `  A )  +  ( vol * `  B
) )  +  C
) )
429425, 428eqtr2d 2420 . . 3  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( ( vol * `  A )  +  ( vol * `  B
) )  +  C
)  =  ( ( ( vol * `  A )  +  ( C  /  2 ) )  +  ( ( vol * `  B
)  +  ( C  /  2 )