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

Theorem ovolicc2lem4OLD 22473
Description: Lemma for ovolicc2 22476. (Contributed by Mario Carneiro, 14-Jun-2014.) Obsolete version of ovolicc2lem4 22474 as of 17-Sep-2020. (New usage is discouraged.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
ovolicc.1  |-  ( ph  ->  A  e.  RR )
ovolicc.2  |-  ( ph  ->  B  e.  RR )
ovolicc.3  |-  ( ph  ->  A  <_  B )
ovolicc2.4  |-  S  =  seq 1 (  +  ,  ( ( abs 
o.  -  )  o.  F ) )
ovolicc2.5  |-  ( ph  ->  F : NN --> (  <_  i^i  ( RR  X.  RR ) ) )
ovolicc2.6  |-  ( ph  ->  U  e.  ( ~P
ran  ( (,)  o.  F )  i^i  Fin ) )
ovolicc2.7  |-  ( ph  ->  ( A [,] B
)  C_  U. U )
ovolicc2.8  |-  ( ph  ->  G : U --> NN )
ovolicc2.9  |-  ( (
ph  /\  t  e.  U )  ->  (
( (,)  o.  F
) `  ( G `  t ) )  =  t )
ovolicc2.10  |-  T  =  { u  e.  U  |  ( u  i^i  ( A [,] B
) )  =/=  (/) }
ovolicc2.11  |-  ( ph  ->  H : T --> T )
ovolicc2.12  |-  ( (
ph  /\  t  e.  T )  ->  if ( ( 2nd `  ( F `  ( G `  t ) ) )  <_  B ,  ( 2nd `  ( F `
 ( G `  t ) ) ) ,  B )  e.  ( H `  t
) )
ovolicc2.13  |-  ( ph  ->  A  e.  C )
ovolicc2.14  |-  ( ph  ->  C  e.  T )
ovolicc2.15  |-  K  =  seq 1 ( ( H  o.  1st ) ,  ( NN  X.  { C } ) )
ovolicc2.16  |-  W  =  { n  e.  NN  |  B  e.  ( K `  n ) }
ovolicc2lem4OLD.17  |-  M  =  sup ( W ,  RR ,  `'  <  )
Assertion
Ref Expression
ovolicc2lem4OLD  |-  ( ph  ->  ( B  -  A
)  <_  sup ( ran  S ,  RR* ,  <  ) )
Distinct variable groups:    t, n, u, A    B, n, t, u    t, H    C, n, t    n, F, t   
n, K, t, u   
n, G, t    n, M, t    n, W    ph, n, t    T, n, t    U, n, t, u
Allowed substitution hints:    ph( u)    C( u)    S( u, t, n)    T( u)    F( u)    G( u)    H( u, n)    M( u)    W( u, t)

Proof of Theorem ovolicc2lem4OLD
Dummy variables  m  x  y  z  i 
j are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 arch 10866 . . . . 5  |-  ( x  e.  RR  ->  E. z  e.  NN  x  <  z
)
21ad2antlr 733 . . . 4  |-  ( ( ( ph  /\  x  e.  RR )  /\  A. y  e.  ( ( G  o.  K ) " ( 1 ... M ) ) y  <_  x )  ->  E. z  e.  NN  x  <  z )
3 df-ima 4847 . . . . . . . . . . . . . . . 16  |-  ( ( G  o.  K )
" ( 1 ... M ) )  =  ran  ( ( G  o.  K )  |`  ( 1 ... M
) )
4 ovolicc2.8 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  G : U --> NN )
5 nnuz 11194 . . . . . . . . . . . . . . . . . . . . 21  |-  NN  =  ( ZZ>= `  1 )
6 ovolicc2.15 . . . . . . . . . . . . . . . . . . . . 21  |-  K  =  seq 1 ( ( H  o.  1st ) ,  ( NN  X.  { C } ) )
7 1zzd 10968 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  1  e.  ZZ )
8 ovolicc2.14 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  C  e.  T )
9 ovolicc2.11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  H : T --> T )
105, 6, 7, 8, 9algrf 14532 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  K : NN --> T )
11 ovolicc2.10 . . . . . . . . . . . . . . . . . . . . 21  |-  T  =  { u  e.  U  |  ( u  i^i  ( A [,] B
) )  =/=  (/) }
12 ssrab2 3514 . . . . . . . . . . . . . . . . . . . . 21  |-  { u  e.  U  |  (
u  i^i  ( A [,] B ) )  =/=  (/) }  C_  U
1311, 12eqsstri 3462 . . . . . . . . . . . . . . . . . . . 20  |-  T  C_  U
14 fss 5737 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( K : NN --> T  /\  T  C_  U )  ->  K : NN --> U )
1510, 13, 14sylancl 668 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  K : NN --> U )
16 fco 5739 . . . . . . . . . . . . . . . . . . 19  |-  ( ( G : U --> NN  /\  K : NN --> U )  ->  ( G  o.  K ) : NN --> NN )
174, 15, 16syl2anc 667 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( G  o.  K
) : NN --> NN )
18 elfznn 11828 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  ( 1 ... M )  ->  i  e.  NN )
1918ssriv 3436 . . . . . . . . . . . . . . . . . 18  |-  ( 1 ... M )  C_  NN
20 fssres 5749 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( G  o.  K
) : NN --> NN  /\  ( 1 ... M
)  C_  NN )  ->  ( ( G  o.  K )  |`  (
1 ... M ) ) : ( 1 ... M ) --> NN )
2117, 19, 20sylancl 668 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( G  o.  K )  |`  (
1 ... M ) ) : ( 1 ... M ) --> NN )
22 frn 5735 . . . . . . . . . . . . . . . . 17  |-  ( ( ( G  o.  K
)  |`  ( 1 ... M ) ) : ( 1 ... M
) --> NN  ->  ran  ( ( G  o.  K )  |`  (
1 ... M ) ) 
C_  NN )
2321, 22syl 17 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ran  ( ( G  o.  K )  |`  ( 1 ... M
) )  C_  NN )
243, 23syl5eqss 3476 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( G  o.  K ) " (
1 ... M ) ) 
C_  NN )
25 nnssre 10613 . . . . . . . . . . . . . . 15  |-  NN  C_  RR
2624, 25syl6ss 3444 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( G  o.  K ) " (
1 ... M ) ) 
C_  RR )
2726ad3antrrr 736 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K
) " ( 1 ... M ) ) )  ->  ( ( G  o.  K ) " ( 1 ... M ) )  C_  RR )
28 simpr 463 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K
) " ( 1 ... M ) ) )  ->  y  e.  ( ( G  o.  K ) " (
1 ... M ) ) )
2927, 28sseldd 3433 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K
) " ( 1 ... M ) ) )  ->  y  e.  RR )
30 simpllr 769 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K
) " ( 1 ... M ) ) )  ->  x  e.  RR )
31 nnre 10616 . . . . . . . . . . . . 13  |-  ( z  e.  NN  ->  z  e.  RR )
3231ad2antlr 733 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K
) " ( 1 ... M ) ) )  ->  z  e.  RR )
33 lelttr 9724 . . . . . . . . . . . 12  |-  ( ( y  e.  RR  /\  x  e.  RR  /\  z  e.  RR )  ->  (
( y  <_  x  /\  x  <  z )  ->  y  <  z
) )
3429, 30, 32, 33syl3anc 1268 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K
) " ( 1 ... M ) ) )  ->  ( (
y  <_  x  /\  x  <  z )  -> 
y  <  z )
)
3534ancomsd 456 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K
) " ( 1 ... M ) ) )  ->  ( (
x  <  z  /\  y  <_  x )  -> 
y  <  z )
)
3635expdimp 439 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  x  e.  RR )  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K
) " ( 1 ... M ) ) )  /\  x  < 
z )  ->  (
y  <_  x  ->  y  <  z ) )
3736an32s 813 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  x  e.  RR )  /\  z  e.  NN )  /\  x  <  z
)  /\  y  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  ( y  <_  x  ->  y  <  z ) )
3837ralimdva 2796 . . . . . . 7  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  z  e.  NN )  /\  x  <  z
)  ->  ( A. y  e.  ( ( G  o.  K ) " ( 1 ... M ) ) y  <_  x  ->  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )
3938impancom 442 . . . . . 6  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  z  e.  NN )  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <_  x )  ->  ( x  <  z  ->  A. y  e.  ( ( G  o.  K
) " ( 1 ... M ) ) y  <  z ) )
4039an32s 813 . . . . 5  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  A. y  e.  ( ( G  o.  K
) " ( 1 ... M ) ) y  <_  x )  /\  z  e.  NN )  ->  ( x  < 
z  ->  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )
4140reximdva 2862 . . . 4  |-  ( ( ( ph  /\  x  e.  RR )  /\  A. y  e.  ( ( G  o.  K ) " ( 1 ... M ) ) y  <_  x )  -> 
( E. z  e.  NN  x  <  z  ->  E. z  e.  NN  A. y  e.  ( ( G  o.  K )
" ( 1 ... M ) ) y  <  z ) )
422, 41mpd 15 . . 3  |-  ( ( ( ph  /\  x  e.  RR )  /\  A. y  e.  ( ( G  o.  K ) " ( 1 ... M ) ) y  <_  x )  ->  E. z  e.  NN  A. y  e.  ( ( G  o.  K )
" ( 1 ... M ) ) y  <  z )
43 fzfid 12186 . . . . 5  |-  ( ph  ->  ( 1 ... M
)  e.  Fin )
44 fvres 5879 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( 1 ... M )  ->  (
( ( G  o.  K )  |`  (
1 ... M ) ) `
 i )  =  ( ( G  o.  K ) `  i
) )
4544adantl 468 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( ( G  o.  K )  |`  (
1 ... M ) ) `
 i )  =  ( ( G  o.  K ) `  i
) )
46 fvco3 5942 . . . . . . . . . . . . . . 15  |-  ( ( K : NN --> T  /\  i  e.  NN )  ->  ( ( G  o.  K ) `  i
)  =  ( G `
 ( K `  i ) ) )
4710, 18, 46syl2an 480 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( G  o.  K
) `  i )  =  ( G `  ( K `  i ) ) )
4845, 47eqtrd 2485 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( ( G  o.  K )  |`  (
1 ... M ) ) `
 i )  =  ( G `  ( K `  i )
) )
4948adantrr 723 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
( ( ( G  o.  K )  |`  ( 1 ... M
) ) `  i
)  =  ( G `
 ( K `  i ) ) )
50 fvres 5879 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 1 ... M )  ->  (
( ( G  o.  K )  |`  (
1 ... M ) ) `
 j )  =  ( ( G  o.  K ) `  j
) )
5150ad2antll 735 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
( ( ( G  o.  K )  |`  ( 1 ... M
) ) `  j
)  =  ( ( G  o.  K ) `
 j ) )
52 elfznn 11828 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 1 ... M )  ->  j  e.  NN )
5352adantl 468 . . . . . . . . . . . . . 14  |-  ( ( i  e.  ( 1 ... M )  /\  j  e.  ( 1 ... M ) )  ->  j  e.  NN )
54 fvco3 5942 . . . . . . . . . . . . . 14  |-  ( ( K : NN --> T  /\  j  e.  NN )  ->  ( ( G  o.  K ) `  j
)  =  ( G `
 ( K `  j ) ) )
5510, 53, 54syl2an 480 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
( ( G  o.  K ) `  j
)  =  ( G `
 ( K `  j ) ) )
5651, 55eqtrd 2485 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
( ( ( G  o.  K )  |`  ( 1 ... M
) ) `  j
)  =  ( G `
 ( K `  j ) ) )
5749, 56eqeq12d 2466 . . . . . . . . . . 11  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
( ( ( ( G  o.  K )  |`  ( 1 ... M
) ) `  i
)  =  ( ( ( G  o.  K
)  |`  ( 1 ... M ) ) `  j )  <->  ( G `  ( K `  i
) )  =  ( G `  ( K `
 j ) ) ) )
58 fveq2 5865 . . . . . . . . . . . . 13  |-  ( ( G `  ( K `
 i ) )  =  ( G `  ( K `  j ) )  ->  ( F `  ( G `  ( K `  i )
) )  =  ( F `  ( G `
 ( K `  j ) ) ) )
5958fveq2d 5869 . . . . . . . . . . . 12  |-  ( ( G `  ( K `
 i ) )  =  ( G `  ( K `  j ) )  ->  ( 2nd `  ( F `  ( G `  ( K `  i ) ) ) )  =  ( 2nd `  ( F `  ( G `  ( K `  j ) ) ) ) )
6019a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( 1 ... M
)  C_  NN )
61 elfznn 11828 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  e.  ( 1 ... M )  ->  n  e.  NN )
6261ad2antlr 733 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  n  e.  ( 1 ... M
) )  /\  m  e.  W )  ->  n  e.  NN )
6362nnred 10624 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  ( 1 ... M
) )  /\  m  e.  W )  ->  n  e.  RR )
64 ovolicc2.16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  W  =  { n  e.  NN  |  B  e.  ( K `  n ) }
65 ssrab2 3514 . . . . . . . . . . . . . . . . . . . . . . 23  |-  { n  e.  NN  |  B  e.  ( K `  n
) }  C_  NN
6664, 65eqsstri 3462 . . . . . . . . . . . . . . . . . . . . . 22  |-  W  C_  NN
6766, 25sstri 3441 . . . . . . . . . . . . . . . . . . . . 21  |-  W  C_  RR
68 ovolicc2lem4OLD.17 . . . . . . . . . . . . . . . . . . . . . 22  |-  M  =  sup ( W ,  RR ,  `'  <  )
6966, 5sseqtri 3464 . . . . . . . . . . . . . . . . . . . . . . 23  |-  W  C_  ( ZZ>= `  1 )
70 1z 10967 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  1  e.  ZZ
715uzinf 12179 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 1  e.  ZZ  ->  -.  NN  e.  Fin )
7270, 71ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  -.  NN  e.  Fin
73 ovolicc2.6 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  U  e.  ( ~P
ran  ( (,)  o.  F )  i^i  Fin ) )
74 elin 3617 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( U  e.  ( ~P ran  ( (,)  o.  F )  i^i  Fin )  <->  ( U  e.  ~P ran  ( (,) 
o.  F )  /\  U  e.  Fin )
)
7573, 74sylib 200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  ( U  e.  ~P ran  ( (,)  o.  F
)  /\  U  e.  Fin ) )
7675simprd 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  U  e.  Fin )
77 ssfi 7792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( U  e.  Fin  /\  T  C_  U )  ->  T  e.  Fin )
7876, 13, 77sylancl 668 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  T  e.  Fin )
7978adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  W  =  (/) )  ->  T  e.  Fin )
8010adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  W  =  (/) )  ->  K : NN
--> T )
81 fveq2 5865 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( K `  i )  =  ( K `  j )  ->  ( G `  ( K `  i ) )  =  ( G `  ( K `  j )
) )
8281fveq2d 5869 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( K `  i )  =  ( K `  j )  ->  ( F `  ( G `  ( K `  i
) ) )  =  ( F `  ( G `  ( K `  j ) ) ) )
8382fveq2d 5869 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( K `  i )  =  ( K `  j )  ->  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) )  =  ( 2nd `  ( F `
 ( G `  ( K `  j ) ) ) ) )
84 simpll 760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  ph )
85 simprl 764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  i  e.  NN )
86 ral0 3874 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  A. m  e.  (/)  n  <_  m
87 simplr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  W  =  (/) )
8887raleqdv 2993 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  ( A. m  e.  W  n  <_  m  <->  A. m  e.  (/)  n  <_  m ) )
8986, 88mpbiri 237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  A. m  e.  W  n  <_  m )
9089ralrimivw 2803 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  A. n  e.  NN  A. m  e.  W  n  <_  m
)
91 rabid2 2968 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( NN  =  { n  e.  NN  |  A. m  e.  W  n  <_  m }  <->  A. n  e.  NN  A. m  e.  W  n  <_  m )
9290, 91sylibr 216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  NN  =  { n  e.  NN  |  A. m  e.  W  n  <_  m } )
9385, 92eleqtrd 2531 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  i  e.  { n  e.  NN  |  A. m  e.  W  n  <_  m } )
94 simprr 766 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  j  e.  NN )
9594, 92eleqtrd 2531 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  j  e.  { n  e.  NN  |  A. m  e.  W  n  <_  m } )
96 ovolicc.1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  A  e.  RR )
97 ovolicc.2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  B  e.  RR )
98 ovolicc.3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  A  <_  B )
99 ovolicc2.4 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  S  =  seq 1 (  +  ,  ( ( abs 
o.  -  )  o.  F ) )
100 ovolicc2.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  F : NN --> (  <_  i^i  ( RR  X.  RR ) ) )
101 ovolicc2.7 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  ( A [,] B
)  C_  U. U )
102 ovolicc2.9 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  t  e.  U )  ->  (
( (,)  o.  F
) `  ( G `  t ) )  =  t )
103 ovolicc2.12 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  t  e.  T )  ->  if ( ( 2nd `  ( F `  ( G `  t ) ) )  <_  B ,  ( 2nd `  ( F `
 ( G `  t ) ) ) ,  B )  e.  ( H `  t
) )
104 ovolicc2.13 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  A  e.  C )
10596, 97, 98, 99, 100, 73, 101, 4, 102, 11, 9, 103, 104, 8, 6, 64ovolicc2lem3 22472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  ( i  e.  { n  e.  NN  |  A. m  e.  W  n  <_  m }  /\  j  e.  { n  e.  NN  |  A. m  e.  W  n  <_  m } ) )  -> 
( i  =  j  <-> 
( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  =  ( 2nd `  ( F `  ( G `  ( K `  j
) ) ) ) ) )
10684, 93, 95, 105syl12anc 1266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  ( i  =  j  <->  ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  =  ( 2nd `  ( F `  ( G `  ( K `  j
) ) ) ) ) )
10783, 106syl5ibr 225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  ( ( K `  i )  =  ( K `  j )  ->  i  =  j ) )
108107ralrimivva 2809 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  W  =  (/) )  ->  A. i  e.  NN  A. j  e.  NN  ( ( K `
 i )  =  ( K `  j
)  ->  i  =  j ) )
109 dff13 6159 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( K : NN -1-1-> T  <->  ( K : NN --> T  /\  A. i  e.  NN  A. j  e.  NN  ( ( K `
 i )  =  ( K `  j
)  ->  i  =  j ) ) )
11080, 108, 109sylanbrc 670 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  W  =  (/) )  ->  K : NN
-1-1-> T )
111 f1domg 7589 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( T  e.  Fin  ->  ( K : NN -1-1-> T  ->  NN 
~<_  T ) )
11279, 110, 111sylc 62 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  W  =  (/) )  ->  NN  ~<_  T )
113 domfi 7793 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( T  e.  Fin  /\  NN 
~<_  T )  ->  NN  e.  Fin )
11479, 112, 113syl2anc 667 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  W  =  (/) )  ->  NN  e.  Fin )
115114ex 436 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( W  =  (/)  ->  NN  e.  Fin )
)
116115necon3bd 2638 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( -.  NN  e.  Fin  ->  W  =/=  (/) ) )
11772, 116mpi 20 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  W  =/=  (/) )
118 infmssuzclOLD 11247 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( W  C_  ( ZZ>= ` 
1 )  /\  W  =/=  (/) )  ->  sup ( W ,  RR ,  `'  <  )  e.  W
)
11969, 117, 118sylancr 669 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  sup ( W ,  RR ,  `'  <  )  e.  W )
12068, 119syl5eqel 2533 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  M  e.  W )
12167, 120sseldi 3430 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  M  e.  RR )
122121ad2antrr 732 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  ( 1 ... M
) )  /\  m  e.  W )  ->  M  e.  RR )
12367sseli 3428 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  e.  W  ->  m  e.  RR )
124123adantl 468 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  ( 1 ... M
) )  /\  m  e.  W )  ->  m  e.  RR )
125 elfzle2 11803 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  ( 1 ... M )  ->  n  <_  M )
126125ad2antlr 733 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  ( 1 ... M
) )  /\  m  e.  W )  ->  n  <_  M )
127 infmssuzleOLD 11246 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( W  C_  ( ZZ>= ` 
1 )  /\  m  e.  W )  ->  sup ( W ,  RR ,  `'  <  )  <_  m
)
12869, 127mpan 676 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  e.  W  ->  sup ( W ,  RR ,  `'  <  )  <_  m
)
12968, 128syl5eqbr 4436 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  e.  W  ->  M  <_  m )
130129adantl 468 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  ( 1 ... M
) )  /\  m  e.  W )  ->  M  <_  m )
13163, 122, 124, 126, 130letrd 9792 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  n  e.  ( 1 ... M
) )  /\  m  e.  W )  ->  n  <_  m )
132131ralrimiva 2802 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  ( 1 ... M
) )  ->  A. m  e.  W  n  <_  m )
13360, 132ssrabdv 3508 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( 1 ... M
)  C_  { n  e.  NN  |  A. m  e.  W  n  <_  m } )
134133adantr 467 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
( 1 ... M
)  C_  { n  e.  NN  |  A. m  e.  W  n  <_  m } )
135 simprl 764 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
i  e.  ( 1 ... M ) )
136134, 135sseldd 3433 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
i  e.  { n  e.  NN  |  A. m  e.  W  n  <_  m } )
137 simprr 766 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
j  e.  ( 1 ... M ) )
138134, 137sseldd 3433 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
j  e.  { n  e.  NN  |  A. m  e.  W  n  <_  m } )
139136, 138jca 535 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
( i  e.  {
n  e.  NN  |  A. m  e.  W  n  <_  m }  /\  j  e.  { n  e.  NN  |  A. m  e.  W  n  <_  m } ) )
140139, 105syldan 473 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
( i  =  j  <-> 
( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  =  ( 2nd `  ( F `  ( G `  ( K `  j
) ) ) ) ) )
14159, 140syl5ibr 225 . . . . . . . . . . 11  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
( ( G `  ( K `  i ) )  =  ( G `
 ( K `  j ) )  -> 
i  =  j ) )
14257, 141sylbid 219 . . . . . . . . . 10  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
( ( ( ( G  o.  K )  |`  ( 1 ... M
) ) `  i
)  =  ( ( ( G  o.  K
)  |`  ( 1 ... M ) ) `  j )  ->  i  =  j ) )
143142ralrimivva 2809 . . . . . . . . 9  |-  ( ph  ->  A. i  e.  ( 1 ... M ) A. j  e.  ( 1 ... M ) ( ( ( ( G  o.  K )  |`  ( 1 ... M
) ) `  i
)  =  ( ( ( G  o.  K
)  |`  ( 1 ... M ) ) `  j )  ->  i  =  j ) )
144 dff13 6159 . . . . . . . . 9  |-  ( ( ( G  o.  K
)  |`  ( 1 ... M ) ) : ( 1 ... M
) -1-1-> NN  <->  ( ( ( G  o.  K )  |`  ( 1 ... M
) ) : ( 1 ... M ) --> NN  /\  A. i  e.  ( 1 ... M
) A. j  e.  ( 1 ... M
) ( ( ( ( G  o.  K
)  |`  ( 1 ... M ) ) `  i )  =  ( ( ( G  o.  K )  |`  (
1 ... M ) ) `
 j )  -> 
i  =  j ) ) )
14521, 143, 144sylanbrc 670 . . . . . . . 8  |-  ( ph  ->  ( ( G  o.  K )  |`  (
1 ... M ) ) : ( 1 ... M ) -1-1-> NN )
146 f1f1orn 5825 . . . . . . . 8  |-  ( ( ( G  o.  K
)  |`  ( 1 ... M ) ) : ( 1 ... M
) -1-1-> NN  ->  ( ( G  o.  K )  |`  ( 1 ... M
) ) : ( 1 ... M ) -1-1-onto-> ran  ( ( G  o.  K )  |`  (
1 ... M ) ) )
147145, 146syl 17 . . . . . . 7  |-  ( ph  ->  ( ( G  o.  K )  |`  (
1 ... M ) ) : ( 1 ... M ) -1-1-onto-> ran  ( ( G  o.  K )  |`  ( 1 ... M
) ) )
148 f1oeq3 5807 . . . . . . . 8  |-  ( ( ( G  o.  K
) " ( 1 ... M ) )  =  ran  ( ( G  o.  K )  |`  ( 1 ... M
) )  ->  (
( ( G  o.  K )  |`  (
1 ... M ) ) : ( 1 ... M ) -1-1-onto-> ( ( G  o.  K ) " (
1 ... M ) )  <-> 
( ( G  o.  K )  |`  (
1 ... M ) ) : ( 1 ... M ) -1-1-onto-> ran  ( ( G  o.  K )  |`  ( 1 ... M
) ) ) )
1493, 148ax-mp 5 . . . . . . 7  |-  ( ( ( G  o.  K
)  |`  ( 1 ... M ) ) : ( 1 ... M
)
-1-1-onto-> ( ( G  o.  K ) " (
1 ... M ) )  <-> 
( ( G  o.  K )  |`  (
1 ... M ) ) : ( 1 ... M ) -1-1-onto-> ran  ( ( G  o.  K )  |`  ( 1 ... M
) ) )
150147, 149sylibr 216 . . . . . 6  |-  ( ph  ->  ( ( G  o.  K )  |`  (
1 ... M ) ) : ( 1 ... M ) -1-1-onto-> ( ( G  o.  K ) " (
1 ... M ) ) )
151 f1ofo 5821 . . . . . 6  |-  ( ( ( G  o.  K
)  |`  ( 1 ... M ) ) : ( 1 ... M
)
-1-1-onto-> ( ( G  o.  K ) " (
1 ... M ) )  ->  ( ( G  o.  K )  |`  ( 1 ... M
) ) : ( 1 ... M )
-onto-> ( ( G  o.  K ) " (
1 ... M ) ) )
152150, 151syl 17 . . . . 5  |-  ( ph  ->  ( ( G  o.  K )  |`  (
1 ... M ) ) : ( 1 ... M ) -onto-> ( ( G  o.  K )
" ( 1 ... M ) ) )
153 fofi 7860 . . . . 5  |-  ( ( ( 1 ... M
)  e.  Fin  /\  ( ( G  o.  K )  |`  (
1 ... M ) ) : ( 1 ... M ) -onto-> ( ( G  o.  K )
" ( 1 ... M ) ) )  ->  ( ( G  o.  K ) "
( 1 ... M
) )  e.  Fin )
15443, 152, 153syl2anc 667 . . . 4  |-  ( ph  ->  ( ( G  o.  K ) " (
1 ... M ) )  e.  Fin )
155 fimaxre2 10552 . . . 4  |-  ( ( ( ( G  o.  K ) " (
1 ... M ) ) 
C_  RR  /\  (
( G  o.  K
) " ( 1 ... M ) )  e.  Fin )  ->  E. x  e.  RR  A. y  e.  ( ( G  o.  K )
" ( 1 ... M ) ) y  <_  x )
15626, 154, 155syl2anc 667 . . 3  |-  ( ph  ->  E. x  e.  RR  A. y  e.  ( ( G  o.  K )
" ( 1 ... M ) ) y  <_  x )
15742, 156r19.29a 2932 . 2  |-  ( ph  ->  E. z  e.  NN  A. y  e.  ( ( G  o.  K )
" ( 1 ... M ) ) y  <  z )
15897, 96resubcld 10047 . . . . 5  |-  ( ph  ->  ( B  -  A
)  e.  RR )
159158rexrd 9690 . . . 4  |-  ( ph  ->  ( B  -  A
)  e.  RR* )
160159adantr 467 . . 3  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  ( B  -  A )  e.  RR* )
161 fzfid 12186 . . . . . 6  |-  ( ph  ->  ( 1 ... z
)  e.  Fin )
162 elfznn 11828 . . . . . . . . 9  |-  ( j  e.  ( 1 ... z )  ->  j  e.  NN )
163 eqid 2451 . . . . . . . . . . . 12  |-  ( ( abs  o.  -  )  o.  F )  =  ( ( abs  o.  -  )  o.  F )
164163ovolfsf 22424 . . . . . . . . . . 11  |-  ( F : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  (
( abs  o.  -  )  o.  F ) : NN --> ( 0 [,) +oo ) )
165100, 164syl 17 . . . . . . . . . 10  |-  ( ph  ->  ( ( abs  o.  -  )  o.  F
) : NN --> ( 0 [,) +oo ) )
166165ffvelrnda 6022 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  F ) `  j )  e.  ( 0 [,) +oo )
)
167162, 166sylan2 477 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 1 ... z
) )  ->  (
( ( abs  o.  -  )  o.  F
) `  j )  e.  ( 0 [,) +oo ) )
168 elrege0 11738 . . . . . . . 8  |-  ( ( ( ( abs  o.  -  )  o.  F
) `  j )  e.  ( 0 [,) +oo ) 
<->  ( ( ( ( abs  o.  -  )  o.  F ) `  j
)  e.  RR  /\  0  <_  ( ( ( abs  o.  -  )  o.  F ) `  j
) ) )
169167, 168sylib 200 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( 1 ... z
) )  ->  (
( ( ( abs 
o.  -  )  o.  F ) `  j
)  e.  RR  /\  0  <_  ( ( ( abs  o.  -  )  o.  F ) `  j
) ) )
170169simpld 461 . . . . . 6  |-  ( (
ph  /\  j  e.  ( 1 ... z
) )  ->  (
( ( abs  o.  -  )  o.  F
) `  j )  e.  RR )
171161, 170fsumrecl 13800 . . . . 5  |-  ( ph  -> 
sum_ j  e.  ( 1 ... z ) ( ( ( abs 
o.  -  )  o.  F ) `  j
)  e.  RR )
172171adantr 467 . . . 4  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  sum_ j  e.  ( 1 ... z
) ( ( ( abs  o.  -  )  o.  F ) `  j
)  e.  RR )
173172rexrd 9690 . . 3  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  sum_ j  e.  ( 1 ... z
) ( ( ( abs  o.  -  )  o.  F ) `  j
)  e.  RR* )
174163, 99ovolsf 22425 . . . . . . . . 9  |-  ( F : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  S : NN --> ( 0 [,) +oo ) )
175100, 174syl 17 . . . . . . . 8  |-  ( ph  ->  S : NN --> ( 0 [,) +oo ) )
176 frn 5735 . . . . . . . 8  |-  ( S : NN --> ( 0 [,) +oo )  ->  ran  S  C_  ( 0 [,) +oo ) )
177175, 176syl 17 . . . . . . 7  |-  ( ph  ->  ran  S  C_  (
0 [,) +oo )
)
178 rge0ssre 11740 . . . . . . 7  |-  ( 0 [,) +oo )  C_  RR
179177, 178syl6ss 3444 . . . . . 6  |-  ( ph  ->  ran  S  C_  RR )
180 ressxr 9684 . . . . . 6  |-  RR  C_  RR*
181179, 180syl6ss 3444 . . . . 5  |-  ( ph  ->  ran  S  C_  RR* )
182 supxrcl 11600 . . . . 5  |-  ( ran 
S  C_  RR*  ->  sup ( ran  S ,  RR* ,  <  )  e.  RR* )
183181, 182syl 17 . . . 4  |-  ( ph  ->  sup ( ran  S ,  RR* ,  <  )  e.  RR* )
184183adantr 467 . . 3  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  sup ( ran  S ,  RR* ,  <  )  e.  RR* )
185158adantr 467 . . . 4  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  ( B  -  A )  e.  RR )
18624sselda 3432 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  j  e.  NN )
187178, 166sseldi 3430 . . . . . . 7  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  F ) `  j )  e.  RR )
188186, 187syldan 473 . . . . . 6  |-  ( (
ph  /\  j  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  ( (
( abs  o.  -  )  o.  F ) `  j
)  e.  RR )
189154, 188fsumrecl 13800 . . . . 5  |-  ( ph  -> 
sum_ j  e.  ( ( G  o.  K
) " ( 1 ... M ) ) ( ( ( abs 
o.  -  )  o.  F ) `  j
)  e.  RR )
190189adantr 467 . . . 4  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  sum_ j  e.  ( ( G  o.  K ) " (
1 ... M ) ) ( ( ( abs 
o.  -  )  o.  F ) `  j
)  e.  RR )
191 inss2 3653 . . . . . . . . . . 11  |-  (  <_  i^i  ( RR  X.  RR ) )  C_  ( RR  X.  RR )
192 fss 5737 . . . . . . . . . . 11  |-  ( ( F : NN --> (  <_  i^i  ( RR  X.  RR ) )  /\  (  <_  i^i  ( RR  X.  RR ) )  C_  ( RR  X.  RR ) )  ->  F : NN --> ( RR  X.  RR ) )
193100, 191, 192sylancl 668 . . . . . . . . . 10  |-  ( ph  ->  F : NN --> ( RR 
X.  RR ) )
19466, 120sseldi 3430 . . . . . . . . . . . 12  |-  ( ph  ->  M  e.  NN )
19515, 194ffvelrnd 6023 . . . . . . . . . . 11  |-  ( ph  ->  ( K `  M
)  e.  U )
1964, 195ffvelrnd 6023 . . . . . . . . . 10  |-  ( ph  ->  ( G `  ( K `  M )
)  e.  NN )
197193, 196ffvelrnd 6023 . . . . . . . . 9  |-  ( ph  ->  ( F `  ( G `  ( K `  M ) ) )  e.  ( RR  X.  RR ) )
198 xp2nd 6824 . . . . . . . . 9  |-  ( ( F `  ( G `
 ( K `  M ) ) )  e.  ( RR  X.  RR )  ->  ( 2nd `  ( F `  ( G `  ( K `  M ) ) ) )  e.  RR )
199197, 198syl 17 . . . . . . . 8  |-  ( ph  ->  ( 2nd `  ( F `  ( G `  ( K `  M
) ) ) )  e.  RR )
20013, 8sseldi 3430 . . . . . . . . . . 11  |-  ( ph  ->  C  e.  U )
2014, 200ffvelrnd 6023 . . . . . . . . . 10  |-  ( ph  ->  ( G `  C
)  e.  NN )
202193, 201ffvelrnd 6023 . . . . . . . . 9  |-  ( ph  ->  ( F `  ( G `  C )
)  e.  ( RR 
X.  RR ) )
203 xp1st 6823 . . . . . . . . 9  |-  ( ( F `  ( G `
 C ) )  e.  ( RR  X.  RR )  ->  ( 1st `  ( F `  ( G `  C )
) )  e.  RR )
204202, 203syl 17 . . . . . . . 8  |-  ( ph  ->  ( 1st `  ( F `  ( G `  C ) ) )  e.  RR )
205199, 204resubcld 10047 . . . . . . 7  |-  ( ph  ->  ( ( 2nd `  ( F `  ( G `  ( K `  M
) ) ) )  -  ( 1st `  ( F `  ( G `  C ) ) ) )  e.  RR )
206 fveq2 5865 . . . . . . . . . 10  |-  ( j  =  ( G `  ( K `  i ) )  ->  ( (
( abs  o.  -  )  o.  F ) `  j
)  =  ( ( ( abs  o.  -  )  o.  F ) `  ( G `  ( K `  i )
) ) )
207187recnd 9669 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  F ) `  j )  e.  CC )
208186, 207syldan 473 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  ( (
( abs  o.  -  )  o.  F ) `  j
)  e.  CC )
209206, 43, 150, 48, 208fsumf1o 13789 . . . . . . . . 9  |-  ( ph  -> 
sum_ j  e.  ( ( G  o.  K
) " ( 1 ... M ) ) ( ( ( abs 
o.  -  )  o.  F ) `  j
)  =  sum_ i  e.  ( 1 ... M
) ( ( ( abs  o.  -  )  o.  F ) `  ( G `  ( K `  i ) ) ) )
210100adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  F : NN --> (  <_  i^i  ( RR  X.  RR ) ) )
2114adantr 467 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  G : U --> NN )
212 ffvelrn 6020 . . . . . . . . . . . . 13  |-  ( ( K : NN --> U  /\  i  e.  NN )  ->  ( K `  i
)  e.  U )
21315, 18, 212syl2an 480 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( K `  i )  e.  U )
214211, 213ffvelrnd 6023 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( G `  ( K `  i ) )  e.  NN )
215163ovolfsval 22423 . . . . . . . . . . 11  |-  ( ( F : NN --> (  <_  i^i  ( RR  X.  RR ) )  /\  ( G `  ( K `  i ) )  e.  NN )  ->  (
( ( abs  o.  -  )  o.  F
) `  ( G `  ( K `  i
) ) )  =  ( ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  -  ( 1st `  ( F `  ( G `  ( K `  i
) ) ) ) ) )
216210, 214, 215syl2anc 667 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( ( abs  o.  -  )  o.  F
) `  ( G `  ( K `  i
) ) )  =  ( ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  -  ( 1st `  ( F `  ( G `  ( K `  i
) ) ) ) ) )
217216sumeq2dv 13769 . . . . . . . . 9  |-  ( ph  -> 
sum_ i  e.  ( 1 ... M ) ( ( ( abs 
o.  -  )  o.  F ) `  ( G `  ( K `  i ) ) )  =  sum_ i  e.  ( 1 ... M ) ( ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  -  ( 1st `  ( F `  ( G `  ( K `  i
) ) ) ) ) )
218193adantr 467 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  NN )  ->  F : NN
--> ( RR  X.  RR ) )
2194adantr 467 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  NN )  ->  G : U
--> NN )
22015ffvelrnda 6022 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  NN )  ->  ( K `
 i )  e.  U )
221219, 220ffvelrnd 6023 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  NN )  ->  ( G `
 ( K `  i ) )  e.  NN )
222218, 221ffvelrnd 6023 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  NN )  ->  ( F `
 ( G `  ( K `  i ) ) )  e.  ( RR  X.  RR ) )
223 xp2nd 6824 . . . . . . . . . . . . . 14  |-  ( ( F `  ( G `
 ( K `  i ) ) )  e.  ( RR  X.  RR )  ->  ( 2nd `  ( F `  ( G `  ( K `  i ) ) ) )  e.  RR )
224222, 223syl 17 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  NN )  ->  ( 2nd `  ( F `  ( G `  ( K `  i ) ) ) )  e.  RR )
22518, 224sylan2 477 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) )  e.  RR )
226225recnd 9669 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) )  e.  CC )
227193adantr 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  F : NN --> ( RR  X.  RR ) )
228227, 214ffvelrnd 6023 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( F `  ( G `  ( K `  i
) ) )  e.  ( RR  X.  RR ) )
229 xp1st 6823 . . . . . . . . . . . . 13  |-  ( ( F `  ( G `
 ( K `  i ) ) )  e.  ( RR  X.  RR )  ->  ( 1st `  ( F `  ( G `  ( K `  i ) ) ) )  e.  RR )
230228, 229syl 17 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( 1st `  ( F `  ( G `  ( K `
 i ) ) ) )  e.  RR )
231230recnd 9669 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( 1st `  ( F `  ( G `  ( K `
 i ) ) ) )  e.  CC )
23243, 226, 231fsumsub 13849 . . . . . . . . . 10  |-  ( ph  -> 
sum_ i  e.  ( 1 ... M ) ( ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  -  ( 1st `  ( F `  ( G `  ( K `  i
) ) ) ) )  =  ( sum_ i  e.  ( 1 ... M ) ( 2nd `  ( F `
 ( G `  ( K `  i ) ) ) )  -  sum_ i  e.  ( 1 ... M ) ( 1st `  ( F `
 ( G `  ( K `  i ) ) ) ) ) )
23369, 120sseldi 3430 . . . . . . . . . . . . 13  |-  ( ph  ->  M  e.  ( ZZ>= ` 
1 ) )
234 fveq2 5865 . . . . . . . . . . . . . . . 16  |-  ( i  =  M  ->  ( K `  i )  =  ( K `  M ) )
235234fveq2d 5869 . . . . . . . . . . . . . . 15  |-  ( i  =  M  ->  ( G `  ( K `  i ) )  =  ( G `  ( K `  M )
) )
236235fveq2d 5869 . . . . . . . . . . . . . 14  |-  ( i  =  M  ->  ( F `  ( G `  ( K `  i
) ) )  =  ( F `  ( G `  ( K `  M ) ) ) )
237236fveq2d 5869 . . . . . . . . . . . . 13  |-  ( i  =  M  ->  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) )  =  ( 2nd `  ( F `
 ( G `  ( K `  M ) ) ) ) )
238233, 226, 237fsumm1 13812 . . . . . . . . . . . 12  |-  ( ph  -> 
sum_ i  e.  ( 1 ... M ) ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  =  ( sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  +  ( 2nd `  ( F `  ( G `  ( K `  M
) ) ) ) ) )
239 fzfid 12186 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1 ... ( M  -  1 ) )  e.  Fin )
240 elfznn 11828 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( 1 ... ( M  -  1 ) )  ->  i  e.  NN )
241240, 224sylan2 477 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) )  e.  RR )
242239, 241fsumrecl 13800 . . . . . . . . . . . . . 14  |-  ( ph  -> 
sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  e.  RR )
243242recnd 9669 . . . . . . . . . . . . 13  |-  ( ph  -> 
sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  e.  CC )
244199recnd 9669 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 2nd `  ( F `  ( G `  ( K `  M
) ) ) )  e.  CC )
245243, 244addcomd 9835 . . . . . . . . . . . 12  |-  ( ph  ->  ( sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  +  ( 2nd `  ( F `  ( G `  ( K `  M
) ) ) ) )  =  ( ( 2nd `  ( F `
 ( G `  ( K `  M ) ) ) )  + 
sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) ) ) )
246238, 245eqtrd 2485 . . . . . . . . . . 11  |-  ( ph  -> 
sum_ i  e.  ( 1 ... M ) ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  =  ( ( 2nd `  ( F `  ( G `  ( K `  M ) ) ) )  +  sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) ) ) )
247 fveq2 5865 . . . . . . . . . . . . . . . 16  |-  ( i  =  1  ->  ( K `  i )  =  ( K ` 
1 ) )
248247fveq2d 5869 . . . . . . . . . . . . . . 15  |-  ( i  =  1  ->  ( G `  ( K `  i ) )  =  ( G `  ( K `  1 )
) )
249248fveq2d 5869 . . . . . . . . . . . . . 14  |-  ( i  =  1  ->  ( F `  ( G `  ( K `  i
) ) )  =  ( F `  ( G `  ( K `  1 ) ) ) )
250249fveq2d 5869 . . . . . . . . . . . . 13  |-  ( i  =  1  ->  ( 1st `  ( F `  ( G `  ( K `
 i ) ) ) )  =  ( 1st `  ( F `
 ( G `  ( K `  1 ) ) ) ) )
251233, 231, 250fsum1p 13814 . . . . . . . . . . . 12  |-  ( ph  -> 
sum_ i  e.  ( 1 ... M ) ( 1st `  ( F `  ( G `  ( K `  i
) ) ) )  =  ( ( 1st `  ( F `  ( G `  ( K `  1 ) ) ) )  +  sum_ i  e.  ( (
1  +  1 ) ... M ) ( 1st `  ( F `
 ( G `  ( K `  i ) ) ) ) ) )
2525, 6, 7, 8algr0 14531 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( K `  1
)  =  C )
253252fveq2d 5869 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( G `  ( K `  1 )
)  =  ( G `
 C ) )
254253fveq2d 5869 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( F `  ( G `  ( K `  1 ) ) )  =  ( F `
 ( G `  C ) ) )
255254fveq2d 5869 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1st `  ( F `  ( G `  ( K `  1
) ) ) )  =  ( 1st `  ( F `  ( G `  C ) ) ) )
2567peano2zd 11043 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1  +  1 )  e.  ZZ )
257194nnzd 11039 . . . . . . . . . . . . . . 15  |-  ( ph  ->  M  e.  ZZ )
258 fzp1ss 11847 . . . . . . . . . . . . . . . . . 18  |-  ( 1  e.  ZZ  ->  (
( 1  +  1 ) ... M ) 
C_  ( 1 ... M ) )
25970, 258mp1i 13 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( 1  +  1 ) ... M
)  C_  ( 1 ... M ) )
260259sselda 3432 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ( 1  +  1 ) ... M
) )  ->  i  e.  ( 1 ... M
) )
261260, 231syldan 473 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ( 1  +  1 ) ... M
) )  ->  ( 1st `  ( F `  ( G `  ( K `
 i ) ) ) )  e.  CC )
262 fveq2 5865 . . . . . . . . . . . . . . . . . 18  |-  ( i  =  ( j  +  1 )  ->  ( K `  i )  =  ( K `  ( j  +  1 ) ) )
263262fveq2d 5869 . . . . . . . . . . . . . . . . 17  |-  ( i  =  ( j  +  1 )  ->  ( G `  ( K `  i ) )  =  ( G `  ( K `  ( j  +  1 ) ) ) )
264263fveq2d 5869 . . . . . . . . . . . . . . . 16  |-  ( i  =  ( j  +  1 )  ->  ( F `  ( G `  ( K `  i
) ) )  =  ( F `  ( G `  ( K `  ( j  +  1 ) ) ) ) )
265264fveq2d 5869 . . . . . . . . . . . . . . 15  |-  ( i  =  ( j  +  1 )  ->  ( 1st `  ( F `  ( G `  ( K `
 i ) ) ) )  =  ( 1st `  ( F `
 ( G `  ( K `  ( j  +  1 ) ) ) ) ) )
2667, 256, 257, 261, 265fsumshftm 13842 . . . . . . . . . . . . . 14  |-  ( ph  -> 
sum_ i  e.  ( ( 1  +  1 ) ... M ) ( 1st `  ( F `  ( G `  ( K `  i
) ) ) )  =  sum_ j  e.  ( ( ( 1  +  1 )  -  1 ) ... ( M  -  1 ) ) ( 1st `  ( F `  ( G `  ( K `  (
j  +  1 ) ) ) ) ) )
267 ax-1cn 9597 . . . . . . . . . . . . . . . . . 18  |-  1  e.  CC
268267, 267pncan3oi 9891 . . . . . . . . . . . . . . . . 17  |-  ( ( 1  +  1 )  -  1 )  =  1
269268oveq1i 6300 . . . . . . . . . . . . . . . 16  |-  ( ( ( 1  +  1 )  -  1 ) ... ( M  - 
1 ) )  =  ( 1 ... ( M  -  1 ) )
270269sumeq1i 13764 . . . . . . . . . . . . . . 15  |-  sum_ j  e.  ( ( ( 1  +  1 )  - 
1 ) ... ( M  -  1 ) ) ( 1st `  ( F `  ( G `  ( K `  (
j  +  1 ) ) ) ) )  =  sum_ j  e.  ( 1 ... ( M  -  1 ) ) ( 1st `  ( F `  ( G `  ( K `  (
j  +  1 ) ) ) ) )
271 oveq1 6297 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  i  ->  (
j  +  1 )  =  ( i  +  1 ) )
272271fveq2d 5869 . . . . . . . . . . . . . . . . . . 19  |-  ( j  =  i  ->  ( K `  ( j  +  1 ) )  =  ( K `  ( i  +  1 ) ) )
273272fveq2d 5869 . . . . . . . . . . . . . . . . . 18  |-  ( j  =  i  ->  ( G `  ( K `  ( j  +  1 ) ) )  =  ( G `  ( K `  ( i  +  1 ) ) ) )
274273fveq2d 5869 . . . . . . . . . . . . . . . . 17  |-  ( j  =  i  ->  ( F `  ( G `  ( K `  (
j  +  1 ) ) ) )  =  ( F `  ( G `  ( K `  ( i  +  1 ) ) ) ) )
275274fveq2d 5869 . . . . . . . . . . . . . . . 16  |-  ( j  =  i  ->  ( 1st `  ( F `  ( G `  ( K `
 ( j  +  1 ) ) ) ) )  =  ( 1st `  ( F `
 ( G `  ( K `  ( i  +  1 ) ) ) ) ) )
276275cbvsumv 13762 . . . . . . . . . . . . . . 15  |-  sum_ j  e.  ( 1 ... ( M  -  1 ) ) ( 1st `  ( F `  ( G `  ( K `  (
j  +  1 ) ) ) ) )  =  sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 1st `  ( F `  ( G `  ( K `  (
i  +  1 ) ) ) ) )
277270, 276eqtri 2473 . . . . . . . . . . . . . 14  |-  sum_ j  e.  ( ( ( 1  +  1 )  - 
1 ) ... ( M  -  1 ) ) ( 1st `  ( F `  ( G `  ( K `  (
j  +  1 ) ) ) ) )  =  sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 1st `  ( F `  ( G `  ( K `  (
i  +  1 ) ) ) ) )
278266, 277syl6eq 2501 . . . . . . . . . . . . 13  |-  ( ph  -> 
sum_ i  e.  ( ( 1  +  1 ) ... M ) ( 1st `  ( F `  ( G `  ( K `  i
) ) ) )  =  sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 1st `  ( F `  ( G `  ( K `  (
i  +  1 ) ) ) ) ) )
279255, 278oveq12d 6308 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 1st `  ( F `  ( G `  ( K `  1
) ) ) )  +  sum_ i  e.  ( ( 1  +  1 ) ... M ) ( 1st `  ( F `  ( G `  ( K `  i
) ) ) ) )  =  ( ( 1st `  ( F `
 ( G `  C ) ) )  +  sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 1st `  ( F `  ( G `  ( K `  (
i  +  1 ) ) ) ) ) ) )
280251, 279eqtrd 2485 . . . . . . . . . . 11  |-  ( ph  -> 
sum_ i  e.  ( 1 ... M ) ( 1st `  ( F `  ( G `  ( K `  i
) ) ) )  =  ( ( 1st `  ( F `  ( G `  C )
) )  +  sum_ i  e.  ( 1 ... ( M  - 
1 ) ) ( 1st `  ( F `
 ( G `  ( K `  ( i  +  1 ) ) ) ) ) ) )
281246, 280oveq12d 6308 . . . . . . . . . 10  |-  ( ph  ->  ( sum_ i  e.  ( 1 ... M ) ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  -  sum_ i  e.  ( 1 ... M ) ( 1st `  ( F `  ( G `  ( K `  i
) ) ) ) )  =  ( ( ( 2nd `  ( F `  ( G `  ( K `  M
) ) ) )  +  sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) ) )  -  ( ( 1st `  ( F `
 ( G `  C ) ) )  +  sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 1st `  ( F `  ( G `  ( K `  (
i  +  1 ) ) ) ) ) ) ) )
282204recnd 9669 . . . . . . . . . . 11  |-  ( ph  ->  ( 1st `  ( F `  ( G `  C ) ) )  e.  CC )
283 peano2nn 10621 . . . . . . . . . . . . . . . . . 18  |-  ( i  e.  NN  ->  (
i  +  1 )  e.  NN )
284 ffvelrn 6020 . . . . . . . . . . . . . . . . . 18  |-  ( ( K : NN --> U  /\  ( i  +  1 )  e.  NN )  ->  ( K `  ( i  +  1 ) )  e.  U
)
28515, 283, 284syl2an 480 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  NN )  ->  ( K `
 ( i  +  1 ) )  e.  U )
286219, 285ffvelrnd 6023 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  NN )  ->  ( G `
 ( K `  ( i  +  1 ) ) )  e.  NN )
287218, 286ffvelrnd 6023 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  NN )  ->  ( F `
 ( G `  ( K `  ( i  +  1 ) ) ) )  e.  ( RR  X.  RR ) )
288 xp1st 6823 . . . . . . . . . . . . . . 15  |-  ( ( F `  ( G `
 ( K `  ( i  +  1 ) ) ) )  e.  ( RR  X.  RR )  ->  ( 1st `  ( F `  ( G `  ( K `  ( i  +  1 ) ) ) ) )  e.  RR )
289287, 288syl 17 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  NN )  ->  ( 1st `  ( F `  ( G `  ( K `  ( i  +  1 ) ) ) ) )  e.  RR )
290240, 289sylan2 477 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  ( 1st `  ( F `  ( G `  ( K `
 ( i  +  1 ) ) ) ) )  e.  RR )
291239, 290fsumrecl 13800 . . . . . . . . . . . 12  |-  ( ph  -> 
sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 1st `  ( F `  ( G `  ( K `  (
i  +  1 ) ) ) ) )  e.  RR )
292291recnd 9669 . . . . . . . . . . 11  |-  ( ph  -> 
sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 1st `  ( F `  ( G `  ( K `  (
i  +  1 ) ) ) ) )  e.  CC )
293244, 243, 282, 292addsub4d 10033 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( 2nd `  ( F `  ( G `  ( K `  M ) ) ) )  +  sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) ) )  -  ( ( 1st `  ( F `
 ( G `  C ) ) )  +  sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 1st `  ( F `  ( G `  ( K `  (
i  +  1 ) ) ) ) ) ) )  =  ( ( ( 2nd `  ( F `  ( G `  ( K `  M
) ) ) )  -  ( 1st `  ( F `  ( G `  C ) ) ) )  +  ( sum_ i  e.  ( 1 ... ( M  - 
1 ) ) ( 2nd `  ( F `
 ( G `  ( K `  i ) ) ) )  -  sum_ i  e.  ( 1 ... ( M  - 
1 ) ) ( 1st `  ( F `
 ( G `  ( K `  ( i  +  1 ) ) ) ) ) ) ) )
294232, 281, 2933eqtrd 2489 . . . . . . . . 9  |-  ( ph  -> 
sum_ i  e.  ( 1 ... M ) ( ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  -  ( 1st `  ( F `  ( G `  ( K `  i
) ) ) ) )  =  ( ( ( 2nd `  ( F `  ( G `  ( K `  M
) ) ) )  -  ( 1st `  ( F `  ( G `  C ) ) ) )  +  ( sum_ i  e.  ( 1 ... ( M  - 
1 ) ) ( 2nd `  ( F `
 ( G `  ( K `  i ) ) ) )  -  sum_ i  e.  ( 1 ... ( M  - 
1 ) ) ( 1st `  ( F `
 ( G `  ( K `  ( i  +  1 ) ) ) ) ) ) ) )
295209, 217, 2943eqtrd 2489 . . . . . . . 8  |-  ( ph  -> 
sum_ j  e.  ( ( G  o.  K
) " ( 1 ... M ) ) ( ( ( abs 
o.  -  )  o.  F ) `  j
)  =  ( ( ( 2nd `  ( F `  ( G `  ( K `  M
) ) ) )  -  ( 1st `  ( F `  ( G `  C ) ) ) )  +  ( sum_ i  e.  ( 1 ... ( M  - 
1 ) ) ( 2nd `  ( F `
 ( G `  ( K `  i ) ) ) )  -  sum_ i  e.  ( 1 ... ( M  - 
1 ) ) ( 1st `  ( F `
 ( G `  ( K `  ( i  +  1 ) ) ) ) ) ) ) )
296295, 189eqeltrrd 2530 . . . . . . 7  |-  ( ph  ->  ( ( ( 2nd `  ( F `  ( G `  ( K `  M ) ) ) )  -  ( 1st `  ( F `  ( G `  C )
) ) )  +  ( sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  -  sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 1st `  ( F `  ( G `  ( K `  (
i  +  1 ) ) ) ) ) ) )  e.  RR )
297 fveq2 5865 . . . . . . . . . . . . . . 15  |-  ( n  =  M  ->  ( K `  n )  =  ( K `  M ) )
298297eleq2d 2514 . . . . . . . . . . . . . 14  |-  ( n  =  M  ->  ( B  e.  ( K `  n )  <->  B  e.  ( K `  M ) ) )
299298, 64elrab2 3198 . . . . . . . . . . . . 13  |-  ( M  e.  W  <->  ( M  e.  NN  /\  B  e.  ( K `  M
) ) )
300120, 299sylib 200 . . . . . . . . . . . 12  |-  ( ph  ->  ( M  e.  NN  /\  B  e.  ( K `
 M ) ) )
301300simprd 465 . . . . . . . . . . 11  |-  ( ph  ->  B  e.  ( K `
 M ) )
30296, 97, 98, 99, 100, 73, 101, 4, 102ovolicc2lem1 22470 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( K `  M )  e.  U
)  ->  ( B  e.  ( K `  M
)  <->  ( B  e.  RR  /\  ( 1st `  ( F `  ( G `  ( K `  M ) ) ) )  <  B  /\  B  <  ( 2nd `  ( F `  ( G `  ( K `  M
) ) ) ) ) ) )
303195, 302mpdan 674 . . . . . . . . . . 11  |-  ( ph  ->  ( B  e.  ( K `  M )  <-> 
( B  e.  RR  /\  ( 1st `  ( F `  ( G `  ( K `  M
) ) ) )  <  B  /\  B  <  ( 2nd `  ( F `  ( G `  ( K `  M
) ) ) ) ) ) )
304301, 303mpbid 214 . . . . . . . . . 10  |-  ( ph  ->  ( B  e.  RR  /\  ( 1st `  ( F `  ( G `  ( K `  M
) ) ) )  <  B  /\  B  <  ( 2nd `  ( F `  ( G `  ( K `  M
) ) ) ) ) )
305304simp3d 1022 . . . . . . . . 9  |-  ( ph  ->  B  <  ( 2nd `  ( F `  ( G `  ( K `  M ) ) ) ) )
30696, 97, 98, 99, 100, 73, 101, 4, 102ovolicc2lem1 22470 . . . . . . . . . . . 12  |-  ( (
ph  /\  C  e.  U )  ->  ( A  e.  C  <->  ( A  e.  RR  /\  ( 1st `  ( F `  ( G `  C )
) )  <  A  /\  A  <  ( 2nd `  ( F `  ( G `  C )
) ) ) ) )
307200, 306mpdan 674 . . . . . . . . . . 11  |-  ( ph  ->  ( A  e.  C  <->  ( A  e.  RR  /\  ( 1st `  ( F `
 ( G `  C ) ) )  <  A  /\  A  <  ( 2nd `  ( F `  ( G `  C ) ) ) ) ) )
308104, 307mpbid 214 . . . . . . . . . 10  |-  ( ph  ->  ( A  e.  RR  /\  ( 1st `  ( F `  ( G `  C ) ) )  <  A  /\  A  <  ( 2nd `  ( F `  ( G `  C ) ) ) ) )
309308simp2d 1021 . . . . . . . . 9  |-  ( ph  ->  ( 1st `  ( F `  ( G `  C ) ) )  <  A )
31097, 204, 199, 96, 305, 309lt2subd 10237 . . . . . . . 8  |-  ( ph  ->  ( B  -  A
)  <  ( ( 2nd `  ( F `  ( G `  ( K `
 M ) ) ) )  -  ( 1st `  ( F `  ( G `  C ) ) ) ) )
311158, 205, 310ltled 9783 . . . . . . 7  |-  ( ph  ->  ( B  -  A
)  <_  ( ( 2nd `  ( F `  ( G `  ( K `
 M ) ) ) )  -  ( 1st `  ( F `  ( G `  C ) ) ) ) )
312240adantl 468 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  i  e.  NN )
313 simpr 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  i  e.  ( 1 ... ( M  -  1 ) ) )
314257adantr 467 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  M  e.  ZZ )
315 elfzm11 11865 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 1  e.  ZZ  /\  M  e.  ZZ )  ->  ( i  e.  ( 1 ... ( M  -  1 ) )  <-> 
( i  e.  ZZ  /\  1  <_  i  /\  i  <  M ) ) )
31670, 314, 315sylancr 669 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  (
i  e.  ( 1 ... ( M  - 
1 ) )  <->  ( i  e.  ZZ  /\  1  <_ 
i  /\  i  <  M ) ) )
317313, 316mpbid 214 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  (
i  e.  ZZ  /\  1  <_  i  /\  i  <  M ) )
318317simp3d 1022 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  i  <  M )
319312nnred 10624 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  i  e.  RR )
320121adantr 467 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  M  e.  RR )
321319, 320ltnled 9782 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  (
i  <  M  <->  -.  M  <_  i ) )
322318, 321mpbid 214 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  -.  M  <_  i )
323 infmssuzleOLD 11246 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( W  C_  ( ZZ>= ` 
1 )  /\  i  e.  W )  ->  sup ( W ,  RR ,  `'  <  )  <_  i
)
32469, 323mpan 676 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  e.  W  ->  sup ( W ,  RR ,  `'  <  )  <_  i
)
32568, 324syl5eqbr 4436 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  W  ->  M  <_  i )
326322, 325nsyl 125 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  -.  i  e.  W )
327312, 326jca 535 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  (
i  e.  NN  /\  -.  i  e.  W
) )
32896, 97, 98, 99, 100, 73, 101, 4, 102, 11, 9, 103, 104, 8, 6, 64ovolicc2lem2 22471 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( i  e.  NN  /\  -.  i  e.  W ) )  -> 
( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  <_  B )
329327, 328syldan 473 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) )  <_  B
)
330329iftrued 3889 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  if ( ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  <_  B ,  ( 2nd `  ( F `
 ( G `  ( K `  i ) ) ) ) ,  B )  =  ( 2nd `  ( F `
 ( G `  ( K `  i ) ) ) ) )
331 ffvelrn 6020 . . . . . . . . . . . . . . . . 17  |-  ( ( K : NN --> T  /\  i  e.  NN )  ->  ( K `  i
)  e.  T )
33210, 240, 331syl2an 480 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  ( K `  i )  e.  T )
333103ralrimiva 2802 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  A. t  e.  T  if ( ( 2nd `  ( F `  ( G `  t ) ) )  <_  B ,  ( 2nd `  ( F `
 ( G `  t ) ) ) ,  B )  e.  ( H `  t
) )
334333adantr 467 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  A. t  e.  T  if (
( 2nd `  ( F `  ( G `  t ) ) )  <_  B ,  ( 2nd `  ( F `
 ( G `  t ) ) ) ,  B )  e.  ( H `  t
) )
335 fveq2 5865 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( t  =  ( K `  i )  ->  ( G `  t )  =  ( G `  ( K `  i ) ) )
336335fveq2d 5869 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  =  ( K `  i )  ->  ( F `  ( G `  t ) )  =  ( F `  ( G `  ( K `  i ) ) ) )
337336fveq2d 5869 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  ( K `  i )  ->  ( 2nd `  ( F `  ( G `  t ) ) )  =  ( 2nd `  ( F `
 ( G `  ( K `  i ) ) ) ) )
338337breq1d 4412 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  ( K `  i )  ->  (
( 2nd `  ( F `  ( G `  t ) ) )  <_  B  <->  ( 2nd `  ( F `  ( G `  ( K `  i ) ) ) )  <_  B )
)
339338, 337ifbieq1d 3904 . . . . . . . . . . . . . . . . . 18  |-  ( t  =  ( K `  i )  ->  if ( ( 2nd `  ( F `  ( G `  t ) ) )  <_  B ,  ( 2nd `  ( F `
 ( G `  t ) ) ) ,  B )  =  if ( ( 2nd `  ( F `  ( G `  ( K `  i ) ) ) )  <_  B , 
( 2nd `  ( F `  ( G `  ( K `  i
) ) ) ) ,  B ) )
340 fveq2 5865 . . . . . . . . . . . . . . . . . 18  |-  ( t  =  ( K `  i )  ->  ( H `  t )  =  ( H `  ( K `  i ) ) )
341339, 340eleq12d 2523 . . . . . . . . . . . . . . . . 17  |-  ( t  =  ( K `  i )  ->  ( if ( ( 2nd `  ( F `  ( G `  t ) ) )  <_  B ,  ( 2nd `  ( F `
 ( G `  t ) ) ) ,  B )  e.  ( H `  t
)  <->  if ( ( 2nd `  ( F `  ( G `  ( K `  i ) ) ) )  <_  B , 
( 2nd `  ( F `  ( G `  ( K `  i
) ) ) ) ,  B )  e.  ( H `  ( K `  i )
) ) )
342341rspcv 3146 . . . . . . . . . . . . . . . 16  |-  ( ( K `  i )  e.  T  ->  ( A. t  e.  T  if ( ( 2nd `  ( F `  ( G `  t ) ) )  <_  B ,  ( 2nd `  ( F `
 ( G `  t ) ) ) ,  B )  e.  ( H `  t
)  ->  if (
( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  <_  B ,  ( 2nd `  ( F `
 ( G `  ( K `  i ) ) ) ) ,  B )  e.  ( H `  ( K `
 i ) ) ) )
343332, 334, 342sylc 62 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  if ( ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  <_  B ,  ( 2nd `  ( F `
 ( G `  ( K `  i ) ) ) ) ,  B )  e.  ( H `  ( K `
 i ) ) )
344330, 343eqeltrrd 2530 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) )  e.  ( H `  ( K `
 i ) ) )
3455, 6, 7, 8, 9algrp1 14533 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  NN )  ->  ( K `
 ( i  +  1 ) )  =  ( H `  ( K `  i )
) )
346240, 345sylan2 477 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  ( K `  ( i  +  1 ) )  =  ( H `  ( K `  i ) ) )
347344, 346eleqtrrd 2532 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) )  e.  ( K `  ( i  +  1 ) ) )
348240, 285sylan2 477 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  ( K `  ( i  +  1 ) )  e.  U )
34996, 97, 98, 99, 100, 73, 101, 4, 102ovolicc2lem1 22470 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( K `  ( i  +  1 ) )  e.  U
)  ->  ( ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) )  e.  ( K `  ( i  +  1 ) )  <-> 
( ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  e.  RR  /\  ( 1st `  ( F `  ( G `  ( K `
 ( i  +  1 ) ) ) ) )  <  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) )  /\  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) )  <  ( 2nd `  ( F `  ( G `  ( K `
 ( i  +  1 ) ) ) ) ) ) ) )
350348, 349syldan 473 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  (
( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  e.  ( K `  ( i  +  1 ) )  <->  ( ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) )  e.  RR  /\  ( 1st `  ( F `  ( G `  ( K `  (
i  +  1 ) ) ) ) )  <  ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  /\  ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  <  ( 2nd `  ( F `  ( G `  ( K `  (
i  +  1 ) ) ) ) ) ) ) )
351347, 350mpbid 214 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  (
( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  e.  RR  /\  ( 1st `  ( F `  ( G `  ( K `
 ( i  +  1 ) ) ) ) )  <  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) )  /\  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) )  <  ( 2nd `  ( F `  ( G `  ( K `
 ( i  +  1 ) ) ) ) ) ) )
352351simp2d 1021 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  ( 1st `  ( F `  ( G `  ( K `
 ( i  +  1 ) ) ) ) )  <  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) ) )
353290, 241, 352ltled 9783 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  ( 1st `  ( F `  ( G `  ( K `
 ( i  +  1 ) ) ) ) )  <_  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) ) )
354239, 290, 241, 353fsumle 13859 . . . . . . . . 9  |-  ( ph  -> 
sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 1st `  ( F `  ( G `  ( K `  (
i  +  1 ) ) ) ) )  <_  sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) ) )
355242, 291subge0d 10203 . . . . . . . . 9  |-  ( ph  ->  ( 0  <_  ( sum_ i  e.  ( 1 ... ( M  - 
1 ) ) ( 2nd `  ( F `
 ( G `  ( K `  i ) ) ) )  -  sum_ i  e.  ( 1 ... ( M  - 
1 ) ) ( 1st `  ( F `
 ( G `  ( K `  ( i  +  1 ) ) ) ) ) )  <->  sum_ i  e.  ( 1 ... ( M  - 
1 ) ) ( 1st `  ( F `
 ( G `  ( K `  ( i  +  1 ) ) ) ) )  <_  sum_ i  e.  ( 1 ... ( M  - 
1 ) ) ( 2nd `  ( F `
 ( G `  ( K `  i ) ) ) ) ) )
356354, 355mpbird 236 . . . . . . . 8  |-  ( ph  ->  0  <_  ( sum_ i  e.  ( 1 ... ( M  - 
1 ) ) ( 2nd `  ( F `
 ( G `  ( K `  i ) ) ) )  -  sum_ i  e.  ( 1 ... ( M  - 
1 ) ) ( 1st `  ( F `
 ( G `  ( K `  ( i  +  1 ) ) ) ) ) ) )
357242, 291resubcld 10047 . . . . . . . . 9  |-  ( ph  ->  ( sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  -  sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 1st `  ( F `  ( G `  ( K `  (
i  +  1 ) ) ) ) ) )  e.  RR )
358205, 357addge01d 10201 . . . . . . . 8  |-  ( ph  ->  ( 0  <_  ( sum_ i  e.  ( 1 ... ( M  - 
1 ) ) ( 2nd `  ( F `
 ( G `  ( K `  i ) ) ) )  -  sum_ i  e.  ( 1 ... ( M  - 
1 ) ) ( 1st `  ( F `
 ( G `  ( K `  ( i  +  1 ) ) ) ) ) )  <-> 
( ( 2nd `  ( F `  ( G `  ( K `  M
) ) ) )  -  ( 1st `  ( F `  ( G `  C ) ) ) )  <_  ( (
( 2nd `  ( F `  ( G `  ( K `  M
) ) ) )  -  ( 1st `  ( F `  ( G `  C ) ) ) )  +  ( sum_ i  e.  ( 1 ... ( M  - 
1 ) ) ( 2nd `  ( F `
 ( G `  ( K `  i ) ) ) )  -  sum_ i  e.  ( 1 ... ( M  - 
1 ) ) ( 1st `  ( F `
 ( G `  ( K `  ( i  +  1 ) ) ) ) ) ) ) ) )
359356, 358mpbid 214 . . . . . . 7  |-  ( ph  ->  ( ( 2nd `  ( F `  ( G `  ( K `  M
) ) ) )  -  ( 1st `  ( F `  ( G `  C ) ) ) )  <_  ( (
( 2nd `  ( F `  ( G `  ( K `  M
) ) ) )  -  ( 1st `  ( F `  ( G `  C ) ) ) )  +  ( sum_ i  e.  ( 1 ... ( M  - 
1 ) ) ( 2nd `  ( F `
 ( G `  ( K `  i ) ) ) )  -  sum_ i  e.  ( 1 ... ( M  - 
1 ) ) ( 1st `  ( F `
 ( G `  ( K `  ( i  +  1 ) ) ) ) ) ) ) )
360158, 205, 296, 311, 359letrd 9792 . . . . . 6  |-  ( ph  ->  ( B  -  A
)  <_  ( (
( 2nd `  ( F `  ( G `  ( K `  M
) ) ) )  -  ( 1st `  ( F `  ( G `  C ) ) ) )  +  ( sum_ i  e.  ( 1 ... ( M  - 
1 ) ) ( 2nd `  ( F `
 ( G `  ( K `  i ) ) ) )  -  sum_ i  e.  ( 1 ... ( M  - 
1 ) ) ( 1st `  ( F `
 ( G `  ( K `  ( i  +  1 ) ) ) ) ) ) ) )
361360, 295breqtrrd 4429 . . . . 5  |-  ( ph  ->  ( B  -  A
)  <_  sum_ j  e.  ( ( G  o.  K ) " (
1 ... M ) ) ( ( ( abs 
o.  -  )  o.  F ) `  j
) )
362361adantr 467 . . . 4  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  ( B  -  A )  <_  sum_ j  e.  ( ( G  o.  K ) " (
1 ... M ) ) ( ( ( abs 
o.  -  )  o.  F ) `  j
) )
363 fzfid 12186 . . . . 5  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  ( 1 ... z )  e. 
Fin )
364170adantlr 721 . . . . 5  |-  ( ( ( ph  /\  (
z  e.  NN  /\  A. y  e.  ( ( G  o.  K )
" ( 1 ... M ) ) y  <  z ) )  /\  j  e.  ( 1 ... z ) )  ->  ( (
( abs  o.  -  )  o.  F ) `  j
)  e.  RR )
365169simprd 465 . . . . . 6  |-  ( (
ph  /\  j  e.  ( 1 ... z
) )  ->  0  <_  ( ( ( abs 
o.  -  )  o.  F ) `  j
) )
366365adantlr 721 . . . . 5  |-  ( ( ( ph  /\  (
z  e.  NN  /\  A. y  e.  ( ( G  o.  K )
" ( 1 ... M ) ) y  <  z ) )  /\  j  e.  ( 1 ... z ) )  ->  0  <_  ( ( ( abs  o.  -  )  o.  F
) `  j )
)
36724adantr 467 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  NN )  ->  ( ( G  o.  K )
" ( 1 ... M ) )  C_  NN )
368367sselda 3432 . . . . . . . . . . 11  |-  ( ( ( ph  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  y  e.  NN )
369368nnred 10624 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  y  e.  RR )
37031ad2antlr 733 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  z  e.  RR )
371 ltle 9722 . . . . . . . . . 10  |-  ( ( y  e.  RR  /\  z  e.  RR )  ->  ( y  <  z  ->  y  <_  z )
)
372369, 370, 371syl2anc 667 . . . . . . . . 9  |-  ( ( ( ph  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  ( y  <  z  ->  y  <_  z ) )
373368, 5syl6eleq 2539 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  y  e.  ( ZZ>= `  1 )
)
374 nnz 10959 . . . . . . . . . . 11  |-  ( z  e.  NN  ->  z  e.  ZZ )
375374ad2antlr 733 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  z  e.  ZZ )
376 elfz5 11792 . . . . . . . . . 10  |-  ( ( y  e.  ( ZZ>= ` 
1 )  /\  z  e.  ZZ )  ->  (
y  e.  ( 1 ... z )  <->  y  <_  z ) )
377373, 375, 376syl2anc 667 . . . . . . . . 9  |-  ( ( ( ph  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  ( y  e.  ( 1 ... z
)  <->  y  <_  z
) )
378372, 377sylibrd 238 . . . . . . . 8  |-  ( ( ( ph  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  ( y  <  z  ->  y  e.  ( 1 ... z
) ) )
379378ralimdva 2796 . . . . . . 7  |-  ( (
ph  /\  z  e.  NN )  ->  ( A. y  e.  ( ( G  o.  K ) " ( 1 ... M ) ) y  <  z  ->  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  e.  ( 1 ... z ) ) )
380379impr 625 . . . . . 6  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  e.  ( 1 ... z ) )
381 dfss3 3422 . . . . . 6  |-  ( ( ( G  o.  K
) " ( 1 ... M ) ) 
C_  ( 1 ... z )  <->  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  e.  ( 1 ... z ) )
382380, 381sylibr 216 . . . . 5  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  ( ( G  o.  K ) " ( 1 ... M ) )  C_  ( 1 ... z
) )
383363, 364, 366, 382fsumless 13856 . . . 4  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  sum_ j  e.  ( ( G  o.  K ) " (
1 ... M ) ) ( ( ( abs 
o.  -  )  o.  F ) `  j
)  <_  sum_ j  e.  ( 1 ... z
) ( ( ( abs  o.  -  )  o.  F ) `  j
) )
384185, 190, 172, 362, 383letrd 9792 . . 3  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  ( B  -  A )  <_  sum_ j  e.  ( 1 ... z
) ( ( ( abs  o.  -  )  o.  F ) `  j
) )
385 eqidd 2452 . . . . . 6  |-  ( ( ( ph  /\  (
z  e.  NN  /\  A. y  e.  ( ( G  o.  K )
" ( 1 ... M ) ) y  <  z ) )  /\  j  e.  ( 1 ... z ) )  ->  ( (
( abs  o.  -  )  o.  F ) `  j
)  =  ( ( ( abs  o.  -  )  o.  F ) `  j ) )
386 simprl 764 . . . . . . 7  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  z  e.  NN )
387386, 5syl6eleq 2539 . . . . . 6  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  z  e.  ( ZZ>= `  1 )
)
388364recnd 9669 . . . . . 6  |-  ( ( ( ph  /\  (
z  e.  NN  /\  A. y  e.  ( ( G  o.  K )
" ( 1 ... M ) ) y  <  z ) )  /\  j  e.  ( 1 ... z ) )  ->  ( (
( abs  o.  -  )  o.  F ) `  j
)  e.  CC )
389385, 387, 388fsumser 13796 . . . . 5  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  sum_ j  e.  ( 1 ... z
) ( ( ( abs  o.  -  )  o.  F ) `  j
)  =  (  seq 1 (  +  , 
( ( abs  o.  -  )  o.  F
) ) `  z
) )
39099fveq1i 5866 . . . . 5  |-  ( S `
 z )  =  (  seq 1 (  +  ,  ( ( abs  o.  -  )  o.  F ) ) `  z )
391389, 390syl6eqr 2503 . . . 4  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  sum_ j  e.  ( 1 ... z
) ( ( ( abs  o.  -  )  o.  F ) `  j
)  =  ( S `
 z ) )
392181adantr 467 . . . . 5  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  ran  S  C_  RR* )
393 ffn 5728 . . . . . . . 8  |-  ( S : NN --> ( 0 [,) +oo )  ->  S  Fn  NN )
394175, 393syl 17 . . . . . . 7  |-  ( ph  ->  S  Fn  NN )
395394adantr 467 . . . . . 6  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  S  Fn  NN )
396 fnfvelrn 6019 . . . . . 6  |-  ( ( S  Fn  NN  /\  z  e.  NN )  ->  ( S `  z
)  e.  ran  S
)
397395, 386, 396syl2anc 667 . . . . 5  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  ( S `  z )  e.  ran  S )
398 supxrub 11610 . . . . 5  |-  ( ( ran  S  C_  RR*  /\  ( S `  z )  e.  ran  S )  -> 
( S `  z
)  <_  sup ( ran  S ,  RR* ,  <  ) )
399392, 397, 398syl2anc 667 . . . 4  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  ( S `  z )  <_  sup ( ran  S ,  RR* ,  <  ) )
400391, 399eqbrtrd 4423 . . 3  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  sum_ j  e.  ( 1 ... z
) ( ( ( abs  o.  -  )  o.  F ) `  j
)  <_  sup ( ran  S ,  RR* ,  <  ) )
401160, 173, 184, 384, 400xrletrd 11459 . 2  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  ( B  -  A )  <_  sup ( ran  S ,  RR* ,  <  ) )
402157, 401rexlimddv 2883 1  |-  ( ph  ->  ( B  -  A
)  <_  sup ( ran  S ,  RR* ,  <  ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 188    /\ wa 371    /\ w3a 985    = wceq 1444    e. wcel 1887    =/= wne 2622   A.wral 2737   E.wrex 2738   {crab 2741    i^i cin 3403    C_ wss 3404   (/)c0 3731   ifcif 3881   ~Pcpw 3951   {csn 3968   U.cuni 4198   class class class wbr 4402    X. cxp 4832   `'ccnv 4833   ran crn 4835    |` cres