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

Theorem itgspltprt 31732
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 10979 . . . . 5  |-  ( ph  ->  ( M  +  1 )  e.  ZZ )
3 itgspltprt.2 . . . . . 6  |-  ( ph  ->  N  e.  ( ZZ>= `  ( M  +  1
) ) )
4 eluzelz 11101 . . . . . 6  |-  ( N  e.  ( ZZ>= `  ( M  +  1 ) )  ->  N  e.  ZZ )
53, 4syl 16 . . . . 5  |-  ( ph  ->  N  e.  ZZ )
62, 5, 53jca 1177 . . . 4  |-  ( ph  ->  ( ( M  + 
1 )  e.  ZZ  /\  N  e.  ZZ  /\  N  e.  ZZ )
)
7 eluzle 11104 . . . . 5  |-  ( N  e.  ( ZZ>= `  ( M  +  1 ) )  ->  ( M  +  1 )  <_  N )
83, 7syl 16 . . . 4  |-  ( ph  ->  ( M  +  1 )  <_  N )
9 eluzelre 11102 . . . . . 6  |-  ( N  e.  ( ZZ>= `  ( M  +  1 ) )  ->  N  e.  RR )
103, 9syl 16 . . . . 5  |-  ( ph  ->  N  e.  RR )
1110leidd 10126 . . . 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 11690 . . 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 5856 . . . . . . 7  |-  ( j  =  ( M  + 
1 )  ->  ( P `  j )  =  ( P `  ( M  +  1
) ) )
1615oveq2d 6297 . . . . . 6  |-  ( j  =  ( M  + 
1 )  ->  (
( P `  M
) [,] ( P `
 j ) )  =  ( ( P `
 M ) [,] ( P `  ( M  +  1 ) ) ) )
1716itgeq1d 31709 . . . . 5  |-  ( j  =  ( M  + 
1 )  ->  S. ( ( P `  M ) [,] ( P `  j )
) A  _d t  =  S. ( ( P `  M ) [,] ( P `  ( M  +  1
) ) ) A  _d t )
18 oveq2 6289 . . . . . 6  |-  ( j  =  ( M  + 
1 )  ->  ( M..^ j )  =  ( M..^ ( M  + 
1 ) ) )
1918sumeq1d 13505 . . . . 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 )
2017, 19eqeq12d 2465 . . . 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 ) )
2120imbi2d 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 ) ) )
22 fveq2 5856 . . . . . . 7  |-  ( j  =  k  ->  ( P `  j )  =  ( P `  k ) )
2322oveq2d 6297 . . . . . 6  |-  ( j  =  k  ->  (
( P `  M
) [,] ( P `
 j ) )  =  ( ( P `
 M ) [,] ( P `  k
) ) )
2423itgeq1d 31709 . . . . 5  |-  ( j  =  k  ->  S. ( ( P `  M ) [,] ( P `  j )
) A  _d t  =  S. ( ( P `  M ) [,] ( P `  k ) ) A  _d t )
25 oveq2 6289 . . . . . 6  |-  ( j  =  k  ->  ( M..^ j )  =  ( M..^ k ) )
2625sumeq1d 13505 . . . . 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 )
2724, 26eqeq12d 2465 . . . 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 ) )
2827imbi2d 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 ) ) )
29 fveq2 5856 . . . . . . 7  |-  ( j  =  ( k  +  1 )  ->  ( P `  j )  =  ( P `  ( k  +  1 ) ) )
3029oveq2d 6297 . . . . . 6  |-  ( j  =  ( k  +  1 )  ->  (
( P `  M
) [,] ( P `
 j ) )  =  ( ( P `
 M ) [,] ( P `  (
k  +  1 ) ) ) )
3130itgeq1d 31709 . . . . 5  |-  ( j  =  ( k  +  1 )  ->  S. ( ( P `  M ) [,] ( P `  j )
) A  _d t  =  S. ( ( P `  M ) [,] ( P `  ( k  +  1 ) ) ) A  _d t )
32 oveq2 6289 . . . . . 6  |-  ( j  =  ( k  +  1 )  ->  ( M..^ j )  =  ( M..^ ( k  +  1 ) ) )
3332sumeq1d 13505 . . . . 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 )
3431, 33eqeq12d 2465 . . . 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 ) )
3534imbi2d 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 ) ) )
36 fveq2 5856 . . . . . . 7  |-  ( j  =  N  ->  ( P `  j )  =  ( P `  N ) )
3736oveq2d 6297 . . . . . 6  |-  ( j  =  N  ->  (
( P `  M
) [,] ( P `
 j ) )  =  ( ( P `
 M ) [,] ( P `  N
) ) )
3837itgeq1d 31709 . . . . 5  |-  ( j  =  N  ->  S. ( ( P `  M ) [,] ( P `  j )
) A  _d t  =  S. ( ( P `  M ) [,] ( P `  N ) ) A  _d t )
39 oveq2 6289 . . . . . 6  |-  ( j  =  N  ->  ( M..^ j )  =  ( M..^ N ) )
4039sumeq1d 13505 . . . . 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 )
4138, 40eqeq12d 2465 . . . 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 ) )
4241imbi2d 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 ) ) )
431adantl 466 . . . . . . . 8  |-  ( ( N  e.  ( ZZ>= `  ( M  +  1
) )  /\  ph )  ->  M  e.  ZZ )
44 fzval3 11867 . . . . . . . 8  |-  ( M  e.  ZZ  ->  ( M ... M )  =  ( M..^ ( M  +  1 ) ) )
4543, 44syl 16 . . . . . . 7  |-  ( ( N  e.  ( ZZ>= `  ( M  +  1
) )  /\  ph )  ->  ( M ... M )  =  ( M..^ ( M  + 
1 ) ) )
4645eqcomd 2451 . . . . . 6  |-  ( ( N  e.  ( ZZ>= `  ( M  +  1
) )  /\  ph )  ->  ( M..^ ( M  +  1 ) )  =  ( M ... M ) )
4746sumeq1d 13505 . . . . 5  |-  ( ( 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 )
48 itgspltprt.3 . . . . . . . . . . . 12  |-  ( ph  ->  P : ( M ... N ) --> RR )
4948adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  P : ( M ... N ) --> RR )
501zred 10976 . . . . . . . . . . . . . . 15  |-  ( ph  ->  M  e.  RR )
51 1red 9614 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  1  e.  RR )
5250, 51readdcld 9626 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( M  +  1 )  e.  RR )
5350ltp1d 10483 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  M  <  ( M  +  1 ) )
5450, 52, 10, 53, 8ltletrd 9745 . . . . . . . . . . . . . . 15  |-  ( ph  ->  M  <  N )
5550, 10, 54ltled 9736 . . . . . . . . . . . . . 14  |-  ( ph  ->  M  <_  N )
56 eluz 11105 . . . . . . . . . . . . . . 15  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( N  e.  (
ZZ>= `  M )  <->  M  <_  N ) )
571, 5, 56syl2anc 661 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( N  e.  (
ZZ>= `  M )  <->  M  <_  N ) )
5855, 57mpbird 232 . . . . . . . . . . . . 13  |-  ( ph  ->  N  e.  ( ZZ>= `  M ) )
59 eluzfz1 11704 . . . . . . . . . . . . 13  |-  ( N  e.  ( ZZ>= `  M
)  ->  M  e.  ( M ... N ) )
6058, 59syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  M  e.  ( M ... N ) )
6160adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  M  e.  ( M ... N
) )
6249, 61ffvelrnd 6017 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  ( P `  M )  e.  RR )
63 elfz1 11688 . . . . . . . . . . . . . 14  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( N  e.  ( M ... N )  <-> 
( N  e.  ZZ  /\  M  <_  N  /\  N  <_  N ) ) )
641, 5, 63syl2anc 661 . . . . . . . . . . . . 13  |-  ( ph  ->  ( N  e.  ( M ... N )  <-> 
( N  e.  ZZ  /\  M  <_  N  /\  N  <_  N ) ) )
655, 55, 11, 64mpbir3and 1180 . . . . . . . . . . . 12  |-  ( ph  ->  N  e.  ( M ... N ) )
6648, 65ffvelrnd 6017 . . . . . . . . . . 11  |-  ( ph  ->  ( P `  N
)  e.  RR )
6766adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  ( P `  N )  e.  RR )
6850lep1d 10484 . . . . . . . . . . . . . 14  |-  ( ph  ->  M  <_  ( M  +  1 ) )
69 elfz1 11688 . . . . . . . . . . . . . . 15  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( ( M  + 
1 )  e.  ( M ... N )  <-> 
( ( M  + 
1 )  e.  ZZ  /\  M  <_  ( M  +  1 )  /\  ( M  +  1
)  <_  N )
) )
701, 5, 69syl2anc 661 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( M  + 
1 )  e.  ( M ... N )  <-> 
( ( M  + 
1 )  e.  ZZ  /\  M  <_  ( M  +  1 )  /\  ( M  +  1
)  <_  N )
) )
712, 68, 8, 70mpbir3and 1180 . . . . . . . . . . . . 13  |-  ( ph  ->  ( M  +  1 )  e.  ( M ... N ) )
7248, 71ffvelrnd 6017 . . . . . . . . . . . 12  |-  ( ph  ->  ( P `  ( M  +  1 ) )  e.  RR )
7372adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  ( P `  ( M  +  1 ) )  e.  RR )
74 simpr 461 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )
75 eliccre 31494 . . . . . . . . . . 11  |-  ( ( ( P `  M
)  e.  RR  /\  ( P `  ( M  +  1 ) )  e.  RR  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  t  e.  RR )
7662, 73, 74, 75syl3anc 1229 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  t  e.  RR )
7748, 60ffvelrnd 6017 . . . . . . . . . . . . 13  |-  ( ph  ->  ( P `  M
)  e.  RR )
7877rexrd 9646 . . . . . . . . . . . 12  |-  ( ph  ->  ( P `  M
)  e.  RR* )
7978adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  ( P `  M )  e.  RR* )
8073rexrd 9646 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  ( P `  ( M  +  1 ) )  e.  RR* )
81 iccgelb 11592 . . . . . . . . . . 11  |-  ( ( ( P `  M
)  e.  RR*  /\  ( P `  ( M  +  1 ) )  e.  RR*  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  ( P `  M )  <_  t )
8279, 80, 74, 81syl3anc 1229 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  ( P `  M )  <_  t )
83 iccleub 11591 . . . . . . . . . . . 12  |-  ( ( ( P `  M
)  e.  RR*  /\  ( P `  ( M  +  1 ) )  e.  RR*  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  t  <_  ( P `  ( M  +  1 ) ) )
8479, 80, 74, 83syl3anc 1229 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  t  <_  ( P `  ( M  +  1 ) ) )
8548adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... N
) )  ->  P : ( M ... N ) --> RR )
86 elfzelz 11699 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( ( M  +  1 ) ... N )  ->  i  e.  ZZ )
8786adantl 466 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... N
) )  ->  i  e.  ZZ )
8850adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... N
) )  ->  M  e.  RR )
8987zred 10976 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... N
) )  ->  i  e.  RR )
9052adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... N
) )  ->  ( M  +  1 )  e.  RR )
9153adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... N
) )  ->  M  <  ( M  +  1 ) )
92 elfzle1 11700 . . . . . . . . . . . . . . . . . 18  |-  ( i  e.  ( ( M  +  1 ) ... N )  ->  ( M  +  1 )  <_  i )
9392adantl 466 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... N
) )  ->  ( M  +  1 )  <_  i )
9488, 90, 89, 91, 93ltletrd 9745 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... N
) )  ->  M  <  i )
9588, 89, 94ltled 9736 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... N
) )  ->  M  <_  i )
96 elfzle2 11701 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( ( M  +  1 ) ... N )  ->  i  <_  N )
9796adantl 466 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... N
) )  ->  i  <_  N )
981, 5jca 532 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( M  e.  ZZ  /\  N  e.  ZZ ) )
9998adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... N
) )  ->  ( M  e.  ZZ  /\  N  e.  ZZ ) )
100 elfz1 11688 . . . . . . . . . . . . . . . 16  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( i  e.  ( M ... N )  <-> 
( i  e.  ZZ  /\  M  <_  i  /\  i  <_  N ) ) )
10199, 100syl 16 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... N
) )  ->  (
i  e.  ( M ... N )  <->  ( i  e.  ZZ  /\  M  <_ 
i  /\  i  <_  N ) ) )
10287, 95, 97, 101mpbir3and 1180 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... N
) )  ->  i  e.  ( M ... N
) )
10385, 102ffvelrnd 6017 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... N
) )  ->  ( P `  i )  e.  RR )
10448adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  P : ( M ... N ) --> RR )
105 elfzelz 11699 . . . . . . . . . . . . . . . . 17  |-  ( i  e.  ( ( M  +  1 ) ... ( N  -  1 ) )  ->  i  e.  ZZ )
106105adantl 466 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  i  e.  ZZ )
10750adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  M  e.  RR )
108106zred 10976 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  i  e.  RR )
10952adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  ( M  +  1 )  e.  RR )
11053adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  M  <  ( M  +  1 ) )
111 elfzle1 11700 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  ( ( M  +  1 ) ... ( N  -  1 ) )  ->  ( M  +  1 )  <_  i )
112111adantl 466 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  ( M  +  1 )  <_  i )
113107, 109, 108, 110, 112ltletrd 9745 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  M  <  i )
114107, 108, 113ltled 9736 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  M  <_  i )
11510adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  N  e.  RR )
116 1red 9614 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  1  e.  RR )
117115, 116resubcld 9994 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  ( N  -  1 )  e.  RR )
118 elfzle2 11701 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  ( ( M  +  1 ) ... ( N  -  1 ) )  ->  i  <_  ( N  -  1 ) )
119118adantl 466 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  i  <_  ( N  -  1 ) )
120115ltm1d 10485 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  ( N  -  1 )  <  N )
121108, 117, 115, 119, 120lelttrd 9743 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  i  <  N )
122108, 115, 121ltled 9736 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  i  <_  N )
12398adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  ( M  e.  ZZ  /\  N  e.  ZZ ) )
124123, 100syl 16 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  (
i  e.  ( M ... N )  <->  ( i  e.  ZZ  /\  M  <_ 
i  /\  i  <_  N ) ) )
125106, 114, 122, 124mpbir3and 1180 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  i  e.  ( M ... N
) )
126104, 125ffvelrnd 6017 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  ( P `  i )  e.  RR )
127106peano2zd 10979 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  (
i  +  1 )  e.  ZZ )
128108, 116readdcld 9626 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  (
i  +  1 )  e.  RR )
129107, 108, 116, 113ltadd1dd 10170 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  ( M  +  1 )  <  ( i  +  1 ) )
130107, 109, 128, 110, 129lttrd 9746 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  M  <  ( i  +  1 ) )
131107, 128, 130ltled 9736 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  M  <_  ( i  +  1 ) )
132 zltp1le 10920 . . . . . . . . . . . . . . . . . 18  |-  ( ( i  e.  ZZ  /\  N  e.  ZZ )  ->  ( i  <  N  <->  ( i  +  1 )  <_  N ) )
133105, 5, 132syl2anr 478 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  (
i  <  N  <->  ( i  +  1 )  <_  N ) )
134121, 133mpbid 210 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  (
i  +  1 )  <_  N )
135 elfz1 11688 . . . . . . . . . . . . . . . . 17  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( ( i  +  1 )  e.  ( M ... N )  <-> 
( ( i  +  1 )  e.  ZZ  /\  M  <_  ( i  +  1 )  /\  ( i  +  1 )  <_  N )
) )
136123, 135syl 16 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  (
( i  +  1 )  e.  ( M ... N )  <->  ( (
i  +  1 )  e.  ZZ  /\  M  <_  ( i  +  1 )  /\  ( i  +  1 )  <_  N ) ) )
137127, 131, 134, 136mpbir3and 1180 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  (
i  +  1 )  e.  ( M ... N ) )
138104, 137ffvelrnd 6017 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  ( P `  ( i  +  1 ) )  e.  RR )
139 eluz 11105 . . . . . . . . . . . . . . . . . 18  |-  ( ( M  e.  ZZ  /\  i  e.  ZZ )  ->  ( i  e.  (
ZZ>= `  M )  <->  M  <_  i ) )
1401, 105, 139syl2an 477 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  (
i  e.  ( ZZ>= `  M )  <->  M  <_  i ) )
141114, 140mpbird 232 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  i  e.  ( ZZ>= `  M )
)
1425adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  N  e.  ZZ )
143 elfzo2 11814 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( M..^ N
)  <->  ( i  e.  ( ZZ>= `  M )  /\  N  e.  ZZ  /\  i  <  N ) )
144141, 142, 121, 143syl3anbrc 1181 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  i  e.  ( M..^ N ) )
145 itgspltprt.4 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( M..^ N ) )  ->  ( P `  i )  <  ( P `  ( i  +  1 ) ) )
146144, 145syldan 470 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  ( P `  i )  <  ( P `  (
i  +  1 ) ) )
147126, 138, 146ltled 9736 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  ( P `  i )  <_  ( P `  (
i  +  1 ) ) )
1483, 103, 147monoord 12119 . . . . . . . . . . . 12  |-  ( ph  ->  ( P `  ( M  +  1 ) )  <_  ( P `  N ) )
149148adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  ( P `  ( M  +  1 ) )  <_  ( P `  N ) )
15076, 73, 67, 84, 149letrd 9742 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  t  <_  ( P `  N
) )
15162, 67, 76, 82, 150eliccd 31492 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  t  e.  ( ( P `  M ) [,] ( P `  N )
) )
152 itgspltprt.5 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  N )
) )  ->  A  e.  CC )
153151, 152syldan 470 . . . . . . . 8  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  A  e.  CC )
154 id 22 . . . . . . . . . 10  |-  ( ph  ->  ph )
155 fzolb 11816 . . . . . . . . . . 11  |-  ( M  e.  ( M..^ N
)  <->  ( M  e.  ZZ  /\  N  e.  ZZ  /\  M  < 
N ) )
1561, 5, 54, 155syl3anbrc 1181 . . . . . . . . . 10  |-  ( ph  ->  M  e.  ( M..^ N ) )
157154, 156jca 532 . . . . . . . . 9  |-  ( ph  ->  ( ph  /\  M  e.  ( M..^ N ) ) )
158 eleq1 2515 . . . . . . . . . . . 12  |-  ( i  =  M  ->  (
i  e.  ( M..^ N )  <->  M  e.  ( M..^ N ) ) )
159158anbi2d 703 . . . . . . . . . . 11  |-  ( i  =  M  ->  (
( ph  /\  i  e.  ( M..^ N ) )  <->  ( ph  /\  M  e.  ( M..^ N ) ) ) )
160 fveq2 5856 . . . . . . . . . . . . . 14  |-  ( i  =  M  ->  ( P `  i )  =  ( P `  M ) )
161 oveq1 6288 . . . . . . . . . . . . . . 15  |-  ( i  =  M  ->  (
i  +  1 )  =  ( M  + 
1 ) )
162161fveq2d 5860 . . . . . . . . . . . . . 14  |-  ( i  =  M  ->  ( P `  ( i  +  1 ) )  =  ( P `  ( M  +  1
) ) )
163160, 162oveq12d 6299 . . . . . . . . . . . . 13  |-  ( i  =  M  ->  (
( P `  i
) [,] ( P `
 ( i  +  1 ) ) )  =  ( ( P `
 M ) [,] ( P `  ( M  +  1 ) ) ) )
164163mpteq1d 4518 . . . . . . . . . . . 12  |-  ( i  =  M  ->  (
t  e.  ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) )  |->  A )  =  ( t  e.  ( ( P `
 M ) [,] ( P `  ( M  +  1 ) ) )  |->  A ) )
165164eleq1d 2512 . . . . . . . . . . 11  |-  ( i  =  M  ->  (
( t  e.  ( ( P `  i
) [,] ( P `
 ( i  +  1 ) ) ) 
|->  A )  e.  L^1 
<->  ( t  e.  ( ( P `  M
) [,] ( P `
 ( M  + 
1 ) ) ) 
|->  A )  e.  L^1 ) )
166159, 165imbi12d 320 . . . . . . . . . 10  |-  ( 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 ) ) )
167 itgspltprt.6 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( M..^ N ) )  ->  ( t  e.  ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) )  |->  A )  e.  L^1 )
168166, 167vtoclg 3153 . . . . . . . . 9  |-  ( M  e.  ZZ  ->  (
( ph  /\  M  e.  ( M..^ N ) )  ->  ( t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) )  |->  A )  e.  L^1 ) )
1691, 157, 168sylc 60 . . . . . . . 8  |-  ( ph  ->  ( t  e.  ( ( P `  M
) [,] ( P `
 ( M  + 
1 ) ) ) 
|->  A )  e.  L^1 )
170153, 169itgcl 22168 . . . . . . 7  |-  ( ph  ->  S. ( ( P `
 M ) [,] ( P `  ( M  +  1 ) ) ) A  _d t  e.  CC )
171163itgeq1d 31709 . . . . . . . 8  |-  ( i  =  M  ->  S. ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) ) A  _d t  =  S. ( ( P `  M ) [,] ( P `  ( M  +  1
) ) ) A  _d t )
172171fsum1 13546 . . . . . . 7  |-  ( ( 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 )
1731, 170, 172syl2anc 661 . . . . . 6  |-  ( ph  -> 
sum_ i  e.  ( M ... M ) S. ( ( P `
 i ) [,] ( P `  (
i  +  1 ) ) ) A  _d t  =  S. ( ( P `  M
) [,] ( P `
 ( M  + 
1 ) ) ) A  _d t )
174173adantl 466 . . . . 5  |-  ( ( 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 )
17547, 174eqtr2d 2485 . . . 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 )
176175ex 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 ) )
177 simp3 999 . . . . 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 )
178 simp1 997 . . . . 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 )  -> 
k  e.  ( ( M  +  1 )..^ N ) )
179 simp2 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  ->  S. ( ( P `  M
) [,] ( P `
 k ) ) A  _d t  = 
sum_ i  e.  ( M..^ k ) S. ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) ) A  _d t ) )
180177, 179mpd 15 . . . . 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 )  ->  S. ( ( P `  M ) [,] ( P `  k )
) A  _d t  =  sum_ i  e.  ( M..^ k ) S. ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) ) A  _d t )
18150adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  M  e.  RR )
182 elfzoelz 11811 . . . . . . . . . . . 12  |-  ( k  e.  ( ( M  +  1 )..^ N
)  ->  k  e.  ZZ )
183182zred 10976 . . . . . . . . . . 11  |-  ( k  e.  ( ( M  +  1 )..^ N
)  ->  k  e.  RR )
184183adantl 466 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  k  e.  RR )
18552adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  ( M  +  1 )  e.  RR )
18653adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  M  <  ( M  +  1 ) )
187 elfzole1 11818 . . . . . . . . . . . 12  |-  ( k  e.  ( ( M  +  1 )..^ N
)  ->  ( M  +  1 )  <_ 
k )
188187adantl 466 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  ( M  +  1 )  <_ 
k )
189181, 185, 184, 186, 188ltletrd 9745 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  M  <  k )
190181, 184, 189ltled 9736 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  M  <_  k )
191 eluz 11105 . . . . . . . . . 10  |-  ( ( M  e.  ZZ  /\  k  e.  ZZ )  ->  ( k  e.  (
ZZ>= `  M )  <->  M  <_  k ) )
1921, 182, 191syl2an 477 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  ( k  e.  ( ZZ>= `  M )  <->  M  <_  k ) )
193190, 192mpbird 232 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  k  e.  ( ZZ>= `  M )
)
194 simplll 759 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  ->  ph )
195 eliccxr 31504 . . . . . . . . . . . 12  |-  ( t  e.  ( ( P `
 i ) [,] ( P `  (
i  +  1 ) ) )  ->  t  e.  RR* )
196195adantl 466 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  -> 
t  e.  RR* )
197194, 77syl 16 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  -> 
( P `  M
)  e.  RR )
198194, 48syl 16 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  ->  P : ( M ... N ) --> RR )
199 elfzelz 11699 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( M ... k )  ->  i  e.  ZZ )
200199adantl 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  i  e.  ZZ )
201 elfzle1 11700 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( M ... k )  ->  M  <_  i )
202201adantl 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  M  <_  i )
203200zred 10976 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  i  e.  RR )
20410ad2antrr 725 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  N  e.  RR )
205184adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  k  e.  RR )
206 elfzle2 11701 . . . . . . . . . . . . . . . . . 18  |-  ( i  e.  ( M ... k )  ->  i  <_  k )
207206adantl 466 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  i  <_  k )
208 elfzolt2 11819 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  ( ( M  +  1 )..^ N
)  ->  k  <  N )
209208ad2antlr 726 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  k  <  N )
210203, 205, 204, 207, 209lelttrd 9743 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  i  <  N )
211203, 204, 210ltled 9736 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  i  <_  N )
21298ad2antrr 725 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  ( M  e.  ZZ  /\  N  e.  ZZ ) )
213212, 100syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  (
i  e.  ( M ... N )  <->  ( i  e.  ZZ  /\  M  <_ 
i  /\  i  <_  N ) ) )
214200, 202, 211, 213mpbir3and 1180 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  i  e.  ( M ... N
) )
215214adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  -> 
i  e.  ( M ... N ) )
216198, 215ffvelrnd 6017 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  -> 
( P `  i
)  e.  RR )
217200peano2zd 10979 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  (
i  +  1 )  e.  ZZ )
21850ad2antrr 725 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  M  e.  RR )
219217zred 10976 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  (
i  +  1 )  e.  RR )
22050adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( M ... k ) )  ->  M  e.  RR )
221199zred 10976 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  e.  ( M ... k )  ->  i  e.  RR )
222221adantl 466 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( M ... k ) )  ->  i  e.  RR )
223 1red 9614 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( M ... k ) )  ->  1  e.  RR )
224222, 223readdcld 9626 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( M ... k ) )  ->  ( i  +  1 )  e.  RR )
225201adantl 466 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( M ... k ) )  ->  M  <_  i )
226222ltp1d 10483 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( M ... k ) )  ->  i  <  ( i  +  1 ) )
227220, 222, 224, 225, 226lelttrd 9743 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( M ... k ) )  ->  M  <  ( i  +  1 ) )
228227adantlr 714 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  M  <  ( i  +  1 ) )
229218, 219, 228ltled 9736 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  M  <_  ( i  +  1 ) )
2305, 199anim12ci 567 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( M ... k ) )  ->  ( i  e.  ZZ  /\  N  e.  ZZ ) )
231230adantlr 714 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  (
i  e.  ZZ  /\  N  e.  ZZ )
)
232231, 132syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  (
i  <  N  <->  ( i  +  1 )  <_  N ) )
233210, 232mpbid 210 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  (
i  +  1 )  <_  N )
234212, 135syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) ) )
235217, 229, 233, 234mpbir3and 1180 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  (
i  +  1 )  e.  ( M ... N ) )
236235adantr 465 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  -> 
( i  +  1 )  e.  ( M ... N ) )
237198, 236ffvelrnd 6017 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  -> 
( P `  (
i  +  1 ) )  e.  RR )
238 simpr 461 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  -> 
t  e.  ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) ) )
239 eliccre 31494 . . . . . . . . . . . . 13  |-  ( ( ( P `  i
)  e.  RR  /\  ( P `  ( i  +  1 ) )  e.  RR  /\  t  e.  ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) ) )  ->  t  e.  RR )
240216, 237, 238, 239syl3anc 1229 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  -> 
t  e.  RR )
241 elfzuz 11695 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( M ... k )  ->  i  e.  ( ZZ>= `  M )
)
242241adantl 466 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  i  e.  ( ZZ>= `  M )
)
24348ad3antrrr 729 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... i ) )  ->  P : ( M ... N ) --> RR )
244 elfzelz 11699 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( M ... i )  ->  j  e.  ZZ )
245244adantl 466 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... i ) )  -> 
j  e.  ZZ )
246 elfzle1 11700 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( M ... i )  ->  M  <_  j )
247246adantl 466 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... i ) )  ->  M  <_  j )
248245zred 10976 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... i ) )  -> 
j  e.  RR )
249204adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... i ) )  ->  N  e.  RR )
250203adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... i ) )  -> 
i  e.  RR )
251 elfzle2 11701 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  ( M ... i )  ->  j  <_  i )
252251adantl 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... i ) )  -> 
j  <_  i )
253210adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... i ) )  -> 
i  <  N )
254248, 250, 249, 252, 253lelttrd 9743 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... i ) )  -> 
j  <  N )
255248, 249, 254ltled 9736 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... i ) )  -> 
j  <_  N )
256212adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... i ) )  -> 
( M  e.  ZZ  /\  N  e.  ZZ ) )
257 elfz1 11688 . . . . . . . . . . . . . . . . 17  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( j  e.  ( M ... N )  <-> 
( j  e.  ZZ  /\  M  <_  j  /\  j  <_  N ) ) )
258256, 257syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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 ) ) )
259245, 247, 255, 258mpbir3and 1180 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... i ) )  -> 
j  e.  ( M ... N ) )
260243, 259ffvelrnd 6017 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... i ) )  -> 
( P `  j
)  e.  RR )
26148ad3antrrr 729 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  P : ( M ... N ) --> RR )
262 elfzelz 11699 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  ( M ... ( i  -  1 ) )  ->  j  e.  ZZ )
263262adantl 466 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
j  e.  ZZ )
264 elfzle1 11700 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  ( M ... ( i  -  1 ) )  ->  M  <_  j )
265264adantl 466 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  M  <_  j )
266263zred 10976 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
j  e.  RR )
267204adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  N  e.  RR )
268203adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
i  e.  RR )
269 1red 9614 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
1  e.  RR )
270268, 269resubcld 9994 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( i  -  1 )  e.  RR )
271 elfzle2 11701 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ( M ... ( i  -  1 ) )  ->  j  <_  ( i  -  1 ) )
272271adantl 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
j  <_  ( i  -  1 ) )
273268ltm1d 10485 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( i  -  1 )  <  i )
274266, 270, 268, 272, 273lelttrd 9743 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
j  <  i )
275210adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
i  <  N )
276266, 268, 267, 274, 275lttrd 9746 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
j  <  N )
277266, 267, 276ltled 9736 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
j  <_  N )
278212adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( M  e.  ZZ  /\  N  e.  ZZ ) )
279278, 257syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( 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 ) ) )
280263, 265, 277, 279mpbir3and 1180 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
j  e.  ( M ... N ) )
281261, 280ffvelrnd 6017 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( P `  j
)  e.  RR )
282263peano2zd 10979 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( j  +  1 )  e.  ZZ )
283181ad2antrr 725 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  M  e.  RR )
284266, 269readdcld 9626 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( j  +  1 )  e.  RR )
28550adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  M  e.  RR )
286262zred 10976 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ( M ... ( i  -  1 ) )  ->  j  e.  RR )
287286adantl 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  j  e.  RR )
288 1red 9614 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  1  e.  RR )
289287, 288readdcld 9626 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  ( j  +  1 )  e.  RR )
290264adantl 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  M  <_  j )
291287ltp1d 10483 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  j  <  ( j  +  1 ) )
292285, 287, 289, 290, 291lelttrd 9743 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  M  <  ( j  +  1 ) )
293292adant423 31379 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  M  <  ( j  +  1 ) )
294283, 284, 293ltled 9736 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  M  <_  ( j  +  1 ) )
295 zltp1le 10920 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( j  e.  ZZ  /\  i  e.  ZZ )  ->  ( j  <  i  <->  ( j  +  1 )  <_  i ) )
296262, 200, 295syl2anr 478 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( j  <  i  <->  ( j  +  1 )  <_  i ) )
297274, 296mpbid 210 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( j  +  1 )  <_  i )
298284, 268, 267, 297, 275lelttrd 9743 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( j  +  1 )  <  N )
299284, 267, 298ltled 9736 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( j  +  1 )  <_  N )
300 elfz1 11688 . . . . . . . . . . . . . . . . . 18  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( ( j  +  1 )  e.  ( M ... N )  <-> 
( ( j  +  1 )  e.  ZZ  /\  M  <_  ( j  +  1 )  /\  ( j  +  1 )  <_  N )
) )
301278, 300syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( 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 )
) )
302282, 294, 299, 301mpbir3and 1180 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( j  +  1 )  e.  ( M ... N ) )
303261, 302ffvelrnd 6017 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( P `  (
j  +  1 ) )  e.  RR )
304 simplll 759 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  ph )
305 elfzuz 11695 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  ( M ... ( i  -  1 ) )  ->  j  e.  ( ZZ>= `  M )
)
306305adantl 466 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
j  e.  ( ZZ>= `  M ) )
307304, 5syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  N  e.  ZZ )
308 elfzo2 11814 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( M..^ N
)  <->  ( j  e.  ( ZZ>= `  M )  /\  N  e.  ZZ  /\  j  <  N ) )
309306, 307, 276, 308syl3anbrc 1181 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
j  e.  ( M..^ N ) )
310 eleq1 2515 . . . . . . . . . . . . . . . . . . 19  |-  ( i  =  j  ->  (
i  e.  ( M..^ N )  <->  j  e.  ( M..^ N ) ) )
311310anbi2d 703 . . . . . . . . . . . . . . . . . 18  |-  ( i  =  j  ->  (
( ph  /\  i  e.  ( M..^ N ) )  <->  ( ph  /\  j  e.  ( M..^ N ) ) ) )
312 fveq2 5856 . . . . . . . . . . . . . . . . . . 19  |-  ( i  =  j  ->  ( P `  i )  =  ( P `  j ) )
313 oveq1 6288 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  =  j  ->  (
i  +  1 )  =  ( j  +  1 ) )
314313fveq2d 5860 . . . . . . . . . . . . . . . . . . 19  |-  ( i  =  j  ->  ( P `  ( i  +  1 ) )  =  ( P `  ( j  +  1 ) ) )
315312, 314breq12d 4450 . . . . . . . . . . . . . . . . . 18  |-  ( i  =  j  ->  (
( P `  i
)  <  ( P `  ( i  +  1 ) )  <->  ( P `  j )  <  ( P `  ( j  +  1 ) ) ) )
316311, 315imbi12d 320 . . . . . . . . . . . . . . . . 17  |-  ( i  =  j  ->  (
( ( ph  /\  i  e.  ( M..^ N ) )  -> 
( P `  i
)  <  ( P `  ( i  +  1 ) ) )  <->  ( ( ph  /\  j  e.  ( M..^ N ) )  ->  ( P `  j )  <  ( P `  ( j  +  1 ) ) ) ) )
317316, 145chvarv 2000 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( P `  j )  <  ( P `  ( j  +  1 ) ) )
318304, 309, 317syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( P `  j
)  <  ( P `  ( j  +  1 ) ) )
319281, 303, 318ltled 9736 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( P `  j
)  <_  ( P `  ( j  +  1 ) ) )
320242, 260, 319monoord 12119 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  ( P `  M )  <_  ( P `  i
) )
321320adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  -> 
( P `  M
)  <_  ( P `  i ) )
322216rexrd 9646 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  -> 
( P `  i
)  e.  RR* )
323237rexrd 9646 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  -> 
( P `  (
i  +  1 ) )  e.  RR* )
324 iccgelb 11592 . . . . . . . . . . . . 13  |-  ( ( ( P `  i
)  e.  RR*  /\  ( P `  ( i  +  1 ) )  e.  RR*  /\  t  e.  ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) ) )  ->  ( P `  i )  <_  t )
325322, 323, 238, 324syl3anc 1229 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  -> 
( P `  i
)  <_  t )
326197, 216, 240, 321, 325letrd 9742 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  -> 
( P `  M
)  <_  t )
327194, 66syl 16 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  -> 
( P `  N
)  e.  RR )
328 iccleub 11591 . . . . . . . . . . . . 13  |-  ( ( ( P `  i
)  e.  RR*  /\  ( P `  ( i  +  1 ) )  e.  RR*  /\  t  e.  ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) ) )  ->  t  <_  ( P `  (
i  +  1 ) ) )
329322, 323, 238, 328syl3anc 1229 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  -> 
t  <_  ( P `  ( i  +  1 ) ) )
3305ad2antrr 725 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  N  e.  ZZ )
331 eluz 11105 . . . . . . . . . . . . . . . 16  |-  ( ( ( i  +  1 )  e.  ZZ  /\  N  e.  ZZ )  ->  ( N  e.  (
ZZ>= `  ( i  +  1 ) )  <->  ( i  +  1 )  <_  N ) )
332217, 330, 331syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  ( N  e.  ( ZZ>= `  ( i  +  1 ) )  <->  ( i  +  1 )  <_  N ) )
333233, 332mpbird 232 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  N  e.  ( ZZ>= `  ( i  +  1 ) ) )
334333adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  ->  N  e.  ( ZZ>= `  ( i  +  1 ) ) )
33548ad3antrrr 729 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( (
i  +  1 ) ... N ) )  ->  P : ( M ... N ) --> RR )
336 elfzelz 11699 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( ( i  +  1 ) ... N )  ->  j  e.  ZZ )
337336adantl 466 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( (
i  +  1 ) ... N ) )  ->  j  e.  ZZ )
338 elfzel1 11698 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  e.  ( M ... k )  ->  M  e.  ZZ )
339338zred 10976 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  ( M ... k )  ->  M  e.  RR )
340339adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( i  e.  ( M ... k )  /\  j  e.  ( (
i  +  1 ) ... N ) )  ->  M  e.  RR )
341336zred 10976 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  ( ( i  +  1 ) ... N )  ->  j  e.  RR )
342341adantl 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( i  e.  ( M ... k )  /\  j  e.  ( (
i  +  1 ) ... N ) )  ->  j  e.  RR )
343221adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( i  e.  ( M ... k )  /\  j  e.  ( (
i  +  1 ) ... N ) )  ->  i  e.  RR )
344 1red 9614 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( i  e.  ( M ... k )  /\  j  e.  ( (
i  +  1 ) ... N ) )  ->  1  e.  RR )
345343, 344readdcld 9626 . . . . . . . . . . . . . . . . . . 19  |-  ( ( i  e.  ( M ... k )  /\  j  e.  ( (
i  +  1 ) ... N ) )  ->  ( i  +  1 )  e.  RR )
346201adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( i  e.  ( M ... k )  /\  j  e.  ( (
i  +  1 ) ... N ) )  ->  M  <_  i
)
347343ltp1d 10483 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( i  e.  ( M ... k )  /\  j  e.  ( (
i  +  1 ) ... N ) )  ->  i  <  (
i  +  1 ) )
348340, 343, 345, 346, 347lelttrd 9743 . . . . . . . . . . . . . . . . . . 19  |-  ( ( i  e.  ( M ... k )  /\  j  e.  ( (
i  +  1 ) ... N ) )  ->  M  <  (
i  +  1 ) )
349 elfzle1 11700 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  ( ( i  +  1 ) ... N )  ->  (
i  +  1 )  <_  j )
350349adantl 466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( i  e.  ( M ... k )  /\  j  e.  ( (
i  +  1 ) ... N ) )  ->  ( i  +  1 )  <_  j
)
351340, 345, 342, 348, 350ltletrd 9745 . . . . . . . . . . . . . . . . . 18  |-  ( ( i  e.  ( M ... k )  /\  j  e.  ( (
i  +  1 ) ... N ) )  ->  M  <  j
)
352340, 342, 351ltled 9736 . . . . . . . . . . . . . . . . 17  |-  ( ( i  e.  ( M ... k )  /\  j  e.  ( (
i  +  1 ) ... N ) )  ->  M  <_  j
)
353352adantll 713 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( (
i  +  1 ) ... N ) )  ->  M  <_  j
)
354 elfzle2 11701 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( ( i  +  1 ) ... N )  ->  j  <_  N )
355354adantl 466 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( (
i  +  1 ) ... N ) )  ->  j  <_  N
)
356212adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( (
i  +  1 ) ... N ) )  ->  ( M  e.  ZZ  /\  N  e.  ZZ ) )
357356, 257syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( (
i  +  1 ) ... N ) )  ->  ( j  e.  ( M ... N
)  <->  ( j  e.  ZZ  /\  M  <_ 
j  /\  j  <_  N ) ) )
358337, 353, 355, 357mpbir3and 1180 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( (
i  +  1 ) ... N ) )  ->  j  e.  ( M ... N ) )
359335, 358ffvelrnd 6017 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( (
i  +  1 ) ... N ) )  ->  ( P `  j )  e.  RR )
360359adantlr 714 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  /\  j  e.  ( (
i  +  1 ) ... N ) )  ->  ( P `  j )  e.  RR )
361 simplll 759 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( (
i  +  1 ) ... ( N  - 
1 ) ) )  ->  ph )
362 simplr 755 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( (
i  +  1 ) ... ( N  - 
1 ) ) )  ->  i  e.  ( M ... k ) )
363 simpr 461 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( (
i  +  1 ) ... ( N  - 
1 ) ) )  ->  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )
364483ad2ant1 1018 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  P :
( M ... N
) --> RR )
365 elfzelz 11699 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  ( ( i  +  1 ) ... ( N  -  1 ) )  ->  j  e.  ZZ )
3663653ad2ant3 1020 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  j  e.  ZZ )
367503ad2ant1 1018 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  M  e.  RR )
368366zred 10976 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  j  e.  RR )
3692243adant3 1017 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  ( i  +  1 )  e.  RR )
3702273adant3 1017 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  M  <  ( i  +  1 ) )
371 elfzle1 11700 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ( ( i  +  1 ) ... ( N  -  1 ) )  ->  (
i  +  1 )  <_  j )
3723713ad2ant3 1020 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  ( i  +  1 )  <_ 
j )
373367, 369, 368, 370, 372ltletrd 9745 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  M  <  j )
374367, 368, 373ltled 9736 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  M  <_  j )
375365adantl 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  j  e.  ZZ )
376375zred 10976 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  j  e.  RR )
37710adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  N  e.  RR )
378 1red 9614 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  1  e.  RR )
379377, 378resubcld 9994 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  ( N  -  1 )  e.  RR )
380 elfzle2 11701 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  e.  ( ( i  +  1 ) ... ( N  -  1 ) )  ->  j  <_  ( N  -  1 ) )
381380adantl 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  j  <_  ( N  -  1 ) )
382377ltm1d 10485 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  ( N  -  1 )  <  N )
383376, 379, 377, 381, 382lelttrd 9743 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  j  <  N )
384376, 377, 383ltled 9736 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  j  <_  N )
3853843adant2 1016 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  j  <_  N )
386983ad2ant1 1018 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  ( M  e.  ZZ  /\  N  e.  ZZ ) )
387386, 257syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  ( j  e.  ( M ... N
)  <->  ( j  e.  ZZ  /\  M  <_ 
j  /\  j  <_  N ) ) )
388366, 374, 385, 387mpbir3and 1180 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  j  e.  ( M ... N ) )
389364, 388ffvelrnd 6017 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  ( P `  j )  e.  RR )
390366peano2zd 10979 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  ( j  +  1 )  e.  ZZ )
391390zred 10976 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  ( j  +  1 )  e.  RR )
3922213ad2ant2 1019 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  i  e.  RR )
393 1red 9614 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  1  e.  RR )
3942263adant3 1017 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  i  <  ( i  +  1 ) )
395392, 369, 368, 394, 372ltletrd 9745 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  i  <  j )
396392, 368, 395ltled 9736 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  i  <_  j )
397392, 368, 393, 396leadd1dd 10173 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  ( i  +  1 )  <_ 
( j  +  1 ) )
398367, 369, 391, 370, 397ltletrd 9745 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  M  <  ( j  +  1 ) )
399367, 391, 398ltled 9736 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  M  <_  ( j  +  1 ) )
400 zltp1le 10920 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( j  e.  ZZ  /\  N  e.  ZZ )  ->  ( j  <  N  <->  ( j  +  1 )  <_  N ) )
401365, 5, 400syl2anr 478 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  (
j  <  N  <->  ( j  +  1 )  <_  N ) )
402383, 401mpbid 210 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  (
j  +  1 )  <_  N )
4034023adant2 1016 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  ( j  +  1 )  <_  N )
404386, 300syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  ( (
j  +  1 )  e.  ( M ... N )  <->  ( (
j  +  1 )  e.  ZZ  /\  M  <_  ( j  +  1 )  /\  ( j  +  1 )  <_  N ) ) )
405390, 399, 403, 404mpbir3and 1180 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  ( j  +  1 )  e.  ( M ... N
) )
406364, 405ffvelrnd 6017 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  ( P `  ( j  +  1 ) )  e.  RR )
407 simp1 997 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  ph )
40813ad2ant1 1018 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  M  e.  ZZ )
409 eluz 11105 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( M  e.  ZZ  /\  j  e.  ZZ )  ->  ( j  e.  (
ZZ>= `  M )  <->  M  <_  j ) )
410408, 366, 409syl2anc 661 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  ( j  e.  ( ZZ>= `  M )  <->  M  <_  j ) )
411374, 410mpbird 232 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  j  e.  ( ZZ>= `  M )
)
41253ad2ant1 1018 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  N  e.  ZZ )
4133833adant2 1016 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  j  <  N )
414411, 412, 413, 308syl3anbrc 1181 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  j  e.  ( M..^ N ) )
415407, 414, 317syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  ( P `  j )  <  ( P `  ( j  +  1 ) ) )
416389, 406, 415ltled 9736 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  ( P `  j )  <_  ( P `  ( j  +  1 ) ) )
417361, 362, 363, 416syl3anc 1229 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( (
i  +  1 ) ... ( N  - 
1 ) ) )  ->  ( P `  j )  <_  ( P `  ( j  +  1 ) ) )
418417adantlr 714 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  /\  j  e.  ( (
i  +  1 ) ... ( N  - 
1 ) ) )  ->  ( P `  j )  <_  ( P `  ( j  +  1 ) ) )
419334, 360, 418monoord 12119 . . . . . . . . . . . 12  |-  (