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

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

Proof of Theorem ovolicc2lem4OLD
Dummy variables  m  x  y  z  i 
j are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 arch 10867 . . . . 5  |-  ( x  e.  RR  ->  E. z  e.  NN  x  <  z
)
21ad2antlr 731 . . . 4  |-  ( ( ( ph  /\  x  e.  RR )  /\  A. y  e.  ( ( G  o.  K ) " ( 1 ... M ) ) y  <_  x )  ->  E. z  e.  NN  x  <  z )
3 df-ima 4863 . . . . . . . . . . . . . . . 16  |-  ( ( G  o.  K )
" ( 1 ... M ) )  =  ran  ( ( G  o.  K )  |`  ( 1 ... M
) )
4 ovolicc2.8 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  G : U --> NN )
5 nnuz 11195 . . . . . . . . . . . . . . . . . . . . 21  |-  NN  =  ( ZZ>= `  1 )
6 ovolicc2.15 . . . . . . . . . . . . . . . . . . . . 21  |-  K  =  seq 1 ( ( H  o.  1st ) ,  ( NN  X.  { C } ) )
7 1zzd 10969 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  1  e.  ZZ )
8 ovolicc2.14 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  C  e.  T )
9 ovolicc2.11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  H : T --> T )
105, 6, 7, 8, 9algrf 14520 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  K : NN --> T )
11 ovolicc2.10 . . . . . . . . . . . . . . . . . . . . 21  |-  T  =  { u  e.  U  |  ( u  i^i  ( A [,] B
) )  =/=  (/) }
12 ssrab2 3546 . . . . . . . . . . . . . . . . . . . . 21  |-  { u  e.  U  |  (
u  i^i  ( A [,] B ) )  =/=  (/) }  C_  U
1311, 12eqsstri 3494 . . . . . . . . . . . . . . . . . . . 20  |-  T  C_  U
14 fss 5751 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( K : NN --> T  /\  T  C_  U )  ->  K : NN --> U )
1510, 13, 14sylancl 666 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  K : NN --> U )
16 fco 5753 . . . . . . . . . . . . . . . . . . 19  |-  ( ( G : U --> NN  /\  K : NN --> U )  ->  ( G  o.  K ) : NN --> NN )
174, 15, 16syl2anc 665 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( G  o.  K
) : NN --> NN )
18 elfznn 11829 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  ( 1 ... M )  ->  i  e.  NN )
1918ssriv 3468 . . . . . . . . . . . . . . . . . 18  |-  ( 1 ... M )  C_  NN
20 fssres 5763 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( G  o.  K
) : NN --> NN  /\  ( 1 ... M
)  C_  NN )  ->  ( ( G  o.  K )  |`  (
1 ... M ) ) : ( 1 ... M ) --> NN )
2117, 19, 20sylancl 666 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( G  o.  K )  |`  (
1 ... M ) ) : ( 1 ... M ) --> NN )
22 frn 5749 . . . . . . . . . . . . . . . . 17  |-  ( ( ( G  o.  K
)  |`  ( 1 ... M ) ) : ( 1 ... M
) --> NN  ->  ran  ( ( G  o.  K )  |`  (
1 ... M ) ) 
C_  NN )
2321, 22syl 17 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ran  ( ( G  o.  K )  |`  ( 1 ... M
) )  C_  NN )
243, 23syl5eqss 3508 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( G  o.  K ) " (
1 ... M ) ) 
C_  NN )
25 nnssre 10614 . . . . . . . . . . . . . . 15  |-  NN  C_  RR
2624, 25syl6ss 3476 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( G  o.  K ) " (
1 ... M ) ) 
C_  RR )
2726ad3antrrr 734 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K
) " ( 1 ... M ) ) )  ->  ( ( G  o.  K ) " ( 1 ... M ) )  C_  RR )
28 simpr 462 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K
) " ( 1 ... M ) ) )  ->  y  e.  ( ( G  o.  K ) " (
1 ... M ) ) )
2927, 28sseldd 3465 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K
) " ( 1 ... M ) ) )  ->  y  e.  RR )
30 simpllr 767 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K
) " ( 1 ... M ) ) )  ->  x  e.  RR )
31 nnre 10617 . . . . . . . . . . . . 13  |-  ( z  e.  NN  ->  z  e.  RR )
3231ad2antlr 731 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K
) " ( 1 ... M ) ) )  ->  z  e.  RR )
33 lelttr 9725 . . . . . . . . . . . 12  |-  ( ( y  e.  RR  /\  x  e.  RR  /\  z  e.  RR )  ->  (
( y  <_  x  /\  x  <  z )  ->  y  <  z
) )
3429, 30, 32, 33syl3anc 1264 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K
) " ( 1 ... M ) ) )  ->  ( (
y  <_  x  /\  x  <  z )  -> 
y  <  z )
)
3534ancomsd 455 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K
) " ( 1 ... M ) ) )  ->  ( (
x  <  z  /\  y  <_  x )  -> 
y  <  z )
)
3635expdimp 438 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  x  e.  RR )  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K
) " ( 1 ... M ) ) )  /\  x  < 
z )  ->  (
y  <_  x  ->  y  <  z ) )
3736an32s 811 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  x  e.  RR )  /\  z  e.  NN )  /\  x  <  z
)  /\  y  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  ( y  <_  x  ->  y  <  z ) )
3837ralimdva 2833 . . . . . . 7  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  z  e.  NN )  /\  x  <  z
)  ->  ( A. y  e.  ( ( G  o.  K ) " ( 1 ... M ) ) y  <_  x  ->  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )
3938impancom 441 . . . . . 6  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  z  e.  NN )  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <_  x )  ->  ( x  <  z  ->  A. y  e.  ( ( G  o.  K
) " ( 1 ... M ) ) y  <  z ) )
4039an32s 811 . . . . 5  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  A. y  e.  ( ( G  o.  K
) " ( 1 ... M ) ) y  <_  x )  /\  z  e.  NN )  ->  ( x  < 
z  ->  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )
4140reximdva 2900 . . . 4  |-  ( ( ( ph  /\  x  e.  RR )  /\  A. y  e.  ( ( G  o.  K ) " ( 1 ... M ) ) y  <_  x )  -> 
( E. z  e.  NN  x  <  z  ->  E. z  e.  NN  A. y  e.  ( ( G  o.  K )
" ( 1 ... M ) ) y  <  z ) )
422, 41mpd 15 . . 3  |-  ( ( ( ph  /\  x  e.  RR )  /\  A. y  e.  ( ( G  o.  K ) " ( 1 ... M ) ) y  <_  x )  ->  E. z  e.  NN  A. y  e.  ( ( G  o.  K )
" ( 1 ... M ) ) y  <  z )
43 fzfid 12186 . . . . 5  |-  ( ph  ->  ( 1 ... M
)  e.  Fin )
44 fvres 5892 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( 1 ... M )  ->  (
( ( G  o.  K )  |`  (
1 ... M ) ) `
 i )  =  ( ( G  o.  K ) `  i
) )
4544adantl 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( ( G  o.  K )  |`  (
1 ... M ) ) `
 i )  =  ( ( G  o.  K ) `  i
) )
46 fvco3 5955 . . . . . . . . . . . . . . 15  |-  ( ( K : NN --> T  /\  i  e.  NN )  ->  ( ( G  o.  K ) `  i
)  =  ( G `
 ( K `  i ) ) )
4710, 18, 46syl2an 479 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( G  o.  K
) `  i )  =  ( G `  ( K `  i ) ) )
4845, 47eqtrd 2463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( ( G  o.  K )  |`  (
1 ... M ) ) `
 i )  =  ( G `  ( K `  i )
) )
4948adantrr 721 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
( ( ( G  o.  K )  |`  ( 1 ... M
) ) `  i
)  =  ( G `
 ( K `  i ) ) )
50 fvres 5892 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 1 ... M )  ->  (
( ( G  o.  K )  |`  (
1 ... M ) ) `
 j )  =  ( ( G  o.  K ) `  j
) )
5150ad2antll 733 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
( ( ( G  o.  K )  |`  ( 1 ... M
) ) `  j
)  =  ( ( G  o.  K ) `
 j ) )
52 elfznn 11829 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 1 ... M )  ->  j  e.  NN )
5352adantl 467 . . . . . . . . . . . . . 14  |-  ( ( i  e.  ( 1 ... M )  /\  j  e.  ( 1 ... M ) )  ->  j  e.  NN )
54 fvco3 5955 . . . . . . . . . . . . . 14  |-  ( ( K : NN --> T  /\  j  e.  NN )  ->  ( ( G  o.  K ) `  j
)  =  ( G `
 ( K `  j ) ) )
5510, 53, 54syl2an 479 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
( ( G  o.  K ) `  j
)  =  ( G `
 ( K `  j ) ) )
5651, 55eqtrd 2463 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
( ( ( G  o.  K )  |`  ( 1 ... M
) ) `  j
)  =  ( G `
 ( K `  j ) ) )
5749, 56eqeq12d 2444 . . . . . . . . . . 11  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
( ( ( ( G  o.  K )  |`  ( 1 ... M
) ) `  i
)  =  ( ( ( G  o.  K
)  |`  ( 1 ... M ) ) `  j )  <->  ( G `  ( K `  i
) )  =  ( G `  ( K `
 j ) ) ) )
58 fveq2 5878 . . . . . . . . . . . . 13  |-  ( ( G `  ( K `
 i ) )  =  ( G `  ( K `  j ) )  ->  ( F `  ( G `  ( K `  i )
) )  =  ( F `  ( G `
 ( K `  j ) ) ) )
5958fveq2d 5882 . . . . . . . . . . . 12  |-  ( ( G `  ( K `
 i ) )  =  ( G `  ( K `  j ) )  ->  ( 2nd `  ( F `  ( G `  ( K `  i ) ) ) )  =  ( 2nd `  ( F `  ( G `  ( K `  j ) ) ) ) )
6019a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( 1 ... M
)  C_  NN )
61 elfznn 11829 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  e.  ( 1 ... M )  ->  n  e.  NN )
6261ad2antlr 731 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  n  e.  ( 1 ... M
) )  /\  m  e.  W )  ->  n  e.  NN )
6362nnred 10625 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  ( 1 ... M
) )  /\  m  e.  W )  ->  n  e.  RR )
64 ovolicc2.16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  W  =  { n  e.  NN  |  B  e.  ( K `  n ) }
65 ssrab2 3546 . . . . . . . . . . . . . . . . . . . . . . 23  |-  { n  e.  NN  |  B  e.  ( K `  n
) }  C_  NN
6664, 65eqsstri 3494 . . . . . . . . . . . . . . . . . . . . . 22  |-  W  C_  NN
6766, 25sstri 3473 . . . . . . . . . . . . . . . . . . . . 21  |-  W  C_  RR
68 ovolicc2lem4OLD.17 . . . . . . . . . . . . . . . . . . . . . 22  |-  M  =  sup ( W ,  RR ,  `'  <  )
6966, 5sseqtri 3496 . . . . . . . . . . . . . . . . . . . . . . 23  |-  W  C_  ( ZZ>= `  1 )
70 1z 10968 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  1  e.  ZZ
715uzinf 12179 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 1  e.  ZZ  ->  -.  NN  e.  Fin )
7270, 71ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  -.  NN  e.  Fin
73 ovolicc2.6 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  U  e.  ( ~P
ran  ( (,)  o.  F )  i^i  Fin ) )
74 elin 3649 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( U  e.  ( ~P ran  ( (,)  o.  F )  i^i  Fin )  <->  ( U  e.  ~P ran  ( (,) 
o.  F )  /\  U  e.  Fin )
)
7573, 74sylib 199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  ( U  e.  ~P ran  ( (,)  o.  F
)  /\  U  e.  Fin ) )
7675simprd 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  U  e.  Fin )
77 ssfi 7795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( U  e.  Fin  /\  T  C_  U )  ->  T  e.  Fin )
7876, 13, 77sylancl 666 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  T  e.  Fin )
7978adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  W  =  (/) )  ->  T  e.  Fin )
8010adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  W  =  (/) )  ->  K : NN
--> T )
81 fveq2 5878 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( K `  i )  =  ( K `  j )  ->  ( G `  ( K `  i ) )  =  ( G `  ( K `  j )
) )
8281fveq2d 5882 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( K `  i )  =  ( K `  j )  ->  ( F `  ( G `  ( K `  i
) ) )  =  ( F `  ( G `  ( K `  j ) ) ) )
8382fveq2d 5882 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( K `  i )  =  ( K `  j )  ->  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) )  =  ( 2nd `  ( F `
 ( G `  ( K `  j ) ) ) ) )
84 simpll 758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  ph )
85 simprl 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  i  e.  NN )
86 ral0 3902 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  A. m  e.  (/)  n  <_  m
87 simplr 760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  W  =  (/) )
8887raleqdv 3031 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  ( A. m  e.  W  n  <_  m  <->  A. m  e.  (/)  n  <_  m ) )
8986, 88mpbiri 236 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  A. m  e.  W  n  <_  m )
9089ralrimivw 2840 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  A. n  e.  NN  A. m  e.  W  n  <_  m
)
91 rabid2 3006 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( NN  =  { n  e.  NN  |  A. m  e.  W  n  <_  m }  <->  A. n  e.  NN  A. m  e.  W  n  <_  m )
9290, 91sylibr 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  NN  =  { n  e.  NN  |  A. m  e.  W  n  <_  m } )
9385, 92eleqtrd 2512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  i  e.  { n  e.  NN  |  A. m  e.  W  n  <_  m } )
94 simprr 764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  j  e.  NN )
9594, 92eleqtrd 2512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  j  e.  { n  e.  NN  |  A. m  e.  W  n  <_  m } )
96 ovolicc.1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  A  e.  RR )
97 ovolicc.2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  B  e.  RR )
98 ovolicc.3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  A  <_  B )
99 ovolicc2.4 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  S  =  seq 1 (  +  ,  ( ( abs 
o.  -  )  o.  F ) )
100 ovolicc2.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  F : NN --> (  <_  i^i  ( RR  X.  RR ) ) )
101 ovolicc2.7 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  ( A [,] B
)  C_  U. U )
102 ovolicc2.9 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  t  e.  U )  ->  (
( (,)  o.  F
) `  ( G `  t ) )  =  t )
103 ovolicc2.12 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  t  e.  T )  ->  if ( ( 2nd `  ( F `  ( G `  t ) ) )  <_  B ,  ( 2nd `  ( F `
 ( G `  t ) ) ) ,  B )  e.  ( H `  t
) )
104 ovolicc2.13 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  A  e.  C )
10596, 97, 98, 99, 100, 73, 101, 4, 102, 11, 9, 103, 104, 8, 6, 64ovolicc2lem3 22459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  ( i  e.  { n  e.  NN  |  A. m  e.  W  n  <_  m }  /\  j  e.  { n  e.  NN  |  A. m  e.  W  n  <_  m } ) )  -> 
( i  =  j  <-> 
( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  =  ( 2nd `  ( F `  ( G `  ( K `  j
) ) ) ) ) )
10684, 93, 95, 105syl12anc 1262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  ( i  =  j  <->  ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  =  ( 2nd `  ( F `  ( G `  ( K `  j
) ) ) ) ) )
10783, 106syl5ibr 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  W  =  (/) )  /\  (
i  e.  NN  /\  j  e.  NN )
)  ->  ( ( K `  i )  =  ( K `  j )  ->  i  =  j ) )
108107ralrimivva 2846 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  W  =  (/) )  ->  A. i  e.  NN  A. j  e.  NN  ( ( K `
 i )  =  ( K `  j
)  ->  i  =  j ) )
109 dff13 6171 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( K : NN -1-1-> T  <->  ( K : NN --> T  /\  A. i  e.  NN  A. j  e.  NN  ( ( K `
 i )  =  ( K `  j
)  ->  i  =  j ) ) )
11080, 108, 109sylanbrc 668 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  W  =  (/) )  ->  K : NN
-1-1-> T )
111 f1domg 7593 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( T  e.  Fin  ->  ( K : NN -1-1-> T  ->  NN 
~<_  T ) )
11279, 110, 111sylc 62 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  W  =  (/) )  ->  NN  ~<_  T )
113 domfi 7796 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( T  e.  Fin  /\  NN 
~<_  T )  ->  NN  e.  Fin )
11479, 112, 113syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  W  =  (/) )  ->  NN  e.  Fin )
115114ex 435 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( W  =  (/)  ->  NN  e.  Fin )
)
116115necon3bd 2636 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( -.  NN  e.  Fin  ->  W  =/=  (/) ) )
11772, 116mpi 21 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  W  =/=  (/) )
118 infmssuzclOLD 11248 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( W  C_  ( ZZ>= ` 
1 )  /\  W  =/=  (/) )  ->  sup ( W ,  RR ,  `'  <  )  e.  W
)
11969, 117, 118sylancr 667 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  sup ( W ,  RR ,  `'  <  )  e.  W )
12068, 119syl5eqel 2514 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  M  e.  W )
12167, 120sseldi 3462 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  M  e.  RR )
122121ad2antrr 730 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  ( 1 ... M
) )  /\  m  e.  W )  ->  M  e.  RR )
12367sseli 3460 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  e.  W  ->  m  e.  RR )
124123adantl 467 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  ( 1 ... M
) )  /\  m  e.  W )  ->  m  e.  RR )
125 elfzle2 11804 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  ( 1 ... M )  ->  n  <_  M )
126125ad2antlr 731 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  ( 1 ... M
) )  /\  m  e.  W )  ->  n  <_  M )
127 infmssuzleOLD 11247 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( W  C_  ( ZZ>= ` 
1 )  /\  m  e.  W )  ->  sup ( W ,  RR ,  `'  <  )  <_  m
)
12869, 127mpan 674 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  e.  W  ->  sup ( W ,  RR ,  `'  <  )  <_  m
)
12968, 128syl5eqbr 4454 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  e.  W  ->  M  <_  m )
130129adantl 467 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  ( 1 ... M
) )  /\  m  e.  W )  ->  M  <_  m )
13163, 122, 124, 126, 130letrd 9793 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  n  e.  ( 1 ... M
) )  /\  m  e.  W )  ->  n  <_  m )
132131ralrimiva 2839 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  ( 1 ... M
) )  ->  A. m  e.  W  n  <_  m )
13360, 132ssrabdv 3540 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( 1 ... M
)  C_  { n  e.  NN  |  A. m  e.  W  n  <_  m } )
134133adantr 466 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
( 1 ... M
)  C_  { n  e.  NN  |  A. m  e.  W  n  <_  m } )
135 simprl 762 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
i  e.  ( 1 ... M ) )
136134, 135sseldd 3465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
i  e.  { n  e.  NN  |  A. m  e.  W  n  <_  m } )
137 simprr 764 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
j  e.  ( 1 ... M ) )
138134, 137sseldd 3465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
j  e.  { n  e.  NN  |  A. m  e.  W  n  <_  m } )
139136, 138jca 534 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
( i  e.  {
n  e.  NN  |  A. m  e.  W  n  <_  m }  /\  j  e.  { n  e.  NN  |  A. m  e.  W  n  <_  m } ) )
140139, 105syldan 472 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
( i  =  j  <-> 
( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  =  ( 2nd `  ( F `  ( G `  ( K `  j
) ) ) ) ) )
14159, 140syl5ibr 224 . . . . . . . . . . 11  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
( ( G `  ( K `  i ) )  =  ( G `
 ( K `  j ) )  -> 
i  =  j ) )
14257, 141sylbid 218 . . . . . . . . . 10  |-  ( (
ph  /\  ( i  e.  ( 1 ... M
)  /\  j  e.  ( 1 ... M
) ) )  -> 
( ( ( ( G  o.  K )  |`  ( 1 ... M
) ) `  i
)  =  ( ( ( G  o.  K
)  |`  ( 1 ... M ) ) `  j )  ->  i  =  j ) )
143142ralrimivva 2846 . . . . . . . . 9  |-  ( ph  ->  A. i  e.  ( 1 ... M ) A. j  e.  ( 1 ... M ) ( ( ( ( G  o.  K )  |`  ( 1 ... M
) ) `  i
)  =  ( ( ( G  o.  K
)  |`  ( 1 ... M ) ) `  j )  ->  i  =  j ) )
144 dff13 6171 . . . . . . . . 9  |-  ( ( ( G  o.  K
)  |`  ( 1 ... M ) ) : ( 1 ... M
) -1-1-> NN  <->  ( ( ( G  o.  K )  |`  ( 1 ... M
) ) : ( 1 ... M ) --> NN  /\  A. i  e.  ( 1 ... M
) A. j  e.  ( 1 ... M
) ( ( ( ( G  o.  K
)  |`  ( 1 ... M ) ) `  i )  =  ( ( ( G  o.  K )  |`  (
1 ... M ) ) `
 j )  -> 
i  =  j ) ) )
14521, 143, 144sylanbrc 668 . . . . . . . 8  |-  ( ph  ->  ( ( G  o.  K )  |`  (
1 ... M ) ) : ( 1 ... M ) -1-1-> NN )
146 f1f1orn 5839 . . . . . . . 8  |-  ( ( ( G  o.  K
)  |`  ( 1 ... M ) ) : ( 1 ... M
) -1-1-> NN  ->  ( ( G  o.  K )  |`  ( 1 ... M
) ) : ( 1 ... M ) -1-1-onto-> ran  ( ( G  o.  K )  |`  (
1 ... M ) ) )
147145, 146syl 17 . . . . . . 7  |-  ( ph  ->  ( ( G  o.  K )  |`  (
1 ... M ) ) : ( 1 ... M ) -1-1-onto-> ran  ( ( G  o.  K )  |`  ( 1 ... M
) ) )
148 f1oeq3 5821 . . . . . . . 8  |-  ( ( ( G  o.  K
) " ( 1 ... M ) )  =  ran  ( ( G  o.  K )  |`  ( 1 ... M
) )  ->  (
( ( G  o.  K )  |`  (
1 ... M ) ) : ( 1 ... M ) -1-1-onto-> ( ( G  o.  K ) " (
1 ... M ) )  <-> 
( ( G  o.  K )  |`  (
1 ... M ) ) : ( 1 ... M ) -1-1-onto-> ran  ( ( G  o.  K )  |`  ( 1 ... M
) ) ) )
1493, 148ax-mp 5 . . . . . . 7  |-  ( ( ( G  o.  K
)  |`  ( 1 ... M ) ) : ( 1 ... M
)
-1-1-onto-> ( ( G  o.  K ) " (
1 ... M ) )  <-> 
( ( G  o.  K )  |`  (
1 ... M ) ) : ( 1 ... M ) -1-1-onto-> ran  ( ( G  o.  K )  |`  ( 1 ... M
) ) )
150147, 149sylibr 215 . . . . . 6  |-  ( ph  ->  ( ( G  o.  K )  |`  (
1 ... M ) ) : ( 1 ... M ) -1-1-onto-> ( ( G  o.  K ) " (
1 ... M ) ) )
151 f1ofo 5835 . . . . . 6  |-  ( ( ( G  o.  K
)  |`  ( 1 ... M ) ) : ( 1 ... M
)
-1-1-onto-> ( ( G  o.  K ) " (
1 ... M ) )  ->  ( ( G  o.  K )  |`  ( 1 ... M
) ) : ( 1 ... M )
-onto-> ( ( G  o.  K ) " (
1 ... M ) ) )
152150, 151syl 17 . . . . 5  |-  ( ph  ->  ( ( G  o.  K )  |`  (
1 ... M ) ) : ( 1 ... M ) -onto-> ( ( G  o.  K )
" ( 1 ... M ) ) )
153 fofi 7863 . . . . 5  |-  ( ( ( 1 ... M
)  e.  Fin  /\  ( ( G  o.  K )  |`  (
1 ... M ) ) : ( 1 ... M ) -onto-> ( ( G  o.  K )
" ( 1 ... M ) ) )  ->  ( ( G  o.  K ) "
( 1 ... M
) )  e.  Fin )
15443, 152, 153syl2anc 665 . . . 4  |-  ( ph  ->  ( ( G  o.  K ) " (
1 ... M ) )  e.  Fin )
155 fimaxre2 10553 . . . 4  |-  ( ( ( ( G  o.  K ) " (
1 ... M ) ) 
C_  RR  /\  (
( G  o.  K
) " ( 1 ... M ) )  e.  Fin )  ->  E. x  e.  RR  A. y  e.  ( ( G  o.  K )
" ( 1 ... M ) ) y  <_  x )
15626, 154, 155syl2anc 665 . . 3  |-  ( ph  ->  E. x  e.  RR  A. y  e.  ( ( G  o.  K )
" ( 1 ... M ) ) y  <_  x )
15742, 156r19.29a 2970 . 2  |-  ( ph  ->  E. z  e.  NN  A. y  e.  ( ( G  o.  K )
" ( 1 ... M ) ) y  <  z )
15897, 96resubcld 10048 . . . . 5  |-  ( ph  ->  ( B  -  A
)  e.  RR )
159158rexrd 9691 . . . 4  |-  ( ph  ->  ( B  -  A
)  e.  RR* )
160159adantr 466 . . 3  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  ( B  -  A )  e.  RR* )
161 fzfid 12186 . . . . . 6  |-  ( ph  ->  ( 1 ... z
)  e.  Fin )
162 elfznn 11829 . . . . . . . . 9  |-  ( j  e.  ( 1 ... z )  ->  j  e.  NN )
163 eqid 2422 . . . . . . . . . . . 12  |-  ( ( abs  o.  -  )  o.  F )  =  ( ( abs  o.  -  )  o.  F )
164163ovolfsf 22411 . . . . . . . . . . 11  |-  ( F : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  (
( abs  o.  -  )  o.  F ) : NN --> ( 0 [,) +oo ) )
165100, 164syl 17 . . . . . . . . . 10  |-  ( ph  ->  ( ( abs  o.  -  )  o.  F
) : NN --> ( 0 [,) +oo ) )
166165ffvelrnda 6034 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  F ) `  j )  e.  ( 0 [,) +oo )
)
167162, 166sylan2 476 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 1 ... z
) )  ->  (
( ( abs  o.  -  )  o.  F
) `  j )  e.  ( 0 [,) +oo ) )
168 elrege0 11739 . . . . . . . 8  |-  ( ( ( ( abs  o.  -  )  o.  F
) `  j )  e.  ( 0 [,) +oo ) 
<->  ( ( ( ( abs  o.  -  )  o.  F ) `  j
)  e.  RR  /\  0  <_  ( ( ( abs  o.  -  )  o.  F ) `  j
) ) )
169167, 168sylib 199 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( 1 ... z
) )  ->  (
( ( ( abs 
o.  -  )  o.  F ) `  j
)  e.  RR  /\  0  <_  ( ( ( abs  o.  -  )  o.  F ) `  j
) ) )
170169simpld 460 . . . . . 6  |-  ( (
ph  /\  j  e.  ( 1 ... z
) )  ->  (
( ( abs  o.  -  )  o.  F
) `  j )  e.  RR )
171161, 170fsumrecl 13788 . . . . 5  |-  ( ph  -> 
sum_ j  e.  ( 1 ... z ) ( ( ( abs 
o.  -  )  o.  F ) `  j
)  e.  RR )
172171adantr 466 . . . 4  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  sum_ j  e.  ( 1 ... z
) ( ( ( abs  o.  -  )  o.  F ) `  j
)  e.  RR )
173172rexrd 9691 . . 3  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  sum_ j  e.  ( 1 ... z
) ( ( ( abs  o.  -  )  o.  F ) `  j
)  e.  RR* )
174163, 99ovolsf 22412 . . . . . . . . 9  |-  ( F : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  S : NN --> ( 0 [,) +oo ) )
175100, 174syl 17 . . . . . . . 8  |-  ( ph  ->  S : NN --> ( 0 [,) +oo ) )
176 frn 5749 . . . . . . . 8  |-  ( S : NN --> ( 0 [,) +oo )  ->  ran  S  C_  ( 0 [,) +oo ) )
177175, 176syl 17 . . . . . . 7  |-  ( ph  ->  ran  S  C_  (
0 [,) +oo )
)
178 rge0ssre 11741 . . . . . . 7  |-  ( 0 [,) +oo )  C_  RR
179177, 178syl6ss 3476 . . . . . 6  |-  ( ph  ->  ran  S  C_  RR )
180 ressxr 9685 . . . . . 6  |-  RR  C_  RR*
181179, 180syl6ss 3476 . . . . 5  |-  ( ph  ->  ran  S  C_  RR* )
182 supxrcl 11601 . . . . 5  |-  ( ran 
S  C_  RR*  ->  sup ( ran  S ,  RR* ,  <  )  e.  RR* )
183181, 182syl 17 . . . 4  |-  ( ph  ->  sup ( ran  S ,  RR* ,  <  )  e.  RR* )
184183adantr 466 . . 3  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  sup ( ran  S ,  RR* ,  <  )  e.  RR* )
185158adantr 466 . . . 4  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  ( B  -  A )  e.  RR )
18624sselda 3464 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  j  e.  NN )
187178, 166sseldi 3462 . . . . . . 7  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  F ) `  j )  e.  RR )
188186, 187syldan 472 . . . . . 6  |-  ( (
ph  /\  j  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  ( (
( abs  o.  -  )  o.  F ) `  j
)  e.  RR )
189154, 188fsumrecl 13788 . . . . 5  |-  ( ph  -> 
sum_ j  e.  ( ( G  o.  K
) " ( 1 ... M ) ) ( ( ( abs 
o.  -  )  o.  F ) `  j
)  e.  RR )
190189adantr 466 . . . 4  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  sum_ j  e.  ( ( G  o.  K ) " (
1 ... M ) ) ( ( ( abs 
o.  -  )  o.  F ) `  j
)  e.  RR )
191 inss2 3683 . . . . . . . . . . 11  |-  (  <_  i^i  ( RR  X.  RR ) )  C_  ( RR  X.  RR )
192 fss 5751 . . . . . . . . . . 11  |-  ( ( F : NN --> (  <_  i^i  ( RR  X.  RR ) )  /\  (  <_  i^i  ( RR  X.  RR ) )  C_  ( RR  X.  RR ) )  ->  F : NN --> ( RR  X.  RR ) )
193100, 191, 192sylancl 666 . . . . . . . . . 10  |-  ( ph  ->  F : NN --> ( RR 
X.  RR ) )
19466, 120sseldi 3462 . . . . . . . . . . . 12  |-  ( ph  ->  M  e.  NN )
19515, 194ffvelrnd 6035 . . . . . . . . . . 11  |-  ( ph  ->  ( K `  M
)  e.  U )
1964, 195ffvelrnd 6035 . . . . . . . . . 10  |-  ( ph  ->  ( G `  ( K `  M )
)  e.  NN )
197193, 196ffvelrnd 6035 . . . . . . . . 9  |-  ( ph  ->  ( F `  ( G `  ( K `  M ) ) )  e.  ( RR  X.  RR ) )
198 xp2nd 6835 . . . . . . . . 9  |-  ( ( F `  ( G `
 ( K `  M ) ) )  e.  ( RR  X.  RR )  ->  ( 2nd `  ( F `  ( G `  ( K `  M ) ) ) )  e.  RR )
199197, 198syl 17 . . . . . . . 8  |-  ( ph  ->  ( 2nd `  ( F `  ( G `  ( K `  M
) ) ) )  e.  RR )
20013, 8sseldi 3462 . . . . . . . . . . 11  |-  ( ph  ->  C  e.  U )
2014, 200ffvelrnd 6035 . . . . . . . . . 10  |-  ( ph  ->  ( G `  C
)  e.  NN )
202193, 201ffvelrnd 6035 . . . . . . . . 9  |-  ( ph  ->  ( F `  ( G `  C )
)  e.  ( RR 
X.  RR ) )
203 xp1st 6834 . . . . . . . . 9  |-  ( ( F `  ( G `
 C ) )  e.  ( RR  X.  RR )  ->  ( 1st `  ( F `  ( G `  C )
) )  e.  RR )
204202, 203syl 17 . . . . . . . 8  |-  ( ph  ->  ( 1st `  ( F `  ( G `  C ) ) )  e.  RR )
205199, 204resubcld 10048 . . . . . . 7  |-  ( ph  ->  ( ( 2nd `  ( F `  ( G `  ( K `  M
) ) ) )  -  ( 1st `  ( F `  ( G `  C ) ) ) )  e.  RR )
206 fveq2 5878 . . . . . . . . . 10  |-  ( j  =  ( G `  ( K `  i ) )  ->  ( (
( abs  o.  -  )  o.  F ) `  j
)  =  ( ( ( abs  o.  -  )  o.  F ) `  ( G `  ( K `  i )
) ) )
207187recnd 9670 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  NN )  ->  ( ( ( abs  o.  -  )  o.  F ) `  j )  e.  CC )
208186, 207syldan 472 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  ( (
( abs  o.  -  )  o.  F ) `  j
)  e.  CC )
209206, 43, 150, 48, 208fsumf1o 13777 . . . . . . . . 9  |-  ( ph  -> 
sum_ j  e.  ( ( G  o.  K
) " ( 1 ... M ) ) ( ( ( abs 
o.  -  )  o.  F ) `  j
)  =  sum_ i  e.  ( 1 ... M
) ( ( ( abs  o.  -  )  o.  F ) `  ( G `  ( K `  i ) ) ) )
210100adantr 466 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  F : NN --> (  <_  i^i  ( RR  X.  RR ) ) )
2114adantr 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  G : U --> NN )
212 ffvelrn 6032 . . . . . . . . . . . . 13  |-  ( ( K : NN --> U  /\  i  e.  NN )  ->  ( K `  i
)  e.  U )
21315, 18, 212syl2an 479 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( K `  i )  e.  U )
214211, 213ffvelrnd 6035 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( G `  ( K `  i ) )  e.  NN )
215163ovolfsval 22410 . . . . . . . . . . 11  |-  ( ( F : NN --> (  <_  i^i  ( RR  X.  RR ) )  /\  ( G `  ( K `  i ) )  e.  NN )  ->  (
( ( abs  o.  -  )  o.  F
) `  ( G `  ( K `  i
) ) )  =  ( ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  -  ( 1st `  ( F `  ( G `  ( K `  i
) ) ) ) ) )
216210, 214, 215syl2anc 665 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( ( abs  o.  -  )  o.  F
) `  ( G `  ( K `  i
) ) )  =  ( ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  -  ( 1st `  ( F `  ( G `  ( K `  i
) ) ) ) ) )
217216sumeq2dv 13757 . . . . . . . . 9  |-  ( ph  -> 
sum_ i  e.  ( 1 ... M ) ( ( ( abs 
o.  -  )  o.  F ) `  ( G `  ( K `  i ) ) )  =  sum_ i  e.  ( 1 ... M ) ( ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  -  ( 1st `  ( F `  ( G `  ( K `  i
) ) ) ) ) )
218193adantr 466 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  NN )  ->  F : NN
--> ( RR  X.  RR ) )
2194adantr 466 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  NN )  ->  G : U
--> NN )
22015ffvelrnda 6034 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  NN )  ->  ( K `
 i )  e.  U )
221219, 220ffvelrnd 6035 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  NN )  ->  ( G `
 ( K `  i ) )  e.  NN )
222218, 221ffvelrnd 6035 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  NN )  ->  ( F `
 ( G `  ( K `  i ) ) )  e.  ( RR  X.  RR ) )
223 xp2nd 6835 . . . . . . . . . . . . . 14  |-  ( ( F `  ( G `
 ( K `  i ) ) )  e.  ( RR  X.  RR )  ->  ( 2nd `  ( F `  ( G `  ( K `  i ) ) ) )  e.  RR )
224222, 223syl 17 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  NN )  ->  ( 2nd `  ( F `  ( G `  ( K `  i ) ) ) )  e.  RR )
22518, 224sylan2 476 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) )  e.  RR )
226225recnd 9670 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) )  e.  CC )
227193adantr 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  F : NN --> ( RR  X.  RR ) )
228227, 214ffvelrnd 6035 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( F `  ( G `  ( K `  i
) ) )  e.  ( RR  X.  RR ) )
229 xp1st 6834 . . . . . . . . . . . . 13  |-  ( ( F `  ( G `
 ( K `  i ) ) )  e.  ( RR  X.  RR )  ->  ( 1st `  ( F `  ( G `  ( K `  i ) ) ) )  e.  RR )
230228, 229syl 17 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( 1st `  ( F `  ( G `  ( K `
 i ) ) ) )  e.  RR )
231230recnd 9670 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( 1st `  ( F `  ( G `  ( K `
 i ) ) ) )  e.  CC )
23243, 226, 231fsumsub 13837 . . . . . . . . . 10  |-  ( ph  -> 
sum_ i  e.  ( 1 ... M ) ( ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  -  ( 1st `  ( F `  ( G `  ( K `  i
) ) ) ) )  =  ( sum_ i  e.  ( 1 ... M ) ( 2nd `  ( F `
 ( G `  ( K `  i ) ) ) )  -  sum_ i  e.  ( 1 ... M ) ( 1st `  ( F `
 ( G `  ( K `  i ) ) ) ) ) )
23369, 120sseldi 3462 . . . . . . . . . . . . 13  |-  ( ph  ->  M  e.  ( ZZ>= ` 
1 ) )
234 fveq2 5878 . . . . . . . . . . . . . . . 16  |-  ( i  =  M  ->  ( K `  i )  =  ( K `  M ) )
235234fveq2d 5882 . . . . . . . . . . . . . . 15  |-  ( i  =  M  ->  ( G `  ( K `  i ) )  =  ( G `  ( K `  M )
) )
236235fveq2d 5882 . . . . . . . . . . . . . 14  |-  ( i  =  M  ->  ( F `  ( G `  ( K `  i
) ) )  =  ( F `  ( G `  ( K `  M ) ) ) )
237236fveq2d 5882 . . . . . . . . . . . . 13  |-  ( i  =  M  ->  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) )  =  ( 2nd `  ( F `
 ( G `  ( K `  M ) ) ) ) )
238233, 226, 237fsumm1 13800 . . . . . . . . . . . 12  |-  ( ph  -> 
sum_ i  e.  ( 1 ... M ) ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  =  ( sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  +  ( 2nd `  ( F `  ( G `  ( K `  M
) ) ) ) ) )
239 fzfid 12186 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1 ... ( M  -  1 ) )  e.  Fin )
240 elfznn 11829 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( 1 ... ( M  -  1 ) )  ->  i  e.  NN )
241240, 224sylan2 476 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) )  e.  RR )
242239, 241fsumrecl 13788 . . . . . . . . . . . . . 14  |-  ( ph  -> 
sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  e.  RR )
243242recnd 9670 . . . . . . . . . . . . 13  |-  ( ph  -> 
sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  e.  CC )
244199recnd 9670 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 2nd `  ( F `  ( G `  ( K `  M
) ) ) )  e.  CC )
245243, 244addcomd 9836 . . . . . . . . . . . 12  |-  ( ph  ->  ( sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  +  ( 2nd `  ( F `  ( G `  ( K `  M
) ) ) ) )  =  ( ( 2nd `  ( F `
 ( G `  ( K `  M ) ) ) )  + 
sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) ) ) )
246238, 245eqtrd 2463 . . . . . . . . . . 11  |-  ( ph  -> 
sum_ i  e.  ( 1 ... M ) ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  =  ( ( 2nd `  ( F `  ( G `  ( K `  M ) ) ) )  +  sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) ) ) )
247 fveq2 5878 . . . . . . . . . . . . . . . 16  |-  ( i  =  1  ->  ( K `  i )  =  ( K ` 
1 ) )
248247fveq2d 5882 . . . . . . . . . . . . . . 15  |-  ( i  =  1  ->  ( G `  ( K `  i ) )  =  ( G `  ( K `  1 )
) )
249248fveq2d 5882 . . . . . . . . . . . . . 14  |-  ( i  =  1  ->  ( F `  ( G `  ( K `  i
) ) )  =  ( F `  ( G `  ( K `  1 ) ) ) )
250249fveq2d 5882 . . . . . . . . . . . . 13  |-  ( i  =  1  ->  ( 1st `  ( F `  ( G `  ( K `
 i ) ) ) )  =  ( 1st `  ( F `
 ( G `  ( K `  1 ) ) ) ) )
251233, 231, 250fsum1p 13802 . . . . . . . . . . . 12  |-  ( ph  -> 
sum_ i  e.  ( 1 ... M ) ( 1st `  ( F `  ( G `  ( K `  i
) ) ) )  =  ( ( 1st `  ( F `  ( G `  ( K `  1 ) ) ) )  +  sum_ i  e.  ( (
1  +  1 ) ... M ) ( 1st `  ( F `
 ( G `  ( K `  i ) ) ) ) ) )
2525, 6, 7, 8algr0 14519 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( K `  1
)  =  C )
253252fveq2d 5882 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( G `  ( K `  1 )
)  =  ( G `
 C ) )
254253fveq2d 5882 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( F `  ( G `  ( K `  1 ) ) )  =  ( F `
 ( G `  C ) ) )
255254fveq2d 5882 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1st `  ( F `  ( G `  ( K `  1
) ) ) )  =  ( 1st `  ( F `  ( G `  C ) ) ) )
2567peano2zd 11044 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1  +  1 )  e.  ZZ )
257194nnzd 11040 . . . . . . . . . . . . . . 15  |-  ( ph  ->  M  e.  ZZ )
258 fzp1ss 11848 . . . . . . . . . . . . . . . . . 18  |-  ( 1  e.  ZZ  ->  (
( 1  +  1 ) ... M ) 
C_  ( 1 ... M ) )
25970, 258mp1i 13 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( 1  +  1 ) ... M
)  C_  ( 1 ... M ) )
260259sselda 3464 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ( 1  +  1 ) ... M
) )  ->  i  e.  ( 1 ... M
) )
261260, 231syldan 472 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ( 1  +  1 ) ... M
) )  ->  ( 1st `  ( F `  ( G `  ( K `
 i ) ) ) )  e.  CC )
262 fveq2 5878 . . . . . . . . . . . . . . . . . 18  |-  ( i  =  ( j  +  1 )  ->  ( K `  i )  =  ( K `  ( j  +  1 ) ) )
263262fveq2d 5882 . . . . . . . . . . . . . . . . 17  |-  ( i  =  ( j  +  1 )  ->  ( G `  ( K `  i ) )  =  ( G `  ( K `  ( j  +  1 ) ) ) )
264263fveq2d 5882 . . . . . . . . . . . . . . . 16  |-  ( i  =  ( j  +  1 )  ->  ( F `  ( G `  ( K `  i
) ) )  =  ( F `  ( G `  ( K `  ( j  +  1 ) ) ) ) )
265264fveq2d 5882 . . . . . . . . . . . . . . 15  |-  ( i  =  ( j  +  1 )  ->  ( 1st `  ( F `  ( G `  ( K `
 i ) ) ) )  =  ( 1st `  ( F `
 ( G `  ( K `  ( j  +  1 ) ) ) ) ) )
2667, 256, 257, 261, 265fsumshftm 13830 . . . . . . . . . . . . . 14  |-  ( ph  -> 
sum_ i  e.  ( ( 1  +  1 ) ... M ) ( 1st `  ( F `  ( G `  ( K `  i
) ) ) )  =  sum_ j  e.  ( ( ( 1  +  1 )  -  1 ) ... ( M  -  1 ) ) ( 1st `  ( F `  ( G `  ( K `  (
j  +  1 ) ) ) ) ) )
267 ax-1cn 9598 . . . . . . . . . . . . . . . . . 18  |-  1  e.  CC
268267, 267pncan3oi 9892 . . . . . . . . . . . . . . . . 17  |-  ( ( 1  +  1 )  -  1 )  =  1
269268oveq1i 6312 . . . . . . . . . . . . . . . 16  |-  ( ( ( 1  +  1 )  -  1 ) ... ( M  - 
1 ) )  =  ( 1 ... ( M  -  1 ) )
270269sumeq1i 13752 . . . . . . . . . . . . . . 15  |-  sum_ j  e.  ( ( ( 1  +  1 )  - 
1 ) ... ( M  -  1 ) ) ( 1st `  ( F `  ( G `  ( K `  (
j  +  1 ) ) ) ) )  =  sum_ j  e.  ( 1 ... ( M  -  1 ) ) ( 1st `  ( F `  ( G `  ( K `  (
j  +  1 ) ) ) ) )
271 oveq1 6309 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  i  ->  (
j  +  1 )  =  ( i  +  1 ) )
272271fveq2d 5882 . . . . . . . . . . . . . . . . . . 19  |-  ( j  =  i  ->  ( K `  ( j  +  1 ) )  =  ( K `  ( i  +  1 ) ) )
273272fveq2d 5882 . . . . . . . . . . . . . . . . . 18  |-  ( j  =  i  ->  ( G `  ( K `  ( j  +  1 ) ) )  =  ( G `  ( K `  ( i  +  1 ) ) ) )
274273fveq2d 5882 . . . . . . . . . . . . . . . . 17  |-  ( j  =  i  ->  ( F `  ( G `  ( K `  (
j  +  1 ) ) ) )  =  ( F `  ( G `  ( K `  ( i  +  1 ) ) ) ) )
275274fveq2d 5882 . . . . . . . . . . . . . . . 16  |-  ( j  =  i  ->  ( 1st `  ( F `  ( G `  ( K `
 ( j  +  1 ) ) ) ) )  =  ( 1st `  ( F `
 ( G `  ( K `  ( i  +  1 ) ) ) ) ) )
276275cbvsumv 13750 . . . . . . . . . . . . . . 15  |-  sum_ j  e.  ( 1 ... ( M  -  1 ) ) ( 1st `  ( F `  ( G `  ( K `  (
j  +  1 ) ) ) ) )  =  sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 1st `  ( F `  ( G `  ( K `  (
i  +  1 ) ) ) ) )
277270, 276eqtri 2451 . . . . . . . . . . . . . 14  |-  sum_ j  e.  ( ( ( 1  +  1 )  - 
1 ) ... ( M  -  1 ) ) ( 1st `  ( F `  ( G `  ( K `  (
j  +  1 ) ) ) ) )  =  sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 1st `  ( F `  ( G `  ( K `  (
i  +  1 ) ) ) ) )
278266, 277syl6eq 2479 . . . . . . . . . . . . 13  |-  ( ph  -> 
sum_ i  e.  ( ( 1  +  1 ) ... M ) ( 1st `  ( F `  ( G `  ( K `  i
) ) ) )  =  sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 1st `  ( F `  ( G `  ( K `  (
i  +  1 ) ) ) ) ) )
279255, 278oveq12d 6320 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 1st `  ( F `  ( G `  ( K `  1
) ) ) )  +  sum_ i  e.  ( ( 1  +  1 ) ... M ) ( 1st `  ( F `  ( G `  ( K `  i
) ) ) ) )  =  ( ( 1st `  ( F `
 ( G `  C ) ) )  +  sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 1st `  ( F `  ( G `  ( K `  (
i  +  1 ) ) ) ) ) ) )
280251, 279eqtrd 2463 . . . . . . . . . . 11  |-  ( ph  -> 
sum_ i  e.  ( 1 ... M ) ( 1st `  ( F `  ( G `  ( K `  i
) ) ) )  =  ( ( 1st `  ( F `  ( G `  C )
) )  +  sum_ i  e.  ( 1 ... ( M  - 
1 ) ) ( 1st `  ( F `
 ( G `  ( K `  ( i  +  1 ) ) ) ) ) ) )
281246, 280oveq12d 6320 . . . . . . . . . 10  |-  ( ph  ->  ( sum_ i  e.  ( 1 ... M ) ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  -  sum_ i  e.  ( 1 ... M ) ( 1st `  ( F `  ( G `  ( K `  i
) ) ) ) )  =  ( ( ( 2nd `  ( F `  ( G `  ( K `  M
) ) ) )  +  sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) ) )  -  ( ( 1st `  ( F `
 ( G `  C ) ) )  +  sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 1st `  ( F `  ( G `  ( K `  (
i  +  1 ) ) ) ) ) ) ) )
282204recnd 9670 . . . . . . . . . . 11  |-  ( ph  ->  ( 1st `  ( F `  ( G `  C ) ) )  e.  CC )
283 peano2nn 10622 . . . . . . . . . . . . . . . . . 18  |-  ( i  e.  NN  ->  (
i  +  1 )  e.  NN )
284 ffvelrn 6032 . . . . . . . . . . . . . . . . . 18  |-  ( ( K : NN --> U  /\  ( i  +  1 )  e.  NN )  ->  ( K `  ( i  +  1 ) )  e.  U
)
28515, 283, 284syl2an 479 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  NN )  ->  ( K `
 ( i  +  1 ) )  e.  U )
286219, 285ffvelrnd 6035 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  NN )  ->  ( G `
 ( K `  ( i  +  1 ) ) )  e.  NN )
287218, 286ffvelrnd 6035 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  NN )  ->  ( F `
 ( G `  ( K `  ( i  +  1 ) ) ) )  e.  ( RR  X.  RR ) )
288 xp1st 6834 . . . . . . . . . . . . . . 15  |-  ( ( F `  ( G `
 ( K `  ( i  +  1 ) ) ) )  e.  ( RR  X.  RR )  ->  ( 1st `  ( F `  ( G `  ( K `  ( i  +  1 ) ) ) ) )  e.  RR )
289287, 288syl 17 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  NN )  ->  ( 1st `  ( F `  ( G `  ( K `  ( i  +  1 ) ) ) ) )  e.  RR )
290240, 289sylan2 476 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  ( 1st `  ( F `  ( G `  ( K `
 ( i  +  1 ) ) ) ) )  e.  RR )
291239, 290fsumrecl 13788 . . . . . . . . . . . 12  |-  ( ph  -> 
sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 1st `  ( F `  ( G `  ( K `  (
i  +  1 ) ) ) ) )  e.  RR )
292291recnd 9670 . . . . . . . . . . 11  |-  ( ph  -> 
sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 1st `  ( F `  ( G `  ( K `  (
i  +  1 ) ) ) ) )  e.  CC )
293244, 243, 282, 292addsub4d 10034 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( 2nd `  ( F `  ( G `  ( K `  M ) ) ) )  +  sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) ) )  -  ( ( 1st `  ( F `
 ( G `  C ) ) )  +  sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 1st `  ( F `  ( G `  ( K `  (
i  +  1 ) ) ) ) ) ) )  =  ( ( ( 2nd `  ( F `  ( G `  ( K `  M
) ) ) )  -  ( 1st `  ( F `  ( G `  C ) ) ) )  +  ( sum_ i  e.  ( 1 ... ( M  - 
1 ) ) ( 2nd `  ( F `
 ( G `  ( K `  i ) ) ) )  -  sum_ i  e.  ( 1 ... ( M  - 
1 ) ) ( 1st `  ( F `
 ( G `  ( K `  ( i  +  1 ) ) ) ) ) ) ) )
294232, 281, 2933eqtrd 2467 . . . . . . . . 9  |-  ( ph  -> 
sum_ i  e.  ( 1 ... M ) ( ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  -  ( 1st `  ( F `  ( G `  ( K `  i
) ) ) ) )  =  ( ( ( 2nd `  ( F `  ( G `  ( K `  M
) ) ) )  -  ( 1st `  ( F `  ( G `  C ) ) ) )  +  ( sum_ i  e.  ( 1 ... ( M  - 
1 ) ) ( 2nd `  ( F `
 ( G `  ( K `  i ) ) ) )  -  sum_ i  e.  ( 1 ... ( M  - 
1 ) ) ( 1st `  ( F `
 ( G `  ( K `  ( i  +  1 ) ) ) ) ) ) ) )
295209, 217, 2943eqtrd 2467 . . . . . . . 8  |-  ( ph  -> 
sum_ j  e.  ( ( G  o.  K
) " ( 1 ... M ) ) ( ( ( abs 
o.  -  )  o.  F ) `  j
)  =  ( ( ( 2nd `  ( F `  ( G `  ( K `  M
) ) ) )  -  ( 1st `  ( F `  ( G `  C ) ) ) )  +  ( sum_ i  e.  ( 1 ... ( M  - 
1 ) ) ( 2nd `  ( F `
 ( G `  ( K `  i ) ) ) )  -  sum_ i  e.  ( 1 ... ( M  - 
1 ) ) ( 1st `  ( F `
 ( G `  ( K `  ( i  +  1 ) ) ) ) ) ) ) )
296295, 189eqeltrrd 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 )
297 fveq2 5878 . . . . . . . . . . . . . . 15  |-  ( n  =  M  ->  ( K `  n )  =  ( K `  M ) )
298297eleq2d 2492 . . . . . . . . . . . . . 14  |-  ( n  =  M  ->  ( B  e.  ( K `  n )  <->  B  e.  ( K `  M ) ) )
299298, 64elrab2 3231 . . . . . . . . . . . . 13  |-  ( M  e.  W  <->  ( M  e.  NN  /\  B  e.  ( K `  M
) ) )
300120, 299sylib 199 . . . . . . . . . . . 12  |-  ( ph  ->  ( M  e.  NN  /\  B  e.  ( K `
 M ) ) )
301300simprd 464 . . . . . . . . . . 11  |-  ( ph  ->  B  e.  ( K `
 M ) )
30296, 97, 98, 99, 100, 73, 101, 4, 102ovolicc2lem1 22457 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( K `  M )  e.  U
)  ->  ( B  e.  ( K `  M
)  <->  ( B  e.  RR  /\  ( 1st `  ( F `  ( G `  ( K `  M ) ) ) )  <  B  /\  B  <  ( 2nd `  ( F `  ( G `  ( K `  M
) ) ) ) ) ) )
303195, 302mpdan 672 . . . . . . . . . . 11  |-  ( ph  ->  ( B  e.  ( K `  M )  <-> 
( B  e.  RR  /\  ( 1st `  ( F `  ( G `  ( K `  M
) ) ) )  <  B  /\  B  <  ( 2nd `  ( F `  ( G `  ( K `  M
) ) ) ) ) ) )
304301, 303mpbid 213 . . . . . . . . . 10  |-  ( ph  ->  ( B  e.  RR  /\  ( 1st `  ( F `  ( G `  ( K `  M
) ) ) )  <  B  /\  B  <  ( 2nd `  ( F `  ( G `  ( K `  M
) ) ) ) ) )
305304simp3d 1019 . . . . . . . . 9  |-  ( ph  ->  B  <  ( 2nd `  ( F `  ( G `  ( K `  M ) ) ) ) )
30696, 97, 98, 99, 100, 73, 101, 4, 102ovolicc2lem1 22457 . . . . . . . . . . . 12  |-  ( (
ph  /\  C  e.  U )  ->  ( A  e.  C  <->  ( A  e.  RR  /\  ( 1st `  ( F `  ( G `  C )
) )  <  A  /\  A  <  ( 2nd `  ( F `  ( G `  C )
) ) ) ) )
307200, 306mpdan 672 . . . . . . . . . . 11  |-  ( ph  ->  ( A  e.  C  <->  ( A  e.  RR  /\  ( 1st `  ( F `
 ( G `  C ) ) )  <  A  /\  A  <  ( 2nd `  ( F `  ( G `  C ) ) ) ) ) )
308104, 307mpbid 213 . . . . . . . . . 10  |-  ( ph  ->  ( A  e.  RR  /\  ( 1st `  ( F `  ( G `  C ) ) )  <  A  /\  A  <  ( 2nd `  ( F `  ( G `  C ) ) ) ) )
309308simp2d 1018 . . . . . . . . 9  |-  ( ph  ->  ( 1st `  ( F `  ( G `  C ) ) )  <  A )
31097, 204, 199, 96, 305, 309lt2subd 10238 . . . . . . . 8  |-  ( ph  ->  ( B  -  A
)  <  ( ( 2nd `  ( F `  ( G `  ( K `
 M ) ) ) )  -  ( 1st `  ( F `  ( G `  C ) ) ) ) )
311158, 205, 310ltled 9784 . . . . . . 7  |-  ( ph  ->  ( B  -  A
)  <_  ( ( 2nd `  ( F `  ( G `  ( K `
 M ) ) ) )  -  ( 1st `  ( F `  ( G `  C ) ) ) ) )
312240adantl 467 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  i  e.  NN )
313 simpr 462 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  i  e.  ( 1 ... ( M  -  1 ) ) )
314257adantr 466 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  M  e.  ZZ )
315 elfzm11 11866 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 1  e.  ZZ  /\  M  e.  ZZ )  ->  ( i  e.  ( 1 ... ( M  -  1 ) )  <-> 
( i  e.  ZZ  /\  1  <_  i  /\  i  <  M ) ) )
31670, 314, 315sylancr 667 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  (
i  e.  ( 1 ... ( M  - 
1 ) )  <->  ( i  e.  ZZ  /\  1  <_ 
i  /\  i  <  M ) ) )
317313, 316mpbid 213 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  (
i  e.  ZZ  /\  1  <_  i  /\  i  <  M ) )
318317simp3d 1019 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  i  <  M )
319312nnred 10625 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  i  e.  RR )
320121adantr 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  M  e.  RR )
321319, 320ltnled 9783 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  (
i  <  M  <->  -.  M  <_  i ) )
322318, 321mpbid 213 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  -.  M  <_  i )
323 infmssuzleOLD 11247 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( W  C_  ( ZZ>= ` 
1 )  /\  i  e.  W )  ->  sup ( W ,  RR ,  `'  <  )  <_  i
)
32469, 323mpan 674 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  e.  W  ->  sup ( W ,  RR ,  `'  <  )  <_  i
)
32568, 324syl5eqbr 4454 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  W  ->  M  <_  i )
326322, 325nsyl 124 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  -.  i  e.  W )
327312, 326jca 534 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  (
i  e.  NN  /\  -.  i  e.  W
) )
32896, 97, 98, 99, 100, 73, 101, 4, 102, 11, 9, 103, 104, 8, 6, 64ovolicc2lem2 22458 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( i  e.  NN  /\  -.  i  e.  W ) )  -> 
( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  <_  B )
329327, 328syldan 472 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) )  <_  B
)
330329iftrued 3917 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  if ( ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  <_  B ,  ( 2nd `  ( F `
 ( G `  ( K `  i ) ) ) ) ,  B )  =  ( 2nd `  ( F `
 ( G `  ( K `  i ) ) ) ) )
331 ffvelrn 6032 . . . . . . . . . . . . . . . . 17  |-  ( ( K : NN --> T  /\  i  e.  NN )  ->  ( K `  i
)  e.  T )
33210, 240, 331syl2an 479 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  ( K `  i )  e.  T )
333103ralrimiva 2839 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  A. t  e.  T  if ( ( 2nd `  ( F `  ( G `  t ) ) )  <_  B ,  ( 2nd `  ( F `
 ( G `  t ) ) ) ,  B )  e.  ( H `  t
) )
334333adantr 466 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  A. t  e.  T  if (
( 2nd `  ( F `  ( G `  t ) ) )  <_  B ,  ( 2nd `  ( F `
 ( G `  t ) ) ) ,  B )  e.  ( H `  t
) )
335 fveq2 5878 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( t  =  ( K `  i )  ->  ( G `  t )  =  ( G `  ( K `  i ) ) )
336335fveq2d 5882 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  =  ( K `  i )  ->  ( F `  ( G `  t ) )  =  ( F `  ( G `  ( K `  i ) ) ) )
337336fveq2d 5882 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  ( K `  i )  ->  ( 2nd `  ( F `  ( G `  t ) ) )  =  ( 2nd `  ( F `
 ( G `  ( K `  i ) ) ) ) )
338337breq1d 4430 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  ( K `  i )  ->  (
( 2nd `  ( F `  ( G `  t ) ) )  <_  B  <->  ( 2nd `  ( F `  ( G `  ( K `  i ) ) ) )  <_  B )
)
339338, 337ifbieq1d 3932 . . . . . . . . . . . . . . . . . 18  |-  ( t  =  ( K `  i )  ->  if ( ( 2nd `  ( F `  ( G `  t ) ) )  <_  B ,  ( 2nd `  ( F `
 ( G `  t ) ) ) ,  B )  =  if ( ( 2nd `  ( F `  ( G `  ( K `  i ) ) ) )  <_  B , 
( 2nd `  ( F `  ( G `  ( K `  i
) ) ) ) ,  B ) )
340 fveq2 5878 . . . . . . . . . . . . . . . . . 18  |-  ( t  =  ( K `  i )  ->  ( H `  t )  =  ( H `  ( K `  i ) ) )
341339, 340eleq12d 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 )
) ) )
342341rspcv 3178 . . . . . . . . . . . . . . . 16  |-  ( ( K `  i )  e.  T  ->  ( A. t  e.  T  if ( ( 2nd `  ( F `  ( G `  t ) ) )  <_  B ,  ( 2nd `  ( F `
 ( G `  t ) ) ) ,  B )  e.  ( H `  t
)  ->  if (
( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  <_  B ,  ( 2nd `  ( F `
 ( G `  ( K `  i ) ) ) ) ,  B )  e.  ( H `  ( K `
 i ) ) ) )
343332, 334, 342sylc 62 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  if ( ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  <_  B ,  ( 2nd `  ( F `
 ( G `  ( K `  i ) ) ) ) ,  B )  e.  ( H `  ( K `
 i ) ) )
344330, 343eqeltrrd 2511 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) )  e.  ( H `  ( K `
 i ) ) )
3455, 6, 7, 8, 9algrp1 14521 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  NN )  ->  ( K `
 ( i  +  1 ) )  =  ( H `  ( K `  i )
) )
346240, 345sylan2 476 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  ( K `  ( i  +  1 ) )  =  ( H `  ( K `  i ) ) )
347344, 346eleqtrrd 2513 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) )  e.  ( K `  ( i  +  1 ) ) )
348240, 285sylan2 476 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  ( K `  ( i  +  1 ) )  e.  U )
34996, 97, 98, 99, 100, 73, 101, 4, 102ovolicc2lem1 22457 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( K `  ( i  +  1 ) )  e.  U
)  ->  ( ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) )  e.  ( K `  ( i  +  1 ) )  <-> 
( ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  e.  RR  /\  ( 1st `  ( F `  ( G `  ( K `
 ( i  +  1 ) ) ) ) )  <  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) )  /\  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) )  <  ( 2nd `  ( F `  ( G `  ( K `
 ( i  +  1 ) ) ) ) ) ) ) )
350348, 349syldan 472 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  (
( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  e.  ( K `  ( i  +  1 ) )  <->  ( ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) )  e.  RR  /\  ( 1st `  ( F `  ( G `  ( K `  (
i  +  1 ) ) ) ) )  <  ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  /\  ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  <  ( 2nd `  ( F `  ( G `  ( K `  (
i  +  1 ) ) ) ) ) ) ) )
351347, 350mpbid 213 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  (
( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  e.  RR  /\  ( 1st `  ( F `  ( G `  ( K `
 ( i  +  1 ) ) ) ) )  <  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) )  /\  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) )  <  ( 2nd `  ( F `  ( G `  ( K `
 ( i  +  1 ) ) ) ) ) ) )
352351simp2d 1018 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  ( 1st `  ( F `  ( G `  ( K `
 ( i  +  1 ) ) ) ) )  <  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) ) )
353290, 241, 352ltled 9784 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 1 ... ( M  -  1 ) ) )  ->  ( 1st `  ( F `  ( G `  ( K `
 ( i  +  1 ) ) ) ) )  <_  ( 2nd `  ( F `  ( G `  ( K `
 i ) ) ) ) )
354239, 290, 241, 353fsumle 13847 . . . . . . . . 9  |-  ( ph  -> 
sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 1st `  ( F `  ( G `  ( K `  (
i  +  1 ) ) ) ) )  <_  sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) ) )
355242, 291subge0d 10204 . . . . . . . . 9  |-  ( ph  ->  ( 0  <_  ( sum_ i  e.  ( 1 ... ( M  - 
1 ) ) ( 2nd `  ( F `
 ( G `  ( K `  i ) ) ) )  -  sum_ i  e.  ( 1 ... ( M  - 
1 ) ) ( 1st `  ( F `
 ( G `  ( K `  ( i  +  1 ) ) ) ) ) )  <->  sum_ i  e.  ( 1 ... ( M  - 
1 ) ) ( 1st `  ( F `
 ( G `  ( K `  ( i  +  1 ) ) ) ) )  <_  sum_ i  e.  ( 1 ... ( M  - 
1 ) ) ( 2nd `  ( F `
 ( G `  ( K `  i ) ) ) ) ) )
356354, 355mpbird 235 . . . . . . . 8  |-  ( ph  ->  0  <_  ( sum_ i  e.  ( 1 ... ( M  - 
1 ) ) ( 2nd `  ( F `
 ( G `  ( K `  i ) ) ) )  -  sum_ i  e.  ( 1 ... ( M  - 
1 ) ) ( 1st `  ( F `
 ( G `  ( K `  ( i  +  1 ) ) ) ) ) ) )
357242, 291resubcld 10048 . . . . . . . . 9  |-  ( ph  ->  ( sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 2nd `  ( F `  ( G `  ( K `  i
) ) ) )  -  sum_ i  e.  ( 1 ... ( M  -  1 ) ) ( 1st `  ( F `  ( G `  ( K `  (
i  +  1 ) ) ) ) ) )  e.  RR )
358205, 357addge01d 10202 . . . . . . . 8  |-  ( ph  ->  ( 0  <_  ( sum_ i  e.  ( 1 ... ( M  - 
1 ) ) ( 2nd `  ( F `
 ( G `  ( K `  i ) ) ) )  -  sum_ i  e.  ( 1 ... ( M  - 
1 ) ) ( 1st `  ( F `
 ( G `  ( K `  ( i  +  1 ) ) ) ) ) )  <-> 
( ( 2nd `  ( F `  ( G `  ( K `  M
) ) ) )  -  ( 1st `  ( F `  ( G `  C ) ) ) )  <_  ( (
( 2nd `  ( F `  ( G `  ( K `  M
) ) ) )  -  ( 1st `  ( F `  ( G `  C ) ) ) )  +  ( sum_ i  e.  ( 1 ... ( M  - 
1 ) ) ( 2nd `  ( F `
 ( G `  ( K `  i ) ) ) )  -  sum_ i  e.  ( 1 ... ( M  - 
1 ) ) ( 1st `  ( F `
 ( G `  ( K `  ( i  +  1 ) ) ) ) ) ) ) ) )
359356, 358mpbid 213 . . . . . . 7  |-  ( ph  ->  ( ( 2nd `  ( F `  ( G `  ( K `  M
) ) ) )  -  ( 1st `  ( F `  ( G `  C ) ) ) )  <_  ( (
( 2nd `  ( F `  ( G `  ( K `  M
) ) ) )  -  ( 1st `  ( F `  ( G `  C ) ) ) )  +  ( sum_ i  e.  ( 1 ... ( M  - 
1 ) ) ( 2nd `  ( F `
 ( G `  ( K `  i ) ) ) )  -  sum_ i  e.  ( 1 ... ( M  - 
1 ) ) ( 1st `  ( F `
 ( G `  ( K `  ( i  +  1 ) ) ) ) ) ) ) )
360158, 205, 296, 311, 359letrd 9793 . . . . . 6  |-  ( ph  ->  ( B  -  A
)  <_  ( (
( 2nd `  ( F `  ( G `  ( K `  M
) ) ) )  -  ( 1st `  ( F `  ( G `  C ) ) ) )  +  ( sum_ i  e.  ( 1 ... ( M  - 
1 ) ) ( 2nd `  ( F `
 ( G `  ( K `  i ) ) ) )  -  sum_ i  e.  ( 1 ... ( M  - 
1 ) ) ( 1st `  ( F `
 ( G `  ( K `  ( i  +  1 ) ) ) ) ) ) ) )
361360, 295breqtrrd 4447 . . . . 5  |-  ( ph  ->  ( B  -  A
)  <_  sum_ j  e.  ( ( G  o.  K ) " (
1 ... M ) ) ( ( ( abs 
o.  -  )  o.  F ) `  j
) )
362361adantr 466 . . . 4  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  ( B  -  A )  <_  sum_ j  e.  ( ( G  o.  K ) " (
1 ... M ) ) ( ( ( abs 
o.  -  )  o.  F ) `  j
) )
363 fzfid 12186 . . . . 5  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  ( 1 ... z )  e. 
Fin )
364170adantlr 719 . . . . 5  |-  ( ( ( ph  /\  (
z  e.  NN  /\  A. y  e.  ( ( G  o.  K )
" ( 1 ... M ) ) y  <  z ) )  /\  j  e.  ( 1 ... z ) )  ->  ( (
( abs  o.  -  )  o.  F ) `  j
)  e.  RR )
365169simprd 464 . . . . . 6  |-  ( (
ph  /\  j  e.  ( 1 ... z
) )  ->  0  <_  ( ( ( abs 
o.  -  )  o.  F ) `  j
) )
366365adantlr 719 . . . . 5  |-  ( ( ( ph  /\  (
z  e.  NN  /\  A. y  e.  ( ( G  o.  K )
" ( 1 ... M ) ) y  <  z ) )  /\  j  e.  ( 1 ... z ) )  ->  0  <_  ( ( ( abs  o.  -  )  o.  F
) `  j )
)
36724adantr 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  NN )  ->  ( ( G  o.  K )
" ( 1 ... M ) )  C_  NN )
368367sselda 3464 . . . . . . . . . . 11  |-  ( ( ( ph  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  y  e.  NN )
369368nnred 10625 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  y  e.  RR )
37031ad2antlr 731 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  z  e.  RR )
371 ltle 9723 . . . . . . . . . 10  |-  ( ( y  e.  RR  /\  z  e.  RR )  ->  ( y  <  z  ->  y  <_  z )
)
372369, 370, 371syl2anc 665 . . . . . . . . 9  |-  ( ( ( ph  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  ( y  <  z  ->  y  <_  z ) )
373368, 5syl6eleq 2520 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  y  e.  ( ZZ>= `  1 )
)
374 nnz 10960 . . . . . . . . . . 11  |-  ( z  e.  NN  ->  z  e.  ZZ )
375374ad2antlr 731 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  z  e.  ZZ )
376 elfz5 11793 . . . . . . . . . 10  |-  ( ( y  e.  ( ZZ>= ` 
1 )  /\  z  e.  ZZ )  ->  (
y  e.  ( 1 ... z )  <->  y  <_  z ) )
377373, 375, 376syl2anc 665 . . . . . . . . 9  |-  ( ( ( ph  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  ( y  e.  ( 1 ... z
)  <->  y  <_  z
) )
378372, 377sylibrd 237 . . . . . . . 8  |-  ( ( ( ph  /\  z  e.  NN )  /\  y  e.  ( ( G  o.  K ) " (
1 ... M ) ) )  ->  ( y  <  z  ->  y  e.  ( 1 ... z
) ) )
379378ralimdva 2833 . . . . . . 7  |-  ( (
ph  /\  z  e.  NN )  ->  ( A. y  e.  ( ( G  o.  K ) " ( 1 ... M ) ) y  <  z  ->  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  e.  ( 1 ... z ) ) )
380379impr 623 . . . . . 6  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  e.  ( 1 ... z ) )
381 dfss3 3454 . . . . . 6  |-  ( ( ( G  o.  K
) " ( 1 ... M ) ) 
C_  ( 1 ... z )  <->  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  e.  ( 1 ... z ) )
382380, 381sylibr 215 . . . . 5  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  ( ( G  o.  K ) " ( 1 ... M ) )  C_  ( 1 ... z
) )
383363, 364, 366, 382fsumless 13844 . . . 4  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  sum_ j  e.  ( ( G  o.  K ) " (
1 ... M ) ) ( ( ( abs 
o.  -  )  o.  F ) `  j
)  <_  sum_ j  e.  ( 1 ... z
) ( ( ( abs  o.  -  )  o.  F ) `  j
) )
384185, 190, 172, 362, 383letrd 9793 . . 3  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  ( B  -  A )  <_  sum_ j  e.  ( 1 ... z
) ( ( ( abs  o.  -  )  o.  F ) `  j
) )
385 eqidd 2423 . . . . . 6  |-  ( ( ( ph  /\  (
z  e.  NN  /\  A. y  e.  ( ( G  o.  K )
" ( 1 ... M ) ) y  <  z ) )  /\  j  e.  ( 1 ... z ) )  ->  ( (
( abs  o.  -  )  o.  F ) `  j
)  =  ( ( ( abs  o.  -  )  o.  F ) `  j ) )
386 simprl 762 . . . . . . 7  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  z  e.  NN )
387386, 5syl6eleq 2520 . . . . . 6  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  z  e.  ( ZZ>= `  1 )
)
388364recnd 9670 . . . . . 6  |-  ( ( ( ph  /\  (
z  e.  NN  /\  A. y  e.  ( ( G  o.  K )
" ( 1 ... M ) ) y  <  z ) )  /\  j  e.  ( 1 ... z ) )  ->  ( (
( abs  o.  -  )  o.  F ) `  j
)  e.  CC )
389385, 387, 388fsumser 13784 . . . . 5  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  sum_ j  e.  ( 1 ... z
) ( ( ( abs  o.  -  )  o.  F ) `  j
)  =  (  seq 1 (  +  , 
( ( abs  o.  -  )  o.  F
) ) `  z
) )
39099fveq1i 5879 . . . . 5  |-  ( S `
 z )  =  (  seq 1 (  +  ,  ( ( abs  o.  -  )  o.  F ) ) `  z )
391389, 390syl6eqr 2481 . . . 4  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  sum_ j  e.  ( 1 ... z
) ( ( ( abs  o.  -  )  o.  F ) `  j
)  =  ( S `
 z ) )
392181adantr 466 . . . . 5  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  ran  S  C_  RR* )
393 ffn 5743 . . . . . . . 8  |-  ( S : NN --> ( 0 [,) +oo )  ->  S  Fn  NN )
394175, 393syl 17 . . . . . . 7  |-  ( ph  ->  S  Fn  NN )
395394adantr 466 . . . . . 6  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  S  Fn  NN )
396 fnfvelrn 6031 . . . . . 6  |-  ( ( S  Fn  NN  /\  z  e.  NN )  ->  ( S `  z
)  e.  ran  S
)
397395, 386, 396syl2anc 665 . . . . 5  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  ( S `  z )  e.  ran  S )
398 supxrub 11611 . . . . 5  |-  ( ( ran  S  C_  RR*  /\  ( S `  z )  e.  ran  S )  -> 
( S `  z
)  <_  sup ( ran  S ,  RR* ,  <  ) )
399392, 397, 398syl2anc 665 . . . 4  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  ( S `  z )  <_  sup ( ran  S ,  RR* ,  <  ) )
400391, 399eqbrtrd 4441 . . 3  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  sum_ j  e.  ( 1 ... z
) ( ( ( abs  o.  -  )  o.  F ) `  j
)  <_  sup ( ran  S ,  RR* ,  <  ) )
401160, 173, 184, 384, 400xrletrd 11460 . 2  |-  ( (
ph  /\  ( z  e.  NN  /\  A. y  e.  ( ( G  o.  K ) " (
1 ... M ) ) y  <  z ) )  ->  ( B  -  A )  <_  sup ( ran  S ,  RR* ,  <  ) )
402157, 401rexlimddv 2921 1  |-  ( ph  ->  ( B  -  A
)  <_  sup ( ran  S ,  RR* ,  <  ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    /\ wa 370    /\ w3a 982    = wceq 1437    e. wcel 1868    =/= wne 2618   A.wral 2775   E.wrex 2776   {crab 2779    i^i cin 3435    C_ wss 3436   (/)c0 3761   ifcif 3909   ~Pcpw 3979   {csn 3996   U.cuni 4216   class class class wbr 4420    X. cxp 4848   `'ccnv 4849   ran crn 4851    |` cres 4852   "cima