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

Theorem ovolicc2lem4 18895
Description: Lemma for ovolicc2 18897. (Contributed by Mario Carneiro, 14-Jun-2014.)
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 ) }
ovolicc2.17  |-  M  =  sup ( W ,  RR ,  `'  <  )
Assertion
Ref Expression
ovolicc2lem4  |-  ( 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 ovolicc2lem4
Dummy variables  m  x  y  z  i 
j are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-ima 4718 . . . . . 6  |-  ( ( G  o.  K )
" ( 1 ... M ) )  =  ran  ( ( G  o.  K )  |`  ( 1 ... M
) )
2 ovolicc2.8 . . . . . . . . 9  |-  ( ph  ->  G : U --> NN )
3 nnuz 10279 . . . . . . . . . . 11  |-  NN  =  ( ZZ>= `  1 )
4 ovolicc2.15 . . . . . . . . . . 11  |-  K  =  seq  1 ( ( H  o.  1st ) ,  ( NN  X.  { C } ) )
5 1z 10069 . . . . . . . . . . . 12  |-  1  e.  ZZ
65a1i 10 . . . . . . . . . . 11  |-  ( ph  ->  1  e.  ZZ )
7 ovolicc2.14 . . . . . . . . . . 11  |-  ( ph  ->  C  e.  T )
8 ovolicc2.11 . . . . . . . . . . 11  |-  ( ph  ->  H : T --> T )
93, 4, 6, 7, 8algrf 12759 . . . . . . . . . 10  |-  ( ph  ->  K : NN --> T )
10 ovolicc2.10 . . . . . . . . . . 11  |-  T  =  { u  e.  U  |  ( u  i^i  ( A [,] B
) )  =/=  (/) }
11 ssrab2 3271 . . . . . . . . . . 11  |-  { u  e.  U  |  (
u  i^i  ( A [,] B ) )  =/=  (/) }  C_  U
1210, 11eqsstri 3221 . . . . . . . . . 10  |-  T  C_  U
13 fss 5413 . . . . . . . . . 10  |-  ( ( K : NN --> T  /\  T  C_  U )  ->  K : NN --> U )
149, 12, 13sylancl 643 . . . . . . . . 9  |-  ( ph  ->  K : NN --> U )
15 fco 5414 . . . . . . . . 9  |-  ( ( G : U --> NN  /\  K : NN --> U )  ->  ( G  o.  K ) : NN --> NN )
162, 14, 15syl2anc 642 . . . . . . . 8  |-  ( ph  ->  ( G  o.  K
) : NN --> NN )
17 elfznn 10835 . . . . . . . . 9  |-  ( i  e.  ( 1 ... M )  ->  i  e.  NN )
1817ssriv 3197 . . . . . . . 8  |-  ( 1 ... M )  C_  NN
19 fssres 5424 . . . . . . . 8  |-  ( ( ( G  o.  K
) : NN --> NN  /\  ( 1 ... M
)  C_  NN )  ->  ( ( G  o.  K )  |`  (
1 ... M ) ) : ( 1 ... M ) --> NN )
2016, 18, 19sylancl 643 . . . . . . 7  |-  ( ph  ->  ( ( G  o.  K )  |`  (
1 ... M ) ) : ( 1 ... M ) --> NN )
21 frn 5411 . . . . . . 7  |-  ( ( ( G  o.  K
)  |`  ( 1 ... M ) ) : ( 1 ... M
) --> NN  ->  ran  ( ( G  o.  K )  |`  (
1 ... M ) ) 
C_  NN )
2220, 21syl 15 . . . . . 6  |-  ( ph  ->  ran  ( ( G  o.  K )  |`  ( 1 ... M
) )  C_  NN )
231, 22syl5eqss 3235 . . . . 5  |-  ( ph  ->  ( ( G  o.  K ) " (
1 ... M ) ) 
C_  NN )
24 nnssre 9766 . . . . 5  |-  NN  C_  RR
2523, 24syl6ss 3204 . . . 4  |-  ( ph  ->  ( ( G  o.  K ) " (
1 ... M ) ) 
C_  RR )
26 fzfid 11051 . . . . 5  |-  ( ph  ->  ( 1 ... M
)  e.  Fin )
27 fvres 5558 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( 1 ... M )  ->  (
( ( G  o.  K )  |`  (
1 ... M ) ) `
 i )  =  ( ( G  o.  K ) `  i
) )
2827adantl 452 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( ( G  o.  K )  |`  (
1 ... M ) ) `
 i )  =  ( ( G  o.  K ) `  i
) )
29 fvco3 5612 . . . . . . . . . . . . . . 15  |-  ( ( K : NN --> T  /\  i  e.  NN )  ->  ( ( G  o.  K ) `  i
)  =  ( G `
 ( K `  i ) ) )
309, 17, 29syl2an 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( G  o.  K
) `  i )  =  ( G `  ( K `  i ) ) )
3128, 30eqtrd 2328 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( ( G  o.  K )  |`  (
1 ... M ) ) `
 i )  =  ( G `  ( K `  i )
) )
3231adantrr 697 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
( ( ( G  o.  K )  |`  ( 1 ... M
) ) `  i
)  =  ( G `
 ( K `  i ) ) )
33 fvres 5558 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 1 ... M )  ->  (
( ( G  o.  K )  |`  (
1 ... M ) ) `
 j )  =  ( ( G  o.  K ) `  j
) )
3433ad2antll 709 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
( ( ( G  o.  K )  |`  ( 1 ... M
) ) `  j
)  =  ( ( G  o.  K ) `
 j ) )
35 elfznn 10835 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 1 ... M )  ->  j  e.  NN )
3635adantl 452 . . . . . . . . . . . . . 14  |-  ( ( i  e.  ( 1 ... M )  /\  j  e.  ( 1 ... M ) )  ->  j  e.  NN )
37 fvco3 5612 . . . . . . . . . . . . . 14  |-  ( ( K : NN --> T  /\  j  e.  NN )  ->  ( ( G  o.  K ) `  j
)  =  ( G `
 ( K `  j ) ) )
389, 36, 37syl2an 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
( ( G  o.  K ) `  j
)  =  ( G `
 ( K `  j ) ) )
3934, 38eqtrd 2328 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
( ( ( G  o.  K )  |`  ( 1 ... M
) ) `  j
)  =  ( G `
 ( K `  j ) ) )
4032, 39eqeq12d 2310 . . . . . . . . . . 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 ) ) ) )
41 fveq2 5541 . . . . . . . . . . . . 13  |-  ( ( G `  ( K `
 i ) )  =  ( G `  ( K `  j ) )  ->  ( F `  ( G `  ( K `  i )
) )  =  ( F `  ( G `
 ( K `  j ) ) ) )
4241fveq2d 5545 . . . . . . . . . . . 12  |-  ( ( G `  ( K `
 i ) )  =  ( G `  ( K `  j ) )  ->  ( 2nd `  ( F `  ( G `  ( K `  i ) ) ) )  =  ( 2nd `  ( F `  ( G `  ( K `  j ) ) ) ) )
4318a1i 10 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( 1 ... M
)  C_  NN )
44 elfznn 10835 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  e.  ( 1 ... M )  ->  n  e.  NN )
4544ad2antlr 707 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  n  e.  ( 1 ... M
) )  /\  m  e.  W )  ->  n  e.  NN )
4645nnred 9777 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  ( 1 ... M
) )  /\  m  e.  W )  ->  n  e.  RR )
47 ovolicc2.16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  W  =  { n  e.  NN  |  B  e.  ( K `  n ) }
48 ssrab2 3271 . . . . . . . . . . . . . . . . . . . . . . 23  |-  { n  e.  NN  |  B  e.  ( K `  n
) }  C_  NN
4947, 48eqsstri 3221 . . . . . . . . . . . . . . . . . . . . . 22  |-  W  C_  NN
5049, 24sstri 3201 . . . . . . . . . . . . . . . . . . . . 21  |-  W  C_  RR
51 ovolicc2.17 . . . . . . . . . . . . . . . . . . . . . 22  |-  M  =  sup ( W ,  RR ,  `'  <  )
5249, 3sseqtri 3223 . . . . . . . . . . . . . . . . . . . . . . 23  |-  W  C_  ( ZZ>= `  1 )
533uzinf 11044 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 1  e.  ZZ  ->  -.  NN  e.  Fin )
545, 53ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  -.  NN  e.  Fin
55 ovolicc2.6 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  U  e.  ( ~P
ran  ( (,)  o.  F )  i^i  Fin ) )
56 elin 3371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( U  e.  ( ~P ran  ( (,)  o.  F )  i^i  Fin )  <->  ( U  e.  ~P ran  ( (,) 
o.  F )  /\  U  e.  Fin )
)
5755, 56sylib 188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  ( U  e.  ~P ran  ( (,)  o.  F
)  /\  U  e.  Fin ) )
5857simprd 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  U  e.  Fin )
59 ssfi 7099 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( U  e.  Fin  /\  T  C_  U )  ->  T  e.  Fin )
6058, 12, 59sylancl 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  T  e.  Fin )
6160adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  W  =  (/) )  ->  T  e.  Fin )
629adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  W  =  (/) )  ->  K : NN
--> T )
63 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( K `  i )  =  ( K `  j )  ->  ( G `  ( K `  i ) )  =  ( G `  ( K `  j )
) )
6463fveq2d 5545 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( K `  i )  =  ( K `  j )  ->  ( F `  ( G `  ( K `  i
) ) )  =  ( F `  ( G `  ( K `  j ) ) ) )
6564fveq2d 5545 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( K `  i )  =  ( K `  j )  ->  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) )  =  ( 2nd `  ( F `
 ( G `  ( K `  j ) ) ) ) )
66 simpll 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  ph )
67 simprl 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  i  e.  NN )
68 ral0 3571 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  A. m  e.  (/)  n  <_  m
69 simplr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  W  =  (/) )
7069raleqdv 2755 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  ( A. m  e.  W  n  <_  m  <->  A. m  e.  (/)  n  <_  m ) )
7168, 70mpbiri 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  A. m  e.  W  n  <_  m )
7271ralrimivw 2640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  A. n  e.  NN  A. m  e.  W  n  <_  m
)
73 rabid2 2730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( NN  =  { n  e.  NN  |  A. m  e.  W  n  <_  m }  <->  A. n  e.  NN  A. m  e.  W  n  <_  m )
7472, 73sylibr 203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  NN  =  { n  e.  NN  |  A. m  e.  W  n  <_  m } )
7567, 74eleqtrd 2372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  i  e.  { n  e.  NN  |  A. m  e.  W  n  <_  m } )
76 simprr 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  j  e.  NN )
7776, 74eleqtrd 2372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  j  e.  { n  e.  NN  |  A. m  e.  W  n  <_  m } )
78 ovolicc.1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  A  e.  RR )
79 ovolicc.2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  B  e.  RR )
80 ovolicc.3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  A  <_  B )
81 ovolicc2.4 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  S  =  seq  1 (  +  ,  ( ( abs 
o.  -  )  o.  F ) )
82 ovolicc2.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  F : NN --> (  <_  i^i  ( RR  X.  RR ) ) )
83 ovolicc2.7 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  ( A [,] B
)  C_  U. U )
84 ovolicc2.9 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  t  e.  U )  ->  (
( (,)  o.  F
) `  ( G `  t ) )  =  t )
85 ovolicc2.12 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  t  e.  T )  ->  if ( ( 2nd `  ( F `  ( G `  t ) ) )  <_  B ,  ( 2nd `  ( F `
 ( G `  t ) ) ) ,  B )  e.  ( H `  t
) )
86 ovolicc2.13 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  A  e.  C )
8778, 79, 80, 81, 82, 55, 83, 2, 84, 10, 8, 85, 86, 7, 4, 47ovolicc2lem3 18894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) ) ) )
8866, 75, 77, 87syl12anc 1180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  ( i  =  j  <->  ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  =  ( 2nd `  ( F `  ( G `  ( K `  j
) ) ) ) ) )
8965, 88syl5ibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  ( ( K `  i )  =  ( K `  j )  ->  i  =  j ) )
9089ralrimivva 2648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  W  =  (/) )  ->  A. i  e.  NN  A. j  e.  NN  ( ( K `
 i )  =  ( K `  j
)  ->  i  =  j ) )
91 dff13 5799 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( K : NN -1-1-> T  <->  ( K : NN --> T  /\  A. i  e.  NN  A. j  e.  NN  ( ( K `
 i )  =  ( K `  j
)  ->  i  =  j ) ) )
9262, 90, 91sylanbrc 645 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  W  =  (/) )  ->  K : NN
-1-1-> T )
93 f1domg 6897 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( T  e.  Fin  ->  ( K : NN -1-1-> T  ->  NN 
~<_  T ) )
9461, 92, 93sylc 56 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  W  =  (/) )  ->  NN  ~<_  T )
95 domfi 7100 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( T  e.  Fin  /\  NN 
~<_  T )  ->  NN  e.  Fin )
9661, 94, 95syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  W  =  (/) )  ->  NN  e.  Fin )
9796ex 423 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( W  =  (/)  ->  NN  e.  Fin )
)
9897necon3bd 2496 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( -.  NN  e.  Fin  ->  W  =/=  (/) ) )
9954, 98mpi 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  W  =/=  (/) )
100 infmssuzcl 10317 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( W  C_  ( ZZ>= ` 
1 )  /\  W  =/=  (/) )  ->  sup ( W ,  RR ,  `'  <  )  e.  W
)
10152, 99, 100sylancr 644 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  sup ( W ,  RR ,  `'  <  )  e.  W )
10251, 101syl5eqel 2380 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  M  e.  W )
10350, 102sseldi 3191 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  M  e.  RR )
104103ad2antrr 706 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  ( 1 ... M
) )  /\  m  e.  W )  ->  M  e.  RR )
10550sseli 3189 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  e.  W  ->  m  e.  RR )
106105adantl 452 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  ( 1 ... M
) )  /\  m  e.  W )  ->  m  e.  RR )
107 elfzle2 10816 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  ( 1 ... M )  ->  n  <_  M )
108107ad2antlr 707 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  ( 1 ... M
) )  /\  m  e.  W )  ->  n  <_  M )
109 infmssuzle 10316 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( W  C_  ( ZZ>= ` 
1 )  /\  m  e.  W )  ->  sup ( W ,  RR ,  `'  <  )  <_  m
)
11052, 109mpan 651 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  e.  W  ->  sup ( W ,  RR ,  `'  <  )  <_  m
)
11151, 110syl5eqbr 4072 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  e.  W  ->  M  <_  m )
112111adantl 452 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  ( 1 ... M
) )  /\  m  e.  W )  ->  M  <_  m )
11346, 104, 106, 108, 112letrd 8989 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  n  e.  ( 1 ... M
) )  /\  m  e.  W )  ->  n  <_  m )
114113ralrimiva 2639 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  ( 1 ... M
) )  ->  A. m  e.  W  n  <_  m )
11543, 114ssrabdv 3265 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( 1 ... M
)  C_  { n  e.  NN  |  A. m  e.  W  n  <_  m } )
116115adantr 451 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
( 1 ... M
)  C_  { n  e.  NN  |  A. m  e.  W  n  <_  m } )
117 simprl 732 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
i  e.  ( 1 ... M ) )
118116, 117sseldd 3194 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
i  e.  { n  e.  NN  |  A. m  e.  W  n  <_  m } )
119 simprr 733 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
j  e.  ( 1 ... M ) )
120116, 119sseldd 3194 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
j  e.  { n  e.  NN  |  A. m  e.  W  n  <_  m } )
121118, 120jca 518 . . . . . . . . . . . . 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 } ) )
122121, 87syldan 456 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
( i  =  j  <-> 
( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  =  ( 2nd `  ( F `  ( G `  ( K `  j
) ) ) ) ) )
12342, 122syl5ibr 212 . . . . . . . . . . 11  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
( ( G `  ( K `  i ) )  =  ( G `
 ( K `  j ) )  -> 
i  =  j ) )
12440, 123sylbid 206 . . . . . . . . . 10  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
( ( ( ( G  o.  K )  |`  ( 1 ... M
) ) `  i
)  =  ( ( ( G  o.  K
)  |`  ( 1 ... M ) ) `  j )  ->  i  =  j ) )
125124ralrimivva 2648 . . . . . . . . 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 ) )
126 dff13 5799 . . . . . . . . 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 ) ) )
12720, 125, 126sylanbrc 645 . . . . . . . 8  |-  ( ph  ->  ( ( G  o.  K )  |`  (
1 ... M ) ) : ( 1 ... M ) -1-1-> NN )
128 f1f1orn 5499 . . . . . . . 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 ) ) )
129127, 128syl 15 . . . . . . 7  |-  ( ph  ->  ( ( G  o.  K )  |`  (
1 ... M ) ) : ( 1 ... M ) -1-1-onto-> ran  ( ( G  o.  K )  |`  ( 1 ... M
) ) )
130 f1oeq3 5481 . . . . . . . 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
) ) ) )
1311, 130ax-mp 8 . . . . . . 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
) ) )
132129, 131sylibr 203 . . . . . 6  |-  ( ph  ->  ( ( G  o.  K )  |`  (
1 ... M ) ) : ( 1 ... M ) -1-1-onto-> ( ( G  o.  K ) " (
1 ... M ) ) )
133 f1ofo 5495 . . . . . 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 ) ) )
134132, 133syl 15 . . . . 5  |-  ( ph  ->  ( ( G  o.  K )  |`  (
1 ... M ) ) : ( 1 ... M ) -onto-> ( ( G  o.  K )
" ( 1 ... M ) ) )
135 fofi 7158 . . . . 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 )
13626, 134, 135syl2anc 642 . . . 4  |-  ( ph  ->  ( ( G  o.  K ) " (
1 ... M ) )  e.  Fin )
137 fimaxre2 9718 . . . 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 )
13825, 136, 137syl2anc 642 . . 3  |-  ( ph  ->  E. x  e.  RR  A. y  e.  ( ( G  o.  K )
" ( 1 ... M ) ) y  <_  x )
139 arch 9978 . . . . . . 7  |-  ( x  e.  RR  ->  E. z  e.  NN  x  <  z
)
140139ad2antlr 707 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR )  /\  A. y  e.  ( ( G  o.  K ) " ( 1 ... M ) ) y  <_  x )  ->  E. z  e.  NN  x  <  z )
14125ad3antrrr 710 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K
) " ( 1 ... M ) ) )  ->  ( ( G  o.  K ) " ( 1 ... M ) )  C_  RR )
142 simpr 447 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K
) " ( 1 ... M ) ) )  ->  y  e.  ( ( G  o.  K ) " (
1 ... M ) ) )
143141, 142sseldd 3194 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K
) " ( 1 ... M ) ) )  ->  y  e.  RR )
144 simpllr 735 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K
) " ( 1 ... M ) ) )  ->  x  e.  RR )
145 nnre 9769 . . . . . . . . . . . . . . 15  |-  ( z  e.  NN  ->  z  e.  RR )
146145ad2antlr 707 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K
) " ( 1 ... M ) ) )  ->  z  e.  RR )
147 lelttr 8928 . . . . . . . . . . . . . 14  |-  ( ( y  e.  RR  /\  x  e.  RR  /\  z  e.  RR )  ->  (
( y  <_  x  /\  x  <  z )  ->  y  <  z
) )
148143, 144, 146, 147syl3anc 1182 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K
) " ( 1 ... M ) ) )  ->  ( (
y  <_  x  /\  x  <  z )  -> 
y  <  z )
)
149148ancomsd 440 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K
) " ( 1 ... M ) ) )  ->  ( (
x  <  z  /\  y  <_  x )  -> 
y  <  z )
)
150149expdimp 426 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  x  e.  RR )  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K
) " ( 1 ... M ) ) )  /\  x  < 
z )  ->  (
y  <_  x  ->  y  <  z ) )
151150an32s 779 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  x  e.  RR )  /\  z  e.  NN )  /\  x  <  z
)  /\  y  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  ( y  <_  x  ->  y  <  z ) )
152151ralimdva 2634 . . . . . . . . 9  |-  ( ( ( ( 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 ) )
153152impancom 427 . . . . . . . 8  |-  ( ( ( ( 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 ) )
154153an32s 779 . . . . . . 7  |-  ( ( ( ( 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 ) )
155154reximdva 2668 . . . . . 6  |-  ( ( ( 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 ) )
156140, 155mpd 14 . . . . 5  |-  ( ( ( 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 )
157156ex 423 . . . 4  |-  ( (
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 ) )
158157rexlimdva 2680 . . 3  |-  ( ph  ->  ( E. 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 ) )
159138, 158mpd 14 . 2  |-  ( ph  ->  E. z  e.  NN  A. y  e.  ( ( G  o.  K )
" ( 1 ... M ) ) y  <  z )
16079, 78resubcld 9227 . . . . . . 7  |-  ( ph  ->  ( B  -  A
)  e.  RR )
161160rexrd 8897 . . . . . 6  |-  ( ph  ->  ( B  -  A
)  e.  RR* )
162161adantr 451 . . . . 5  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  ( B  -  A )  e.  RR* )
163 fzfid 11051 . . . . . . . 8  |-  ( ph  ->  ( 1 ... z
)  e.  Fin )
164 elfznn 10835 . . . . . . . . . . 11  |-  ( j  e.  ( 1 ... z )  ->  j  e.  NN )
165 eqid 2296 . . . . . . . . . . . . . 14  |-  ( ( abs  o.  -  )  o.  F )  =  ( ( abs  o.  -  )  o.  F )
166165ovolfsf 18847 . . . . . . . . . . . . 13  |-  ( F : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  (
( abs  o.  -  )  o.  F ) : NN --> ( 0 [,)  +oo ) )
16782, 166syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( abs  o.  -  )  o.  F
) : NN --> ( 0 [,)  +oo ) )
168 ffvelrn 5679 . . . . . . . . . . . 12  |-  ( ( ( ( abs  o.  -  )  o.  F
) : NN --> ( 0 [,)  +oo )  /\  j  e.  NN )  ->  (
( ( abs  o.  -  )  o.  F
) `  j )  e.  ( 0 [,)  +oo ) )
169167, 168sylan 457 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  F ) `  j )  e.  ( 0 [,)  +oo )
)
170164, 169sylan2 460 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 1 ... z
) )  ->  (
( ( abs  o.  -  )  o.  F
) `  j )  e.  ( 0 [,)  +oo ) )
171 elrege0 10762 . . . . . . . . . 10  |-  ( ( ( ( abs  o.  -  )  o.  F
) `  j )  e.  ( 0 [,)  +oo ) 
<->  ( ( ( ( abs  o.  -  )  o.  F ) `  j
)  e.  RR  /\  0  <_  ( ( ( abs  o.  -  )  o.  F ) `  j
) ) )
172170, 171sylib 188 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 1 ... z
) )  ->  (
( ( ( abs 
o.  -  )  o.  F ) `  j
)  e.  RR  /\  0  <_  ( ( ( abs  o.  -  )  o.  F ) `  j
) ) )
173172simpld 445 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 1 ... z
) )  ->  (
( ( abs  o.  -  )  o.  F
) `  j )  e.  RR )
174163, 173fsumrecl 12223 . . . . . . 7  |-  ( ph  -> 
sum_ j  e.  ( 1 ... z ) ( ( ( abs 
o.  -  )  o.  F ) `  j
)  e.  RR )
175174adantr 451 . . . . . 6  |-  ( (
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 )
176175rexrd 8897 . . . . 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
)  e.  RR* )
177165, 81ovolsf 18848 . . . . . . . . . . 11  |-  ( F : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  S : NN --> ( 0 [,) 
+oo ) )
17882, 177syl 15 . . . . . . . . . 10  |-  ( ph  ->  S : NN --> ( 0 [,)  +oo ) )
179 frn 5411 . . . . . . . . . 10  |-  ( S : NN --> ( 0 [,)  +oo )  ->  ran  S 
C_  ( 0 [,) 
+oo ) )
180178, 179syl 15 . . . . . . . . 9  |-  ( ph  ->  ran  S  C_  (
0 [,)  +oo ) )
181 0re 8854 . . . . . . . . . 10  |-  0  e.  RR
182 pnfxr 10471 . . . . . . . . . 10  |-  +oo  e.  RR*
183 icossre 10746 . . . . . . . . . 10  |-  ( ( 0  e.  RR  /\  +oo 
e.  RR* )  ->  (
0 [,)  +oo )  C_  RR )
184181, 182, 183mp2an 653 . . . . . . . . 9  |-  ( 0 [,)  +oo )  C_  RR
185180, 184syl6ss 3204 . . . . . . . 8  |-  ( ph  ->  ran  S  C_  RR )
186 ressxr 8892 . . . . . . . 8  |-  RR  C_  RR*
187185, 186syl6ss 3204 . . . . . . 7  |-  ( ph  ->  ran  S  C_  RR* )
188 supxrcl 10649 . . . . . . 7  |-  ( ran 
S  C_  RR*  ->  sup ( ran  S ,  RR* ,  <  )  e.  RR* )
189187, 188syl 15 . . . . . 6  |-  ( ph  ->  sup ( ran  S ,  RR* ,  <  )  e.  RR* )
190189adantr 451 . . . . 5  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  sup ( ran  S ,  RR* ,  <  )  e.  RR* )
191160adantr 451 . . . . . 6  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  ( B  -  A )  e.  RR )
19223sselda 3193 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  j  e.  NN )
193184, 169sseldi 3191 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  F ) `  j )  e.  RR )
194192, 193syldan 456 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  ( (
( abs  o.  -  )  o.  F ) `  j
)  e.  RR )
195136, 194fsumrecl 12223 . . . . . . 7  |-  ( ph  -> 
sum_ j  e.  ( ( G  o.  K
) " ( 1 ... M ) ) ( ( ( abs 
o.  -  )  o.  F ) `  j
)  e.  RR )
196195adantr 451 . . . . . 6  |-  ( (
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 )
197 inss2 3403 . . . . . . . . . . . . 13  |-  (  <_  i^i  ( RR  X.  RR ) )  C_  ( RR  X.  RR )
198 fss 5413 . . . . . . . . . . . . 13  |-  ( ( F : NN --> (  <_  i^i  ( RR  X.  RR ) )  /\  (  <_  i^i  ( RR  X.  RR ) )  C_  ( RR  X.  RR ) )  ->  F : NN --> ( RR  X.  RR ) )
19982, 197, 198sylancl 643 . . . . . . . . . . . 12  |-  ( ph  ->  F : NN --> ( RR 
X.  RR ) )
20049, 102sseldi 3191 . . . . . . . . . . . . . 14  |-  ( ph  ->  M  e.  NN )
201 ffvelrn 5679 . . . . . . . . . . . . . 14  |-  ( ( K : NN --> U  /\  M  e.  NN )  ->  ( K `  M
)  e.  U )
20214, 200, 201syl2anc 642 . . . . . . . . . . . . 13  |-  ( ph  ->  ( K `  M
)  e.  U )
203 ffvelrn 5679 . . . . . . . . . . . . 13  |-  ( ( G : U --> NN  /\  ( K `  M )  e.  U )  -> 
( G `  ( K `  M )
)  e.  NN )
2042, 202, 203syl2anc 642 . . . . . . . . . . . 12  |-  ( ph  ->  ( G `  ( K `  M )
)  e.  NN )
205 ffvelrn 5679 . . . . . . . . . . . 12  |-  ( ( F : NN --> ( RR 
X.  RR )  /\  ( G `  ( K `
 M ) )  e.  NN )  -> 
( F `  ( G `  ( K `  M ) ) )  e.  ( RR  X.  RR ) )
206199, 204, 205syl2anc 642 . . . . . . . . . . 11  |-  ( ph  ->  ( F `  ( G `  ( K `  M ) ) )  e.  ( RR  X.  RR ) )
207 xp2nd 6166 . . . . . . . . . . 11  |-  ( ( F `  ( G `
 ( K `  M ) ) )  e.  ( RR  X.  RR )  ->  ( 2nd `  ( F `  ( G `  ( K `  M ) ) ) )  e.  RR )
208206, 207syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( 2nd `  ( F `  ( G `  ( K `  M
) ) ) )  e.  RR )
20912, 7sseldi 3191 . . . . . . . . . . . . 13  |-  ( ph  ->  C  e.  U )
210 ffvelrn 5679 . . . . . . . . . . . . 13  |-  ( ( G : U --> NN  /\  C  e.  U )  ->  ( G `  C
)  e.  NN )
2112, 209, 210syl2anc 642 . . . . . . . . . . . 12  |-  ( ph  ->  ( G `  C
)  e.  NN )
212 ffvelrn 5679 . . . . . . . . . . . 12  |-  ( ( F : NN --> ( RR 
X.  RR )  /\  ( G `  C )  e.  NN )  -> 
( F `  ( G `  C )
)  e.  ( RR 
X.  RR ) )
213199, 211, 212syl2anc 642 . . . . . . . . . . 11  |-  ( ph  ->  ( F `  ( G `  C )
)  e.  ( RR 
X.  RR ) )
214 xp1st 6165 . . . . . . . . . . 11  |-  ( ( F `  ( G `
 C ) )  e.  ( RR  X.  RR )  ->  ( 1st `  ( F `  ( G `  C )
) )  e.  RR )
215213, 214syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( 1st `  ( F `  ( G `  C ) ) )  e.  RR )
216208, 215resubcld 9227 . . . . . . . . 9  |-  ( ph  ->  ( ( 2nd `  ( F `  ( G `  ( K `  M
) ) ) )  -  ( 1st `  ( F `  ( G `  C ) ) ) )  e.  RR )
217 fveq2 5541 . . . . . . . . . . . 12  |-  ( j  =  ( G `  ( K `  i ) )  ->  ( (
( abs  o.  -  )  o.  F ) `  j
)  =  ( ( ( abs  o.  -  )  o.  F ) `  ( G `  ( K `  i )
) ) )
218193recnd 8877 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  F ) `  j )  e.  CC )
219192, 218syldan 456 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  ( (
( abs  o.  -  )  o.  F ) `  j
)  e.  CC )
220217, 26, 132, 31, 219fsumf1o 12212 . . . . . . . . . . 11  |-  ( 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 ) ) ) )
22182adantr 451 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  F : NN --> (  <_  i^i  ( RR  X.  RR ) ) )
2222adantr 451 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  G : U --> NN )
223 ffvelrn 5679 . . . . . . . . . . . . . . 15  |-  ( ( K : NN --> U  /\  i  e.  NN )  ->  ( K `  i
)  e.  U )
22414, 17, 223syl2an 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( K `  i )  e.  U )
225 ffvelrn 5679 . . . . . . . . . . . . . 14  |-  ( ( G : U --> NN  /\  ( K `  i )  e.  U )  -> 
( G `  ( K `  i )
)  e.  NN )
226222, 224, 225syl2anc 642 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( G `  ( K `  i ) )  e.  NN )
227165ovolfsval 18846 . . . . . . . . . . . . 13  |-  ( ( 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
) ) ) ) ) )
228221, 226, 227syl2anc 642 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( ( abs  o.  -  )  o.  F
) `  ( G `  ( K `  i
) ) )  =  ( ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  -  ( 1st `  ( F `  ( G `  ( K `  i
) ) ) ) ) )
229228sumeq2dv 12192 . . . . . . . . . . 11  |-  ( 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
) ) ) ) ) )
230199adantr 451 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  NN )  ->  F : NN
--> ( RR  X.  RR ) )
2312adantr 451 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  NN )  ->  G : U
--> NN )
23214, 223sylan 457 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  NN )  ->  ( K `
 i )  e.  U )
233231, 232, 225syl2anc 642 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  NN )  ->  ( G `
 ( K `  i ) )  e.  NN )
234 ffvelrn 5679 . . . . . . . . . . . . . . . . 17  |-  ( ( F : NN --> ( RR 
X.  RR )  /\  ( G `  ( K `
 i ) )  e.  NN )  -> 
( F `  ( G `  ( K `  i ) ) )  e.  ( RR  X.  RR ) )
235230, 233, 234syl2anc 642 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  NN )  ->  ( F `
 ( G `  ( K `  i ) ) )  e.  ( RR  X.  RR ) )
236 xp2nd 6166 . . . . . . . . . . . . . . . 16  |-  ( ( F `  ( G `
 ( K `  i ) ) )  e.  ( RR  X.  RR )  ->  ( 2nd `  ( F `  ( G `  ( K `  i ) ) ) )  e.  RR )
237235, 236syl 15 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  NN )  ->  ( 2nd `  ( F `  ( G `  ( K `  i ) ) ) )  e.  RR )
23817, 237sylan2 460 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) )  e.  RR )
239238recnd 8877 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) )  e.  CC )
240199adantr 451 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  F : NN --> ( RR  X.  RR ) )
241240, 226, 234syl2anc 642 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( F `  ( G `  ( K `  i
) ) )  e.  ( RR  X.  RR ) )
242 xp1st 6165 . . . . . . . . . . . . . . 15  |-  ( ( F `  ( G `
 ( K `  i ) ) )  e.  ( RR  X.  RR )  ->  ( 1st `  ( F `  ( G `  ( K `  i ) ) ) )  e.  RR )
243241, 242syl 15 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( 1st `  ( F `  ( G `  ( K `
 i ) ) ) )  e.  RR )
244243recnd 8877 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( 1st `  ( F `  ( G `  ( K `
 i ) ) ) )  e.  CC )
24526, 239, 244fsumsub 12266 . . . . . . . . . . . 12  |-  ( 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 ) ) ) ) ) )
24652, 102sseldi 3191 . . . . . . . . . . . . . . 15  |-  ( ph  ->  M  e.  ( ZZ>= ` 
1 ) )
247 fveq2 5541 . . . . . . . . . . . . . . . . . 18  |-  ( i  =  M  ->  ( K `  i )  =  ( K `  M ) )
248247fveq2d 5545 . . . . . . . . . . . . . . . . 17  |-  ( i  =  M  ->  ( G `  ( K `  i ) )  =  ( G `  ( K `  M )
) )
249248fveq2d 5545 . . . . . . . . . . . . . . . 16  |-  ( i  =  M  ->  ( F `  ( G `  ( K `  i
) ) )  =  ( F `  ( G `  ( K `  M ) ) ) )
250249fveq2d 5545 . . . . . . . . . . . . . . 15  |-  ( i  =  M  ->  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) )  =  ( 2nd `  ( F `
 ( G `  ( K `  M ) ) ) ) )
251246, 239, 250fsumm1 12232 . . . . . . . . . . . . . 14  |-  ( 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
) ) ) ) ) )
252 fzfid 11051 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( 1 ... ( M  -  1 ) )  e.  Fin )
253 elfznn 10835 . . . . . . . . . . . . . . . . . 18  |-  ( i  e.  ( 1 ... ( M  -  1 ) )  ->  i  e.  NN )
254253, 237sylan2 460 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) )  e.  RR )
255252, 254fsumrecl 12223 . . . . . . . . . . . . . . . 16  |-  ( ph  -> 
sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  e.  RR )
256255recnd 8877 . . . . . . . . . . . . . . 15  |-  ( ph  -> 
sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  e.  CC )
257208recnd 8877 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 2nd `  ( F `  ( G `  ( K `  M
) ) ) )  e.  CC )
258256, 257addcomd 9030 . . . . . . . . . . . . . 14  |-  ( 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
) ) ) ) ) )
259251, 258eqtrd 2328 . . . . . . . . . . . . 13  |-  ( 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
) ) ) ) ) )
260 fveq2 5541 . . . . . . . . . . . . . . . . . 18  |-  ( i  =  1  ->  ( K `  i )  =  ( K ` 
1 ) )
261260fveq2d 5545 . . . . . . . . . . . . . . . . 17  |-  ( i  =  1  ->  ( G `  ( K `  i ) )  =  ( G `  ( K `  1 )
) )
262261fveq2d 5545 . . . . . . . . . . . . . . . 16  |-  ( i  =  1  ->  ( F `  ( G `  ( K `  i
) ) )  =  ( F `  ( G `  ( K `  1 ) ) ) )
263262fveq2d 5545 . . . . . . . . . . . . . . 15  |-  ( i  =  1  ->  ( 1st `  ( F `  ( G `  ( K `
 i ) ) ) )  =  ( 1st `  ( F `
 ( G `  ( K `  1 ) ) ) ) )
264246, 244, 263fsum1p 12234 . . . . . . . . . . . . . 14  |-  ( 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 ) ) ) ) ) )
2653, 4, 6, 7algr0 12758 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( K `  1
)  =  C )
266265fveq2d 5545 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( G `  ( K `  1 )
)  =  ( G `
 C ) )
267266fveq2d 5545 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( F `  ( G `  ( K `  1 ) ) )  =  ( F `
 ( G `  C ) ) )
268267fveq2d 5545 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1st `  ( F `  ( G `  ( K `  1
) ) ) )  =  ( 1st `  ( F `  ( G `  C ) ) ) )
2696peano2zd 10136 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( 1  +  1 )  e.  ZZ )
270200nnzd 10132 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  M  e.  ZZ )
271 fzp1ss 10853 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1  e.  ZZ  ->  (
( 1  +  1 ) ... M ) 
C_  ( 1 ... M ) )
2725, 271mp1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( 1  +  1 ) ... M
)  C_  ( 1 ... M ) )
273272sselda 3193 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( ( 1  +  1 ) ... M
) )  ->  i  e.  ( 1 ... M
) )
274273, 244syldan 456 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ( 1  +  1 ) ... M
) )  ->  ( 1st `  ( F `  ( G `  ( K `
 i ) ) ) )  e.  CC )
275 fveq2 5541 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  =  ( j  +  1 )  ->  ( K `  i )  =  ( K `  ( j  +  1 ) ) )
276275fveq2d 5545 . . . . . . . . . . . . . . . . . . 19  |-  ( i  =  ( j  +  1 )  ->  ( G `  ( K `  i ) )  =  ( G `  ( K `  ( j  +  1 ) ) ) )
277276fveq2d 5545 . . . . . . . . . . . . . . . . . 18  |-  ( i  =  ( j  +  1 )  ->  ( F `  ( G `  ( K `  i
) ) )  =  ( F `  ( G `  ( K `  ( j  +  1 ) ) ) ) )
278277fveq2d 5545 . . . . . . . . . . . . . . . . 17  |-  ( i  =  ( j  +  1 )  ->  ( 1st `  ( F `  ( G `  ( K `
 i ) ) ) )  =  ( 1st `  ( F `
 ( G `  ( K `  ( j  +  1 ) ) ) ) ) )
2796, 269, 270, 274, 278fsumshftm 12259 . . . . . . . . . . . . . . . 16  |-  ( 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 ) ) ) ) ) )
280 ax-1cn 8811 . . . . . . . . . . . . . . . . . . . 20  |-  1  e.  CC
281 pncan 9073 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 1  e.  CC  /\  1  e.  CC )  ->  ( ( 1  +  1 )  -  1 )  =  1 )
282280, 280, 281mp2an 653 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 1  +  1 )  -  1 )  =  1
283282oveq1i 5884 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 1  +  1 )  -  1 ) ... ( M  - 
1 ) )  =  ( 1 ... ( M  -  1 ) )
284283sumeq1i 12187 . . . . . . . . . . . . . . . . 17  |-  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 ) ) ) ) )
285 oveq1 5881 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  =  i  ->  (
j  +  1 )  =  ( i  +  1 ) )
286285fveq2d 5545 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  =  i  ->  ( K `  ( j  +  1 ) )  =  ( K `  ( i  +  1 ) ) )
287286fveq2d 5545 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  i  ->  ( G `  ( K `  ( j  +  1 ) ) )  =  ( G `  ( K `  ( i  +  1 ) ) ) )
288287fveq2d 5545 . . . . . . . . . . . . . . . . . . 19  |-  ( j  =  i  ->  ( F `  ( G `  ( K `  (
j  +  1 ) ) ) )  =  ( F `  ( G `  ( K `  ( i  +  1 ) ) ) ) )
289288fveq2d 5545 . . . . . . . . . . . . . . . . . 18  |-  ( j  =  i  ->  ( 1st `  ( F `  ( G `  ( K `
 ( j  +  1 ) ) ) ) )  =  ( 1st `  ( F `
 ( G `  ( K `  ( i  +  1 ) ) ) ) ) )
290289cbvsumv 12185 . . . . . . . . . . . . . . . . 17  |-  sum_ j  e.  ( 1 ... ( M  -  1 ) ) ( 1st `  ( F `  ( G `  ( K `  (
j  +  1 ) ) ) ) )  =  sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 1st `  ( F `  ( G `  ( K `  (
i  +  1 ) ) ) ) )
291284, 290eqtri 2316 . . . . . . . . . . . . . . . 16  |-  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 ) ) ) ) )
292279, 291syl6eq 2344 . . . . . . . . . . . . . . 15  |-  ( ph  -> 
sum_ i  e.  ( ( 1  +  1 ) ... M ) ( 1st `  ( F `  ( G `  ( K `  i
) ) ) )  =  sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 1st `  ( F `  ( G `  ( K `  (
i  +  1 ) ) ) ) ) )
293268, 292oveq12d 5892 . . . . . . . . . . . . . 14  |-  ( 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 ) ) ) ) ) ) )
294264, 293eqtrd 2328 . . . . . . . . . . . . 13  |-  ( 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 ) ) ) ) ) ) )
295259, 294oveq12d 5892 . . . . . . . . . . . 12  |-  ( 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 ) ) ) ) ) ) ) )
296215recnd 8877 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1st `  ( F `  ( G `  C ) ) )  e.  CC )
297 peano2nn 9774 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  e.  NN  ->  (
i  +  1 )  e.  NN )
298 ffvelrn 5679 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( K : NN --> U  /\  ( i  +  1 )  e.  NN )  ->  ( K `  ( i  +  1 ) )  e.  U
)
29914, 297, 298syl2an 463 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  NN )  ->  ( K `
 ( i  +  1 ) )  e.  U )
300 ffvelrn 5679 . . . . . . . . . . . . . . . . . . 19  |-  ( ( G : U --> NN  /\  ( K `  ( i  +  1 ) )  e.  U )  -> 
( G `  ( K `  ( i  +  1 ) ) )  e.  NN )
301231, 299, 300syl2anc 642 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  NN )  ->  ( G `
 ( K `  ( i  +  1 ) ) )  e.  NN )
302 ffvelrn 5679 . . . . . . . . . . . . . . . . . 18  |-  ( ( F : NN --> ( RR 
X.  RR )  /\  ( G `  ( K `
 ( i  +  1 ) ) )  e.  NN )  -> 
( F `  ( G `  ( K `  ( i  +  1 ) ) ) )  e.  ( RR  X.  RR ) )
303230, 301, 302syl2anc 642 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  NN )  ->  ( F `
 ( G `  ( K `  ( i  +  1 ) ) ) )  e.  ( RR  X.  RR ) )
304 xp1st 6165 . . . . . . . . . . . . . . . . 17  |-  ( ( F `  ( G `
 ( K `  ( i  +  1 ) ) ) )  e.  ( RR  X.  RR )  ->  ( 1st `  ( F `  ( G `  ( K `  ( i  +  1 ) ) ) ) )  e.  RR )
305303, 304syl 15 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  NN )  ->  ( 1st `  ( F `  ( G `  ( K `  ( i  +  1 ) ) ) ) )  e.  RR )
306253, 305sylan2 460 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  ( 1st `  ( F `  ( G `  ( K `
 ( i  +  1 ) ) ) ) )  e.  RR )
307252, 306fsumrecl 12223 . . . . . . . . . . . . . 14  |-  ( ph  -> 
sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 1st `  ( F `  ( G `  ( K `  (
i  +  1 ) ) ) ) )  e.  RR )
308307recnd 8877 . . . . . . . . . . . . 13  |-  ( ph  -> 
sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 1st `  ( F `  ( G `  ( K `  (
i  +  1 ) ) ) ) )  e.  CC )
309257, 256, 296, 308addsub4d 9220 . . . . . . . . . . . 12  |-  ( 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 ) ) ) ) ) ) ) )
310245, 295, 3093eqtrd 2332 . . . . . . . . . . 11  |-  ( 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 ) ) ) ) ) ) ) )
311220, 229, 3103eqtrd 2332 . . . . . . . . . 10  |-  ( 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 ) ) ) ) ) ) ) )
312311, 195eqeltrrd 2371 . . . . . . . . 9  |-  ( 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 )
313 fveq2 5541 . . . . . . . . . . . . . . . . 17  |-  ( n  =  M  ->  ( K `  n )  =  ( K `  M ) )
314313eleq2d 2363 . . . . . . . . . . . . . . . 16  |-  ( n  =  M  ->  ( B  e.  ( K `  n )  <->  B  e.  ( K `  M ) ) )
315314, 47elrab2 2938 . . . . . . . . . . . . . . 15  |-  ( M  e.  W  <->  ( M  e.  NN  /\  B  e.  ( K `  M
) ) )
316102, 315sylib 188 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( M  e.  NN  /\  B  e.  ( K `
 M ) ) )
317316simprd 449 . . . . . . . . . . . . 13  |-  ( ph  ->  B  e.  ( K `
 M ) )
31878, 79, 80, 81, 82, 55, 83, 2, 84ovolicc2lem1 18892 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( K `  M )  e.  U
)  ->  ( B  e.  ( K `  M
)  <->  ( B  e.  RR  /\  ( 1st `  ( F `  ( G `  ( K `  M ) ) ) )  <  B  /\  B  <  ( 2nd `  ( F `  ( G `  ( K `  M
) ) ) ) ) ) )
319202, 318mpdan 649 . . . . . . . . . . . . 13  |-  ( ph  ->  ( B  e.  ( K `  M )  <-> 
( B  e.  RR  /\  ( 1st `  ( F `  ( G `  ( K `  M
) ) ) )  <  B  /\  B  <  ( 2nd `  ( F `  ( G `  ( K `  M
) ) ) ) ) ) )
320317, 319mpbid 201 . . . . . . . . . . . 12  |-  ( ph  ->  ( B  e.  RR  /\  ( 1st `  ( F `  ( G `  ( K `  M
) ) ) )  <  B  /\  B  <  ( 2nd `  ( F `  ( G `  ( K `  M
) ) ) ) ) )
321320simp3d 969 . . . . . . . . . . 11  |-  ( ph  ->  B  <  ( 2nd `  ( F `  ( G `  ( K `  M ) ) ) ) )
32278, 79, 80, 81, 82, 55, 83, 2, 84ovolicc2lem1 18892 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  C  e.  U )  ->  ( A  e.  C  <->  ( A  e.  RR  /\  ( 1st `  ( F `  ( G `  C )
) )  <  A  /\  A  <  ( 2nd `  ( F `  ( G `  C )
) ) ) ) )
323209, 322mpdan 649 . . . . . . . . . . . . 13  |-  ( ph  ->  ( A  e.  C  <->  ( A  e.  RR  /\  ( 1st `  ( F `
 ( G `  C ) ) )  <  A  /\  A  <  ( 2nd `  ( F `  ( G `  C ) ) ) ) ) )
32486, 323mpbid 201 . . . . . . . . . . . 12  |-  ( ph  ->  ( A  e.  RR  /\  ( 1st `  ( F `  ( G `  C ) ) )  <  A  /\  A  <  ( 2nd `  ( F `  ( G `  C ) ) ) ) )
325324simp2d 968 . . . . . . . . . . 11  |-  ( ph  ->  ( 1st `  ( F `  ( G `  C ) ) )  <  A )
32679, 215, 208, 78, 321, 325lt2subd 9411 . . . . . . . . . 10  |-  ( ph  ->  ( B  -  A
)  <  ( ( 2nd `  ( F `  ( G `  ( K `
 M ) ) ) )  -  ( 1st `  ( F `  ( G `  C ) ) ) ) )
327160, 216, 326ltled 8983 . . . . . . . . 9  |-  ( ph  ->  ( B  -  A
)  <_  ( ( 2nd `  ( F `  ( G `  ( K `
 M ) ) ) )  -  ( 1st `  ( F `  ( G `  C ) ) ) ) )
328253adantl 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  i  e.  NN )
329 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  i  e.  ( 1 ... ( M  -  1 ) ) )
330270adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  M  e.  ZZ )
331 elfzm11 10869 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( 1  e.  ZZ  /\  M  e.  ZZ )  ->  ( i  e.  ( 1 ... ( M  -  1 ) )  <-> 
( i  e.  ZZ  /\  1  <_  i  /\  i  <  M ) ) )
3325, 330, 331sylancr 644 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  (
i  e.  ( 1 ... ( M  - 
1 ) )  <->  ( i  e.  ZZ  /\  1  <_ 
i  /\  i  <  M ) ) )
333329, 332mpbid 201 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  (
i  e.  ZZ  /\  1  <_  i  /\  i  <  M ) )
334333simp3d 969 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  i  <  M )
335328nnred 9777 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  i  e.  RR )
336103adantr 451 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  M  e.  RR )
337335, 336ltnled 8982 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  (
i  <  M  <->  -.  M  <_  i ) )
338334, 337mpbid 201 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  -.  M  <_  i )
339 infmssuzle 10316 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( W  C_  ( ZZ>= ` 
1 )  /\  i  e.  W )  ->  sup ( W ,  RR ,  `'  <  )  <_  i
)
34052, 339mpan 651 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( i  e.  W  ->  sup ( W ,  RR ,  `'  <  )  <_  i
)
34151, 340syl5eqbr 4072 . . . . . . . . . . . . . . . . . . . . 21  |-  ( i  e.  W  ->  M  <_  i )
342338, 341nsyl 113 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  -.  i  e.  W )
343328, 342jca 518 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  (
i  e.  NN  /\  -.  i  e.  W
) )
34478, 79, 80, 81, 82, 55, 83, 2, 84, 10, 8, 85, 86, 7, 4, 47ovolicc2lem2 18893 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( i  e.  NN  /\  -.  i  e.  W ) )  -> 
( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  <_  B )
345343, 344syldan 456 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) )  <_  B
)
346 iftrue 3584 . . . . . . . . . . . . . . . . . 18  |-  ( ( 2nd `  ( F `
 ( G `  ( K `  i ) ) ) )  <_  B  ->  if ( ( 2nd `  ( F `
 ( G `  ( K `  i ) ) ) )  <_  B ,  ( 2nd `  ( F `  ( G `  ( K `  i ) ) ) ) ,  B )  =  ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) ) )
347345, 346syl 15 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  if ( ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  <_  B ,  ( 2nd `  ( F `
 ( G `  ( K `  i ) ) ) ) ,  B )  =  ( 2nd `  ( F `
 ( G `  ( K `  i ) ) ) ) )
348 ffvelrn 5679 . . . . . . . . . . . . . . . . . . 19  |-  ( ( K : NN --> T  /\  i  e.  NN )  ->  ( K `  i
)  e.  T )
3499, 253, 348syl2an 463 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  ( K `  i )  e.  T )
35085ralrimiva 2639 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  A. t  e.  T  if ( ( 2nd `  ( F `  ( G `  t ) ) )  <_  B ,  ( 2nd `  ( F `
 ( G `  t ) ) ) ,  B )  e.  ( H `  t
) )
351350adantr 451 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  A. t  e.  T  if (
( 2nd `  ( F `  ( G `  t ) ) )  <_  B ,  ( 2nd `  ( F `
 ( G `  t ) ) ) ,  B )  e.  ( H `  t
) )
352 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( t  =  ( K `  i )  ->  ( G `  t )  =  ( G `  ( K `  i ) ) )
353352fveq2d 5545 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( t  =  ( K `  i )  ->  ( F `  ( G `  t ) )  =  ( F `  ( G `  ( K `  i ) ) ) )
354353fveq2d 5545 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( t  =  ( K `  i )  ->  ( 2nd `  ( F `  ( G `  t ) ) )  =  ( 2nd `  ( F `
 ( G `  ( K `  i ) ) ) ) )
355354breq1d 4049 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  =  ( K `  i )  ->  (
( 2nd `  ( F `  ( G `  t ) ) )  <_  B  <->  ( 2nd `  ( F `  ( G `  ( K `  i ) ) ) )  <_  B )
)
356 eqidd 2297 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  =  ( K `  i )  ->  B  =  B )
357355, 354, 356ifbieq12d 3600 . . . . . . . . . . . . . . . . . . . 20  |-  ( 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 ) )
358 fveq2 5541 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  ( K `  i )  ->  ( H `  t )  =  ( H `  ( K `  i ) ) )
359357, 358eleq12d 2364 . . . . . . . . . . . . . . . . . . 19  |-  ( 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 )
) ) )
360359rspcv 2893 . . . . . . . . . . . . . . . . . 18  |-  ( ( 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 ) ) ) )
361349, 351, 360sylc 56 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  if ( ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  <_  B ,  ( 2nd `  ( F `
 ( G `  ( K `  i ) ) ) ) ,  B )  e.  ( H `  ( K `
 i ) ) )
362347, 361eqeltrrd 2371 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) )  e.  ( H `  ( K `
 i ) ) )
3633, 4, 6, 7, 8algrp1 12760 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  NN )  ->  ( K `
 ( i  +  1 ) )  =  ( H `  ( K `  i )
) )
364253, 363sylan2 460 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  ( K `  ( i  +  1 ) )  =  ( H `  ( K `  i ) ) )
365362, 364eleqtrrd 2373 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) )  e.  ( K `  ( i  +  1 ) ) )
366253, 299sylan2 460 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  ( K `  ( i  +  1 ) )  e.  U )
36778, 79, 80, 81, 82, 55, 83, 2, 84ovolicc2lem1 18892 . . . . . . . . . . . . . . . 16  |-  ( (
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 ) ) ) ) ) ) ) )
368366, 367syldan 456 . . . . . . . . . . . . . . 15  |-  ( (
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 ) ) ) ) ) ) ) )
369365, 368mpbid 201 . . . . . . . . . . . . . 14  |-  ( (
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 ) ) ) ) ) ) )
370369simp2d 968 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  ( 1st `  ( F `  ( G `  ( K `
 ( i  +  1 ) ) ) ) )  <  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) ) )
371306, 254, 370ltled 8983 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  ( 1st `  ( F `  ( G `  ( K `
 ( i  +  1 ) ) ) ) )  <_  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) ) )
372252, 306, 254, 371fsumle 12273 . . . . . . . . . . 11  |-  ( ph  -> 
sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 1st `  ( F `  ( G `  ( K `  (
i  +  1 ) ) ) ) )  <_  sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) ) )
373255, 307subge0d 9378 . . . . . . . . . . 11  |-  ( 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 ) ) ) ) ) )
374372, 373mpbird 223 . . . . . . . . . 10  |-  ( 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 ) ) ) ) ) ) )
375255, 307resubcld 9227 . . . . . . . . . . 11  |-  ( 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 )
376216, 375addge01d 9376 . . . . . . . . . 10  |-  ( 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 ) ) ) ) ) ) ) ) )
377374, 376mpbid 201 . . . . . . . . 9  |-  ( 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 ) ) ) ) ) ) ) )
378160, 216, 312, 327, 377letrd 8989 . . . . . . . 8  |-  ( 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 ) ) ) ) ) ) ) )
379378, 311breqtrrd 4065 . . . . . . 7  |-  ( ph  ->  ( B  -  A
)  <_  sum_ j  e.  ( ( G  o.  K ) " (
1 ... M ) ) ( ( ( abs 
o.  -  )  o.  F ) `  j
) )
380379adantr 451 . . . . . 6  |-  ( (
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
) )
381 fzfid 11051 . . . . . . 7  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  ( 1 ... z )  e. 
Fin )
382173adantlr 695 . . . . . . 7  |-  ( ( ( 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 )
383172simprd 449 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 1 ... z
) )  ->  0  <_  ( ( ( abs 
o.  -  )  o.  F ) `  j
) )
384383adantlr 695 . . . . . . 7  |-  ( ( ( ph  /\  (
z  e.  NN  /\  A. y  e.  ( ( G  o.  K )
" ( 1 ... M ) ) y  <  z ) )  /\  j  e.  ( 1 ... z ) )  ->  0  <_  ( ( ( abs  o.  -  )  o.  F
) `  j )
)
38523adantr 451 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  z  e.  NN )  ->  ( ( G  o.  K )
" ( 1 ... M ) )  C_  NN )
386385sselda 3193 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  y  e.  NN )
387386nnred 9777 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  y  e.  RR )
388145ad2antlr 707 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  z  e.  RR )
389 ltle 8926 . . . . . . . . . . . 12  |-  ( ( y  e.  RR  /\  z  e.  RR )  ->  ( y  <  z  ->  y  <_  z )
)
390387, 388, 389syl2anc 642 . . . . . . . . . . 11  |-  ( ( ( ph  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  ( y  <  z  ->  y  <_  z ) )
391386, 3syl6eleq 2386 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  y  e.  ( ZZ>= `  1 )
)
392 nnz 10061 . . . . . . . . . . . . 13  |-  ( z  e.  NN  ->  z  e.  ZZ )
393392ad2antlr 707 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  z  e.  ZZ )
394 elfz5 10806 . . . . . . . . . . . 12  |-  ( ( y  e.  ( ZZ>= ` 
1 )  /\  z  e.  ZZ )  ->  (
y  e.  ( 1 ... z )  <->  y  <_  z ) )
395391, 393, 394syl2anc 642 . . . . . . . . . . 11  |-  ( ( ( ph  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  ( y  e.  ( 1 ... z
)  <->  y  <_  z
) )
396390, 395sylibrd 225 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  ( y  <  z  ->  y  e.  ( 1 ... z
) ) )
397396ralimdva 2634 . . . . . . . . 9  |-  ( (
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 ) ) )
398397impr 602 . . . . . . . 8  |-  ( (
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 ) )
399 dfss3 3183 . . . . . . . 8  |-  ( ( ( G  o.  K
) " ( 1 ... M ) ) 
C_  ( 1 ... z )  <->  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  e.  ( 1 ... z ) )
400398, 399sylibr 203 . . . . . . 7  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  ( ( G  o.  K ) " ( 1 ... M ) )  C_  ( 1 ... z
) )
401381, 382, 384, 400fsumless 12270 . . . . . 6  |-  ( (
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
) )
402191, 196, 175, 380, 401letrd 8989 . . . . 5  |-  ( (
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
) )
403 eqidd 2297 . . . . . . . 8  |-  ( ( ( ph  /\  (
z  e.  NN  /\  A. y  e.  ( ( G  o.  K )
" ( 1 ... M ) ) y  <  z ) )  /\  j  e.  ( 1 ... z ) )  ->