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

Theorem ovolicc2lem4 19416
Description: Lemma for ovolicc2 19418. (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 4891 . . . . . 6  |-  ( ( G  o.  K )
" ( 1 ... M ) )  =  ran  ( ( G  o.  K )  |`  ( 1 ... M
) )
2 ovolicc2.8 . . . . . . . . 9  |-  ( ph  ->  G : U --> NN )
3 nnuz 10521 . . . . . . . . . . 11  |-  NN  =  ( ZZ>= `  1 )
4 ovolicc2.15 . . . . . . . . . . 11  |-  K  =  seq  1 ( ( H  o.  1st ) ,  ( NN  X.  { C } ) )
5 1z 10311 . . . . . . . . . . . 12  |-  1  e.  ZZ
65a1i 11 . . . . . . . . . . 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 13064 . . . . . . . . . 10  |-  ( ph  ->  K : NN --> T )
10 ovolicc2.10 . . . . . . . . . . 11  |-  T  =  { u  e.  U  |  ( u  i^i  ( A [,] B
) )  =/=  (/) }
11 ssrab2 3428 . . . . . . . . . . 11  |-  { u  e.  U  |  (
u  i^i  ( A [,] B ) )  =/=  (/) }  C_  U
1210, 11eqsstri 3378 . . . . . . . . . 10  |-  T  C_  U
13 fss 5599 . . . . . . . . . 10  |-  ( ( K : NN --> T  /\  T  C_  U )  ->  K : NN --> U )
149, 12, 13sylancl 644 . . . . . . . . 9  |-  ( ph  ->  K : NN --> U )
15 fco 5600 . . . . . . . . 9  |-  ( ( G : U --> NN  /\  K : NN --> U )  ->  ( G  o.  K ) : NN --> NN )
162, 14, 15syl2anc 643 . . . . . . . 8  |-  ( ph  ->  ( G  o.  K
) : NN --> NN )
17 elfznn 11080 . . . . . . . . 9  |-  ( i  e.  ( 1 ... M )  ->  i  e.  NN )
1817ssriv 3352 . . . . . . . 8  |-  ( 1 ... M )  C_  NN
19 fssres 5610 . . . . . . . 8  |-  ( ( ( G  o.  K
) : NN --> NN  /\  ( 1 ... M
)  C_  NN )  ->  ( ( G  o.  K )  |`  (
1 ... M ) ) : ( 1 ... M ) --> NN )
2016, 18, 19sylancl 644 . . . . . . 7  |-  ( ph  ->  ( ( G  o.  K )  |`  (
1 ... M ) ) : ( 1 ... M ) --> NN )
21 frn 5597 . . . . . . 7  |-  ( ( ( G  o.  K
)  |`  ( 1 ... M ) ) : ( 1 ... M
) --> NN  ->  ran  ( ( G  o.  K )  |`  (
1 ... M ) ) 
C_  NN )
2220, 21syl 16 . . . . . 6  |-  ( ph  ->  ran  ( ( G  o.  K )  |`  ( 1 ... M
) )  C_  NN )
231, 22syl5eqss 3392 . . . . 5  |-  ( ph  ->  ( ( G  o.  K ) " (
1 ... M ) ) 
C_  NN )
24 nnssre 10004 . . . . 5  |-  NN  C_  RR
2523, 24syl6ss 3360 . . . 4  |-  ( ph  ->  ( ( G  o.  K ) " (
1 ... M ) ) 
C_  RR )
26 fzfid 11312 . . . . 5  |-  ( ph  ->  ( 1 ... M
)  e.  Fin )
27 fvres 5745 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( 1 ... M )  ->  (
( ( G  o.  K )  |`  (
1 ... M ) ) `
 i )  =  ( ( G  o.  K ) `  i
) )
2827adantl 453 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( ( G  o.  K )  |`  (
1 ... M ) ) `
 i )  =  ( ( G  o.  K ) `  i
) )
29 fvco3 5800 . . . . . . . . . . . . . . 15  |-  ( ( K : NN --> T  /\  i  e.  NN )  ->  ( ( G  o.  K ) `  i
)  =  ( G `
 ( K `  i ) ) )
309, 17, 29syl2an 464 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( G  o.  K
) `  i )  =  ( G `  ( K `  i ) ) )
3128, 30eqtrd 2468 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( ( G  o.  K )  |`  (
1 ... M ) ) `
 i )  =  ( G `  ( K `  i )
) )
3231adantrr 698 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
( ( ( G  o.  K )  |`  ( 1 ... M
) ) `  i
)  =  ( G `
 ( K `  i ) ) )
33 fvres 5745 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 1 ... M )  ->  (
( ( G  o.  K )  |`  (
1 ... M ) ) `
 j )  =  ( ( G  o.  K ) `  j
) )
3433ad2antll 710 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
( ( ( G  o.  K )  |`  ( 1 ... M
) ) `  j
)  =  ( ( G  o.  K ) `
 j ) )
35 elfznn 11080 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 1 ... M )  ->  j  e.  NN )
3635adantl 453 . . . . . . . . . . . . . 14  |-  ( ( i  e.  ( 1 ... M )  /\  j  e.  ( 1 ... M ) )  ->  j  e.  NN )
37 fvco3 5800 . . . . . . . . . . . . . 14  |-  ( ( K : NN --> T  /\  j  e.  NN )  ->  ( ( G  o.  K ) `  j
)  =  ( G `
 ( K `  j ) ) )
389, 36, 37syl2an 464 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
( ( G  o.  K ) `  j
)  =  ( G `
 ( K `  j ) ) )
3934, 38eqtrd 2468 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
( ( ( G  o.  K )  |`  ( 1 ... M
) ) `  j
)  =  ( G `
 ( K `  j ) ) )
4032, 39eqeq12d 2450 . . . . . . . . . . 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 5728 . . . . . . . . . . . . 13  |-  ( ( G `  ( K `
 i ) )  =  ( G `  ( K `  j ) )  ->  ( F `  ( G `  ( K `  i )
) )  =  ( F `  ( G `
 ( K `  j ) ) ) )
4241fveq2d 5732 . . . . . . . . . . . 12  |-  ( ( G `  ( K `
 i ) )  =  ( G `  ( K `  j ) )  ->  ( 2nd `  ( F `  ( G `  ( K `  i ) ) ) )  =  ( 2nd `  ( F `  ( G `  ( K `  j ) ) ) ) )
4318a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( 1 ... M
)  C_  NN )
44 elfznn 11080 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  e.  ( 1 ... M )  ->  n  e.  NN )
4544ad2antlr 708 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  n  e.  ( 1 ... M
) )  /\  m  e.  W )  ->  n  e.  NN )
4645nnred 10015 . . . . . . . . . . . . . . . . . . 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 3428 . . . . . . . . . . . . . . . . . . . . . . 23  |-  { n  e.  NN  |  B  e.  ( K `  n
) }  C_  NN
4947, 48eqsstri 3378 . . . . . . . . . . . . . . . . . . . . . 22  |-  W  C_  NN
5049, 24sstri 3357 . . . . . . . . . . . . . . . . . . . . 21  |-  W  C_  RR
51 ovolicc2.17 . . . . . . . . . . . . . . . . . . . . . 22  |-  M  =  sup ( W ,  RR ,  `'  <  )
5249, 3sseqtri 3380 . . . . . . . . . . . . . . . . . . . . . . 23  |-  W  C_  ( ZZ>= `  1 )
533uzinf 11305 . . . . . . . . . . . . . . . . . . . . . . . . 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 3530 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( U  e.  ( ~P ran  ( (,)  o.  F )  i^i  Fin )  <->  ( U  e.  ~P ran  ( (,) 
o.  F )  /\  U  e.  Fin )
)
5755, 56sylib 189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  ( U  e.  ~P ran  ( (,)  o.  F
)  /\  U  e.  Fin ) )
5857simprd 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  U  e.  Fin )
59 ssfi 7329 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( U  e.  Fin  /\  T  C_  U )  ->  T  e.  Fin )
6058, 12, 59sylancl 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  T  e.  Fin )
6160adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  W  =  (/) )  ->  T  e.  Fin )
629adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  W  =  (/) )  ->  K : NN
--> T )
63 fveq2 5728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( K `  i )  =  ( K `  j )  ->  ( G `  ( K `  i ) )  =  ( G `  ( K `  j )
) )
6463fveq2d 5732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( K `  i )  =  ( K `  j )  ->  ( F `  ( G `  ( K `  i
) ) )  =  ( F `  ( G `  ( K `  j ) ) ) )
6564fveq2d 5732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( K `  i )  =  ( K `  j )  ->  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) )  =  ( 2nd `  ( F `
 ( G `  ( K `  j ) ) ) ) )
66 simpll 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  ph )
67 simprl 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  i  e.  NN )
68 ral0 3732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  A. m  e.  (/)  n  <_  m
69 simplr 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  W  =  (/) )
7069raleqdv 2910 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  ( A. m  e.  W  n  <_  m  <->  A. m  e.  (/)  n  <_  m ) )
7168, 70mpbiri 225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  A. m  e.  W  n  <_  m )
7271ralrimivw 2790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  A. n  e.  NN  A. m  e.  W  n  <_  m
)
73 rabid2 2885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( NN  =  { n  e.  NN  |  A. m  e.  W  n  <_  m }  <->  A. n  e.  NN  A. m  e.  W  n  <_  m )
7472, 73sylibr 204 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  NN  =  { n  e.  NN  |  A. m  e.  W  n  <_  m } )
7567, 74eleqtrd 2512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  i  e.  { n  e.  NN  |  A. m  e.  W  n  <_  m } )
76 simprr 734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  j  e.  NN )
7776, 74eleqtrd 2512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 19415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  ( i  =  j  <->  ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  =  ( 2nd `  ( F `  ( G `  ( K `  j
) ) ) ) ) )
8965, 88syl5ibr 213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  ( ( K `  i )  =  ( K `  j )  ->  i  =  j ) )
9089ralrimivva 2798 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  W  =  (/) )  ->  A. i  e.  NN  A. j  e.  NN  ( ( K `
 i )  =  ( K `  j
)  ->  i  =  j ) )
91 dff13 6004 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 646 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  W  =  (/) )  ->  K : NN
-1-1-> T )
93 f1domg 7127 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( T  e.  Fin  ->  ( K : NN -1-1-> T  ->  NN 
~<_  T ) )
9461, 92, 93sylc 58 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  W  =  (/) )  ->  NN  ~<_  T )
95 domfi 7330 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( T  e.  Fin  /\  NN 
~<_  T )  ->  NN  e.  Fin )
9661, 94, 95syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  W  =  (/) )  ->  NN  e.  Fin )
9796ex 424 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( W  =  (/)  ->  NN  e.  Fin )
)
9897necon3bd 2638 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( -.  NN  e.  Fin  ->  W  =/=  (/) ) )
9954, 98mpi 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  W  =/=  (/) )
100 infmssuzcl 10559 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( W  C_  ( ZZ>= ` 
1 )  /\  W  =/=  (/) )  ->  sup ( W ,  RR ,  `'  <  )  e.  W
)
10152, 99, 100sylancr 645 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  sup ( W ,  RR ,  `'  <  )  e.  W )
10251, 101syl5eqel 2520 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  M  e.  W )
10350, 102sseldi 3346 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  M  e.  RR )
104103ad2antrr 707 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  ( 1 ... M
) )  /\  m  e.  W )  ->  M  e.  RR )
10550sseli 3344 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  e.  W  ->  m  e.  RR )
106105adantl 453 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  ( 1 ... M
) )  /\  m  e.  W )  ->  m  e.  RR )
107 elfzle2 11061 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  ( 1 ... M )  ->  n  <_  M )
108107ad2antlr 708 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  ( 1 ... M
) )  /\  m  e.  W )  ->  n  <_  M )
109 infmssuzle 10558 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( W  C_  ( ZZ>= ` 
1 )  /\  m  e.  W )  ->  sup ( W ,  RR ,  `'  <  )  <_  m
)
11052, 109mpan 652 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  e.  W  ->  sup ( W ,  RR ,  `'  <  )  <_  m
)
11151, 110syl5eqbr 4245 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  e.  W  ->  M  <_  m )
112111adantl 453 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  ( 1 ... M
) )  /\  m  e.  W )  ->  M  <_  m )
11346, 104, 106, 108, 112letrd 9227 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  n  e.  ( 1 ... M
) )  /\  m  e.  W )  ->  n  <_  m )
114113ralrimiva 2789 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  ( 1 ... M
) )  ->  A. m  e.  W  n  <_  m )
11543, 114ssrabdv 3422 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( 1 ... M
)  C_  { n  e.  NN  |  A. m  e.  W  n  <_  m } )
116115adantr 452 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
( 1 ... M
)  C_  { n  e.  NN  |  A. m  e.  W  n  <_  m } )
117 simprl 733 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
i  e.  ( 1 ... M ) )
118116, 117sseldd 3349 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
i  e.  { n  e.  NN  |  A. m  e.  W  n  <_  m } )
119 simprr 734 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
j  e.  ( 1 ... M ) )
120116, 119sseldd 3349 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
j  e.  { n  e.  NN  |  A. m  e.  W  n  <_  m } )
121118, 120jca 519 . . . . . . . . . . . . 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 457 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
( i  =  j  <-> 
( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  =  ( 2nd `  ( F `  ( G `  ( K `  j
) ) ) ) ) )
12342, 122syl5ibr 213 . . . . . . . . . . 11  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
( ( G `  ( K `  i ) )  =  ( G `
 ( K `  j ) )  -> 
i  =  j ) )
12440, 123sylbid 207 . . . . . . . . . 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 2798 . . . . . . . . 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 6004 . . . . . . . . 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 646 . . . . . . . 8  |-  ( ph  ->  ( ( G  o.  K )  |`  (
1 ... M ) ) : ( 1 ... M ) -1-1-> NN )
128 f1f1orn 5685 . . . . . . . 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 16 . . . . . . 7  |-  ( ph  ->  ( ( G  o.  K )  |`  (
1 ... M ) ) : ( 1 ... M ) -1-1-onto-> ran  ( ( G  o.  K )  |`  ( 1 ... M
) ) )
130 f1oeq3 5667 . . . . . . . 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 204 . . . . . 6  |-  ( ph  ->  ( ( G  o.  K )  |`  (
1 ... M ) ) : ( 1 ... M ) -1-1-onto-> ( ( G  o.  K ) " (
1 ... M ) ) )
133 f1ofo 5681 . . . . . 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 16 . . . . 5  |-  ( ph  ->  ( ( G  o.  K )  |`  (
1 ... M ) ) : ( 1 ... M ) -onto-> ( ( G  o.  K )
" ( 1 ... M ) ) )
135 fofi 7392 . . . . 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 643 . . . 4  |-  ( ph  ->  ( ( G  o.  K ) " (
1 ... M ) )  e.  Fin )
137 fimaxre2 9956 . . . 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 643 . . 3  |-  ( ph  ->  E. x  e.  RR  A. y  e.  ( ( G  o.  K )
" ( 1 ... M ) ) y  <_  x )
139 arch 10218 . . . . . . 7  |-  ( x  e.  RR  ->  E. z  e.  NN  x  <  z
)
140139ad2antlr 708 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR )  /\  A. y  e.  ( ( G  o.  K ) " ( 1 ... M ) ) y  <_  x )  ->  E. z  e.  NN  x  <  z )
14125ad3antrrr 711 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K
) " ( 1 ... M ) ) )  ->  ( ( G  o.  K ) " ( 1 ... M ) )  C_  RR )
142 simpr 448 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K
) " ( 1 ... M ) ) )  ->  y  e.  ( ( G  o.  K ) " (
1 ... M ) ) )
143141, 142sseldd 3349 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K
) " ( 1 ... M ) ) )  ->  y  e.  RR )
144 simpllr 736 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K
) " ( 1 ... M ) ) )  ->  x  e.  RR )
145 nnre 10007 . . . . . . . . . . . . . . 15  |-  ( z  e.  NN  ->  z  e.  RR )
146145ad2antlr 708 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K
) " ( 1 ... M ) ) )  ->  z  e.  RR )
147 lelttr 9165 . . . . . . . . . . . . . 14  |-  ( ( y  e.  RR  /\  x  e.  RR  /\  z  e.  RR )  ->  (
( y  <_  x  /\  x  <  z )  ->  y  <  z
) )
148143, 144, 146, 147syl3anc 1184 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K
) " ( 1 ... M ) ) )  ->  ( (
y  <_  x  /\  x  <  z )  -> 
y  <  z )
)
149148ancomsd 441 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K
) " ( 1 ... M ) ) )  ->  ( (
x  <  z  /\  y  <_  x )  -> 
y  <  z )
)
150149expdimp 427 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  x  e.  RR )  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K
) " ( 1 ... M ) ) )  /\  x  < 
z )  ->  (
y  <_  x  ->  y  <  z ) )
151150an32s 780 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  x  e.  RR )  /\  z  e.  NN )  /\  x  <  z
)  /\  y  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  ( y  <_  x  ->  y  <  z ) )
152151ralimdva 2784 . . . . . . . . 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 428 . . . . . . . 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 780 . . . . . . 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 2818 . . . . . 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 15 . . . . 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 424 . . . 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 2830 . . 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 15 . 2  |-  ( ph  ->  E. z  e.  NN  A. y  e.  ( ( G  o.  K )
" ( 1 ... M ) ) y  <  z )
16079, 78resubcld 9465 . . . . 5  |-  ( ph  ->  ( B  -  A
)  e.  RR )
161160rexrd 9134 . . . 4  |-  ( ph  ->  ( B  -  A
)  e.  RR* )
162161adantr 452 . . 3  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  ( B  -  A )  e.  RR* )
163 fzfid 11312 . . . . . 6  |-  ( ph  ->  ( 1 ... z
)  e.  Fin )
164 elfznn 11080 . . . . . . . . 9  |-  ( j  e.  ( 1 ... z )  ->  j  e.  NN )
165 eqid 2436 . . . . . . . . . . . 12  |-  ( ( abs  o.  -  )  o.  F )  =  ( ( abs  o.  -  )  o.  F )
166165ovolfsf 19368 . . . . . . . . . . 11  |-  ( F : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  (
( abs  o.  -  )  o.  F ) : NN --> ( 0 [,)  +oo ) )
16782, 166syl 16 . . . . . . . . . 10  |-  ( ph  ->  ( ( abs  o.  -  )  o.  F
) : NN --> ( 0 [,)  +oo ) )
168167ffvelrnda 5870 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  F ) `  j )  e.  ( 0 [,)  +oo )
)
169164, 168sylan2 461 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 1 ... z
) )  ->  (
( ( abs  o.  -  )  o.  F
) `  j )  e.  ( 0 [,)  +oo ) )
170 elrege0 11007 . . . . . . . 8  |-  ( ( ( ( abs  o.  -  )  o.  F
) `  j )  e.  ( 0 [,)  +oo ) 
<->  ( ( ( ( abs  o.  -  )  o.  F ) `  j
)  e.  RR  /\  0  <_  ( ( ( abs  o.  -  )  o.  F ) `  j
) ) )
171169, 170sylib 189 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( 1 ... z
) )  ->  (
( ( ( abs 
o.  -  )  o.  F ) `  j
)  e.  RR  /\  0  <_  ( ( ( abs  o.  -  )  o.  F ) `  j
) ) )
172171simpld 446 . . . . . 6  |-  ( (
ph  /\  j  e.  ( 1 ... z
) )  ->  (
( ( abs  o.  -  )  o.  F
) `  j )  e.  RR )
173163, 172fsumrecl 12528 . . . . 5  |-  ( ph  -> 
sum_ j  e.  ( 1 ... z ) ( ( ( abs 
o.  -  )  o.  F ) `  j
)  e.  RR )
174173adantr 452 . . . 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 )
175174rexrd 9134 . . 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* )
176165, 81ovolsf 19369 . . . . . . . . 9  |-  ( F : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  S : NN --> ( 0 [,) 
+oo ) )
17782, 176syl 16 . . . . . . . 8  |-  ( ph  ->  S : NN --> ( 0 [,)  +oo ) )
178 frn 5597 . . . . . . . 8  |-  ( S : NN --> ( 0 [,)  +oo )  ->  ran  S 
C_  ( 0 [,) 
+oo ) )
179177, 178syl 16 . . . . . . 7  |-  ( ph  ->  ran  S  C_  (
0 [,)  +oo ) )
180 0re 9091 . . . . . . . 8  |-  0  e.  RR
181 pnfxr 10713 . . . . . . . 8  |-  +oo  e.  RR*
182 icossre 10991 . . . . . . . 8  |-  ( ( 0  e.  RR  /\  +oo 
e.  RR* )  ->  (
0 [,)  +oo )  C_  RR )
183180, 181, 182mp2an 654 . . . . . . 7  |-  ( 0 [,)  +oo )  C_  RR
184179, 183syl6ss 3360 . . . . . 6  |-  ( ph  ->  ran  S  C_  RR )
185 ressxr 9129 . . . . . 6  |-  RR  C_  RR*
186184, 185syl6ss 3360 . . . . 5  |-  ( ph  ->  ran  S  C_  RR* )
187 supxrcl 10893 . . . . 5  |-  ( ran 
S  C_  RR*  ->  sup ( ran  S ,  RR* ,  <  )  e.  RR* )
188186, 187syl 16 . . . 4  |-  ( ph  ->  sup ( ran  S ,  RR* ,  <  )  e.  RR* )
189188adantr 452 . . 3  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  sup ( ran  S ,  RR* ,  <  )  e.  RR* )
190160adantr 452 . . . 4  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  ( B  -  A )  e.  RR )
19123sselda 3348 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  j  e.  NN )
192183, 168sseldi 3346 . . . . . . 7  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  F ) `  j )  e.  RR )
193191, 192syldan 457 . . . . . 6  |-  ( (
ph  /\  j  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  ( (
( abs  o.  -  )  o.  F ) `  j
)  e.  RR )
194136, 193fsumrecl 12528 . . . . 5  |-  ( ph  -> 
sum_ j  e.  ( ( G  o.  K
) " ( 1 ... M ) ) ( ( ( abs 
o.  -  )  o.  F ) `  j
)  e.  RR )
195194adantr 452 . . . 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 )
196 inss2 3562 . . . . . . . . . . 11  |-  (  <_  i^i  ( RR  X.  RR ) )  C_  ( RR  X.  RR )
197 fss 5599 . . . . . . . . . . 11  |-  ( ( F : NN --> (  <_  i^i  ( RR  X.  RR ) )  /\  (  <_  i^i  ( RR  X.  RR ) )  C_  ( RR  X.  RR ) )  ->  F : NN --> ( RR  X.  RR ) )
19882, 196, 197sylancl 644 . . . . . . . . . 10  |-  ( ph  ->  F : NN --> ( RR 
X.  RR ) )
19949, 102sseldi 3346 . . . . . . . . . . . 12  |-  ( ph  ->  M  e.  NN )
20014, 199ffvelrnd 5871 . . . . . . . . . . 11  |-  ( ph  ->  ( K `  M
)  e.  U )
2012, 200ffvelrnd 5871 . . . . . . . . . 10  |-  ( ph  ->  ( G `  ( K `  M )
)  e.  NN )
202198, 201ffvelrnd 5871 . . . . . . . . 9  |-  ( ph  ->  ( F `  ( G `  ( K `  M ) ) )  e.  ( RR  X.  RR ) )
203 xp2nd 6377 . . . . . . . . 9  |-  ( ( F `  ( G `
 ( K `  M ) ) )  e.  ( RR  X.  RR )  ->  ( 2nd `  ( F `  ( G `  ( K `  M ) ) ) )  e.  RR )
204202, 203syl 16 . . . . . . . 8  |-  ( ph  ->  ( 2nd `  ( F `  ( G `  ( K `  M
) ) ) )  e.  RR )
20512, 7sseldi 3346 . . . . . . . . . . 11  |-  ( ph  ->  C  e.  U )
2062, 205ffvelrnd 5871 . . . . . . . . . 10  |-  ( ph  ->  ( G `  C
)  e.  NN )
207198, 206ffvelrnd 5871 . . . . . . . . 9  |-  ( ph  ->  ( F `  ( G `  C )
)  e.  ( RR 
X.  RR ) )
208 xp1st 6376 . . . . . . . . 9  |-  ( ( F `  ( G `
 C ) )  e.  ( RR  X.  RR )  ->  ( 1st `  ( F `  ( G `  C )
) )  e.  RR )
209207, 208syl 16 . . . . . . . 8  |-  ( ph  ->  ( 1st `  ( F `  ( G `  C ) ) )  e.  RR )
210204, 209resubcld 9465 . . . . . . 7  |-  ( ph  ->  ( ( 2nd `  ( F `  ( G `  ( K `  M
) ) ) )  -  ( 1st `  ( F `  ( G `  C ) ) ) )  e.  RR )
211 fveq2 5728 . . . . . . . . . 10  |-  ( j  =  ( G `  ( K `  i ) )  ->  ( (
( abs  o.  -  )  o.  F ) `  j
)  =  ( ( ( abs  o.  -  )  o.  F ) `  ( G `  ( K `  i )
) ) )
212192recnd 9114 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  F ) `  j )  e.  CC )
213191, 212syldan 457 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  ( (
( abs  o.  -  )  o.  F ) `  j
)  e.  CC )
214211, 26, 132, 31, 213fsumf1o 12517 . . . . . . . . 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 ) ) ) )
21582adantr 452 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  F : NN --> (  <_  i^i  ( RR  X.  RR ) ) )
2162adantr 452 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  G : U --> NN )
217 ffvelrn 5868 . . . . . . . . . . . . 13  |-  ( ( K : NN --> U  /\  i  e.  NN )  ->  ( K `  i
)  e.  U )
21814, 17, 217syl2an 464 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( K `  i )  e.  U )
219216, 218ffvelrnd 5871 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( G `  ( K `  i ) )  e.  NN )
220165ovolfsval 19367 . . . . . . . . . . 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
) ) ) ) ) )
221215, 219, 220syl2anc 643 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( ( abs  o.  -  )  o.  F
) `  ( G `  ( K `  i
) ) )  =  ( ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  -  ( 1st `  ( F `  ( G `  ( K `  i
) ) ) ) ) )
222221sumeq2dv 12497 . . . . . . . . 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
) ) ) ) ) )
223198adantr 452 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  NN )  ->  F : NN
--> ( RR  X.  RR ) )
2242adantr 452 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  NN )  ->  G : U
--> NN )
22514ffvelrnda 5870 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  NN )  ->  ( K `
 i )  e.  U )
226224, 225ffvelrnd 5871 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  NN )  ->  ( G `
 ( K `  i ) )  e.  NN )
227223, 226ffvelrnd 5871 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  NN )  ->  ( F `
 ( G `  ( K `  i ) ) )  e.  ( RR  X.  RR ) )
228 xp2nd 6377 . . . . . . . . . . . . . 14  |-  ( ( F `  ( G `
 ( K `  i ) ) )  e.  ( RR  X.  RR )  ->  ( 2nd `  ( F `  ( G `  ( K `  i ) ) ) )  e.  RR )
229227, 228syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  NN )  ->  ( 2nd `  ( F `  ( G `  ( K `  i ) ) ) )  e.  RR )
23017, 229sylan2 461 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) )  e.  RR )
231230recnd 9114 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) )  e.  CC )
232198adantr 452 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  F : NN --> ( RR  X.  RR ) )
233232, 219ffvelrnd 5871 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( F `  ( G `  ( K `  i
) ) )  e.  ( RR  X.  RR ) )
234 xp1st 6376 . . . . . . . . . . . . 13  |-  ( ( F `  ( G `
 ( K `  i ) ) )  e.  ( RR  X.  RR )  ->  ( 1st `  ( F `  ( G `  ( K `  i ) ) ) )  e.  RR )
235233, 234syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( 1st `  ( F `  ( G `  ( K `
 i ) ) ) )  e.  RR )
236235recnd 9114 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( 1st `  ( F `  ( G `  ( K `
 i ) ) ) )  e.  CC )
23726, 231, 236fsumsub 12571 . . . . . . . . . 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 ) ) ) ) ) )
23852, 102sseldi 3346 . . . . . . . . . . . . 13  |-  ( ph  ->  M  e.  ( ZZ>= ` 
1 ) )
239 fveq2 5728 . . . . . . . . . . . . . . . 16  |-  ( i  =  M  ->  ( K `  i )  =  ( K `  M ) )
240239fveq2d 5732 . . . . . . . . . . . . . . 15  |-  ( i  =  M  ->  ( G `  ( K `  i ) )  =  ( G `  ( K `  M )
) )
241240fveq2d 5732 . . . . . . . . . . . . . 14  |-  ( i  =  M  ->  ( F `  ( G `  ( K `  i
) ) )  =  ( F `  ( G `  ( K `  M ) ) ) )
242241fveq2d 5732 . . . . . . . . . . . . 13  |-  ( i  =  M  ->  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) )  =  ( 2nd `  ( F `
 ( G `  ( K `  M ) ) ) ) )
243238, 231, 242fsumm1 12537 . . . . . . . . . . . 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
) ) ) ) ) )
244 fzfid 11312 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1 ... ( M  -  1 ) )  e.  Fin )
245 elfznn 11080 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( 1 ... ( M  -  1 ) )  ->  i  e.  NN )
246245, 229sylan2 461 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) )  e.  RR )
247244, 246fsumrecl 12528 . . . . . . . . . . . . . 14  |-  ( ph  -> 
sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  e.  RR )
248247recnd 9114 . . . . . . . . . . . . 13  |-  ( ph  -> 
sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  e.  CC )
249204recnd 9114 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 2nd `  ( F `  ( G `  ( K `  M
) ) ) )  e.  CC )
250248, 249addcomd 9268 . . . . . . . . . . . 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
) ) ) ) ) )
251243, 250eqtrd 2468 . . . . . . . . . . 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
) ) ) ) ) )
252 fveq2 5728 . . . . . . . . . . . . . . . 16  |-  ( i  =  1  ->  ( K `  i )  =  ( K ` 
1 ) )
253252fveq2d 5732 . . . . . . . . . . . . . . 15  |-  ( i  =  1  ->  ( G `  ( K `  i ) )  =  ( G `  ( K `  1 )
) )
254253fveq2d 5732 . . . . . . . . . . . . . 14  |-  ( i  =  1  ->  ( F `  ( G `  ( K `  i
) ) )  =  ( F `  ( G `  ( K `  1 ) ) ) )
255254fveq2d 5732 . . . . . . . . . . . . 13  |-  ( i  =  1  ->  ( 1st `  ( F `  ( G `  ( K `
 i ) ) ) )  =  ( 1st `  ( F `
 ( G `  ( K `  1 ) ) ) ) )
256238, 236, 255fsum1p 12539 . . . . . . . . . . . 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 ) ) ) ) ) )
2573, 4, 6, 7algr0 13063 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( K `  1
)  =  C )
258257fveq2d 5732 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( G `  ( K `  1 )
)  =  ( G `
 C ) )
259258fveq2d 5732 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( F `  ( G `  ( K `  1 ) ) )  =  ( F `
 ( G `  C ) ) )
260259fveq2d 5732 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1st `  ( F `  ( G `  ( K `  1
) ) ) )  =  ( 1st `  ( F `  ( G `  C ) ) ) )
2616peano2zd 10378 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1  +  1 )  e.  ZZ )
262199nnzd 10374 . . . . . . . . . . . . . . 15  |-  ( ph  ->  M  e.  ZZ )
263 fzp1ss 11098 . . . . . . . . . . . . . . . . . 18  |-  ( 1  e.  ZZ  ->  (
( 1  +  1 ) ... M ) 
C_  ( 1 ... M ) )
2645, 263mp1i 12 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( 1  +  1 ) ... M
)  C_  ( 1 ... M ) )
265264sselda 3348 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ( 1  +  1 ) ... M
) )  ->  i  e.  ( 1 ... M
) )
266265, 236syldan 457 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ( 1  +  1 ) ... M
) )  ->  ( 1st `  ( F `  ( G `  ( K `
 i ) ) ) )  e.  CC )
267 fveq2 5728 . . . . . . . . . . . . . . . . . 18  |-  ( i  =  ( j  +  1 )  ->  ( K `  i )  =  ( K `  ( j  +  1 ) ) )
268267fveq2d 5732 . . . . . . . . . . . . . . . . 17  |-  ( i  =  ( j  +  1 )  ->  ( G `  ( K `  i ) )  =  ( G `  ( K `  ( j  +  1 ) ) ) )
269268fveq2d 5732 . . . . . . . . . . . . . . . 16  |-  ( i  =  ( j  +  1 )  ->  ( F `  ( G `  ( K `  i
) ) )  =  ( F `  ( G `  ( K `  ( j  +  1 ) ) ) ) )
270269fveq2d 5732 . . . . . . . . . . . . . . 15  |-  ( i  =  ( j  +  1 )  ->  ( 1st `  ( F `  ( G `  ( K `
 i ) ) ) )  =  ( 1st `  ( F `
 ( G `  ( K `  ( j  +  1 ) ) ) ) ) )
2716, 261, 262, 266, 270fsumshftm 12564 . . . . . . . . . . . . . 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 ) ) ) ) ) )
272 ax-1cn 9048 . . . . . . . . . . . . . . . . . 18  |-  1  e.  CC
273 pncan 9311 . . . . . . . . . . . . . . . . . 18  |-  ( ( 1  e.  CC  /\  1  e.  CC )  ->  ( ( 1  +  1 )  -  1 )  =  1 )
274272, 272, 273mp2an 654 . . . . . . . . . . . . . . . . 17  |-  ( ( 1  +  1 )  -  1 )  =  1
275274oveq1i 6091 . . . . . . . . . . . . . . . 16  |-  ( ( ( 1  +  1 )  -  1 ) ... ( M  - 
1 ) )  =  ( 1 ... ( M  -  1 ) )
276275sumeq1i 12492 . . . . . . . . . . . . . . 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 ) ) ) ) )
277 oveq1 6088 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  i  ->  (
j  +  1 )  =  ( i  +  1 ) )
278277fveq2d 5732 . . . . . . . . . . . . . . . . . . 19  |-  ( j  =  i  ->  ( K `  ( j  +  1 ) )  =  ( K `  ( i  +  1 ) ) )
279278fveq2d 5732 . . . . . . . . . . . . . . . . . 18  |-  ( j  =  i  ->  ( G `  ( K `  ( j  +  1 ) ) )  =  ( G `  ( K `  ( i  +  1 ) ) ) )
280279fveq2d 5732 . . . . . . . . . . . . . . . . 17  |-  ( j  =  i  ->  ( F `  ( G `  ( K `  (
j  +  1 ) ) ) )  =  ( F `  ( G `  ( K `  ( i  +  1 ) ) ) ) )
281280fveq2d 5732 . . . . . . . . . . . . . . . 16  |-  ( j  =  i  ->  ( 1st `  ( F `  ( G `  ( K `
 ( j  +  1 ) ) ) ) )  =  ( 1st `  ( F `
 ( G `  ( K `  ( i  +  1 ) ) ) ) ) )
282281cbvsumv 12490 . . . . . . . . . . . . . . 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 ) ) ) ) )
283276, 282eqtri 2456 . . . . . . . . . . . . . 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 ) ) ) ) )
284271, 283syl6eq 2484 . . . . . . . . . . . . 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 ) ) ) ) ) )
285260, 284oveq12d 6099 . . . . . . . . . . . 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 ) ) ) ) ) ) )
286256, 285eqtrd 2468 . . . . . . . . . . 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 ) ) ) ) ) ) )
287251, 286oveq12d 6099 . . . . . . . . . 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 ) ) ) ) ) ) ) )
288209recnd 9114 . . . . . . . . . . 11  |-  ( ph  ->  ( 1st `  ( F `  ( G `  C ) ) )  e.  CC )
289 peano2nn 10012 . . . . . . . . . . . . . . . . . 18  |-  ( i  e.  NN  ->  (
i  +  1 )  e.  NN )
290 ffvelrn 5868 . . . . . . . . . . . . . . . . . 18  |-  ( ( K : NN --> U  /\  ( i  +  1 )  e.  NN )  ->  ( K `  ( i  +  1 ) )  e.  U
)
29114, 289, 290syl2an 464 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  NN )  ->  ( K `
 ( i  +  1 ) )  e.  U )
292224, 291ffvelrnd 5871 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  NN )  ->  ( G `
 ( K `  ( i  +  1 ) ) )  e.  NN )
293223, 292ffvelrnd 5871 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  NN )  ->  ( F `
 ( G `  ( K `  ( i  +  1 ) ) ) )  e.  ( RR  X.  RR ) )
294 xp1st 6376 . . . . . . . . . . . . . . 15  |-  ( ( F `  ( G `
 ( K `  ( i  +  1 ) ) ) )  e.  ( RR  X.  RR )  ->  ( 1st `  ( F `  ( G `  ( K `  ( i  +  1 ) ) ) ) )  e.  RR )
295293, 294syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  NN )  ->  ( 1st `  ( F `  ( G `  ( K `  ( i  +  1 ) ) ) ) )  e.  RR )
296245, 295sylan2 461 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  ( 1st `  ( F `  ( G `  ( K `
 ( i  +  1 ) ) ) ) )  e.  RR )
297244, 296fsumrecl 12528 . . . . . . . . . . . 12  |-  ( ph  -> 
sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 1st `  ( F `  ( G `  ( K `  (
i  +  1 ) ) ) ) )  e.  RR )
298297recnd 9114 . . . . . . . . . . 11  |-  ( ph  -> 
sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 1st `  ( F `  ( G `  ( K `  (
i  +  1 ) ) ) ) )  e.  CC )
299249, 248, 288, 298addsub4d 9458 . . . . . . . . . 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 ) ) ) ) ) ) ) )
300237, 287, 2993eqtrd 2472 . . . . . . . . 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 ) ) ) ) ) ) ) )
301214, 222, 3003eqtrd 2472 . . . . . . . 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 ) ) ) ) ) ) ) )
302301, 194eqeltrrd 2511 . . . . . . 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 )
303 fveq2 5728 . . . . . . . . . . . . . . 15  |-  ( n  =  M  ->  ( K `  n )  =  ( K `  M ) )
304303eleq2d 2503 . . . . . . . . . . . . . 14  |-  ( n  =  M  ->  ( B  e.  ( K `  n )  <->  B  e.  ( K `  M ) ) )
305304, 47elrab2 3094 . . . . . . . . . . . . 13  |-  ( M  e.  W  <->  ( M  e.  NN  /\  B  e.  ( K `  M
) ) )
306102, 305sylib 189 . . . . . . . . . . . 12  |-  ( ph  ->  ( M  e.  NN  /\  B  e.  ( K `
 M ) ) )
307306simprd 450 . . . . . . . . . . 11  |-  ( ph  ->  B  e.  ( K `
 M ) )
30878, 79, 80, 81, 82, 55, 83, 2, 84ovolicc2lem1 19413 . . . . . . . . . . . 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
) ) ) ) ) ) )
309200, 308mpdan 650 . . . . . . . . . . 11  |-  ( ph  ->  ( B  e.  ( K `  M )  <-> 
( B  e.  RR  /\  ( 1st `  ( F `  ( G `  ( K `  M
) ) ) )  <  B  /\  B  <  ( 2nd `  ( F `  ( G `  ( K `  M
) ) ) ) ) ) )
310307, 309mpbid 202 . . . . . . . . . 10  |-  ( ph  ->  ( B  e.  RR  /\  ( 1st `  ( F `  ( G `  ( K `  M
) ) ) )  <  B  /\  B  <  ( 2nd `  ( F `  ( G `  ( K `  M
) ) ) ) ) )
311310simp3d 971 . . . . . . . . 9  |-  ( ph  ->  B  <  ( 2nd `  ( F `  ( G `  ( K `  M ) ) ) ) )
31278, 79, 80, 81, 82, 55, 83, 2, 84ovolicc2lem1 19413 . . . . . . . . . . . 12  |-  ( (
ph  /\  C  e.  U )  ->  ( A  e.  C  <->  ( A  e.  RR  /\  ( 1st `  ( F `  ( G `  C )
) )  <  A  /\  A  <  ( 2nd `  ( F `  ( G `  C )
) ) ) ) )
313205, 312mpdan 650 . . . . . . . . . . 11  |-  ( ph  ->  ( A  e.  C  <->  ( A  e.  RR  /\  ( 1st `  ( F `
 ( G `  C ) ) )  <  A  /\  A  <  ( 2nd `  ( F `  ( G `  C ) ) ) ) ) )
31486, 313mpbid 202 . . . . . . . . . 10  |-  ( ph  ->  ( A  e.  RR  /\  ( 1st `  ( F `  ( G `  C ) ) )  <  A  /\  A  <  ( 2nd `  ( F `  ( G `  C ) ) ) ) )
315314simp2d 970 . . . . . . . . 9  |-  ( ph  ->  ( 1st `  ( F `  ( G `  C ) ) )  <  A )
31679, 209, 204, 78, 311, 315lt2subd 9649 . . . . . . . 8  |-  ( ph  ->  ( B  -  A
)  <  ( ( 2nd `  ( F `  ( G `  ( K `
 M ) ) ) )  -  ( 1st `  ( F `  ( G `  C ) ) ) ) )
317160, 210, 316ltled 9221 . . . . . . 7  |-  ( ph  ->  ( B  -  A
)  <_  ( ( 2nd `  ( F `  ( G `  ( K `
 M ) ) ) )  -  ( 1st `  ( F `  ( G `  C ) ) ) ) )
318245adantl 453 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  i  e.  NN )
319 simpr 448 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  i  e.  ( 1 ... ( M  -  1 ) ) )
320262adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  M  e.  ZZ )
321 elfzm11 11116 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 1  e.  ZZ  /\  M  e.  ZZ )  ->  ( i  e.  ( 1 ... ( M  -  1 ) )  <-> 
( i  e.  ZZ  /\  1  <_  i  /\  i  <  M ) ) )
3225, 320, 321sylancr 645 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  (
i  e.  ( 1 ... ( M  - 
1 ) )  <->  ( i  e.  ZZ  /\  1  <_ 
i  /\  i  <  M ) ) )
323319, 322mpbid 202 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  (
i  e.  ZZ  /\  1  <_  i  /\  i  <  M ) )
324323simp3d 971 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  i  <  M )
325318nnred 10015 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  i  e.  RR )
326103adantr 452 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  M  e.  RR )
327325, 326ltnled 9220 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  (
i  <  M  <->  -.  M  <_  i ) )
328324, 327mpbid 202 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  -.  M  <_  i )
329 infmssuzle 10558 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( W  C_  ( ZZ>= ` 
1 )  /\  i  e.  W )  ->  sup ( W ,  RR ,  `'  <  )  <_  i
)
33052, 329mpan 652 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  e.  W  ->  sup ( W ,  RR ,  `'  <  )  <_  i
)
33151, 330syl5eqbr 4245 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  W  ->  M  <_  i )
332328, 331nsyl 115 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  -.  i  e.  W )
333318, 332jca 519 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  (
i  e.  NN  /\  -.  i  e.  W
) )
33478, 79, 80, 81, 82, 55, 83, 2, 84, 10, 8, 85, 86, 7, 4, 47ovolicc2lem2 19414 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( i  e.  NN  /\  -.  i  e.  W ) )  -> 
( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  <_  B )
335333, 334syldan 457 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) )  <_  B
)
336 iftrue 3745 . . . . . . . . . . . . . . . 16  |-  ( ( 2nd `  ( F `
 ( G `  ( K `  i ) ) ) )  <_  B  ->  if ( ( 2nd `  ( F `
 ( G `  ( K `  i ) ) ) )  <_  B ,  ( 2nd `  ( F `  ( G `  ( K `  i ) ) ) ) ,  B )  =  ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) ) )
337335, 336syl 16 . . . . . . . . . . . . . . 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 ) ) ) ) )
338 ffvelrn 5868 . . . . . . . . . . . . . . . . 17  |-  ( ( K : NN --> T  /\  i  e.  NN )  ->  ( K `  i
)  e.  T )
3399, 245, 338syl2an 464 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  ( K `  i )  e.  T )
34085ralrimiva 2789 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  A. t  e.  T  if ( ( 2nd `  ( F `  ( G `  t ) ) )  <_  B ,  ( 2nd `  ( F `
 ( G `  t ) ) ) ,  B )  e.  ( H `  t
) )
341340adantr 452 . . . . . . . . . . . . . . . 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
) )
342 fveq2 5728 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( t  =  ( K `  i )  ->  ( G `  t )  =  ( G `  ( K `  i ) ) )
343342fveq2d 5732 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  =  ( K `  i )  ->  ( F `  ( G `  t ) )  =  ( F `  ( G `  ( K `  i ) ) ) )
344343fveq2d 5732 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  ( K `  i )  ->  ( 2nd `  ( F `  ( G `  t ) ) )  =  ( 2nd `  ( F `
 ( G `  ( K `  i ) ) ) ) )
345344breq1d 4222 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  ( K `  i )  ->  (
( 2nd `  ( F `  ( G `  t ) ) )  <_  B  <->  ( 2nd `  ( F `  ( G `  ( K `  i ) ) ) )  <_  B )
)
346 eqidd 2437 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  ( K `  i )  ->  B  =  B )
347345, 344, 346ifbieq12d 3761 . . . . . . . . . . . . . . . . . 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 ) )
348 fveq2 5728 . . . . . . . . . . . . . . . . . 18  |-  ( t  =  ( K `  i )  ->  ( H `  t )  =  ( H `  ( K `  i ) ) )
349347, 348eleq12d 2504 . . . . . . . . . . . . . . . . 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 )
) ) )
350349rspcv 3048 . . . . . . . . . . . . . . . 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 ) ) ) )
351339, 341, 350sylc 58 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  if ( ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  <_  B ,  ( 2nd `  ( F `
 ( G `  ( K `  i ) ) ) ) ,  B )  e.  ( H `  ( K `
 i ) ) )
352337, 351eqeltrrd 2511 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) )  e.  ( H `  ( K `
 i ) ) )
3533, 4, 6, 7, 8algrp1 13065 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  NN )  ->  ( K `
 ( i  +  1 ) )  =  ( H `  ( K `  i )
) )
354245, 353sylan2 461 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  ( K `  ( i  +  1 ) )  =  ( H `  ( K `  i ) ) )
355352, 354eleqtrrd 2513 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) )  e.  ( K `  ( i  +  1 ) ) )
356245, 291sylan2 461 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  ( K `  ( i  +  1 ) )  e.  U )
35778, 79, 80, 81, 82, 55, 83, 2, 84ovolicc2lem1 19413 . . . . . . . . . . . . . 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 ) ) ) ) ) ) ) )
358356, 357syldan 457 . . . . . . . . . . . . 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 ) ) ) ) ) ) ) )
359355, 358mpbid 202 . . . . . . . . . . . 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 ) ) ) ) ) ) )
360359simp2d 970 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  ( 1st `  ( F `  ( G `  ( K `
 ( i  +  1 ) ) ) ) )  <  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) ) )
361296, 246, 360ltled 9221 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  ( 1st `  ( F `  ( G `  ( K `
 ( i  +  1 ) ) ) ) )  <_  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) ) )
362244, 296, 246, 361fsumle 12578 . . . . . . . . 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
) ) ) ) )
363247, 297subge0d 9616 . . . . . . . . 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 ) ) ) ) ) )
364362, 363mpbird 224 . . . . . . . 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 ) ) ) ) ) ) )
365247, 297resubcld 9465 . . . . . . . . 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 )
366210, 365addge01d 9614 . . . . . . . 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 ) ) ) ) ) ) ) ) )
367364, 366mpbid 202 . . . . . . 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 ) ) ) ) ) ) ) )
368160, 210, 302, 317, 367letrd 9227 . . . . . 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 ) ) ) ) ) ) ) )
369368, 301breqtrrd 4238 . . . . 5  |-  ( ph  ->  ( B  -  A
)  <_  sum_ j  e.  ( ( G  o.  K ) " (
1 ... M ) ) ( ( ( abs 
o.  -  )  o.  F ) `  j
) )
370369adantr 452 . . . 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
) )
371 fzfid 11312 . . . . 5  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  ( 1 ... z )  e. 
Fin )
372172adantlr 696 . . . . 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 )
373171simprd 450 . . . . . 6  |-  ( (
ph  /\  j  e.  ( 1 ... z
) )  ->  0  <_  ( ( ( abs 
o.  -  )  o.  F ) `  j
) )
374373adantlr 696 . . . . 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 )
)
37523adantr 452 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  NN )  ->  ( ( G  o.  K )
" ( 1 ... M ) )  C_  NN )
376375sselda 3348 . . . . . . . . . . 11  |-  ( ( ( ph  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  y  e.  NN )
377376nnred 10015 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  y  e.  RR )
378145ad2antlr 708 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  z  e.  RR )
379 ltle 9163 . . . . . . . . . 10  |-  ( ( y  e.  RR  /\  z  e.  RR )  ->  ( y  <  z  ->  y  <_  z )
)
380377, 378, 379syl2anc 643 . . . . . . . . 9  |-  ( ( ( ph  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  ( y  <  z  ->  y  <_  z ) )
381376, 3syl6eleq 2526 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  y  e.  ( ZZ>= `  1 )
)
382 nnz 10303 . . . . . . . . . . 11  |-  ( z  e.  NN  ->  z  e.  ZZ )
383382ad2antlr 708 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  z  e.  ZZ )
384 elfz5 11051 . . . . . . . . . 10  |-  ( ( y  e.  ( ZZ>= ` 
1 )  /\  z  e.  ZZ )  ->  (
y  e.  ( 1 ... z )  <->  y  <_  z ) )
385381, 383, 384syl2anc 643 . . . . . . . . 9  |-  ( ( ( ph  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  ( y  e.  ( 1 ... z
)  <->  y  <_  z
) )
386380, 385sylibrd 226 . . . . . . . 8  |-  ( ( ( ph  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  ( y  <  z  ->  y  e.  ( 1 ... z
) ) )
387386ralimdva 2784 . . . . . . 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 ) ) )
388387impr 603 . . . . . 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 ) )
389 dfss3 3338 . . . . . 6  |-  ( ( ( G  o.  K
) " ( 1 ... M ) ) 
C_  ( 1 ... z )  <->  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  e.  ( 1 ... z ) )
390388, 389sylibr 204 . . . . 5  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  ( ( G  o.  K ) " ( 1 ... M ) )  C_  ( 1 ... z
) )
391371, 372, 374, 390fsumless 12575 . . . 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
) )
392190, 195, 174, 370, 391letrd 9227 . . 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
) )
393 eqidd 2437 . . . . . 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 ) )
394 simprl 733 . . . . . . 7  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  z  e.  NN )
395394, 3syl6eleq 2526 . . . . . 6  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  z  e.  ( ZZ>= `  1 )
)
396372recnd 9114 . . . . . 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 )
397393, 395, 396fsumser 12524 . . . . 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
) )
39881fveq1i 5729 . . . . 5  |-  ( S `
 z )  =  (  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  F ) ) `  z )
399397, 398syl6eqr 2486 . . . 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 ) )
400186adantr 452 . . . . 5  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  ran  S  C_  RR* )
401 ffn 5591 . . . . . . . 8  |-  ( S : NN --> ( 0 [,)  +oo )  ->  S  Fn  NN )
402177, 401syl 16 . . . . . . 7  |-  ( ph  ->  S  Fn  NN )
403402adantr 452 . . . . . 6  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  S  Fn  NN )
404 fnfvelrn 5867 . . . . . 6  |-  ( ( S  Fn  NN  /\  z  e.  NN )  ->  ( S `  z
)  e.  ran  S
)
405403, 394, 404syl2anc 643 . . . . 5  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  ( S `  z )  e.  ran  S )
406 supxrub 10903 . . . . 5  |-  ( ( ran  S  C_  RR*  /\  ( S `  z )  e.  ran  S )  ->