Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  itgspltprt Structured version   Unicode version

Theorem itgspltprt 31620
Description: The  S. integral splits on a given partition  P. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
itgspltprt.1  |-  ( ph  ->  M  e.  ZZ )
itgspltprt.2  |-  ( ph  ->  N  e.  ( ZZ>= `  ( M  +  1
) ) )
itgspltprt.3  |-  ( ph  ->  P : ( M ... N ) --> RR )
itgspltprt.4  |-  ( (
ph  /\  i  e.  ( M..^ N ) )  ->  ( P `  i )  <  ( P `  ( i  +  1 ) ) )
itgspltprt.5  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  N )
) )  ->  A  e.  CC )
itgspltprt.6  |-  ( (
ph  /\  i  e.  ( M..^ N ) )  ->  ( t  e.  ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) )  |->  A )  e.  L^1 )
Assertion
Ref Expression
itgspltprt  |-  ( ph  ->  S. ( ( P `
 M ) [,] ( P `  N
) ) A  _d t  =  sum_ i  e.  ( M..^ N ) S. ( ( P `
 i ) [,] ( P `  (
i  +  1 ) ) ) A  _d t )
Distinct variable groups:    A, i    i, M, t    i, N, t    P, i, t    ph, i,
t
Allowed substitution hint:    A( t)

Proof of Theorem itgspltprt
Dummy variables  j 
k are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 itgspltprt.1 . . . . . 6  |-  ( ph  ->  M  e.  ZZ )
21peano2zd 10981 . . . . 5  |-  ( ph  ->  ( M  +  1 )  e.  ZZ )
3 itgspltprt.2 . . . . . 6  |-  ( ph  ->  N  e.  ( ZZ>= `  ( M  +  1
) ) )
4 eluzelz 11103 . . . . . 6  |-  ( N  e.  ( ZZ>= `  ( M  +  1 ) )  ->  N  e.  ZZ )
53, 4syl 16 . . . . 5  |-  ( ph  ->  N  e.  ZZ )
62, 5, 53jca 1176 . . . 4  |-  ( ph  ->  ( ( M  + 
1 )  e.  ZZ  /\  N  e.  ZZ  /\  N  e.  ZZ )
)
7 eluzle 11106 . . . . 5  |-  ( N  e.  ( ZZ>= `  ( M  +  1 ) )  ->  ( M  +  1 )  <_  N )
83, 7syl 16 . . . 4  |-  ( ph  ->  ( M  +  1 )  <_  N )
9 eluzelre 11104 . . . . . 6  |-  ( N  e.  ( ZZ>= `  ( M  +  1 ) )  ->  N  e.  RR )
103, 9syl 16 . . . . 5  |-  ( ph  ->  N  e.  RR )
1110leidd 10131 . . . 4  |-  ( ph  ->  N  <_  N )
126, 8, 11jca32 535 . . 3  |-  ( ph  ->  ( ( ( M  +  1 )  e.  ZZ  /\  N  e.  ZZ  /\  N  e.  ZZ )  /\  (
( M  +  1 )  <_  N  /\  N  <_  N ) ) )
13 elfz2 11691 . . 3  |-  ( N  e.  ( ( M  +  1 ) ... N )  <->  ( (
( M  +  1 )  e.  ZZ  /\  N  e.  ZZ  /\  N  e.  ZZ )  /\  (
( M  +  1 )  <_  N  /\  N  <_  N ) ) )
1412, 13sylibr 212 . 2  |-  ( ph  ->  N  e.  ( ( M  +  1 ) ... N ) )
15 fveq2 5872 . . . . . . 7  |-  ( j  =  ( M  + 
1 )  ->  ( P `  j )  =  ( P `  ( M  +  1
) ) )
1615oveq2d 6311 . . . . . 6  |-  ( j  =  ( M  + 
1 )  ->  (
( P `  M
) [,] ( P `
 j ) )  =  ( ( P `
 M ) [,] ( P `  ( M  +  1 ) ) ) )
17 itgeq1 22047 . . . . . 6  |-  ( ( ( P `  M
) [,] ( P `
 j ) )  =  ( ( P `
 M ) [,] ( P `  ( M  +  1 ) ) )  ->  S. ( ( P `  M ) [,] ( P `  j )
) A  _d t  =  S. ( ( P `  M ) [,] ( P `  ( M  +  1
) ) ) A  _d t )
1816, 17syl 16 . . . . 5  |-  ( j  =  ( M  + 
1 )  ->  S. ( ( P `  M ) [,] ( P `  j )
) A  _d t  =  S. ( ( P `  M ) [,] ( P `  ( M  +  1
) ) ) A  _d t )
19 oveq2 6303 . . . . . 6  |-  ( j  =  ( M  + 
1 )  ->  ( M..^ j )  =  ( M..^ ( M  + 
1 ) ) )
2019sumeq1d 13503 . . . . 5  |-  ( j  =  ( M  + 
1 )  ->  sum_ i  e.  ( M..^ j ) S. ( ( P `
 i ) [,] ( P `  (
i  +  1 ) ) ) A  _d t  =  sum_ i  e.  ( M..^ ( M  +  1 ) ) S. ( ( P `
 i ) [,] ( P `  (
i  +  1 ) ) ) A  _d t )
2118, 20eqeq12d 2489 . . . 4  |-  ( j  =  ( M  + 
1 )  ->  ( S. ( ( P `  M ) [,] ( P `  j )
) A  _d t  =  sum_ i  e.  ( M..^ j ) S. ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) ) A  _d t  <-> 
S. ( ( P `
 M ) [,] ( P `  ( M  +  1 ) ) ) A  _d t  =  sum_ i  e.  ( M..^ ( M  +  1 ) ) S. ( ( P `
 i ) [,] ( P `  (
i  +  1 ) ) ) A  _d t ) )
2221imbi2d 316 . . 3  |-  ( j  =  ( M  + 
1 )  ->  (
( ph  ->  S. ( ( P `  M
) [,] ( P `
 j ) ) A  _d t  = 
sum_ i  e.  ( M..^ j ) S. ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) ) A  _d t )  <->  ( ph  ->  S. ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) A  _d t  =  sum_ i  e.  ( M..^ ( M  + 
1 ) ) S. ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) ) A  _d t ) ) )
23 fveq2 5872 . . . . . . 7  |-  ( j  =  k  ->  ( P `  j )  =  ( P `  k ) )
2423oveq2d 6311 . . . . . 6  |-  ( j  =  k  ->  (
( P `  M
) [,] ( P `
 j ) )  =  ( ( P `
 M ) [,] ( P `  k
) ) )
25 itgeq1 22047 . . . . . 6  |-  ( ( ( P `  M
) [,] ( P `
 j ) )  =  ( ( P `
 M ) [,] ( P `  k
) )  ->  S. ( ( P `  M ) [,] ( P `  j )
) A  _d t  =  S. ( ( P `  M ) [,] ( P `  k ) ) A  _d t )
2624, 25syl 16 . . . . 5  |-  ( j  =  k  ->  S. ( ( P `  M ) [,] ( P `  j )
) A  _d t  =  S. ( ( P `  M ) [,] ( P `  k ) ) A  _d t )
27 oveq2 6303 . . . . . 6  |-  ( j  =  k  ->  ( M..^ j )  =  ( M..^ k ) )
2827sumeq1d 13503 . . . . 5  |-  ( j  =  k  ->  sum_ i  e.  ( M..^ j ) S. ( ( P `
 i ) [,] ( P `  (
i  +  1 ) ) ) A  _d t  =  sum_ i  e.  ( M..^ k ) S. ( ( P `
 i ) [,] ( P `  (
i  +  1 ) ) ) A  _d t )
2926, 28eqeq12d 2489 . . . 4  |-  ( j  =  k  ->  ( S. ( ( P `  M ) [,] ( P `  j )
) A  _d t  =  sum_ i  e.  ( M..^ j ) S. ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) ) A  _d t  <-> 
S. ( ( P `
 M ) [,] ( P `  k
) ) A  _d t  =  sum_ i  e.  ( M..^ k ) S. ( ( P `
 i ) [,] ( P `  (
i  +  1 ) ) ) A  _d t ) )
3029imbi2d 316 . . 3  |-  ( j  =  k  ->  (
( ph  ->  S. ( ( P `  M
) [,] ( P `
 j ) ) A  _d t  = 
sum_ i  e.  ( M..^ j ) S. ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) ) A  _d t )  <->  ( ph  ->  S. ( ( P `  M ) [,] ( P `  k )
) A  _d t  =  sum_ i  e.  ( M..^ k ) S. ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) ) A  _d t ) ) )
31 fveq2 5872 . . . . . . 7  |-  ( j  =  ( k  +  1 )  ->  ( P `  j )  =  ( P `  ( k  +  1 ) ) )
3231oveq2d 6311 . . . . . 6  |-  ( j  =  ( k  +  1 )  ->  (
( P `  M
) [,] ( P `
 j ) )  =  ( ( P `
 M ) [,] ( P `  (
k  +  1 ) ) ) )
33 itgeq1 22047 . . . . . 6  |-  ( ( ( P `  M
) [,] ( P `
 j ) )  =  ( ( P `
 M ) [,] ( P `  (
k  +  1 ) ) )  ->  S. ( ( P `  M ) [,] ( P `  j )
) A  _d t  =  S. ( ( P `  M ) [,] ( P `  ( k  +  1 ) ) ) A  _d t )
3432, 33syl 16 . . . . 5  |-  ( j  =  ( k  +  1 )  ->  S. ( ( P `  M ) [,] ( P `  j )
) A  _d t  =  S. ( ( P `  M ) [,] ( P `  ( k  +  1 ) ) ) A  _d t )
35 oveq2 6303 . . . . . 6  |-  ( j  =  ( k  +  1 )  ->  ( M..^ j )  =  ( M..^ ( k  +  1 ) ) )
3635sumeq1d 13503 . . . . 5  |-  ( j  =  ( k  +  1 )  ->  sum_ i  e.  ( M..^ j ) S. ( ( P `
 i ) [,] ( P `  (
i  +  1 ) ) ) A  _d t  =  sum_ i  e.  ( M..^ ( k  +  1 ) ) S. ( ( P `
 i ) [,] ( P `  (
i  +  1 ) ) ) A  _d t )
3734, 36eqeq12d 2489 . . . 4  |-  ( j  =  ( k  +  1 )  ->  ( S. ( ( P `  M ) [,] ( P `  j )
) A  _d t  =  sum_ i  e.  ( M..^ j ) S. ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) ) A  _d t  <-> 
S. ( ( P `
 M ) [,] ( P `  (
k  +  1 ) ) ) A  _d t  =  sum_ i  e.  ( M..^ ( k  +  1 ) ) S. ( ( P `
 i ) [,] ( P `  (
i  +  1 ) ) ) A  _d t ) )
3837imbi2d 316 . . 3  |-  ( j  =  ( k  +  1 )  ->  (
( ph  ->  S. ( ( P `  M
) [,] ( P `
 j ) ) A  _d t  = 
sum_ i  e.  ( M..^ j ) S. ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) ) A  _d t )  <->  ( ph  ->  S. ( ( P `  M ) [,] ( P `  ( k  +  1 ) ) ) A  _d t  =  sum_ i  e.  ( M..^ ( k  +  1 ) ) S. ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) ) A  _d t ) ) )
39 fveq2 5872 . . . . . . 7  |-  ( j  =  N  ->  ( P `  j )  =  ( P `  N ) )
4039oveq2d 6311 . . . . . 6  |-  ( j  =  N  ->  (
( P `  M
) [,] ( P `
 j ) )  =  ( ( P `
 M ) [,] ( P `  N
) ) )
41 itgeq1 22047 . . . . . 6  |-  ( ( ( P `  M
) [,] ( P `
 j ) )  =  ( ( P `
 M ) [,] ( P `  N
) )  ->  S. ( ( P `  M ) [,] ( P `  j )
) A  _d t  =  S. ( ( P `  M ) [,] ( P `  N ) ) A  _d t )
4240, 41syl 16 . . . . 5  |-  ( j  =  N  ->  S. ( ( P `  M ) [,] ( P `  j )
) A  _d t  =  S. ( ( P `  M ) [,] ( P `  N ) ) A  _d t )
43 oveq2 6303 . . . . . 6  |-  ( j  =  N  ->  ( M..^ j )  =  ( M..^ N ) )
4443sumeq1d 13503 . . . . 5  |-  ( j  =  N  ->  sum_ i  e.  ( M..^ j ) S. ( ( P `
 i ) [,] ( P `  (
i  +  1 ) ) ) A  _d t  =  sum_ i  e.  ( M..^ N ) S. ( ( P `
 i ) [,] ( P `  (
i  +  1 ) ) ) A  _d t )
4542, 44eqeq12d 2489 . . . 4  |-  ( j  =  N  ->  ( S. ( ( P `  M ) [,] ( P `  j )
) A  _d t  =  sum_ i  e.  ( M..^ j ) S. ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) ) A  _d t  <-> 
S. ( ( P `
 M ) [,] ( P `  N
) ) A  _d t  =  sum_ i  e.  ( M..^ N ) S. ( ( P `
 i ) [,] ( P `  (
i  +  1 ) ) ) A  _d t ) )
4645imbi2d 316 . . 3  |-  ( j  =  N  ->  (
( ph  ->  S. ( ( P `  M
) [,] ( P `
 j ) ) A  _d t  = 
sum_ i  e.  ( M..^ j ) S. ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) ) A  _d t )  <->  ( ph  ->  S. ( ( P `  M ) [,] ( P `  N )
) A  _d t  =  sum_ i  e.  ( M..^ N ) S. ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) ) A  _d t ) ) )
471adantl 466 . . . . . . . . 9  |-  ( ( N  e.  ( ZZ>= `  ( M  +  1
) )  /\  ph )  ->  M  e.  ZZ )
48 fzval3 11865 . . . . . . . . 9  |-  ( M  e.  ZZ  ->  ( M ... M )  =  ( M..^ ( M  +  1 ) ) )
4947, 48syl 16 . . . . . . . 8  |-  ( ( N  e.  ( ZZ>= `  ( M  +  1
) )  /\  ph )  ->  ( M ... M )  =  ( M..^ ( M  + 
1 ) ) )
5049eqcomd 2475 . . . . . . 7  |-  ( ( N  e.  ( ZZ>= `  ( M  +  1
) )  /\  ph )  ->  ( M..^ ( M  +  1 ) )  =  ( M ... M ) )
5150sumeq1d 13503 . . . . . 6  |-  ( ( N  e.  ( ZZ>= `  ( M  +  1
) )  /\  ph )  ->  sum_ i  e.  ( M..^ ( M  + 
1 ) ) S. ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) ) A  _d t  =  sum_ i  e.  ( M ... M ) S. ( ( P `
 i ) [,] ( P `  (
i  +  1 ) ) ) A  _d t )
52 simpl 457 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  ph )
53 itgspltprt.3 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  P : ( M ... N ) --> RR )
5452, 53syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  P : ( M ... N ) --> RR )
551zred 10978 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  M  e.  RR )
56 1re 9607 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  1  e.  RR
5756a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  1  e.  RR )
5855, 57readdcld 9635 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( M  +  1 )  e.  RR )
5955ltp1d 10488 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  M  <  ( M  +  1 ) )
6055, 58, 10, 59, 8ltletrd 9753 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  M  <  N )
6155, 10, 60ltled 9744 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  M  <_  N )
621, 5jca 532 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( M  e.  ZZ  /\  N  e.  ZZ ) )
63 eluz 11107 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( N  e.  (
ZZ>= `  M )  <->  M  <_  N ) )
6462, 63syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( N  e.  (
ZZ>= `  M )  <->  M  <_  N ) )
6561, 64mpbird 232 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  N  e.  ( ZZ>= `  M ) )
66 eluzfz1 11705 . . . . . . . . . . . . . . . . . . . . 21  |-  ( N  e.  ( ZZ>= `  M
)  ->  M  e.  ( M ... N ) )
6765, 66syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  M  e.  ( M ... N ) )
6867adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  M  e.  ( M ... N
) )
6954, 68jca 532 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  ( P : ( M ... N ) --> RR  /\  M  e.  ( M ... N ) ) )
70 ffvelrn 6030 . . . . . . . . . . . . . . . . . 18  |-  ( ( P : ( M ... N ) --> RR 
/\  M  e.  ( M ... N ) )  ->  ( P `  M )  e.  RR )
7169, 70syl 16 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  ( P `  M )  e.  RR )
7255lep1d 10489 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  M  <_  ( M  +  1 ) )
732, 72, 83jca 1176 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( M  + 
1 )  e.  ZZ  /\  M  <_  ( M  +  1 )  /\  ( M  +  1
)  <_  N )
)
74 elfz1 11689 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( ( M  + 
1 )  e.  ( M ... N )  <-> 
( ( M  + 
1 )  e.  ZZ  /\  M  <_  ( M  +  1 )  /\  ( M  +  1
)  <_  N )
) )
7562, 74syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( M  + 
1 )  e.  ( M ... N )  <-> 
( ( M  + 
1 )  e.  ZZ  /\  M  <_  ( M  +  1 )  /\  ( M  +  1
)  <_  N )
) )
7673, 75mpbird 232 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( M  +  1 )  e.  ( M ... N ) )
7753, 76jca 532 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( P : ( M ... N ) --> RR  /\  ( M  +  1 )  e.  ( M ... N
) ) )
78 ffvelrn 6030 . . . . . . . . . . . . . . . . . . 19  |-  ( ( P : ( M ... N ) --> RR 
/\  ( M  + 
1 )  e.  ( M ... N ) )  ->  ( P `  ( M  +  1 ) )  e.  RR )
7977, 78syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( P `  ( M  +  1 ) )  e.  RR )
8052, 79syl 16 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  ( P `  ( M  +  1 ) )  e.  RR )
81 simpr 461 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )
8271, 80, 813jca 1176 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  (
( P `  M
)  e.  RR  /\  ( P `  ( M  +  1 ) )  e.  RR  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) ) )
83 eliccre 31427 . . . . . . . . . . . . . . . 16  |-  ( ( ( P `  M
)  e.  RR  /\  ( P `  ( M  +  1 ) )  e.  RR  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  t  e.  RR )
8482, 83syl 16 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  t  e.  RR )
8553, 67, 70syl2anc 661 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( P `  M
)  e.  RR )
8685rexrd 9655 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( P `  M
)  e.  RR* )
8786adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  ( P `  M )  e.  RR* )
8880rexrd 9655 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  ( P `  ( M  +  1 ) )  e.  RR* )
8987, 88, 813jca 1176 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  (
( P `  M
)  e.  RR*  /\  ( P `  ( M  +  1 ) )  e.  RR*  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) ) )
90 iccgelb 11593 . . . . . . . . . . . . . . . 16  |-  ( ( ( P `  M
)  e.  RR*  /\  ( P `  ( M  +  1 ) )  e.  RR*  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  ( P `  M )  <_  t )
9189, 90syl 16 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  ( P `  M )  <_  t )
925, 61, 113jca 1176 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( N  e.  ZZ  /\  M  <_  N  /\  N  <_  N ) )
93 elfz1 11689 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( N  e.  ( M ... N )  <-> 
( N  e.  ZZ  /\  M  <_  N  /\  N  <_  N ) ) )
9462, 93syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( N  e.  ( M ... N )  <-> 
( N  e.  ZZ  /\  M  <_  N  /\  N  <_  N ) ) )
9592, 94mpbird 232 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  N  e.  ( M ... N ) )
9653, 95jca 532 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( P : ( M ... N ) --> RR  /\  N  e.  ( M ... N
) ) )
97 ffvelrn 6030 . . . . . . . . . . . . . . . . . 18  |-  ( ( P : ( M ... N ) --> RR 
/\  N  e.  ( M ... N ) )  ->  ( P `  N )  e.  RR )
9896, 97syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( P `  N
)  e.  RR )
9952, 98syl 16 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  ( P `  N )  e.  RR )
100 iccleub 11592 . . . . . . . . . . . . . . . . 17  |-  ( ( ( P `  M
)  e.  RR*  /\  ( P `  ( M  +  1 ) )  e.  RR*  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  t  <_  ( P `  ( M  +  1 ) ) )
10189, 100syl 16 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  t  <_  ( P `  ( M  +  1 ) ) )
10253adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... N
) )  ->  P : ( M ... N ) --> RR )
103 elfzelz 11700 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( i  e.  ( ( M  +  1 ) ... N )  ->  i  e.  ZZ )
104103adantl 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... N
) )  ->  i  e.  ZZ )
10555adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... N
) )  ->  M  e.  RR )
106104zred 10978 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... N
) )  ->  i  e.  RR )
10758adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... N
) )  ->  ( M  +  1 )  e.  RR )
10859adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... N
) )  ->  M  <  ( M  +  1 ) )
109 elfzle1 11701 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( i  e.  ( ( M  +  1 ) ... N )  ->  ( M  +  1 )  <_  i )
110109adantl 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... N
) )  ->  ( M  +  1 )  <_  i )
111105, 107, 106, 108, 110ltletrd 9753 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... N
) )  ->  M  <  i )
112105, 106, 111ltled 9744 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... N
) )  ->  M  <_  i )
113 elfzle2 11702 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( i  e.  ( ( M  +  1 ) ... N )  ->  i  <_  N )
114113adantl 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... N
) )  ->  i  <_  N )
115104, 112, 1143jca 1176 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... N
) )  ->  (
i  e.  ZZ  /\  M  <_  i  /\  i  <_  N ) )
11662adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... N
) )  ->  ( M  e.  ZZ  /\  N  e.  ZZ ) )
117 elfz1 11689 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( i  e.  ( M ... N )  <-> 
( i  e.  ZZ  /\  M  <_  i  /\  i  <_  N ) ) )
118116, 117syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... N
) )  ->  (
i  e.  ( M ... N )  <->  ( i  e.  ZZ  /\  M  <_ 
i  /\  i  <_  N ) ) )
119115, 118mpbird 232 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... N
) )  ->  i  e.  ( M ... N
) )
120102, 119jca 532 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... N
) )  ->  ( P : ( M ... N ) --> RR  /\  i  e.  ( M ... N ) ) )
121 ffvelrn 6030 . . . . . . . . . . . . . . . . . . 19  |-  ( ( P : ( M ... N ) --> RR 
/\  i  e.  ( M ... N ) )  ->  ( P `  i )  e.  RR )
122120, 121syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... N
) )  ->  ( P `  i )  e.  RR )
12353adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  P : ( M ... N ) --> RR )
124 elfzelz 11700 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( i  e.  ( ( M  +  1 ) ... ( N  -  1 ) )  ->  i  e.  ZZ )
125124adantl 466 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  i  e.  ZZ )
12655adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  M  e.  RR )
127125zred 10978 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  i  e.  RR )
12858adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  ( M  +  1 )  e.  RR )
12959adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  M  <  ( M  +  1 ) )
130 elfzle1 11701 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( i  e.  ( ( M  +  1 ) ... ( N  -  1 ) )  ->  ( M  +  1 )  <_  i )
131130adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  ( M  +  1 )  <_  i )
132126, 128, 127, 129, 131ltletrd 9753 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  M  <  i )
133126, 127, 132ltled 9744 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  M  <_  i )
13410adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  N  e.  RR )
13556a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  1  e.  RR )
136134, 135resubcld 9999 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  ( N  -  1 )  e.  RR )
137 elfzle2 11702 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( i  e.  ( ( M  +  1 ) ... ( N  -  1 ) )  ->  i  <_  ( N  -  1 ) )
138137adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  i  <_  ( N  -  1 ) )
139134ltm1d 10490 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  ( N  -  1 )  <  N )
140127, 136, 134, 138, 139lelttrd 9751 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  i  <  N )
141127, 134, 140ltled 9744 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  i  <_  N )
142125, 133, 1413jca 1176 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  (
i  e.  ZZ  /\  M  <_  i  /\  i  <_  N ) )
14362adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  ( M  e.  ZZ  /\  N  e.  ZZ ) )
144143, 117syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  (
i  e.  ( M ... N )  <->  ( i  e.  ZZ  /\  M  <_ 
i  /\  i  <_  N ) ) )
145142, 144mpbird 232 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  i  e.  ( M ... N
) )
146123, 145jca 532 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  ( P : ( M ... N ) --> RR  /\  i  e.  ( M ... N ) ) )
147146, 121syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  ( P `  i )  e.  RR )
148125peano2zd 10981 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  (
i  +  1 )  e.  ZZ )
149127, 135readdcld 9635 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  (
i  +  1 )  e.  RR )
150126, 127, 135, 132ltadd1dd 10175 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  ( M  +  1 )  <  ( i  +  1 ) )
151126, 128, 149, 129, 150lttrd 9754 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  M  <  ( i  +  1 ) )
152126, 149, 151ltled 9744 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  M  <_  ( i  +  1 ) )
1535, 124anim12ci 567 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  (
i  e.  ZZ  /\  N  e.  ZZ )
)
154 zltp1le 10924 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( i  e.  ZZ  /\  N  e.  ZZ )  ->  ( i  <  N  <->  ( i  +  1 )  <_  N ) )
155153, 154syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  (
i  <  N  <->  ( i  +  1 )  <_  N ) )
156140, 155mpbid 210 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  (
i  +  1 )  <_  N )
157148, 152, 1563jca 1176 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  (
( i  +  1 )  e.  ZZ  /\  M  <_  ( i  +  1 )  /\  (
i  +  1 )  <_  N ) )
158 elfz1 11689 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( ( i  +  1 )  e.  ( M ... N )  <-> 
( ( i  +  1 )  e.  ZZ  /\  M  <_  ( i  +  1 )  /\  ( i  +  1 )  <_  N )
) )
159143, 158syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  (
( i  +  1 )  e.  ( M ... N )  <->  ( (
i  +  1 )  e.  ZZ  /\  M  <_  ( i  +  1 )  /\  ( i  +  1 )  <_  N ) ) )
160157, 159mpbird 232 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  (
i  +  1 )  e.  ( M ... N ) )
161123, 160jca 532 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  ( P : ( M ... N ) --> RR  /\  ( i  +  1 )  e.  ( M ... N ) ) )
162 ffvelrn 6030 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( P : ( M ... N ) --> RR 
/\  ( i  +  1 )  e.  ( M ... N ) )  ->  ( P `  ( i  +  1 ) )  e.  RR )
163161, 162syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  ( P `  ( i  +  1 ) )  e.  RR )
164 simpl 457 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  ph )
1651, 124anim12i 566 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  ( M  e.  ZZ  /\  i  e.  ZZ ) )
166 eluz 11107 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( M  e.  ZZ  /\  i  e.  ZZ )  ->  ( i  e.  (
ZZ>= `  M )  <->  M  <_  i ) )
167165, 166syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  (
i  e.  ( ZZ>= `  M )  <->  M  <_  i ) )
168133, 167mpbird 232 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  i  e.  ( ZZ>= `  M )
)
169164, 5syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  N  e.  ZZ )
170168, 169, 1403jca 1176 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  (
i  e.  ( ZZ>= `  M )  /\  N  e.  ZZ  /\  i  < 
N ) )
171 elfzo2 11812 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( i  e.  ( M..^ N
)  <->  ( i  e.  ( ZZ>= `  M )  /\  N  e.  ZZ  /\  i  <  N ) )
172170, 171sylibr 212 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  i  e.  ( M..^ N ) )
173164, 172jca 532 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  ( ph  /\  i  e.  ( M..^ N ) ) )
174 itgspltprt.4 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( M..^ N ) )  ->  ( P `  i )  <  ( P `  ( i  +  1 ) ) )
175173, 174syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  ( P `  i )  <  ( P `  (
i  +  1 ) ) )
176147, 163, 175ltled 9744 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  ( P `  i )  <_  ( P `  (
i  +  1 ) ) )
1773, 122, 176monoord 12117 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( P `  ( M  +  1 ) )  <_  ( P `  N ) )
17852, 177syl 16 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  ( P `  ( M  +  1 ) )  <_  ( P `  N ) )
17984, 80, 99, 101, 178letrd 9750 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  t  <_  ( P `  N
) )
18084, 91, 1793jca 1176 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  (
t  e.  RR  /\  ( P `  M )  <_  t  /\  t  <_  ( P `  N
) ) )
18171, 99jca 532 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  (
( P `  M
)  e.  RR  /\  ( P `  N )  e.  RR ) )
182 elicc2 11601 . . . . . . . . . . . . . . 15  |-  ( ( ( P `  M
)  e.  RR  /\  ( P `  N )  e.  RR )  -> 
( t  e.  ( ( P `  M
) [,] ( P `
 N ) )  <-> 
( t  e.  RR  /\  ( P `  M
)  <_  t  /\  t  <_  ( P `  N ) ) ) )
183181, 182syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  (
t  e.  ( ( P `  M ) [,] ( P `  N ) )  <->  ( t  e.  RR  /\  ( P `
 M )  <_ 
t  /\  t  <_  ( P `  N ) ) ) )
184180, 183mpbird 232 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  t  e.  ( ( P `  M ) [,] ( P `  N )
) )
18552, 184jca 532 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  ( ph  /\  t  e.  ( ( P `  M
) [,] ( P `
 N ) ) ) )
186 itgspltprt.5 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  N )
) )  ->  A  e.  CC )
187185, 186syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  A  e.  CC )
188 id 22 . . . . . . . . . . . . 13  |-  ( ph  ->  ph )
189 fzolb 11814 . . . . . . . . . . . . . 14  |-  ( M  e.  ( M..^ N
)  <->  ( M  e.  ZZ  /\  N  e.  ZZ  /\  M  < 
N ) )
1901, 5, 60, 189syl3anbrc 1180 . . . . . . . . . . . . 13  |-  ( ph  ->  M  e.  ( M..^ N ) )
191188, 190jca 532 . . . . . . . . . . . 12  |-  ( ph  ->  ( ph  /\  M  e.  ( M..^ N ) ) )
192 eleq1 2539 . . . . . . . . . . . . . . 15  |-  ( i  =  M  ->  (
i  e.  ( M..^ N )  <->  M  e.  ( M..^ N ) ) )
193192anbi2d 703 . . . . . . . . . . . . . 14  |-  ( i  =  M  ->  (
( ph  /\  i  e.  ( M..^ N ) )  <->  ( ph  /\  M  e.  ( M..^ N ) ) ) )
194 fveq2 5872 . . . . . . . . . . . . . . . . 17  |-  ( i  =  M  ->  ( P `  i )  =  ( P `  M ) )
195 oveq1 6302 . . . . . . . . . . . . . . . . . 18  |-  ( i  =  M  ->  (
i  +  1 )  =  ( M  + 
1 ) )
196195fveq2d 5876 . . . . . . . . . . . . . . . . 17  |-  ( i  =  M  ->  ( P `  ( i  +  1 ) )  =  ( P `  ( M  +  1
) ) )
197194, 196oveq12d 6313 . . . . . . . . . . . . . . . 16  |-  ( i  =  M  ->  (
( P `  i
) [,] ( P `
 ( i  +  1 ) ) )  =  ( ( P `
 M ) [,] ( P `  ( M  +  1 ) ) ) )
198197mpteq1d 4534 . . . . . . . . . . . . . . 15  |-  ( i  =  M  ->  (
t  e.  ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) )  |->  A )  =  ( t  e.  ( ( P `
 M ) [,] ( P `  ( M  +  1 ) ) )  |->  A ) )
199198eleq1d 2536 . . . . . . . . . . . . . 14  |-  ( i  =  M  ->  (
( t  e.  ( ( P `  i
) [,] ( P `
 ( i  +  1 ) ) ) 
|->  A )  e.  L^1 
<->  ( t  e.  ( ( P `  M
) [,] ( P `
 ( M  + 
1 ) ) ) 
|->  A )  e.  L^1 ) )
200193, 199imbi12d 320 . . . . . . . . . . . . 13  |-  ( i  =  M  ->  (
( ( ph  /\  i  e.  ( M..^ N ) )  -> 
( t  e.  ( ( P `  i
) [,] ( P `
 ( i  +  1 ) ) ) 
|->  A )  e.  L^1 )  <->  ( ( ph  /\  M  e.  ( M..^ N ) )  -> 
( t  e.  ( ( P `  M
) [,] ( P `
 ( M  + 
1 ) ) ) 
|->  A )  e.  L^1 ) ) )
201 itgspltprt.6 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( M..^ N ) )  ->  ( t  e.  ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) )  |->  A )  e.  L^1 )
202201a1i 11 . . . . . . . . . . . . 13  |-  ( i  e.  ZZ  ->  (
( ph  /\  i  e.  ( M..^ N ) )  ->  ( t  e.  ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) )  |->  A )  e.  L^1 ) )
203200, 202vtoclga 3182 . . . . . . . . . . . 12  |-  ( M  e.  ZZ  ->  (
( ph  /\  M  e.  ( M..^ N ) )  ->  ( t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) )  |->  A )  e.  L^1 ) )
2041, 191, 203sylc 60 . . . . . . . . . . 11  |-  ( ph  ->  ( t  e.  ( ( P `  M
) [,] ( P `
 ( M  + 
1 ) ) ) 
|->  A )  e.  L^1 )
205187, 204itgcl 22058 . . . . . . . . . 10  |-  ( ph  ->  S. ( ( P `
 M ) [,] ( P `  ( M  +  1 ) ) ) A  _d t  e.  CC )
206205idi 2 . . . . . . . . 9  |-  ( ph  ->  S. ( ( P `
 M ) [,] ( P `  ( M  +  1 ) ) ) A  _d t  e.  CC )
2071, 206jca 532 . . . . . . . 8  |-  ( ph  ->  ( M  e.  ZZ  /\  S. ( ( P `
 M ) [,] ( P `  ( M  +  1 ) ) ) A  _d t  e.  CC ) )
208 itgeq1 22047 . . . . . . . . . 10  |-  ( ( ( P `  i
) [,] ( P `
 ( i  +  1 ) ) )  =  ( ( P `
 M ) [,] ( P `  ( M  +  1 ) ) )  ->  S. ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) ) A  _d t  =  S. ( ( P `  M ) [,] ( P `  ( M  +  1
) ) ) A  _d t )
209197, 208syl 16 . . . . . . . . 9  |-  ( i  =  M  ->  S. ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) ) A  _d t  =  S. ( ( P `  M ) [,] ( P `  ( M  +  1
) ) ) A  _d t )
210209fsum1 13544 . . . . . . . 8  |-  ( ( M  e.  ZZ  /\  S. ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) A  _d t  e.  CC )  ->  sum_ i  e.  ( M ... M ) S. ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) ) A  _d t  =  S. ( ( P `  M ) [,] ( P `  ( M  +  1
) ) ) A  _d t )
211207, 210syl 16 . . . . . . 7  |-  ( ph  -> 
sum_ i  e.  ( M ... M ) S. ( ( P `
 i ) [,] ( P `  (
i  +  1 ) ) ) A  _d t  =  S. ( ( P `  M
) [,] ( P `
 ( M  + 
1 ) ) ) A  _d t )
212211adantl 466 . . . . . 6  |-  ( ( N  e.  ( ZZ>= `  ( M  +  1
) )  /\  ph )  ->  sum_ i  e.  ( M ... M ) S. ( ( P `
 i ) [,] ( P `  (
i  +  1 ) ) ) A  _d t  =  S. ( ( P `  M
) [,] ( P `
 ( M  + 
1 ) ) ) A  _d t )
213 eqidd 2468 . . . . . 6  |-  ( ( N  e.  ( ZZ>= `  ( M  +  1
) )  /\  ph )  ->  S. ( ( P `  M ) [,] ( P `  ( M  +  1
) ) ) A  _d t  =  S. ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) A  _d t )
21451, 212, 2133eqtrd 2512 . . . . 5  |-  ( ( N  e.  ( ZZ>= `  ( M  +  1
) )  /\  ph )  ->  sum_ i  e.  ( M..^ ( M  + 
1 ) ) S. ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) ) A  _d t  =  S. ( ( P `  M ) [,] ( P `  ( M  +  1
) ) ) A  _d t )
215214eqcomd 2475 . . . 4  |-  ( ( N  e.  ( ZZ>= `  ( M  +  1
) )  /\  ph )  ->  S. ( ( P `  M ) [,] ( P `  ( M  +  1
) ) ) A  _d t  =  sum_ i  e.  ( M..^ ( M  +  1
) ) S. ( ( P `  i
) [,] ( P `
 ( i  +  1 ) ) ) A  _d t )
216215ex 434 . . 3  |-  ( N  e.  ( ZZ>= `  ( M  +  1 ) )  ->  ( ph  ->  S. ( ( P `
 M ) [,] ( P `  ( M  +  1 ) ) ) A  _d t  =  sum_ i  e.  ( M..^ ( M  +  1 ) ) S. ( ( P `
 i ) [,] ( P `  (
i  +  1 ) ) ) A  _d t ) )
217 simp3 998 . . . . . 6  |-  ( ( k  e.  ( ( M  +  1 )..^ N )  /\  ( ph  ->  S. ( ( P `  M ) [,] ( P `  k ) ) A  _d t  =  sum_ i  e.  ( M..^ k ) S. ( ( P `  i
) [,] ( P `
 ( i  +  1 ) ) ) A  _d t )  /\  ph )  ->  ph )
218 simp1 996 . . . . . 6  |-  ( ( k  e.  ( ( M  +  1 )..^ N )  /\  ( ph  ->  S. ( ( P `  M ) [,] ( P `  k ) ) A  _d t  =  sum_ i  e.  ( M..^ k ) S. ( ( P `  i
) [,] ( P `
 ( i  +  1 ) ) ) A  _d t )  /\  ph )  -> 
k  e.  ( ( M  +  1 )..^ N ) )
219 simp2 997 . . . . . . . 8  |-  ( ( k  e.  ( ( M  +  1 )..^ N )  /\  ( ph  ->  S. ( ( P `  M ) [,] ( P `  k ) ) A  _d t  =  sum_ i  e.  ( M..^ k ) S. ( ( P `  i
) [,] ( P `
 ( i  +  1 ) ) ) A  _d t )  /\  ph )  -> 
( ph  ->  S. ( ( P `  M
) [,] ( P `
 k ) ) A  _d t  = 
sum_ i  e.  ( M..^ k ) S. ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) ) A  _d t ) )
220217, 219jca 532 . . . . . . 7  |-  ( ( k  e.  ( ( M  +  1 )..^ N )  /\  ( ph  ->  S. ( ( P `  M ) [,] ( P `  k ) ) A  _d t  =  sum_ i  e.  ( M..^ k ) S. ( ( P `  i
) [,] ( P `
 ( i  +  1 ) ) ) A  _d t )  /\  ph )  -> 
( ph  /\  ( ph  ->  S. ( ( P `  M ) [,] ( P `  k ) ) A  _d t  =  sum_ i  e.  ( M..^ k ) S. ( ( P `  i
) [,] ( P `
 ( i  +  1 ) ) ) A  _d t ) ) )
221 pm3.35 587 . . . . . . 7  |-  ( (
ph  /\  ( ph  ->  S. ( ( P `
 M ) [,] ( P `  k
) ) A  _d t  =  sum_ i  e.  ( M..^ k ) S. ( ( P `
 i ) [,] ( P `  (
i  +  1 ) ) ) A  _d t ) )  ->  S. ( ( P `  M ) [,] ( P `  k )
) A  _d t  =  sum_ i  e.  ( M..^ k ) S. ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) ) A  _d t )
222220, 221syl 16 . . . . . 6  |-  ( ( k  e.  ( ( M  +  1 )..^ N )  /\  ( ph  ->  S. ( ( P `  M ) [,] ( P `  k ) ) A  _d t  =  sum_ i  e.  ( M..^ k ) S. ( ( P `  i
) [,] ( P `
 ( i  +  1 ) ) ) A  _d t )  /\  ph )  ->  S. ( ( P `  M ) [,] ( P `  k )
) A  _d t  =  sum_ i  e.  ( M..^ k ) S. ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) ) A  _d t )
223217, 218, 2223jca 1176 . . . . 5  |-  ( ( k  e.  ( ( M  +  1 )..^ N )  /\  ( ph  ->  S. ( ( P `  M ) [,] ( P `  k ) ) A  _d t  =  sum_ i  e.  ( M..^ k ) S. ( ( P `  i
) [,] ( P `
 ( i  +  1 ) ) ) A  _d t )  /\  ph )  -> 
( ph  /\  k  e.  ( ( M  + 
1 )..^ N )  /\  S. ( ( P `  M ) [,] ( P `  k ) ) A  _d t  =  sum_ i  e.  ( M..^ k ) S. ( ( P `  i
) [,] ( P `
 ( i  +  1 ) ) ) A  _d t ) )
22455adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  M  e.  RR )
225 elfzoelz 11809 . . . . . . . . . . . . 13  |-  ( k  e.  ( ( M  +  1 )..^ N
)  ->  k  e.  ZZ )
226225zred 10978 . . . . . . . . . . . 12  |-  ( k  e.  ( ( M  +  1 )..^ N
)  ->  k  e.  RR )
227226adantl 466 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  k  e.  RR )
22858adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  ( M  +  1 )  e.  RR )
22959adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  M  <  ( M  +  1 ) )
230 elfzole1 11816 . . . . . . . . . . . . 13  |-  ( k  e.  ( ( M  +  1 )..^ N
)  ->  ( M  +  1 )  <_ 
k )
231230adantl 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  ( M  +  1 )  <_ 
k )
232224, 228, 227, 229, 231ltletrd 9753 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  M  <  k )
233224, 227, 232ltled 9744 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  M  <_  k )
2341, 225anim12i 566 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  ( M  e.  ZZ  /\  k  e.  ZZ ) )
235 eluz 11107 . . . . . . . . . . 11  |-  ( ( M  e.  ZZ  /\  k  e.  ZZ )  ->  ( k  e.  (
ZZ>= `  M )  <->  M  <_  k ) )
236234, 235syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  ( k  e.  ( ZZ>= `  M )  <->  M  <_  k ) )
237233, 236mpbird 232 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  k  e.  ( ZZ>= `  M )
)
238188ad3antrrr 729 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  ->  ph )
239 eliccxr 31437 . . . . . . . . . . . . . . 15  |-  ( t  e.  ( ( P `
 i ) [,] ( P `  (
i  +  1 ) ) )  ->  t  e.  RR* )
240239adantl 466 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  -> 
t  e.  RR* )
241238, 85syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  -> 
( P `  M
)  e.  RR )
242238, 53syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  ->  P : ( M ... N ) --> RR )
243 elfzelz 11700 . . . . . . . . . . . . . . . . . . . . 21  |-  ( i  e.  ( M ... k )  ->  i  e.  ZZ )
244243adantl 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  i  e.  ZZ )
245 elfzle1 11701 . . . . . . . . . . . . . . . . . . . . 21  |-  ( i  e.  ( M ... k )  ->  M  <_  i )
246245adantl 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  M  <_  i )
247244zred 10978 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  i  e.  RR )
24810ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  N  e.  RR )
249227adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  k  e.  RR )
250 elfzle2 11702 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( i  e.  ( M ... k )  ->  i  <_  k )
251250adantl 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  i  <_  k )
252 elfzolt2 11817 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  e.  ( ( M  +  1 )..^ N
)  ->  k  <  N )
253252ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  k  <  N )
254247, 249, 248, 251, 253lelttrd 9751 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  i  <  N )
255247, 248, 254ltled 9744 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  i  <_  N )
256244, 246, 2553jca 1176 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  (
i  e.  ZZ  /\  M  <_  i  /\  i  <_  N ) )
25762ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  ( M  e.  ZZ  /\  N  e.  ZZ ) )
258257, 117syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  (
i  e.  ( M ... N )  <->  ( i  e.  ZZ  /\  M  <_ 
i  /\  i  <_  N ) ) )
259256, 258mpbird 232 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  i  e.  ( M ... N
) )
260259adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  -> 
i  e.  ( M ... N ) )
261242, 260jca 532 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  -> 
( P : ( M ... N ) --> RR  /\  i  e.  ( M ... N
) ) )
262261, 121syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  -> 
( P `  i
)  e.  RR )
263244peano2zd 10981 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  (
i  +  1 )  e.  ZZ )
264224adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  M  e.  RR )
265263zred 10978 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  (
i  +  1 )  e.  RR )
26655adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  i  e.  ( M ... k ) )  ->  M  e.  RR )
267243zred 10978 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( i  e.  ( M ... k )  ->  i  e.  RR )
268267adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  i  e.  ( M ... k ) )  ->  i  e.  RR )
26956a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  i  e.  ( M ... k ) )  ->  1  e.  RR )
270268, 269readdcld 9635 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  i  e.  ( M ... k ) )  ->  ( i  +  1 )  e.  RR )
271245adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  i  e.  ( M ... k ) )  ->  M  <_  i )
272268ltp1d 10488 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  i  e.  ( M ... k ) )  ->  i  <  ( i  +  1 ) )
273266, 268, 270, 271, 272lelttrd 9751 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  i  e.  ( M ... k ) )  ->  M  <  ( i  +  1 ) )
274273adantlr 714 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  M  <  ( i  +  1 ) )
275264, 265, 274ltled 9744 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  M  <_  ( i  +  1 ) )
2765, 243anim12ci 567 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  i  e.  ( M ... k ) )  ->  ( i  e.  ZZ  /\  N  e.  ZZ ) )
277276adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  (
i  e.  ZZ  /\  N  e.  ZZ )
)
278277, 154syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  (
i  <  N  <->  ( i  +  1 )  <_  N ) )
279254, 278mpbid 210 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  (
i  +  1 )  <_  N )
280263, 275, 2793jca 1176 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  (
( i  +  1 )  e.  ZZ  /\  M  <_  ( i  +  1 )  /\  (
i  +  1 )  <_  N ) )
281257, 158syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  (
( i  +  1 )  e.  ( M ... N )  <->  ( (
i  +  1 )  e.  ZZ  /\  M  <_  ( i  +  1 )  /\  ( i  +  1 )  <_  N ) ) )
282280, 281mpbird 232 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  (
i  +  1 )  e.  ( M ... N ) )
283282adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  -> 
( i  +  1 )  e.  ( M ... N ) )
284242, 283jca 532 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  -> 
( P : ( M ... N ) --> RR  /\  ( i  +  1 )  e.  ( M ... N
) ) )
285284, 162syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  -> 
( P `  (
i  +  1 ) )  e.  RR )
286 simpr 461 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  -> 
t  e.  ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) ) )
287262, 285, 2863jca 1176 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  -> 
( ( P `  i )  e.  RR  /\  ( P `  (
i  +  1 ) )  e.  RR  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) ) )
288 eliccre 31427 . . . . . . . . . . . . . . . 16  |-  ( ( ( P `  i
)  e.  RR  /\  ( P `  ( i  +  1 ) )  e.  RR  /\  t  e.  ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) ) )  ->  t  e.  RR )
289287, 288syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  -> 
t  e.  RR )
290 elfzuz 11696 . . . . . . . . . . . . . . . . . 18  |-  ( i  e.  ( M ... k )  ->  i  e.  ( ZZ>= `  M )
)
291290adantl 466 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  i  e.  ( ZZ>= `  M )
)
29253ad3antrrr 729 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... i ) )  ->  P : ( M ... N ) --> RR )
293 elfzelz 11700 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  e.  ( M ... i )  ->  j  e.  ZZ )
294293adantl 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... i ) )  -> 
j  e.  ZZ )
295 elfzle1 11701 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  e.  ( M ... i )  ->  M  <_  j )
296295adantl 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... i ) )  ->  M  <_  j )
297294zred 10978 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... i ) )  -> 
j  e.  RR )
298248adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... i ) )  ->  N  e.  RR )
299247adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... i ) )  -> 
i  e.  RR )
300 elfzle2 11702 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( j  e.  ( M ... i )  ->  j  <_  i )
301300adantl 466 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... i ) )  -> 
j  <_  i )
302254adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... i ) )  -> 
i  <  N )
303297, 299, 298, 301, 302lelttrd 9751 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... i ) )  -> 
j  <  N )
304297, 298, 303ltled 9744 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... i ) )  -> 
j  <_  N )
305294, 296, 3043jca 1176 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... i ) )  -> 
( j  e.  ZZ  /\  M  <_  j  /\  j  <_  N ) )
306257adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... i ) )  -> 
( M  e.  ZZ  /\  N  e.  ZZ ) )
307 elfz1 11689 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( j  e.  ( M ... N )  <-> 
( j  e.  ZZ  /\  M  <_  j  /\  j  <_  N ) ) )
308306, 307syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... i ) )  -> 
( j  e.  ( M ... N )  <-> 
( j  e.  ZZ  /\  M  <_  j  /\  j  <_  N ) ) )
309305, 308mpbird 232 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... i ) )  -> 
j  e.  ( M ... N ) )
310292, 309jca 532 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... i ) )  -> 
( P : ( M ... N ) --> RR  /\  j  e.  ( M ... N
) ) )
311 ffvelrn 6030 . . . . . . . . . . . . . . . . . 18  |-  ( ( P : ( M ... N ) --> RR 
/\  j  e.  ( M ... N ) )  ->  ( P `  j )  e.  RR )
312310, 311syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... i ) )  -> 
( P `  j
)  e.  RR )
31353ad3antrrr 729 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  P : ( M ... N ) --> RR )
314 elfzelz 11700 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  e.  ( M ... ( i  -  1 ) )  ->  j  e.  ZZ )
315314adantl 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
j  e.  ZZ )
316 elfzle1 11701 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  e.  ( M ... ( i  -  1 ) )  ->  M  <_  j )
317316adantl 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  M  <_  j )
318315zred 10978 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
j  e.  RR )
319248adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  N  e.  RR )
320247adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
i  e.  RR )
32156a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
1  e.  RR )
322320, 321resubcld 9999 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( i  -  1 )  e.  RR )
323 elfzle2 11702 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( j  e.  ( M ... ( i  -  1 ) )  ->  j  <_  ( i  -  1 ) )
324323adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
j  <_  ( i  -  1 ) )
325320ltm1d 10490 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( i  -  1 )  <  i )
326318, 322, 320, 324, 325lelttrd 9751 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
j  <  i )
327254adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
i  <  N )
328318, 320, 319, 326, 327lttrd 9754 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
j  <  N )
329318, 319, 328ltled 9744 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
j  <_  N )
330315, 317, 3293jca 1176 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( j  e.  ZZ  /\  M  <_  j  /\  j  <_  N ) )
331257adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( M  e.  ZZ  /\  N  e.  ZZ ) )
332331, 307syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( j  e.  ( M ... N )  <-> 
( j  e.  ZZ  /\  M  <_  j  /\  j  <_  N ) ) )
333330, 332mpbird 232 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
j  e.  ( M ... N ) )
334313, 333jca 532 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( P : ( M ... N ) --> RR  /\  j  e.  ( M ... N
) ) )
335334, 311syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( P `  j
)  e.  RR )
336315peano2zd 10981 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( j  +  1 )  e.  ZZ )
337264adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  M  e.  RR )
338318, 321readdcld 9635 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( j  +  1 )  e.  RR )
339 simplll 757 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  ph )
340 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
j  e.  ( M ... ( i  - 
1 ) ) )
341339, 340jca 532 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( ph  /\  j  e.  ( M ... (
i  -  1 ) ) ) )
34255adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  M  e.  RR )
343314zred 10978 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( j  e.  ( M ... ( i  -  1 ) )  ->  j  e.  RR )
344343adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  j  e.  RR )
34556a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  1  e.  RR )
346344, 345readdcld 9635 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  ( j  +  1 )  e.  RR )
347316adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  M  <_  j )
348344ltp1d 10488 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  j  <  ( j  +  1 ) )
349342, 344, 346, 347, 348lelttrd 9751 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  M  <  ( j  +  1 ) )
350341, 349syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  M  <  ( j  +  1 ) )
351337, 338, 350ltled 9744 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  M  <_  ( j  +  1 ) )
352244, 314anim12ci 567 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( j  e.  ZZ  /\  i  e.  ZZ ) )
353 zltp1le 10924 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( j  e.  ZZ  /\  i  e.  ZZ )  ->  ( j  <  i  <->  ( j  +  1 )  <_  i ) )
354352, 353syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( j  <  i  <->  ( j  +  1 )  <_  i ) )
355326, 354mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( j  +  1 )  <_  i )
356338, 320, 319, 355, 327lelttrd 9751 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( j  +  1 )  <  N )
357338, 319, 356ltled 9744 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( j  +  1 )  <_  N )
358336, 351, 3573jca 1176 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( ( j  +  1 )  e.  ZZ  /\  M  <_  ( j  +  1 )  /\  ( j  +  1 )  <_  N )
)
359 elfz1 11689 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( ( j  +  1 )  e.  ( M ... N )  <-> 
( ( j  +  1 )  e.  ZZ  /\  M  <_  ( j  +  1 )  /\  ( j  +  1 )  <_  N )
) )
360331, 359syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( ( j  +  1 )  e.  ( M ... N )  <-> 
( ( j  +  1 )  e.  ZZ  /\  M  <_  ( j  +  1 )  /\  ( j  +  1 )  <_  N )
) )
361358, 360mpbird 232 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( j  +  1 )  e.  ( M ... N ) )
362313, 361jca 532 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( P : ( M ... N ) --> RR  /\  ( j  +  1 )  e.  ( M ... N
) ) )
363 ffvelrn 6030 . . . . . . . . . . . . . . . . . . 19  |-  ( ( P : ( M ... N ) --> RR 
/\  ( j  +  1 )  e.  ( M ... N ) )  ->  ( P `  ( j  +  1 ) )  e.  RR )
364362, 363syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( P `  (
j  +  1 ) )  e.  RR )
365 elfzuz 11696 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  e.  ( M ... ( i  -  1 ) )  ->  j  e.  ( ZZ>= `  M )
)
366365adantl 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
j  e.  ( ZZ>= `  M ) )
367339, 5syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  N  e.  ZZ )
368366, 367, 3283jca 1176 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( j  e.  (
ZZ>= `  M )  /\  N  e.  ZZ  /\  j  <  N ) )
369 elfzo2 11812 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ( M..^ N
)  <->  ( j  e.  ( ZZ>= `  M )  /\  N  e.  ZZ  /\  j  <  N ) )
370368, 369sylibr 212 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
j  e.  ( M..^ N ) )
371339, 370jca 532 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( ph  /\  j  e.  ( M..^ N ) ) )
372 nfv 1683 . . . . . . . . . . . . . . . . . . . 20  |-  F/ i ( ( ph  /\  j  e.  ( M..^ N ) )  -> 
( P `  j
)  <  ( P `  ( j  +  1 ) ) )
373 eleq1 2539 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( i  =  j  ->  (
i  e.  ( M..^ N )  <->  j  e.  ( M..^ N ) ) )
374373anbi2d 703 . . . . . . . . . . . . . . . . . . . . 21  |-  ( i  =  j  ->  (
( ph  /\  i  e.  ( M..^ N ) )  <->  ( ph  /\  j  e.  ( M..^ N ) ) ) )
375 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( i  =  j  ->  ( P `  i )  =  ( P `  j ) )
376 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( i  =  j  ->  (
i  +  1 )  =  ( j  +  1 ) )
377376fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( i  =  j  ->  ( P `  ( i  +  1 ) )  =  ( P `  ( j  +  1 ) ) )
378375, 377breq12d 4466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( i  =  j  ->  (
( P `  i
)  <  ( P `  ( i  +  1 ) )  <->  ( P `  j )  <  ( P `  ( j  +  1 ) ) ) )
379374, 378imbi12d 320 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  =  j  ->  (
( ( ph  /\  i  e.  ( M..^ N ) )  -> 
( P `  i
)  <  ( P `  ( i  +  1 ) ) )  <->  ( ( ph  /\  j  e.  ( M..^ N ) )  ->  ( P `  j )  <  ( P `  ( j  +  1 ) ) ) ) )
380372, 379, 174chvar 1982 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( P `  j )  <  ( P `  ( j  +  1 ) ) )
381371, 380syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( P `  j
)  <  ( P `  ( j  +  1 ) ) )
382335, 364, 381ltled 9744 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( P `  j
)  <_  ( P `  ( j  +  1 ) ) )
383291, 312, 382monoord 12117 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  ( P `  M )  <_  ( P `  i
) )
384383adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  -> 
( P `  M
)  <_  ( P `  i ) )
385262rexrd 9655 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  -> 
( P `  i
)  e.  RR* )
386285rexrd 9655 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  -> 
( P `  (
i  +  1 ) )  e.  RR* )
387385, 386, 2863jca 1176 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  -> 
( ( P `  i )  e.  RR*  /\  ( P `  (
i  +  1 ) )  e.  RR*  /\  t  e.  ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) ) ) )
388 iccgelb 11593 . . . . . . . . . . . . . . . 16  |-  ( ( ( P `  i
)  e.  RR*  /\  ( P `  ( i  +  1 ) )  e.  RR*  /\  t  e.  ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) ) )  ->  ( P `  i )  <_  t )
389387, 388syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  -> 
( P `  i
)  <_  t )
390241, 262, 289, 384, 389letrd 9750 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  -> 
( P `  M
)  <_  t )
391238, 98syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  -> 
( P `  N
)  e.  RR )
392 iccleub 11592 . . . . . . . . . . . . . . . 16  |-  ( ( ( P `  i
)  e.  RR*  /\  ( P `  ( i  +  1 ) )  e.  RR*  /\  t  e.  ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) ) )  ->  t  <_  ( P `  (
i  +  1 ) ) )
393387, 392syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  -> 
t  <_  ( P `  ( i  +  1 ) ) )
394257simprd 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  N  e.  ZZ )
395263, 394jca 532 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  (
( i  +  1 )  e.  ZZ  /\  N  e.  ZZ )
)
396 eluz 11107 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( i  +  1 )  e.  ZZ  /\  N  e.  ZZ )  ->  ( N  e.  (
ZZ>= `  ( i  +  1 ) )  <->  ( i  +  1 )  <_  N ) )
397395, 396syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  k  e.  ( ( M <