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

Theorem itgspltprt 37673
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 11043 . . . . 5  |-  ( ph  ->  ( M  +  1 )  e.  ZZ )
3 itgspltprt.2 . . . . . 6  |-  ( ph  ->  N  e.  ( ZZ>= `  ( M  +  1
) ) )
4 eluzelz 11168 . . . . . 6  |-  ( N  e.  ( ZZ>= `  ( M  +  1 ) )  ->  N  e.  ZZ )
53, 4syl 17 . . . . 5  |-  ( ph  ->  N  e.  ZZ )
62, 5, 53jca 1185 . . . 4  |-  ( ph  ->  ( ( M  + 
1 )  e.  ZZ  /\  N  e.  ZZ  /\  N  e.  ZZ )
)
7 eluzle 11171 . . . . 5  |-  ( N  e.  ( ZZ>= `  ( M  +  1 ) )  ->  ( M  +  1 )  <_  N )
83, 7syl 17 . . . 4  |-  ( ph  ->  ( M  +  1 )  <_  N )
9 eluzelre 11169 . . . . . 6  |-  ( N  e.  ( ZZ>= `  ( M  +  1 ) )  ->  N  e.  RR )
103, 9syl 17 . . . . 5  |-  ( ph  ->  N  e.  RR )
1110leidd 10180 . . . 4  |-  ( ph  ->  N  <_  N )
126, 8, 11jca32 537 . . 3  |-  ( ph  ->  ( ( ( M  +  1 )  e.  ZZ  /\  N  e.  ZZ  /\  N  e.  ZZ )  /\  (
( M  +  1 )  <_  N  /\  N  <_  N ) ) )
13 elfz2 11791 . . 3  |-  ( N  e.  ( ( M  +  1 ) ... N )  <->  ( (
( M  +  1 )  e.  ZZ  /\  N  e.  ZZ  /\  N  e.  ZZ )  /\  (
( M  +  1 )  <_  N  /\  N  <_  N ) ) )
1412, 13sylibr 215 . 2  |-  ( ph  ->  N  e.  ( ( M  +  1 ) ... N ) )
15 fveq2 5877 . . . . . . 7  |-  ( j  =  ( M  + 
1 )  ->  ( P `  j )  =  ( P `  ( M  +  1
) ) )
1615oveq2d 6317 . . . . . 6  |-  ( j  =  ( M  + 
1 )  ->  (
( P `  M
) [,] ( P `
 j ) )  =  ( ( P `
 M ) [,] ( P `  ( M  +  1 ) ) ) )
1716itgeq1d 37650 . . . . 5  |-  ( j  =  ( M  + 
1 )  ->  S. ( ( P `  M ) [,] ( P `  j )
) A  _d t  =  S. ( ( P `  M ) [,] ( P `  ( M  +  1
) ) ) A  _d t )
18 oveq2 6309 . . . . . 6  |-  ( j  =  ( M  + 
1 )  ->  ( M..^ j )  =  ( M..^ ( M  + 
1 ) ) )
1918sumeq1d 13752 . . . . 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 2444 . . . 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 317 . . 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 5877 . . . . . . 7  |-  ( j  =  k  ->  ( P `  j )  =  ( P `  k ) )
2322oveq2d 6317 . . . . . 6  |-  ( j  =  k  ->  (
( P `  M
) [,] ( P `
 j ) )  =  ( ( P `
 M ) [,] ( P `  k
) ) )
2423itgeq1d 37650 . . . . 5  |-  ( j  =  k  ->  S. ( ( P `  M ) [,] ( P `  j )
) A  _d t  =  S. ( ( P `  M ) [,] ( P `  k ) ) A  _d t )
25 oveq2 6309 . . . . . 6  |-  ( j  =  k  ->  ( M..^ j )  =  ( M..^ k ) )
2625sumeq1d 13752 . . . . 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 2444 . . . 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 317 . . 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 5877 . . . . . . 7  |-  ( j  =  ( k  +  1 )  ->  ( P `  j )  =  ( P `  ( k  +  1 ) ) )
3029oveq2d 6317 . . . . . 6  |-  ( j  =  ( k  +  1 )  ->  (
( P `  M
) [,] ( P `
 j ) )  =  ( ( P `
 M ) [,] ( P `  (
k  +  1 ) ) ) )
3130itgeq1d 37650 . . . . 5  |-  ( j  =  ( k  +  1 )  ->  S. ( ( P `  M ) [,] ( P `  j )
) A  _d t  =  S. ( ( P `  M ) [,] ( P `  ( k  +  1 ) ) ) A  _d t )
32 oveq2 6309 . . . . . 6  |-  ( j  =  ( k  +  1 )  ->  ( M..^ j )  =  ( M..^ ( k  +  1 ) ) )
3332sumeq1d 13752 . . . . 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 2444 . . . 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 317 . . 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 5877 . . . . . . 7  |-  ( j  =  N  ->  ( P `  j )  =  ( P `  N ) )
3736oveq2d 6317 . . . . . 6  |-  ( j  =  N  ->  (
( P `  M
) [,] ( P `
 j ) )  =  ( ( P `
 M ) [,] ( P `  N
) ) )
3837itgeq1d 37650 . . . . 5  |-  ( j  =  N  ->  S. ( ( P `  M ) [,] ( P `  j )
) A  _d t  =  S. ( ( P `  M ) [,] ( P `  N ) ) A  _d t )
39 oveq2 6309 . . . . . 6  |-  ( j  =  N  ->  ( M..^ j )  =  ( M..^ N ) )
4039sumeq1d 13752 . . . . 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 2444 . . . 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 317 . . 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 467 . . . . . . . 8  |-  ( ( N  e.  ( ZZ>= `  ( M  +  1
) )  /\  ph )  ->  M  e.  ZZ )
44 fzval3 11982 . . . . . . . 8  |-  ( M  e.  ZZ  ->  ( M ... M )  =  ( M..^ ( M  +  1 ) ) )
4543, 44syl 17 . . . . . . 7  |-  ( ( N  e.  ( ZZ>= `  ( M  +  1
) )  /\  ph )  ->  ( M ... M )  =  ( M..^ ( M  + 
1 ) ) )
4645eqcomd 2430 . . . . . 6  |-  ( ( N  e.  ( ZZ>= `  ( M  +  1
) )  /\  ph )  ->  ( M..^ ( M  +  1 ) )  =  ( M ... M ) )
4746sumeq1d 13752 . . . . 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 466 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  P : ( M ... N ) --> RR )
501zred 11040 . . . . . . . . . . . . . . 15  |-  ( ph  ->  M  e.  RR )
51 1red 9658 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  1  e.  RR )
5250, 51readdcld 9670 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( M  +  1 )  e.  RR )
5350ltp1d 10537 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  M  <  ( M  +  1 ) )
5450, 52, 10, 53, 8ltletrd 9795 . . . . . . . . . . . . . . 15  |-  ( ph  ->  M  <  N )
5550, 10, 54ltled 9783 . . . . . . . . . . . . . 14  |-  ( ph  ->  M  <_  N )
56 eluz 11172 . . . . . . . . . . . . . . 15  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( N  e.  (
ZZ>= `  M )  <->  M  <_  N ) )
571, 5, 56syl2anc 665 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( N  e.  (
ZZ>= `  M )  <->  M  <_  N ) )
5855, 57mpbird 235 . . . . . . . . . . . . 13  |-  ( ph  ->  N  e.  ( ZZ>= `  M ) )
59 eluzfz1 11806 . . . . . . . . . . . . 13  |-  ( N  e.  ( ZZ>= `  M
)  ->  M  e.  ( M ... N ) )
6058, 59syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  M  e.  ( M ... N ) )
6160adantr 466 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  M  e.  ( M ... N
) )
6249, 61ffvelrnd 6034 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  ( P `  M )  e.  RR )
63 elfz1 11789 . . . . . . . . . . . . . 14  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( N  e.  ( M ... N )  <-> 
( N  e.  ZZ  /\  M  <_  N  /\  N  <_  N ) ) )
641, 5, 63syl2anc 665 . . . . . . . . . . . . 13  |-  ( ph  ->  ( N  e.  ( M ... N )  <-> 
( N  e.  ZZ  /\  M  <_  N  /\  N  <_  N ) ) )
655, 55, 11, 64mpbir3and 1188 . . . . . . . . . . . 12  |-  ( ph  ->  N  e.  ( M ... N ) )
6648, 65ffvelrnd 6034 . . . . . . . . . . 11  |-  ( ph  ->  ( P `  N
)  e.  RR )
6766adantr 466 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  ( P `  N )  e.  RR )
6850lep1d 10538 . . . . . . . . . . . . . 14  |-  ( ph  ->  M  <_  ( M  +  1 ) )
69 elfz1 11789 . . . . . . . . . . . . . . 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 665 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( M  + 
1 )  e.  ( M ... N )  <-> 
( ( M  + 
1 )  e.  ZZ  /\  M  <_  ( M  +  1 )  /\  ( M  +  1
)  <_  N )
) )
712, 68, 8, 70mpbir3and 1188 . . . . . . . . . . . . 13  |-  ( ph  ->  ( M  +  1 )  e.  ( M ... N ) )
7248, 71ffvelrnd 6034 . . . . . . . . . . . 12  |-  ( ph  ->  ( P `  ( M  +  1 ) )  e.  RR )
7372adantr 466 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  ( P `  ( M  +  1 ) )  e.  RR )
74 simpr 462 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )
75 eliccre 37431 . . . . . . . . . . 11  |-  ( ( ( P `  M
)  e.  RR  /\  ( P `  ( M  +  1 ) )  e.  RR  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  t  e.  RR )
7662, 73, 74, 75syl3anc 1264 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  t  e.  RR )
7748, 60ffvelrnd 6034 . . . . . . . . . . . . 13  |-  ( ph  ->  ( P `  M
)  e.  RR )
7877rexrd 9690 . . . . . . . . . . . 12  |-  ( ph  ->  ( P `  M
)  e.  RR* )
7978adantr 466 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  ( P `  M )  e.  RR* )
8073rexrd 9690 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  ( P `  ( M  +  1 ) )  e.  RR* )
81 iccgelb 11691 . . . . . . . . . . 11  |-  ( ( ( P `  M
)  e.  RR*  /\  ( P `  ( M  +  1 ) )  e.  RR*  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  ( P `  M )  <_  t )
8279, 80, 74, 81syl3anc 1264 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  ( P `  M )  <_  t )
83 iccleub 11690 . . . . . . . . . . . 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 1264 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  t  <_  ( P `  ( M  +  1 ) ) )
8548adantr 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... N
) )  ->  P : ( M ... N ) --> RR )
86 elfzelz 11800 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( ( M  +  1 ) ... N )  ->  i  e.  ZZ )
8786adantl 467 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... N
) )  ->  i  e.  ZZ )
8850adantr 466 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... N
) )  ->  M  e.  RR )
8987zred 11040 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... N
) )  ->  i  e.  RR )
9052adantr 466 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... N
) )  ->  ( M  +  1 )  e.  RR )
9153adantr 466 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... N
) )  ->  M  <  ( M  +  1 ) )
92 elfzle1 11802 . . . . . . . . . . . . . . . . . 18  |-  ( i  e.  ( ( M  +  1 ) ... N )  ->  ( M  +  1 )  <_  i )
9392adantl 467 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... N
) )  ->  ( M  +  1 )  <_  i )
9488, 90, 89, 91, 93ltletrd 9795 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... N
) )  ->  M  <  i )
9588, 89, 94ltled 9783 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... N
) )  ->  M  <_  i )
96 elfzle2 11803 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( ( M  +  1 ) ... N )  ->  i  <_  N )
9796adantl 467 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... N
) )  ->  i  <_  N )
981, 5jca 534 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( M  e.  ZZ  /\  N  e.  ZZ ) )
9998adantr 466 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... N
) )  ->  ( M  e.  ZZ  /\  N  e.  ZZ ) )
100 elfz1 11789 . . . . . . . . . . . . . . . 16  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( i  e.  ( M ... N )  <-> 
( i  e.  ZZ  /\  M  <_  i  /\  i  <_  N ) ) )
10199, 100syl 17 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... N
) )  ->  (
i  e.  ( M ... N )  <->  ( i  e.  ZZ  /\  M  <_ 
i  /\  i  <_  N ) ) )
10287, 95, 97, 101mpbir3and 1188 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... N
) )  ->  i  e.  ( M ... N
) )
10385, 102ffvelrnd 6034 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... N
) )  ->  ( P `  i )  e.  RR )
10448adantr 466 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  P : ( M ... N ) --> RR )
105 elfzelz 11800 . . . . . . . . . . . . . . . . 17  |-  ( i  e.  ( ( M  +  1 ) ... ( N  -  1 ) )  ->  i  e.  ZZ )
106105adantl 467 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  i  e.  ZZ )
10750adantr 466 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  M  e.  RR )
108106zred 11040 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  i  e.  RR )
10952adantr 466 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  ( M  +  1 )  e.  RR )
11053adantr 466 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  M  <  ( M  +  1 ) )
111 elfzle1 11802 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  ( ( M  +  1 ) ... ( N  -  1 ) )  ->  ( M  +  1 )  <_  i )
112111adantl 467 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  ( M  +  1 )  <_  i )
113107, 109, 108, 110, 112ltletrd 9795 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  M  <  i )
114107, 108, 113ltled 9783 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  M  <_  i )
11510adantr 466 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  N  e.  RR )
116 1red 9658 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  1  e.  RR )
117115, 116resubcld 10047 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  ( N  -  1 )  e.  RR )
118 elfzle2 11803 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  ( ( M  +  1 ) ... ( N  -  1 ) )  ->  i  <_  ( N  -  1 ) )
119118adantl 467 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  i  <_  ( N  -  1 ) )
120115ltm1d 10539 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  ( N  -  1 )  <  N )
121108, 117, 115, 119, 120lelttrd 9793 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  i  <  N )
122108, 115, 121ltled 9783 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  i  <_  N )
12398adantr 466 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  ( M  e.  ZZ  /\  N  e.  ZZ ) )
124123, 100syl 17 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  (
i  e.  ( M ... N )  <->  ( i  e.  ZZ  /\  M  <_ 
i  /\  i  <_  N ) ) )
125106, 114, 122, 124mpbir3and 1188 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  i  e.  ( M ... N
) )
126104, 125ffvelrnd 6034 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  ( P `  i )  e.  RR )
127106peano2zd 11043 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  (
i  +  1 )  e.  ZZ )
128108, 116readdcld 9670 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  (
i  +  1 )  e.  RR )
129107, 108, 116, 113ltadd1dd 10224 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  ( M  +  1 )  <  ( i  +  1 ) )
130107, 109, 128, 110, 129lttrd 9796 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  M  <  ( i  +  1 ) )
131107, 128, 130ltled 9783 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  M  <_  ( i  +  1 ) )
132 zltp1le 10986 . . . . . . . . . . . . . . . . . 18  |-  ( ( i  e.  ZZ  /\  N  e.  ZZ )  ->  ( i  <  N  <->  ( i  +  1 )  <_  N ) )
133105, 5, 132syl2anr 480 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  (
i  <  N  <->  ( i  +  1 )  <_  N ) )
134121, 133mpbid 213 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  (
i  +  1 )  <_  N )
135 elfz1 11789 . . . . . . . . . . . . . . . . 17  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( ( i  +  1 )  e.  ( M ... N )  <-> 
( ( i  +  1 )  e.  ZZ  /\  M  <_  ( i  +  1 )  /\  ( i  +  1 )  <_  N )
) )
136123, 135syl 17 . . . . . . . . . . . . . . . 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 1188 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  (
i  +  1 )  e.  ( M ... N ) )
138104, 137ffvelrnd 6034 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  ( P `  ( i  +  1 ) )  e.  RR )
139 eluz 11172 . . . . . . . . . . . . . . . . . 18  |-  ( ( M  e.  ZZ  /\  i  e.  ZZ )  ->  ( i  e.  (
ZZ>= `  M )  <->  M  <_  i ) )
1401, 105, 139syl2an 479 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  (
i  e.  ( ZZ>= `  M )  <->  M  <_  i ) )
141114, 140mpbird 235 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  i  e.  ( ZZ>= `  M )
)
1425adantr 466 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  N  e.  ZZ )
143 elfzo2 11923 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( M..^ N
)  <->  ( i  e.  ( ZZ>= `  M )  /\  N  e.  ZZ  /\  i  <  N ) )
144141, 142, 121, 143syl3anbrc 1189 . . . . . . . . . . . . . . 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 472 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  ( P `  i )  <  ( P `  (
i  +  1 ) ) )
147126, 138, 146ltled 9783 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( ( M  + 
1 ) ... ( N  -  1 ) ) )  ->  ( P `  i )  <_  ( P `  (
i  +  1 ) ) )
1483, 103, 147monoord 12242 . . . . . . . . . . . 12  |-  ( ph  ->  ( P `  ( M  +  1 ) )  <_  ( P `  N ) )
149148adantr 466 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  ( P `  ( M  +  1 ) )  <_  ( P `  N ) )
15076, 73, 67, 84, 149letrd 9792 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  t  <_  ( P `  N
) )
15162, 67, 76, 82, 150eliccd 37429 . . . . . . . . 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 472 . . . . . . . 8  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) ) )  ->  A  e.  CC )
154 id 23 . . . . . . . . . 10  |-  ( ph  ->  ph )
155 fzolb 11926 . . . . . . . . . . 11  |-  ( M  e.  ( M..^ N
)  <->  ( M  e.  ZZ  /\  N  e.  ZZ  /\  M  < 
N ) )
1561, 5, 54, 155syl3anbrc 1189 . . . . . . . . . 10  |-  ( ph  ->  M  e.  ( M..^ N ) )
157154, 156jca 534 . . . . . . . . 9  |-  ( ph  ->  ( ph  /\  M  e.  ( M..^ N ) ) )
158 eleq1 2494 . . . . . . . . . . . 12  |-  ( i  =  M  ->  (
i  e.  ( M..^ N )  <->  M  e.  ( M..^ N ) ) )
159158anbi2d 708 . . . . . . . . . . 11  |-  ( i  =  M  ->  (
( ph  /\  i  e.  ( M..^ N ) )  <->  ( ph  /\  M  e.  ( M..^ N ) ) ) )
160 fveq2 5877 . . . . . . . . . . . . . 14  |-  ( i  =  M  ->  ( P `  i )  =  ( P `  M ) )
161 oveq1 6308 . . . . . . . . . . . . . . 15  |-  ( i  =  M  ->  (
i  +  1 )  =  ( M  + 
1 ) )
162161fveq2d 5881 . . . . . . . . . . . . . 14  |-  ( i  =  M  ->  ( P `  ( i  +  1 ) )  =  ( P `  ( M  +  1
) ) )
163160, 162oveq12d 6319 . . . . . . . . . . . . 13  |-  ( i  =  M  ->  (
( P `  i
) [,] ( P `
 ( i  +  1 ) ) )  =  ( ( P `
 M ) [,] ( P `  ( M  +  1 ) ) ) )
164163mpteq1d 4502 . . . . . . . . . . . 12  |-  ( i  =  M  ->  (
t  e.  ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) )  |->  A )  =  ( t  e.  ( ( P `
 M ) [,] ( P `  ( M  +  1 ) ) )  |->  A ) )
165164eleq1d 2491 . . . . . . . . . . 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 321 . . . . . . . . . 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 3139 . . . . . . . . 9  |-  ( M  e.  ZZ  ->  (
( ph  /\  M  e.  ( M..^ N ) )  ->  ( t  e.  ( ( P `  M ) [,] ( P `  ( M  +  1 ) ) )  |->  A )  e.  L^1 ) )
1691, 157, 168sylc 62 . . . . . . . 8  |-  ( ph  ->  ( t  e.  ( ( P `  M
) [,] ( P `
 ( M  + 
1 ) ) ) 
|->  A )  e.  L^1 )
170153, 169itgcl 22725 . . . . . . 7  |-  ( ph  ->  S. ( ( P `
 M ) [,] ( P `  ( M  +  1 ) ) ) A  _d t  e.  CC )
171163itgeq1d 37650 . . . . . . . 8  |-  ( i  =  M  ->  S. ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) ) A  _d t  =  S. ( ( P `  M ) [,] ( P `  ( M  +  1
) ) ) A  _d t )
172171fsum1 13793 . . . . . . 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 665 . . . . . 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 467 . . . . 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 2464 . . . 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 435 . . 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 1007 . . . . 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 1005 . . . . 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 1006 . . . . . 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 466 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  M  e.  RR )
182 elfzoelz 11920 . . . . . . . . . . . 12  |-  ( k  e.  ( ( M  +  1 )..^ N
)  ->  k  e.  ZZ )
183182zred 11040 . . . . . . . . . . 11  |-  ( k  e.  ( ( M  +  1 )..^ N
)  ->  k  e.  RR )
184183adantl 467 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  k  e.  RR )
18552adantr 466 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  ( M  +  1 )  e.  RR )
18653adantr 466 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  M  <  ( M  +  1 ) )
187 elfzole1 11928 . . . . . . . . . . . 12  |-  ( k  e.  ( ( M  +  1 )..^ N
)  ->  ( M  +  1 )  <_ 
k )
188187adantl 467 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  ( M  +  1 )  <_ 
k )
189181, 185, 184, 186, 188ltletrd 9795 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  M  <  k )
190181, 184, 189ltled 9783 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  M  <_  k )
191 eluz 11172 . . . . . . . . . 10  |-  ( ( M  e.  ZZ  /\  k  e.  ZZ )  ->  ( k  e.  (
ZZ>= `  M )  <->  M  <_  k ) )
1921, 182, 191syl2an 479 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  ( k  e.  ( ZZ>= `  M )  <->  M  <_  k ) )
193190, 192mpbird 235 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  k  e.  ( ZZ>= `  M )
)
194 simplll 766 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  ->  ph )
195 eliccxr 37440 . . . . . . . . . . . 12  |-  ( t  e.  ( ( P `
 i ) [,] ( P `  (
i  +  1 ) ) )  ->  t  e.  RR* )
196195adantl 467 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  -> 
t  e.  RR* )
197194, 77syl 17 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  -> 
( P `  M
)  e.  RR )
198194, 48syl 17 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  ->  P : ( M ... N ) --> RR )
199 elfzelz 11800 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( M ... k )  ->  i  e.  ZZ )
200199adantl 467 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  i  e.  ZZ )
201 elfzle1 11802 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( M ... k )  ->  M  <_  i )
202201adantl 467 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  M  <_  i )
203200zred 11040 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  i  e.  RR )
20410ad2antrr 730 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  N  e.  RR )
205184adantr 466 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  k  e.  RR )
206 elfzle2 11803 . . . . . . . . . . . . . . . . . 18  |-  ( i  e.  ( M ... k )  ->  i  <_  k )
207206adantl 467 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  i  <_  k )
208 elfzolt2 11929 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  ( ( M  +  1 )..^ N
)  ->  k  <  N )
209208ad2antlr 731 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  k  <  N )
210203, 205, 204, 207, 209lelttrd 9793 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  i  <  N )
211203, 204, 210ltled 9783 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  i  <_  N )
21298ad2antrr 730 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  ( M  e.  ZZ  /\  N  e.  ZZ ) )
213212, 100syl 17 . . . . . . . . . . . . . . 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 1188 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  i  e.  ( M ... N
) )
215214adantr 466 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  -> 
i  e.  ( M ... N ) )
216198, 215ffvelrnd 6034 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  -> 
( P `  i
)  e.  RR )
217200peano2zd 11043 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  (
i  +  1 )  e.  ZZ )
21850ad2antrr 730 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  M  e.  RR )
219217zred 11040 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  (
i  +  1 )  e.  RR )
22050adantr 466 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( M ... k ) )  ->  M  e.  RR )
221199zred 11040 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  e.  ( M ... k )  ->  i  e.  RR )
222221adantl 467 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( M ... k ) )  ->  i  e.  RR )
223 1red 9658 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( M ... k ) )  ->  1  e.  RR )
224222, 223readdcld 9670 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( M ... k ) )  ->  ( i  +  1 )  e.  RR )
225201adantl 467 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( M ... k ) )  ->  M  <_  i )
226222ltp1d 10537 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( M ... k ) )  ->  i  <  ( i  +  1 ) )
227220, 222, 224, 225, 226lelttrd 9793 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( M ... k ) )  ->  M  <  ( i  +  1 ) )
228227adantlr 719 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  M  <  ( i  +  1 ) )
229218, 219, 228ltled 9783 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  M  <_  ( i  +  1 ) )
2305, 199anim12ci 569 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( M ... k ) )  ->  ( i  e.  ZZ  /\  N  e.  ZZ ) )
231230adantlr 719 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  (
i  e.  ZZ  /\  N  e.  ZZ )
)
232231, 132syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  (
i  <  N  <->  ( i  +  1 )  <_  N ) )
233210, 232mpbid 213 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  (
i  +  1 )  <_  N )
234212, 135syl 17 . . . . . . . . . . . . . . . 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 1188 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  (
i  +  1 )  e.  ( M ... N ) )
236235adantr 466 . . . . . . . . . . . . . 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 6034 . . . . . . . . . . . . 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 462 . . . . . . . . . . . . 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 37431 . . . . . . . . . . . . 13  |-  ( ( ( P `  i
)  e.  RR  /\  ( P `  ( i  +  1 ) )  e.  RR  /\  t  e.  ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) ) )  ->  t  e.  RR )
240216, 237, 238, 239syl3anc 1264 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  -> 
t  e.  RR )
241 elfzuz 11796 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( M ... k )  ->  i  e.  ( ZZ>= `  M )
)
242241adantl 467 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  i  e.  ( ZZ>= `  M )
)
24348ad3antrrr 734 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... i ) )  ->  P : ( M ... N ) --> RR )
244 elfzelz 11800 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( M ... i )  ->  j  e.  ZZ )
245244adantl 467 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... i ) )  -> 
j  e.  ZZ )
246 elfzle1 11802 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( M ... i )  ->  M  <_  j )
247246adantl 467 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... i ) )  ->  M  <_  j )
248245zred 11040 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... i ) )  -> 
j  e.  RR )
249204adantr 466 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... i ) )  ->  N  e.  RR )
250203adantr 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... i ) )  -> 
i  e.  RR )
251 elfzle2 11803 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  ( M ... i )  ->  j  <_  i )
252251adantl 467 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... i ) )  -> 
j  <_  i )
253210adantr 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... i ) )  -> 
i  <  N )
254248, 250, 249, 252, 253lelttrd 9793 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... i ) )  -> 
j  <  N )
255248, 249, 254ltled 9783 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... i ) )  -> 
j  <_  N )
256212adantr 466 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... i ) )  -> 
( M  e.  ZZ  /\  N  e.  ZZ ) )
257 elfz1 11789 . . . . . . . . . . . . . . . . 17  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( j  e.  ( M ... N )  <-> 
( j  e.  ZZ  /\  M  <_  j  /\  j  <_  N ) ) )
258256, 257syl 17 . . . . . . . . . . . . . . . 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 1188 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... i ) )  -> 
j  e.  ( M ... N ) )
260243, 259ffvelrnd 6034 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... i ) )  -> 
( P `  j
)  e.  RR )
26148ad3antrrr 734 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  P : ( M ... N ) --> RR )
262 elfzelz 11800 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  ( M ... ( i  -  1 ) )  ->  j  e.  ZZ )
263262adantl 467 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
j  e.  ZZ )
264 elfzle1 11802 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  ( M ... ( i  -  1 ) )  ->  M  <_  j )
265264adantl 467 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  M  <_  j )
266263zred 11040 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
j  e.  RR )
267204adantr 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  N  e.  RR )
268203adantr 466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
i  e.  RR )
269 1red 9658 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
1  e.  RR )
270268, 269resubcld 10047 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( i  -  1 )  e.  RR )
271 elfzle2 11803 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ( M ... ( i  -  1 ) )  ->  j  <_  ( i  -  1 ) )
272271adantl 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
j  <_  ( i  -  1 ) )
273268ltm1d 10539 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( i  -  1 )  <  i )
274266, 270, 268, 272, 273lelttrd 9793 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
j  <  i )
275210adantr 466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
i  <  N )
276266, 268, 267, 274, 275lttrd 9796 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
j  <  N )
277266, 267, 276ltled 9783 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
j  <_  N )
278212adantr 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( M  e.  ZZ  /\  N  e.  ZZ ) )
279278, 257syl 17 . . . . . . . . . . . . . . . . 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 1188 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
j  e.  ( M ... N ) )
281261, 280ffvelrnd 6034 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( P `  j
)  e.  RR )
282263peano2zd 11043 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( j  +  1 )  e.  ZZ )
283181ad2antrr 730 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  M  e.  RR )
284266, 269readdcld 9670 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( j  +  1 )  e.  RR )
28550adantr 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  M  e.  RR )
286262zred 11040 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ( M ... ( i  -  1 ) )  ->  j  e.  RR )
287286adantl 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  j  e.  RR )
288 1red 9658 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  1  e.  RR )
289287, 288readdcld 9670 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  ( j  +  1 )  e.  RR )
290264adantl 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  M  <_  j )
291287ltp1d 10537 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  j  <  ( j  +  1 ) )
292285, 287, 289, 290, 291lelttrd 9793 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  M  <  ( j  +  1 ) )
293292adant423 37225 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  M  <  ( j  +  1 ) )
294283, 284, 293ltled 9783 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  M  <_  ( j  +  1 ) )
295 zltp1le 10986 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( j  e.  ZZ  /\  i  e.  ZZ )  ->  ( j  <  i  <->  ( j  +  1 )  <_  i ) )
296262, 200, 295syl2anr 480 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( j  <  i  <->  ( j  +  1 )  <_  i ) )
297274, 296mpbid 213 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( j  +  1 )  <_  i )
298284, 268, 267, 297, 275lelttrd 9793 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( j  +  1 )  <  N )
299284, 267, 298ltled 9783 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( j  +  1 )  <_  N )
300 elfz1 11789 . . . . . . . . . . . . . . . . . 18  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( ( j  +  1 )  e.  ( M ... N )  <-> 
( ( j  +  1 )  e.  ZZ  /\  M  <_  ( j  +  1 )  /\  ( j  +  1 )  <_  N )
) )
301278, 300syl 17 . . . . . . . . . . . . . . . . 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 1188 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( j  +  1 )  e.  ( M ... N ) )
303261, 302ffvelrnd 6034 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( P `  (
j  +  1 ) )  e.  RR )
304 simplll 766 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  ph )
305 elfzuz 11796 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  ( M ... ( i  -  1 ) )  ->  j  e.  ( ZZ>= `  M )
)
306305adantl 467 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
j  e.  ( ZZ>= `  M ) )
307304, 5syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  ->  N  e.  ZZ )
308 elfzo2 11923 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( M..^ N
)  <->  ( j  e.  ( ZZ>= `  M )  /\  N  e.  ZZ  /\  j  <  N ) )
309306, 307, 276, 308syl3anbrc 1189 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
j  e.  ( M..^ N ) )
310 eleq1 2494 . . . . . . . . . . . . . . . . . . 19  |-  ( i  =  j  ->  (
i  e.  ( M..^ N )  <->  j  e.  ( M..^ N ) ) )
311310anbi2d 708 . . . . . . . . . . . . . . . . . 18  |-  ( i  =  j  ->  (
( ph  /\  i  e.  ( M..^ N ) )  <->  ( ph  /\  j  e.  ( M..^ N ) ) ) )
312 fveq2 5877 . . . . . . . . . . . . . . . . . . 19  |-  ( i  =  j  ->  ( P `  i )  =  ( P `  j ) )
313 oveq1 6308 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  =  j  ->  (
i  +  1 )  =  ( j  +  1 ) )
314313fveq2d 5881 . . . . . . . . . . . . . . . . . . 19  |-  ( i  =  j  ->  ( P `  ( i  +  1 ) )  =  ( P `  ( j  +  1 ) ) )
315312, 314breq12d 4433 . . . . . . . . . . . . . . . . . 18  |-  ( i  =  j  ->  (
( P `  i
)  <  ( P `  ( i  +  1 ) )  <->  ( P `  j )  <  ( P `  ( j  +  1 ) ) ) )
316311, 315imbi12d 321 . . . . . . . . . . . . . . . . 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 2068 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( P `  j )  <  ( P `  ( j  +  1 ) ) )
318304, 309, 317syl2anc 665 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( P `  j
)  <  ( P `  ( j  +  1 ) ) )
319281, 303, 318ltled 9783 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( M ... ( i  -  1 ) ) )  -> 
( P `  j
)  <_  ( P `  ( j  +  1 ) ) )
320242, 260, 319monoord 12242 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  ( P `  M )  <_  ( P `  i
) )
321320adantr 466 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  -> 
( P `  M
)  <_  ( P `  i ) )
322216rexrd 9690 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  -> 
( P `  i
)  e.  RR* )
323237rexrd 9690 . . . . . . . . . . . . 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 11691 . . . . . . . . . . . . 13  |-  ( ( ( P `  i
)  e.  RR*  /\  ( P `  ( i  +  1 ) )  e.  RR*  /\  t  e.  ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) ) )  ->  ( P `  i )  <_  t )
325322, 323, 238, 324syl3anc 1264 . . . . . . . . . . . 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 9792 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  -> 
( P `  M
)  <_  t )
327194, 66syl 17 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  -> 
( P `  N
)  e.  RR )
328 iccleub 11690 . . . . . . . . . . . . 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 1264 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  -> 
t  <_  ( P `  ( i  +  1 ) ) )
3305ad2antrr 730 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  N  e.  ZZ )
331 eluz 11172 . . . . . . . . . . . . . . . 16  |-  ( ( ( i  +  1 )  e.  ZZ  /\  N  e.  ZZ )  ->  ( N  e.  (
ZZ>= `  ( i  +  1 ) )  <->  ( i  +  1 )  <_  N ) )
332217, 330, 331syl2anc 665 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  ( N  e.  ( ZZ>= `  ( i  +  1 ) )  <->  ( i  +  1 )  <_  N ) )
333233, 332mpbird 235 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  N  e.  ( ZZ>= `  ( i  +  1 ) ) )
334333adantr 466 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  t  e.  ( ( P `  i ) [,] ( P `  (
i  +  1 ) ) ) )  ->  N  e.  ( ZZ>= `  ( i  +  1 ) ) )
33548ad3antrrr 734 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( (
i  +  1 ) ... N ) )  ->  P : ( M ... N ) --> RR )
336 elfzelz 11800 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( ( i  +  1 ) ... N )  ->  j  e.  ZZ )
337336adantl 467 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( (
i  +  1 ) ... N ) )  ->  j  e.  ZZ )
338 elfzel1 11799 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  e.  ( M ... k )  ->  M  e.  ZZ )
339338zred 11040 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  ( M ... k )  ->  M  e.  RR )
340339adantr 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( i  e.  ( M ... k )  /\  j  e.  ( (
i  +  1 ) ... N ) )  ->  M  e.  RR )
341336zred 11040 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  ( ( i  +  1 ) ... N )  ->  j  e.  RR )
342341adantl 467 . . . . . . . . . . . . . . . . . 18  |-  ( ( i  e.  ( M ... k )  /\  j  e.  ( (
i  +  1 ) ... N ) )  ->  j  e.  RR )
343221adantr 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( i  e.  ( M ... k )  /\  j  e.  ( (
i  +  1 ) ... N ) )  ->  i  e.  RR )
344 1red 9658 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( i  e.  ( M ... k )  /\  j  e.  ( (
i  +  1 ) ... N ) )  ->  1  e.  RR )
345343, 344readdcld 9670 . . . . . . . . . . . . . . . . . . 19  |-  ( ( i  e.  ( M ... k )  /\  j  e.  ( (
i  +  1 ) ... N ) )  ->  ( i  +  1 )  e.  RR )
346201adantr 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( i  e.  ( M ... k )  /\  j  e.  ( (
i  +  1 ) ... N ) )  ->  M  <_  i
)
347343ltp1d 10537 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( i  e.  ( M ... k )  /\  j  e.  ( (
i  +  1 ) ... N ) )  ->  i  <  (
i  +  1 ) )
348340, 343, 345, 346, 347lelttrd 9793 . . . . . . . . . . . . . . . . . . 19  |-  ( ( i  e.  ( M ... k )  /\  j  e.  ( (
i  +  1 ) ... N ) )  ->  M  <  (
i  +  1 ) )
349 elfzle1 11802 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  ( ( i  +  1 ) ... N )  ->  (
i  +  1 )  <_  j )
350349adantl 467 . . . . . . . . . . . . . . . . . . 19  |-  ( ( i  e.  ( M ... k )  /\  j  e.  ( (
i  +  1 ) ... N ) )  ->  ( i  +  1 )  <_  j
)
351340, 345, 342, 348, 350ltletrd 9795 . . . . . . . . . . . . . . . . . 18  |-  ( ( i  e.  ( M ... k )  /\  j  e.  ( (
i  +  1 ) ... N ) )  ->  M  <  j
)
352340, 342, 351ltled 9783 . . . . . . . . . . . . . . . . 17  |-  ( ( i  e.  ( M ... k )  /\  j  e.  ( (
i  +  1 ) ... N ) )  ->  M  <_  j
)
353352adantll 718 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( (
i  +  1 ) ... N ) )  ->  M  <_  j
)
354 elfzle2 11803 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( ( i  +  1 ) ... N )  ->  j  <_  N )
355354adantl 467 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( (
i  +  1 ) ... N ) )  ->  j  <_  N
)
356212adantr 466 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( (
i  +  1 ) ... N ) )  ->  ( M  e.  ZZ  /\  N  e.  ZZ ) )
357356, 257syl 17 . . . . . . . . . . . . . . . 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 1188 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( (
i  +  1 ) ... N ) )  ->  j  e.  ( M ... N ) )
359335, 358ffvelrnd 6034 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( (
i  +  1 ) ... N ) )  ->  ( P `  j )  e.  RR )
360359adantlr 719 . . . . . . . . . . . . 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 766 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( (
i  +  1 ) ... ( N  - 
1 ) ) )  ->  ph )
362 simplr 760 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( (
i  +  1 ) ... ( N  - 
1 ) ) )  ->  i  e.  ( M ... k ) )
363 simpr 462 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( (
i  +  1 ) ... ( N  - 
1 ) ) )  ->  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )
364483ad2ant1 1026 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  P :
( M ... N
) --> RR )
365 elfzelz 11800 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  ( ( i  +  1 ) ... ( N  -  1 ) )  ->  j  e.  ZZ )
3663653ad2ant3 1028 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  j  e.  ZZ )
367503ad2ant1 1026 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  M  e.  RR )
368366zred 11040 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  j  e.  RR )
3692243adant3 1025 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  ( i  +  1 )  e.  RR )
3702273adant3 1025 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  M  <  ( i  +  1 ) )
371 elfzle1 11802 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ( ( i  +  1 ) ... ( N  -  1 ) )  ->  (
i  +  1 )  <_  j )
3723713ad2ant3 1028 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  ( i  +  1 )  <_ 
j )
373367, 369, 368, 370, 372ltletrd 9795 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  M  <  j )
374367, 368, 373ltled 9783 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  M  <_  j )
375365adantl 467 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  j  e.  ZZ )
376375zred 11040 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  j  e.  RR )
37710adantr 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  N  e.  RR )
378 1red 9658 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  1  e.  RR )
379377, 378resubcld 10047 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  ( N  -  1 )  e.  RR )
380 elfzle2 11803 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  e.  ( ( i  +  1 ) ... ( N  -  1 ) )  ->  j  <_  ( N  -  1 ) )
381380adantl 467 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  j  <_  ( N  -  1 ) )
382377ltm1d 10539 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  ( N  -  1 )  <  N )
383376, 379, 377, 381, 382lelttrd 9793 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  j  <  N )
384376, 377, 383ltled 9783 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  j  <_  N )
3853843adant2 1024 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  j  <_  N )
386983ad2ant1 1026 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  ( M  e.  ZZ  /\  N  e.  ZZ ) )
387386, 257syl 17 . . . . . . . . . . . . . . . . . 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 1188 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  j  e.  ( M ... N ) )
389364, 388ffvelrnd 6034 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  ( P `  j )  e.  RR )
390366peano2zd 11043 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  ( j  +  1 )  e.  ZZ )
391390zred 11040 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  ( j  +  1 )  e.  RR )
3922213ad2ant2 1027 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  i  e.  RR )
393 1red 9658 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  1  e.  RR )
3942263adant3 1025 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  i  <  ( i  +  1 ) )
395392, 369, 368, 394, 372ltletrd 9795 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  i  <  j )
396392, 368, 395ltled 9783 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  i  <_  j )
397392, 368, 393, 396leadd1dd 10227 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  ( i  +  1 )  <_ 
( j  +  1 ) )
398367, 369, 391, 370, 397ltletrd 9795 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  M  <  ( j  +  1 ) )
399367, 391, 398ltled 9783 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  M  <_  ( j  +  1 ) )
400 zltp1le 10986 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( j  e.  ZZ  /\  N  e.  ZZ )  ->  ( j  <  N  <->  ( j  +  1 )  <_  N ) )
401365, 5, 400syl2anr 480 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  (
j  <  N  <->  ( j  +  1 )  <_  N ) )
402383, 401mpbid 213 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  (
j  +  1 )  <_  N )
4034023adant2 1024 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  ( j  +  1 )  <_  N )
404386, 300syl 17 . . . . . . . . . . . . . . . . . 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 1188 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  ( j  +  1 )  e.  ( M ... N
) )
406364, 405ffvelrnd 6034 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  ( P `  ( j  +  1 ) )  e.  RR )
407 simp1 1005 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  ph )
40813ad2ant1 1026 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  M  e.  ZZ )
409 eluz 11172 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( M  e.  ZZ  /\  j  e.  ZZ )  ->  ( j  e.  (
ZZ>= `  M )  <->  M  <_  j ) )
410408, 366, 409syl2anc 665 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  ( j  e.  ( ZZ>= `  M )  <->  M  <_  j ) )
411374, 410mpbird 235 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  j  e.  ( ZZ>= `  M )
)
41253ad2ant1 1026 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  N  e.  ZZ )
4133833adant2 1024 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  j  <  N )
414411, 412, 413, 308syl3anbrc 1189 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  j  e.  ( M..^ N ) )
415407, 414, 317syl2anc 665 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  ( P `  j )  <  ( P `  ( j  +  1 ) ) )
416389, 406, 415ltled 9783 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( M ... k )  /\  j  e.  ( ( i  +  1 ) ... ( N  -  1 ) ) )  ->  ( P `  j )  <_  ( P `  ( j  +  1 ) ) )
417361, 362, 363, 416syl3anc 1264 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) )  /\  i  e.  ( M ... k ) )  /\  j  e.  ( (
i  +  1 ) ... ( N  - 
1 ) ) )  ->  ( P `  j )  <_  ( P `  ( j  +  1 ) ) )
418417adantlr 719 . . . . . . . . . . . . 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 12242 . . . . . . . . . . . 12  |-  (