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

Theorem iblspltprt 37947
Description: If a function is integrable on any interval of a partition, then it is integrable on the whole interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
iblspltprt.1  |-  F/ t
ph
iblspltprt.2  |-  ( ph  ->  M  e.  ZZ )
iblspltprt.3  |-  ( ph  ->  N  e.  ( ZZ>= `  ( M  +  1
) ) )
iblspltprt.4  |-  ( (
ph  /\  i  e.  ( M ... N ) )  ->  ( P `  i )  e.  RR )
iblspltprt.5  |-  ( (
ph  /\  i  e.  ( M..^ N ) )  ->  ( P `  i )  <  ( P `  ( i  +  1 ) ) )
iblspltprt.6  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  N )
) )  ->  A  e.  CC )
iblspltprt.7  |-  ( (
ph  /\  i  e.  ( M..^ N ) )  ->  ( t  e.  ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) )  |->  A )  e.  L^1 )
Assertion
Ref Expression
iblspltprt  |-  ( ph  ->  ( t  e.  ( ( P `  M
) [,] ( P `
 N ) ) 
|->  A )  e.  L^1 )
Distinct variable groups:    A, i    i, M, t    i, N, t    P, i, t    ph, i
Allowed substitution hints:    ph( t)    A( t)

Proof of Theorem iblspltprt
Dummy variables  k 
j are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 iblspltprt.3 . . . 4  |-  ( ph  ->  N  e.  ( ZZ>= `  ( M  +  1
) ) )
2 eluzelz 11192 . . . 4  |-  ( N  e.  ( ZZ>= `  ( M  +  1 ) )  ->  N  e.  ZZ )
31, 2syl 17 . . 3  |-  ( ph  ->  N  e.  ZZ )
4 eluzle 11195 . . . 4  |-  ( N  e.  ( ZZ>= `  ( M  +  1 ) )  ->  ( M  +  1 )  <_  N )
51, 4syl 17 . . 3  |-  ( ph  ->  ( M  +  1 )  <_  N )
63zred 11063 . . . 4  |-  ( ph  ->  N  e.  RR )
76leidd 10201 . . 3  |-  ( ph  ->  N  <_  N )
8 iblspltprt.2 . . . . 5  |-  ( ph  ->  M  e.  ZZ )
98peano2zd 11066 . . . 4  |-  ( ph  ->  ( M  +  1 )  e.  ZZ )
10 elfz1 11815 . . . 4  |-  ( ( ( M  +  1 )  e.  ZZ  /\  N  e.  ZZ )  ->  ( N  e.  ( ( M  +  1 ) ... N )  <-> 
( N  e.  ZZ  /\  ( M  +  1 )  <_  N  /\  N  <_  N ) ) )
119, 3, 10syl2anc 673 . . 3  |-  ( ph  ->  ( N  e.  ( ( M  +  1 ) ... N )  <-> 
( N  e.  ZZ  /\  ( M  +  1 )  <_  N  /\  N  <_  N ) ) )
123, 5, 7, 11mpbir3and 1213 . 2  |-  ( ph  ->  N  e.  ( ( M  +  1 ) ... N ) )
13 fveq2 5879 . . . . . . 7  |-  ( j  =  ( M  + 
1 )  ->  ( P `  j )  =  ( P `  ( M  +  1
) ) )
1413oveq2d 6324 . . . . . 6  |-  ( j  =  ( M  + 
1 )  ->  (
( P `  M
) [,] ( P `
 j ) )  =  ( ( P `
 M ) [,] ( P `  ( M  +  1 ) ) ) )
1514mpteq1d 4477 . . . . 5  |-  ( j  =  ( M  + 
1 )  ->  (
t  e.  ( ( P `  M ) [,] ( P `  j ) )  |->  A )  =  ( t  e.  ( ( P `
 M ) [,] ( P `  ( M  +  1 ) ) )  |->  A ) )
1615eleq1d 2533 . . . 4  |-  ( j  =  ( M  + 
1 )  ->  (
( t  e.  ( ( P `  M
) [,] ( P `
 j ) ) 
|->  A )  e.  L^1 
<->  ( t  e.  ( ( P `  M
) [,] ( P `
 ( M  + 
1 ) ) ) 
|->  A )  e.  L^1 ) )
1716imbi2d 323 . . 3  |-  ( j  =  ( M  + 
1 )  ->  (
( ph  ->  ( t  e.  ( ( P `
 M ) [,] ( P `  j
) )  |->  A )  e.  L^1 )  <-> 
( ph  ->  ( t  e.  ( ( P `
 M ) [,] ( P `  ( M  +  1 ) ) )  |->  A )  e.  L^1 ) ) )
18 fveq2 5879 . . . . . . 7  |-  ( j  =  k  ->  ( P `  j )  =  ( P `  k ) )
1918oveq2d 6324 . . . . . 6  |-  ( j  =  k  ->  (
( P `  M
) [,] ( P `
 j ) )  =  ( ( P `
 M ) [,] ( P `  k
) ) )
2019mpteq1d 4477 . . . . 5  |-  ( j  =  k  ->  (
t  e.  ( ( P `  M ) [,] ( P `  j ) )  |->  A )  =  ( t  e.  ( ( P `
 M ) [,] ( P `  k
) )  |->  A ) )
2120eleq1d 2533 . . . 4  |-  ( j  =  k  ->  (
( t  e.  ( ( P `  M
) [,] ( P `
 j ) ) 
|->  A )  e.  L^1 
<->  ( t  e.  ( ( P `  M
) [,] ( P `
 k ) ) 
|->  A )  e.  L^1 ) )
2221imbi2d 323 . . 3  |-  ( j  =  k  ->  (
( ph  ->  ( t  e.  ( ( P `
 M ) [,] ( P `  j
) )  |->  A )  e.  L^1 )  <-> 
( ph  ->  ( t  e.  ( ( P `
 M ) [,] ( P `  k
) )  |->  A )  e.  L^1 ) ) )
23 fveq2 5879 . . . . . . 7  |-  ( j  =  ( k  +  1 )  ->  ( P `  j )  =  ( P `  ( k  +  1 ) ) )
2423oveq2d 6324 . . . . . 6  |-  ( j  =  ( k  +  1 )  ->  (
( P `  M
) [,] ( P `
 j ) )  =  ( ( P `
 M ) [,] ( P `  (
k  +  1 ) ) ) )
2524mpteq1d 4477 . . . . 5  |-  ( j  =  ( k  +  1 )  ->  (
t  e.  ( ( P `  M ) [,] ( P `  j ) )  |->  A )  =  ( t  e.  ( ( P `
 M ) [,] ( P `  (
k  +  1 ) ) )  |->  A ) )
2625eleq1d 2533 . . . 4  |-  ( j  =  ( k  +  1 )  ->  (
( t  e.  ( ( P `  M
) [,] ( P `
 j ) ) 
|->  A )  e.  L^1 
<->  ( t  e.  ( ( P `  M
) [,] ( P `
 ( k  +  1 ) ) ) 
|->  A )  e.  L^1 ) )
2726imbi2d 323 . . 3  |-  ( j  =  ( k  +  1 )  ->  (
( ph  ->  ( t  e.  ( ( P `
 M ) [,] ( P `  j
) )  |->  A )  e.  L^1 )  <-> 
( ph  ->  ( t  e.  ( ( P `
 M ) [,] ( P `  (
k  +  1 ) ) )  |->  A )  e.  L^1 ) ) )
28 fveq2 5879 . . . . . . 7  |-  ( j  =  N  ->  ( P `  j )  =  ( P `  N ) )
2928oveq2d 6324 . . . . . 6  |-  ( j  =  N  ->  (
( P `  M
) [,] ( P `
 j ) )  =  ( ( P `
 M ) [,] ( P `  N
) ) )
3029mpteq1d 4477 . . . . 5  |-  ( j  =  N  ->  (
t  e.  ( ( P `  M ) [,] ( P `  j ) )  |->  A )  =  ( t  e.  ( ( P `
 M ) [,] ( P `  N
) )  |->  A ) )
3130eleq1d 2533 . . . 4  |-  ( j  =  N  ->  (
( t  e.  ( ( P `  M
) [,] ( P `
 j ) ) 
|->  A )  e.  L^1 
<->  ( t  e.  ( ( P `  M
) [,] ( P `
 N ) ) 
|->  A )  e.  L^1 ) )
3231imbi2d 323 . . 3  |-  ( j  =  N  ->  (
( ph  ->  ( t  e.  ( ( P `
 M ) [,] ( P `  j
) )  |->  A )  e.  L^1 )  <-> 
( ph  ->  ( t  e.  ( ( P `
 M ) [,] ( P `  N
) )  |->  A )  e.  L^1 ) ) )
33 uzid 11197 . . . . . . 7  |-  ( M  e.  ZZ  ->  M  e.  ( ZZ>= `  M )
)
348, 33syl 17 . . . . . 6  |-  ( ph  ->  M  e.  ( ZZ>= `  M ) )
358zred 11063 . . . . . . 7  |-  ( ph  ->  M  e.  RR )
36 1red 9676 . . . . . . . 8  |-  ( ph  ->  1  e.  RR )
3735, 36readdcld 9688 . . . . . . 7  |-  ( ph  ->  ( M  +  1 )  e.  RR )
3835ltp1d 10559 . . . . . . 7  |-  ( ph  ->  M  <  ( M  +  1 ) )
3935, 37, 6, 38, 5ltletrd 9812 . . . . . 6  |-  ( ph  ->  M  <  N )
40 elfzo2 11950 . . . . . 6  |-  ( M  e.  ( M..^ N
)  <->  ( M  e.  ( ZZ>= `  M )  /\  N  e.  ZZ  /\  M  <  N ) )
4134, 3, 39, 40syl3anbrc 1214 . . . . 5  |-  ( ph  ->  M  e.  ( M..^ N ) )
42 fveq2 5879 . . . . . . . . . 10  |-  ( i  =  M  ->  ( P `  i )  =  ( P `  M ) )
43 oveq1 6315 . . . . . . . . . . 11  |-  ( i  =  M  ->  (
i  +  1 )  =  ( M  + 
1 ) )
4443fveq2d 5883 . . . . . . . . . 10  |-  ( i  =  M  ->  ( P `  ( i  +  1 ) )  =  ( P `  ( M  +  1
) ) )
4542, 44oveq12d 6326 . . . . . . . . 9  |-  ( i  =  M  ->  (
( P `  i
) [,] ( P `
 ( i  +  1 ) ) )  =  ( ( P `
 M ) [,] ( P `  ( M  +  1 ) ) ) )
4645mpteq1d 4477 . . . . . . . 8  |-  ( i  =  M  ->  (
t  e.  ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) )  |->  A )  =  ( t  e.  ( ( P `
 M ) [,] ( P `  ( M  +  1 ) ) )  |->  A ) )
4746eleq1d 2533 . . . . . . 7  |-  ( i  =  M  ->  (
( t  e.  ( ( P `  i
) [,] ( P `
 ( i  +  1 ) ) ) 
|->  A )  e.  L^1 
<->  ( t  e.  ( ( P `  M
) [,] ( P `
 ( M  + 
1 ) ) ) 
|->  A )  e.  L^1 ) )
4847imbi2d 323 . . . . . 6  |-  ( i  =  M  ->  (
( ph  ->  ( t  e.  ( ( P `
 i ) [,] ( P `  (
i  +  1 ) ) )  |->  A )  e.  L^1 )  <-> 
( ph  ->  ( t  e.  ( ( P `
 M ) [,] ( P `  ( M  +  1 ) ) )  |->  A )  e.  L^1 ) ) )
49 iblspltprt.7 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( M..^ N ) )  ->  ( t  e.  ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) )  |->  A )  e.  L^1 )
5049expcom 442 . . . . . 6  |-  ( i  e.  ( M..^ N
)  ->  ( ph  ->  ( t  e.  ( ( P `  i
) [,] ( P `
 ( i  +  1 ) ) ) 
|->  A )  e.  L^1 ) )
5148, 50vtoclga 3099 . . . . 5  |-  ( M  e.  ( M..^ N
)  ->  ( ph  ->  ( t  e.  ( ( P `  M
) [,] ( P `
 ( M  + 
1 ) ) ) 
|->  A )  e.  L^1 ) )
5241, 51mpcom 36 . . . 4  |-  ( ph  ->  ( t  e.  ( ( P `  M
) [,] ( P `
 ( M  + 
1 ) ) ) 
|->  A )  e.  L^1 )
5352a1i 11 . . 3  |-  ( N  e.  ( ZZ>= `  ( M  +  1 ) )  ->  ( ph  ->  ( t  e.  ( ( P `  M
) [,] ( P `
 ( M  + 
1 ) ) ) 
|->  A )  e.  L^1 ) )
54 nfv 1769 . . . . . 6  |-  F/ t  k  e.  ( ( M  +  1 )..^ N )
55 iblspltprt.1 . . . . . . 7  |-  F/ t
ph
56 nfmpt1 4485 . . . . . . . 8  |-  F/_ t
( t  e.  ( ( P `  M
) [,] ( P `
 k ) ) 
|->  A )
5756nfel1 2626 . . . . . . 7  |-  F/ t ( t  e.  ( ( P `  M
) [,] ( P `
 k ) ) 
|->  A )  e.  L^1
5855, 57nfim 2023 . . . . . 6  |-  F/ t ( ph  ->  (
t  e.  ( ( P `  M ) [,] ( P `  k ) )  |->  A )  e.  L^1 )
5954, 58, 55nf3an 2033 . . . . 5  |-  F/ t ( k  e.  ( ( M  +  1 )..^ N )  /\  ( ph  ->  ( t  e.  ( ( P `  M ) [,] ( P `  k )
)  |->  A )  e.  L^1 )  /\  ph )
60 simp3 1032 . . . . . 6  |-  ( ( k  e.  ( ( M  +  1 )..^ N )  /\  ( ph  ->  ( t  e.  ( ( P `  M ) [,] ( P `  k )
)  |->  A )  e.  L^1 )  /\  ph )  ->  ph )
61 simp1 1030 . . . . . 6  |-  ( ( k  e.  ( ( M  +  1 )..^ N )  /\  ( ph  ->  ( t  e.  ( ( P `  M ) [,] ( P `  k )
)  |->  A )  e.  L^1 )  /\  ph )  ->  k  e.  ( ( M  + 
1 )..^ N ) )
6235leidd 10201 . . . . . . . . . . . . 13  |-  ( ph  ->  M  <_  M )
6335, 6, 39ltled 9800 . . . . . . . . . . . . 13  |-  ( ph  ->  M  <_  N )
64 elfz1 11815 . . . . . . . . . . . . . 14  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( M  e.  ( M ... N )  <-> 
( M  e.  ZZ  /\  M  <_  M  /\  M  <_  N ) ) )
658, 3, 64syl2anc 673 . . . . . . . . . . . . 13  |-  ( ph  ->  ( M  e.  ( M ... N )  <-> 
( M  e.  ZZ  /\  M  <_  M  /\  M  <_  N ) ) )
668, 62, 63, 65mpbir3and 1213 . . . . . . . . . . . 12  |-  ( ph  ->  M  e.  ( M ... N ) )
6766ancli 560 . . . . . . . . . . . 12  |-  ( ph  ->  ( ph  /\  M  e.  ( M ... N
) ) )
68 eleq1 2537 . . . . . . . . . . . . . . 15  |-  ( i  =  M  ->  (
i  e.  ( M ... N )  <->  M  e.  ( M ... N ) ) )
6968anbi2d 718 . . . . . . . . . . . . . 14  |-  ( i  =  M  ->  (
( ph  /\  i  e.  ( M ... N
) )  <->  ( ph  /\  M  e.  ( M ... N ) ) ) )
7042eleq1d 2533 . . . . . . . . . . . . . 14  |-  ( i  =  M  ->  (
( P `  i
)  e.  RR  <->  ( P `  M )  e.  RR ) )
7169, 70imbi12d 327 . . . . . . . . . . . . 13  |-  ( i  =  M  ->  (
( ( ph  /\  i  e.  ( M ... N ) )  -> 
( P `  i
)  e.  RR )  <-> 
( ( ph  /\  M  e.  ( M ... N ) )  -> 
( P `  M
)  e.  RR ) ) )
72 iblspltprt.4 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( M ... N ) )  ->  ( P `  i )  e.  RR )
7371, 72vtoclg 3093 . . . . . . . . . . . 12  |-  ( M  e.  ( M ... N )  ->  (
( ph  /\  M  e.  ( M ... N
) )  ->  ( P `  M )  e.  RR ) )
7466, 67, 73sylc 61 . . . . . . . . . . 11  |-  ( ph  ->  ( P `  M
)  e.  RR )
7574adantr 472 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  ( P `  M )  e.  RR )
7675rexrd 9708 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  ( P `  M )  e.  RR* )
77 simpl 464 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  ph )
78 elfzoelz 11947 . . . . . . . . . . . . 13  |-  ( k  e.  ( ( M  +  1 )..^ N
)  ->  k  e.  ZZ )
7978adantl 473 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  k  e.  ZZ )
8035adantr 472 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  M  e.  RR )
8179zred 11063 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  k  e.  RR )
8237adantr 472 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  ( M  +  1 )  e.  RR )
8338adantr 472 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  M  <  ( M  +  1 ) )
84 elfzole1 11955 . . . . . . . . . . . . . . 15  |-  ( k  e.  ( ( M  +  1 )..^ N
)  ->  ( M  +  1 )  <_ 
k )
8584adantl 473 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  ( M  +  1 )  <_ 
k )
8680, 82, 81, 83, 85ltletrd 9812 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  M  <  k )
8780, 81, 86ltled 9800 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  M  <_  k )
886adantr 472 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  N  e.  RR )
89 elfzolt2 11956 . . . . . . . . . . . . . 14  |-  ( k  e.  ( ( M  +  1 )..^ N
)  ->  k  <  N )
9089adantl 473 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  k  <  N )
9181, 88, 90ltled 9800 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  k  <_  N )
928, 3jca 541 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( M  e.  ZZ  /\  N  e.  ZZ ) )
9392adantr 472 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  ( M  e.  ZZ  /\  N  e.  ZZ ) )
94 elfz1 11815 . . . . . . . . . . . . 13  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( k  e.  ( M ... N )  <-> 
( k  e.  ZZ  /\  M  <_  k  /\  k  <_  N ) ) )
9593, 94syl 17 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  ( k  e.  ( M ... N
)  <->  ( k  e.  ZZ  /\  M  <_ 
k  /\  k  <_  N ) ) )
9679, 87, 91, 95mpbir3and 1213 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  k  e.  ( M ... N ) )
97 eleq1 2537 . . . . . . . . . . . . . 14  |-  ( i  =  k  ->  (
i  e.  ( M ... N )  <->  k  e.  ( M ... N ) ) )
9897anbi2d 718 . . . . . . . . . . . . 13  |-  ( i  =  k  ->  (
( ph  /\  i  e.  ( M ... N
) )  <->  ( ph  /\  k  e.  ( M ... N ) ) ) )
99 fveq2 5879 . . . . . . . . . . . . . 14  |-  ( i  =  k  ->  ( P `  i )  =  ( P `  k ) )
10099eleq1d 2533 . . . . . . . . . . . . 13  |-  ( i  =  k  ->  (
( P `  i
)  e.  RR  <->  ( P `  k )  e.  RR ) )
10198, 100imbi12d 327 . . . . . . . . . . . 12  |-  ( i  =  k  ->  (
( ( ph  /\  i  e.  ( M ... N ) )  -> 
( P `  i
)  e.  RR )  <-> 
( ( ph  /\  k  e.  ( M ... N ) )  -> 
( P `  k
)  e.  RR ) ) )
102101, 72chvarv 2120 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( M ... N ) )  ->  ( P `  k )  e.  RR )
10377, 96, 102syl2anc 673 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  ( P `  k )  e.  RR )
104103rexrd 9708 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  ( P `  k )  e.  RR* )
10579peano2zd 11066 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  ( k  +  1 )  e.  ZZ )
106105zred 11063 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  ( k  +  1 )  e.  RR )
107 1red 9676 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  1  e.  RR )
10880, 81, 107, 86ltadd1dd 10245 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  ( M  +  1 )  < 
( k  +  1 ) )
10980, 82, 106, 83, 108lttrd 9813 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  M  <  ( k  +  1 ) )
11080, 106, 109ltled 9800 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  M  <_  ( k  +  1 ) )
111 zltp1le 11010 . . . . . . . . . . . . . 14  |-  ( ( k  e.  ZZ  /\  N  e.  ZZ )  ->  ( k  <  N  <->  ( k  +  1 )  <_  N ) )
11278, 3, 111syl2anr 486 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  ( k  <  N  <->  ( k  +  1 )  <_  N
) )
11390, 112mpbid 215 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  ( k  +  1 )  <_  N )
114 elfz1 11815 . . . . . . . . . . . . 13  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( ( k  +  1 )  e.  ( M ... N )  <-> 
( ( k  +  1 )  e.  ZZ  /\  M  <_  ( k  +  1 )  /\  ( k  +  1 )  <_  N )
) )
11593, 114syl 17 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  ( (
k  +  1 )  e.  ( M ... N )  <->  ( (
k  +  1 )  e.  ZZ  /\  M  <_  ( k  +  1 )  /\  ( k  +  1 )  <_  N ) ) )
116105, 110, 113, 115mpbir3and 1213 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  ( k  +  1 )  e.  ( M ... N
) )
11777, 116jca 541 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  ( ph  /\  ( k  +  1 )  e.  ( M ... N ) ) )
118 eleq1 2537 . . . . . . . . . . . . . 14  |-  ( i  =  ( k  +  1 )  ->  (
i  e.  ( M ... N )  <->  ( k  +  1 )  e.  ( M ... N
) ) )
119118anbi2d 718 . . . . . . . . . . . . 13  |-  ( i  =  ( k  +  1 )  ->  (
( ph  /\  i  e.  ( M ... N
) )  <->  ( ph  /\  ( k  +  1 )  e.  ( M ... N ) ) ) )
120 fveq2 5879 . . . . . . . . . . . . . 14  |-  ( i  =  ( k  +  1 )  ->  ( P `  i )  =  ( P `  ( k  +  1 ) ) )
121120eleq1d 2533 . . . . . . . . . . . . 13  |-  ( i  =  ( k  +  1 )  ->  (
( P `  i
)  e.  RR  <->  ( P `  ( k  +  1 ) )  e.  RR ) )
122119, 121imbi12d 327 . . . . . . . . . . . 12  |-  ( i  =  ( k  +  1 )  ->  (
( ( ph  /\  i  e.  ( M ... N ) )  -> 
( P `  i
)  e.  RR )  <-> 
( ( ph  /\  ( k  +  1 )  e.  ( M ... N ) )  ->  ( P `  ( k  +  1 ) )  e.  RR ) ) )
123122, 72vtoclg 3093 . . . . . . . . . . 11  |-  ( ( k  +  1 )  e.  ( M ... N )  ->  (
( ph  /\  (
k  +  1 )  e.  ( M ... N ) )  -> 
( P `  (
k  +  1 ) )  e.  RR ) )
124116, 117, 123sylc 61 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  ( P `  ( k  +  1 ) )  e.  RR )
125124rexrd 9708 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  ( P `  ( k  +  1 ) )  e.  RR* )
126 eluz 11196 . . . . . . . . . . . 12  |-  ( ( M  e.  ZZ  /\  k  e.  ZZ )  ->  ( k  e.  (
ZZ>= `  M )  <->  M  <_  k ) )
1278, 78, 126syl2an 485 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  ( k  e.  ( ZZ>= `  M )  <->  M  <_  k ) )
12887, 127mpbird 240 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  k  e.  ( ZZ>= `  M )
)
129 simpll 768 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  ph )
130 elfzelz 11826 . . . . . . . . . . . . 13  |-  ( i  e.  ( M ... k )  ->  i  e.  ZZ )
131130adantl 473 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  i  e.  ZZ )
132 elfzle1 11828 . . . . . . . . . . . . 13  |-  ( i  e.  ( M ... k )  ->  M  <_  i )
133132adantl 473 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  M  <_  i )
134131zred 11063 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  i  e.  RR )
135129, 6syl 17 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  N  e.  RR )
13681adantr 472 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  k  e.  RR )
137 elfzle2 11829 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( M ... k )  ->  i  <_  k )
138137adantl 473 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  i  <_  k )
13990adantr 472 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  k  <  N )
140134, 136, 135, 138, 139lelttrd 9810 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  i  <  N )
141134, 135, 140ltled 9800 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  i  <_  N )
142 elfz1 11815 . . . . . . . . . . . . 13  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( i  e.  ( M ... N )  <-> 
( i  e.  ZZ  /\  M  <_  i  /\  i  <_  N ) ) )
143129, 92, 1423syl 18 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  (
i  e.  ( M ... N )  <->  ( i  e.  ZZ  /\  M  <_ 
i  /\  i  <_  N ) ) )
144131, 133, 141, 143mpbir3and 1213 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  i  e.  ( M ... N
) )
145129, 144, 72syl2anc 673 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... k
) )  ->  ( P `  i )  e.  RR )
146 simpll 768 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... (
k  -  1 ) ) )  ->  ph )
147 elfzelz 11826 . . . . . . . . . . . . . 14  |-  ( i  e.  ( M ... ( k  -  1 ) )  ->  i  e.  ZZ )
148147adantl 473 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... (
k  -  1 ) ) )  ->  i  e.  ZZ )
149 elfzle1 11828 . . . . . . . . . . . . . 14  |-  ( i  e.  ( M ... ( k  -  1 ) )  ->  M  <_  i )
150149adantl 473 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... (
k  -  1 ) ) )  ->  M  <_  i )
151148zred 11063 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... (
k  -  1 ) ) )  ->  i  e.  RR )
152146, 6syl 17 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... (
k  -  1 ) ) )  ->  N  e.  RR )
15381adantr 472 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... (
k  -  1 ) ) )  ->  k  e.  RR )
154 1red 9676 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... (
k  -  1 ) ) )  ->  1  e.  RR )
155153, 154resubcld 10068 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... (
k  -  1 ) ) )  ->  (
k  -  1 )  e.  RR )
156 elfzle2 11829 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( M ... ( k  -  1 ) )  ->  i  <_  ( k  -  1 ) )
157156adantl 473 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... (
k  -  1 ) ) )  ->  i  <_  ( k  -  1 ) )
15878zred 11063 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  ( ( M  +  1 )..^ N
)  ->  k  e.  RR )
159 1red 9676 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  ( ( M  +  1 )..^ N
)  ->  1  e.  RR )
160158, 159resubcld 10068 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  ( ( M  +  1 )..^ N
)  ->  ( k  -  1 )  e.  RR )
161 elfzoel2 11946 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  ( ( M  +  1 )..^ N
)  ->  N  e.  ZZ )
162161zred 11063 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  ( ( M  +  1 )..^ N
)  ->  N  e.  RR )
163158ltm1d 10561 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  ( ( M  +  1 )..^ N
)  ->  ( k  -  1 )  < 
k )
164160, 158, 162, 163, 89lttrd 9813 . . . . . . . . . . . . . . . 16  |-  ( k  e.  ( ( M  +  1 )..^ N
)  ->  ( k  -  1 )  < 
N )
165164ad2antlr 741 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... (
k  -  1 ) ) )  ->  (
k  -  1 )  <  N )
166151, 155, 152, 157, 165lelttrd 9810 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... (
k  -  1 ) ) )  ->  i  <  N )
167151, 152, 166ltled 9800 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... (
k  -  1 ) ) )  ->  i  <_  N )
168146, 92, 1423syl 18 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... (
k  -  1 ) ) )  ->  (
i  e.  ( M ... N )  <->  ( i  e.  ZZ  /\  M  <_ 
i  /\  i  <_  N ) ) )
169148, 150, 167, 168mpbir3and 1213 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... (
k  -  1 ) ) )  ->  i  e.  ( M ... N
) )
170146, 169, 72syl2anc 673 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... (
k  -  1 ) ) )  ->  ( P `  i )  e.  RR )
171148peano2zd 11066 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... (
k  -  1 ) ) )  ->  (
i  +  1 )  e.  ZZ )
172 elfzel1 11825 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( M ... ( k  -  1 ) )  ->  M  e.  ZZ )
173172zred 11063 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( M ... ( k  -  1 ) )  ->  M  e.  RR )
174147zred 11063 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( M ... ( k  -  1 ) )  ->  i  e.  RR )
175 1red 9676 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( M ... ( k  -  1 ) )  ->  1  e.  RR )
176174, 175readdcld 9688 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( M ... ( k  -  1 ) )  ->  (
i  +  1 )  e.  RR )
177174ltp1d 10559 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( M ... ( k  -  1 ) )  ->  i  <  ( i  +  1 ) )
178173, 174, 176, 149, 177lelttrd 9810 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( M ... ( k  -  1 ) )  ->  M  <  ( i  +  1 ) )
179173, 176, 178ltled 9800 . . . . . . . . . . . . . 14  |-  ( i  e.  ( M ... ( k  -  1 ) )  ->  M  <_  ( i  +  1 ) )
180179adantl 473 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... (
k  -  1 ) ) )  ->  M  <_  ( i  +  1 ) )
181146, 1, 23syl 18 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... (
k  -  1 ) ) )  ->  N  e.  ZZ )
182 zltp1le 11010 . . . . . . . . . . . . . . 15  |-  ( ( i  e.  ZZ  /\  N  e.  ZZ )  ->  ( i  <  N  <->  ( i  +  1 )  <_  N ) )
183148, 181, 182syl2anc 673 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... (
k  -  1 ) ) )  ->  (
i  <  N  <->  ( i  +  1 )  <_  N ) )
184166, 183mpbid 215 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... (
k  -  1 ) ) )  ->  (
i  +  1 )  <_  N )
185 elfz1 11815 . . . . . . . . . . . . . 14  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( ( i  +  1 )  e.  ( M ... N )  <-> 
( ( i  +  1 )  e.  ZZ  /\  M  <_  ( i  +  1 )  /\  ( i  +  1 )  <_  N )
) )
186146, 92, 1853syl 18 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... (
k  -  1 ) ) )  ->  (
( i  +  1 )  e.  ( M ... N )  <->  ( (
i  +  1 )  e.  ZZ  /\  M  <_  ( i  +  1 )  /\  ( i  +  1 )  <_  N ) ) )
187171, 180, 184, 186mpbir3and 1213 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... (
k  -  1 ) ) )  ->  (
i  +  1 )  e.  ( M ... N ) )
188146, 187jca 541 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... (
k  -  1 ) ) )  ->  ( ph  /\  ( i  +  1 )  e.  ( M ... N ) ) )
189 eleq1 2537 . . . . . . . . . . . . . . 15  |-  ( k  =  ( i  +  1 )  ->  (
k  e.  ( M ... N )  <->  ( i  +  1 )  e.  ( M ... N
) ) )
190189anbi2d 718 . . . . . . . . . . . . . 14  |-  ( k  =  ( i  +  1 )  ->  (
( ph  /\  k  e.  ( M ... N
) )  <->  ( ph  /\  ( i  +  1 )  e.  ( M ... N ) ) ) )
191 fveq2 5879 . . . . . . . . . . . . . . 15  |-  ( k  =  ( i  +  1 )  ->  ( P `  k )  =  ( P `  ( i  +  1 ) ) )
192191eleq1d 2533 . . . . . . . . . . . . . 14  |-  ( k  =  ( i  +  1 )  ->  (
( P `  k
)  e.  RR  <->  ( P `  ( i  +  1 ) )  e.  RR ) )
193190, 192imbi12d 327 . . . . . . . . . . . . 13  |-  ( k  =  ( i  +  1 )  ->  (
( ( ph  /\  k  e.  ( M ... N ) )  -> 
( P `  k
)  e.  RR )  <-> 
( ( ph  /\  ( i  +  1 )  e.  ( M ... N ) )  ->  ( P `  ( i  +  1 ) )  e.  RR ) ) )
194193, 102vtoclg 3093 . . . . . . . . . . . 12  |-  ( ( i  +  1 )  e.  ( M ... N )  ->  (
( ph  /\  (
i  +  1 )  e.  ( M ... N ) )  -> 
( P `  (
i  +  1 ) )  e.  RR ) )
195187, 188, 194sylc 61 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... (
k  -  1 ) ) )  ->  ( P `  ( i  +  1 ) )  e.  RR )
196 elfzuz 11822 . . . . . . . . . . . . . 14  |-  ( i  e.  ( M ... ( k  -  1 ) )  ->  i  e.  ( ZZ>= `  M )
)
197196adantl 473 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... (
k  -  1 ) ) )  ->  i  e.  ( ZZ>= `  M )
)
198 elfzo2 11950 . . . . . . . . . . . . 13  |-  ( i  e.  ( M..^ N
)  <->  ( i  e.  ( ZZ>= `  M )  /\  N  e.  ZZ  /\  i  <  N ) )
199197, 181, 166, 198syl3anbrc 1214 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... (
k  -  1 ) ) )  ->  i  e.  ( M..^ N ) )
200 iblspltprt.5 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( M..^ N ) )  ->  ( P `  i )  <  ( P `  ( i  +  1 ) ) )
201146, 199, 200syl2anc 673 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... (
k  -  1 ) ) )  ->  ( P `  i )  <  ( P `  (
i  +  1 ) ) )
202170, 195, 201ltled 9800 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( M ... (
k  -  1 ) ) )  ->  ( P `  i )  <_  ( P `  (
i  +  1 ) ) )
203128, 145, 202monoord 12281 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  ( P `  M )  <_  ( P `  k )
)
204161adantl 473 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  N  e.  ZZ )
205 elfzo2 11950 . . . . . . . . . . . 12  |-  ( k  e.  ( M..^ N
)  <->  ( k  e.  ( ZZ>= `  M )  /\  N  e.  ZZ  /\  k  <  N ) )
206128, 204, 90, 205syl3anbrc 1214 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  k  e.  ( M..^ N ) )
207 eleq1 2537 . . . . . . . . . . . . . 14  |-  ( i  =  k  ->  (
i  e.  ( M..^ N )  <->  k  e.  ( M..^ N ) ) )
208207anbi2d 718 . . . . . . . . . . . . 13  |-  ( i  =  k  ->  (
( ph  /\  i  e.  ( M..^ N ) )  <->  ( ph  /\  k  e.  ( M..^ N ) ) ) )
209 oveq1 6315 . . . . . . . . . . . . . . 15  |-  ( i  =  k  ->  (
i  +  1 )  =  ( k  +  1 ) )
210209fveq2d 5883 . . . . . . . . . . . . . 14  |-  ( i  =  k  ->  ( P `  ( i  +  1 ) )  =  ( P `  ( k  +  1 ) ) )
21199, 210breq12d 4408 . . . . . . . . . . . . 13  |-  ( i  =  k  ->  (
( P `  i
)  <  ( P `  ( i  +  1 ) )  <->  ( P `  k )  <  ( P `  ( k  +  1 ) ) ) )
212208, 211imbi12d 327 . . . . . . . . . . . 12  |-  ( i  =  k  ->  (
( ( ph  /\  i  e.  ( M..^ N ) )  -> 
( P `  i
)  <  ( P `  ( i  +  1 ) ) )  <->  ( ( ph  /\  k  e.  ( M..^ N ) )  ->  ( P `  k )  <  ( P `  ( k  +  1 ) ) ) ) )
213212, 200chvarv 2120 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( P `  k )  <  ( P `  ( k  +  1 ) ) )
21477, 206, 213syl2anc 673 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  ( P `  k )  <  ( P `  ( k  +  1 ) ) )
215103, 124, 214ltled 9800 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  ( P `  k )  <_  ( P `  ( k  +  1 ) ) )
216 iccintsng 37720 . . . . . . . . 9  |-  ( ( ( ( P `  M )  e.  RR*  /\  ( P `  k
)  e.  RR*  /\  ( P `  ( k  +  1 ) )  e.  RR* )  /\  (
( P `  M
)  <_  ( P `  k )  /\  ( P `  k )  <_  ( P `  (
k  +  1 ) ) ) )  -> 
( ( ( P `
 M ) [,] ( P `  k
) )  i^i  (
( P `  k
) [,] ( P `
 ( k  +  1 ) ) ) )  =  { ( P `  k ) } )
21776, 104, 125, 203, 215, 216syl32anc 1300 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  ( (
( P `  M
) [,] ( P `
 k ) )  i^i  ( ( P `
 k ) [,] ( P `  (
k  +  1 ) ) ) )  =  { ( P `  k ) } )
218217fveq2d 5883 . . . . . . 7  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  ( vol* `  ( ( ( P `  M ) [,] ( P `  k ) )  i^i  ( ( P `  k ) [,] ( P `  ( k  +  1 ) ) ) ) )  =  ( vol* `  { ( P `  k ) } ) )
219 ovolsn 22526 . . . . . . . 8  |-  ( ( P `  k )  e.  RR  ->  ( vol* `  { ( P `  k ) } )  =  0 )
220103, 219syl 17 . . . . . . 7  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  ( vol* `  { ( P `
 k ) } )  =  0 )
221218, 220eqtrd 2505 . . . . . 6  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  ( vol* `  ( ( ( P `  M ) [,] ( P `  k ) )  i^i  ( ( P `  k ) [,] ( P `  ( k  +  1 ) ) ) ) )  =  0 )
22260, 61, 221syl2anc 673 . . . . 5  |-  ( ( k  e.  ( ( M  +  1 )..^ N )  /\  ( ph  ->  ( t  e.  ( ( P `  M ) [,] ( P `  k )
)  |->  A )  e.  L^1 )  /\  ph )  ->  ( vol* `  ( ( ( P `  M ) [,] ( P `  k ) )  i^i  ( ( P `  k ) [,] ( P `  ( k  +  1 ) ) ) ) )  =  0 )
22375, 124, 103, 203, 215eliccd 37697 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  ( P `  k )  e.  ( ( P `  M
) [,] ( P `
 ( k  +  1 ) ) ) )
22475, 124, 2233jca 1210 . . . . . . 7  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  ( ( P `  M )  e.  RR  /\  ( P `
 ( k  +  1 ) )  e.  RR  /\  ( P `
 k )  e.  ( ( P `  M ) [,] ( P `  ( k  +  1 ) ) ) ) )
22560, 61, 224syl2anc 673 . . . . . 6  |-  ( ( k  e.  ( ( M  +  1 )..^ N )  /\  ( ph  ->  ( t  e.  ( ( P `  M ) [,] ( P `  k )
)  |->  A )  e.  L^1 )  /\  ph )  ->  ( ( P `  M )  e.  RR  /\  ( P `
 ( k  +  1 ) )  e.  RR  /\  ( P `
 k )  e.  ( ( P `  M ) [,] ( P `  ( k  +  1 ) ) ) ) )
226 iccsplit 11791 . . . . . 6  |-  ( ( ( P `  M
)  e.  RR  /\  ( P `  ( k  +  1 ) )  e.  RR  /\  ( P `  k )  e.  ( ( P `  M ) [,] ( P `  ( k  +  1 ) ) ) )  ->  (
( P `  M
) [,] ( P `
 ( k  +  1 ) ) )  =  ( ( ( P `  M ) [,] ( P `  k ) )  u.  ( ( P `  k ) [,] ( P `  ( k  +  1 ) ) ) ) )
227225, 226syl 17 . . . . 5  |-  ( ( k  e.  ( ( M  +  1 )..^ N )  /\  ( ph  ->  ( t  e.  ( ( P `  M ) [,] ( P `  k )
)  |->  A )  e.  L^1 )  /\  ph )  ->  ( ( P `  M ) [,] ( P `  (
k  +  1 ) ) )  =  ( ( ( P `  M ) [,] ( P `  k )
)  u.  ( ( P `  k ) [,] ( P `  ( k  +  1 ) ) ) ) )
228 simpl3 1035 . . . . . 6  |-  ( ( ( k  e.  ( ( M  +  1 )..^ N )  /\  ( ph  ->  ( t  e.  ( ( P `  M ) [,] ( P `  k )
)  |->  A )  e.  L^1 )  /\  ph )  /\  t  e.  ( ( P `  M ) [,] ( P `  ( k  +  1 ) ) ) )  ->  ph )
229 simpl1 1033 . . . . . 6  |-  ( ( ( k  e.  ( ( M  +  1 )..^ N )  /\  ( ph  ->  ( t  e.  ( ( P `  M ) [,] ( P `  k )
)  |->  A )  e.  L^1 )  /\  ph )  /\  t  e.  ( ( P `  M ) [,] ( P `  ( k  +  1 ) ) ) )  ->  k  e.  ( ( M  + 
1 )..^ N ) )
230 simpr 468 . . . . . 6  |-  ( ( ( k  e.  ( ( M  +  1 )..^ N )  /\  ( ph  ->  ( t  e.  ( ( P `  M ) [,] ( P `  k )
)  |->  A )  e.  L^1 )  /\  ph )  /\  t  e.  ( ( P `  M ) [,] ( P `  ( k  +  1 ) ) ) )  ->  t  e.  ( ( P `  M ) [,] ( P `  ( k  +  1 ) ) ) )
231 simp1 1030 . . . . . . 7  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N )  /\  t  e.  ( ( P `  M
) [,] ( P `
 ( k  +  1 ) ) ) )  ->  ph )
232 eliccxr 37708 . . . . . . . . 9  |-  ( t  e.  ( ( P `
 M ) [,] ( P `  (
k  +  1 ) ) )  ->  t  e.  RR* )
2332323ad2ant3 1053 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N )  /\  t  e.  ( ( P `  M
) [,] ( P `
 ( k  +  1 ) ) ) )  ->  t  e.  RR* )
23474rexrd 9708 . . . . . . . . . 10  |-  ( ph  ->  ( P `  M
)  e.  RR* )
2352343ad2ant1 1051 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N )  /\  t  e.  ( ( P `  M
) [,] ( P `
 ( k  +  1 ) ) ) )  ->  ( P `  M )  e.  RR* )
2361253adant3 1050 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N )  /\  t  e.  ( ( P `  M
) [,] ( P `
 ( k  +  1 ) ) ) )  ->  ( P `  ( k  +  1 ) )  e.  RR* )
237 simp3 1032 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N )  /\  t  e.  ( ( P `  M
) [,] ( P `
 ( k  +  1 ) ) ) )  ->  t  e.  ( ( P `  M ) [,] ( P `  ( k  +  1 ) ) ) )
238 iccgelb 11716 . . . . . . . . 9  |-  ( ( ( P `  M
)  e.  RR*  /\  ( P `  ( k  +  1 ) )  e.  RR*  /\  t  e.  ( ( P `  M ) [,] ( P `  ( k  +  1 ) ) ) )  ->  ( P `  M )  <_  t )
239235, 236, 237, 238syl3anc 1292 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N )  /\  t  e.  ( ( P `  M
) [,] ( P `
 ( k  +  1 ) ) ) )  ->  ( P `  M )  <_  t
)
24075, 124jca 541 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  ( ( P `  M )  e.  RR  /\  ( P `
 ( k  +  1 ) )  e.  RR ) )
2412403adant3 1050 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N )  /\  t  e.  ( ( P `  M
) [,] ( P `
 ( k  +  1 ) ) ) )  ->  ( ( P `  M )  e.  RR  /\  ( P `
 ( k  +  1 ) )  e.  RR ) )
242 iccssre 11741 . . . . . . . . . . 11  |-  ( ( ( P `  M
)  e.  RR  /\  ( P `  ( k  +  1 ) )  e.  RR )  -> 
( ( P `  M ) [,] ( P `  ( k  +  1 ) ) )  C_  RR )
243242sseld 3417 . . . . . . . . . 10  |-  ( ( ( P `  M
)  e.  RR  /\  ( P `  ( k  +  1 ) )  e.  RR )  -> 
( t  e.  ( ( P `  M
) [,] ( P `
 ( k  +  1 ) ) )  ->  t  e.  RR ) )
244241, 237, 243sylc 61 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N )  /\  t  e.  ( ( P `  M
) [,] ( P `
 ( k  +  1 ) ) ) )  ->  t  e.  RR )
2451243adant3 1050 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N )  /\  t  e.  ( ( P `  M
) [,] ( P `
 ( k  +  1 ) ) ) )  ->  ( P `  ( k  +  1 ) )  e.  RR )
246 elfz1 11815 . . . . . . . . . . . . . 14  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( N  e.  ( M ... N )  <-> 
( N  e.  ZZ  /\  M  <_  N  /\  N  <_  N ) ) )
2478, 3, 246syl2anc 673 . . . . . . . . . . . . 13  |-  ( ph  ->  ( N  e.  ( M ... N )  <-> 
( N  e.  ZZ  /\  M  <_  N  /\  N  <_  N ) ) )
2483, 63, 7, 247mpbir3and 1213 . . . . . . . . . . . 12  |-  ( ph  ->  N  e.  ( M ... N ) )
249248ancli 560 . . . . . . . . . . 11  |-  ( ph  ->  ( ph  /\  N  e.  ( M ... N
) ) )
250 eleq1 2537 . . . . . . . . . . . . . 14  |-  ( i  =  N  ->  (
i  e.  ( M ... N )  <->  N  e.  ( M ... N ) ) )
251250anbi2d 718 . . . . . . . . . . . . 13  |-  ( i  =  N  ->  (
( ph  /\  i  e.  ( M ... N
) )  <->  ( ph  /\  N  e.  ( M ... N ) ) ) )
252 fveq2 5879 . . . . . . . . . . . . . 14  |-  ( i  =  N  ->  ( P `  i )  =  ( P `  N ) )
253252eleq1d 2533 . . . . . . . . . . . . 13  |-  ( i  =  N  ->  (
( P `  i
)  e.  RR  <->  ( P `  N )  e.  RR ) )
254251, 253imbi12d 327 . . . . . . . . . . . 12  |-  ( i  =  N  ->  (
( ( ph  /\  i  e.  ( M ... N ) )  -> 
( P `  i
)  e.  RR )  <-> 
( ( ph  /\  N  e.  ( M ... N ) )  -> 
( P `  N
)  e.  RR ) ) )
255254, 72vtoclg 3093 . . . . . . . . . . 11  |-  ( N  e.  ZZ  ->  (
( ph  /\  N  e.  ( M ... N
) )  ->  ( P `  N )  e.  RR ) )
2563, 249, 255sylc 61 . . . . . . . . . 10  |-  ( ph  ->  ( P `  N
)  e.  RR )
2572563ad2ant1 1051 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N )  /\  t  e.  ( ( P `  M
) [,] ( P `
 ( k  +  1 ) ) ) )  ->  ( P `  N )  e.  RR )
258 elicc1 11705 . . . . . . . . . . . 12  |-  ( ( ( P `  M
)  e.  RR*  /\  ( P `  ( k  +  1 ) )  e.  RR* )  ->  (
t  e.  ( ( P `  M ) [,] ( P `  ( k  +  1 ) ) )  <->  ( t  e.  RR*  /\  ( P `
 M )  <_ 
t  /\  t  <_  ( P `  ( k  +  1 ) ) ) ) )
259235, 236, 258syl2anc 673 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N )  /\  t  e.  ( ( P `  M
) [,] ( P `
 ( k  +  1 ) ) ) )  ->  ( t  e.  ( ( P `  M ) [,] ( P `  ( k  +  1 ) ) )  <->  ( t  e. 
RR*  /\  ( P `  M )  <_  t  /\  t  <_  ( P `
 ( k  +  1 ) ) ) ) )
260237, 259mpbid 215 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N )  /\  t  e.  ( ( P `  M
) [,] ( P `
 ( k  +  1 ) ) ) )  ->  ( t  e.  RR*  /\  ( P `
 M )  <_ 
t  /\  t  <_  ( P `  ( k  +  1 ) ) ) )
261260simp3d 1044 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N )  /\  t  e.  ( ( P `  M
) [,] ( P `
 ( k  +  1 ) ) ) )  ->  t  <_  ( P `  ( k  +  1 ) ) )
262 elfzop1le2 37592 . . . . . . . . . . . . 13  |-  ( k  e.  ( ( M  +  1 )..^ N
)  ->  ( k  +  1 )  <_  N )
26378peano2zd 11066 . . . . . . . . . . . . . 14  |-  ( k  e.  ( ( M  +  1 )..^ N
)  ->  ( k  +  1 )  e.  ZZ )
264 eluz 11196 . . . . . . . . . . . . . 14  |-  ( ( ( k  +  1 )  e.  ZZ  /\  N  e.  ZZ )  ->  ( N  e.  (
ZZ>= `  ( k  +  1 ) )  <->  ( k  +  1 )  <_  N ) )
265263, 161, 264syl2anc 673 . . . . . . . . . . . . 13  |-  ( k  e.  ( ( M  +  1 )..^ N
)  ->  ( N  e.  ( ZZ>= `  ( k  +  1 ) )  <-> 
( k  +  1 )  <_  N )
)
266262, 265mpbird 240 . . . . . . . . . . . 12  |-  ( k  e.  ( ( M  +  1 )..^ N
)  ->  N  e.  ( ZZ>= `  ( k  +  1 ) ) )
267266adantl 473 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  N  e.  ( ZZ>= `  ( k  +  1 ) ) )
268 simpll 768 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( ( k  +  1 ) ... N
) )  ->  ph )
269 elfzelz 11826 . . . . . . . . . . . . . 14  |-  ( i  e.  ( ( k  +  1 ) ... N )  ->  i  e.  ZZ )
270269adantl 473 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( ( k  +  1 ) ... N
) )  ->  i  e.  ZZ )
271268, 35syl 17 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( ( k  +  1 ) ... N
) )  ->  M  e.  RR )
272270zred 11063 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( ( k  +  1 ) ... N
) )  ->  i  e.  RR )
27381adantr 472 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( ( k  +  1 ) ... N
) )  ->  k  e.  RR )
27486adantr 472 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( ( k  +  1 ) ... N
) )  ->  M  <  k )
275158adantr 472 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  ( ( M  +  1 )..^ N )  /\  i  e.  ( ( k  +  1 ) ... N
) )  ->  k  e.  RR )
276 1red 9676 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  ( ( M  +  1 )..^ N )  /\  i  e.  ( ( k  +  1 ) ... N
) )  ->  1  e.  RR )
277275, 276readdcld 9688 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  ( ( M  +  1 )..^ N )  /\  i  e.  ( ( k  +  1 ) ... N
) )  ->  (
k  +  1 )  e.  RR )
278269zred 11063 . . . . . . . . . . . . . . . . . 18  |-  ( i  e.  ( ( k  +  1 ) ... N )  ->  i  e.  RR )
279278adantl 473 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  ( ( M  +  1 )..^ N )  /\  i  e.  ( ( k  +  1 ) ... N
) )  ->  i  e.  RR )
280275ltp1d 10559 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  ( ( M  +  1 )..^ N )  /\  i  e.  ( ( k  +  1 ) ... N
) )  ->  k  <  ( k  +  1 ) )
281 elfzle1 11828 . . . . . . . . . . . . . . . . . 18  |-  ( i  e.  ( ( k  +  1 ) ... N )  ->  (
k  +  1 )  <_  i )
282281adantl 473 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  ( ( M  +  1 )..^ N )  /\  i  e.  ( ( k  +  1 ) ... N
) )  ->  (
k  +  1 )  <_  i )
283275, 277, 279, 280, 282ltletrd 9812 . . . . . . . . . . . . . . . 16  |-  ( ( k  e.  ( ( M  +  1 )..^ N )  /\  i  e.  ( ( k  +  1 ) ... N
) )  ->  k  <  i )
284283adantll 728 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( ( k  +  1 ) ... N
) )  ->  k  <  i )
285271, 273, 272, 274, 284lttrd 9813 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( ( k  +  1 ) ... N
) )  ->  M  <  i )
286271, 272, 285ltled 9800 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( ( k  +  1 ) ... N
) )  ->  M  <_  i )
287 elfzle2 11829 . . . . . . . . . . . . . 14  |-  ( i  e.  ( ( k  +  1 ) ... N )  ->  i  <_  N )
288287adantl 473 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( ( k  +  1 ) ... N
) )  ->  i  <_  N )
289268, 92, 1423syl 18 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( ( k  +  1 ) ... N
) )  ->  (
i  e.  ( M ... N )  <->  ( i  e.  ZZ  /\  M  <_ 
i  /\  i  <_  N ) ) )
290270, 286, 288, 289mpbir3and 1213 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( ( k  +  1 ) ... N
) )  ->  i  e.  ( M ... N
) )
291268, 290, 72syl2anc 673 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( ( k  +  1 ) ... N
) )  ->  ( P `  i )  e.  RR )
292 simpll 768 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  ph )
293 elfzelz 11826 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( ( k  +  1 ) ... ( N  -  1 ) )  ->  i  e.  ZZ )
294293adantl 473 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  i  e.  ZZ )
295292, 35syl 17 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  M  e.  RR )
296294zred 11063 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  i  e.  RR )
29781adantr 472 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  k  e.  RR )
29886adantr 472 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  M  <  k )
299158adantr 472 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  ( ( M  +  1 )..^ N )  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  k  e.  RR )
300 1red 9676 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  ( ( M  +  1 )..^ N )  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  1  e.  RR )
301299, 300readdcld 9688 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  ( ( M  +  1 )..^ N )  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  (
k  +  1 )  e.  RR )
302293zred 11063 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  ( ( k  +  1 ) ... ( N  -  1 ) )  ->  i  e.  RR )
303302adantl 473 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  ( ( M  +  1 )..^ N )  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  i  e.  RR )
304299ltp1d 10559 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  ( ( M  +  1 )..^ N )  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  k  <  ( k  +  1 ) )
305 elfzle1 11828 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  ( ( k  +  1 ) ... ( N  -  1 ) )  ->  (
k  +  1 )  <_  i )
306305adantl 473 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  ( ( M  +  1 )..^ N )  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  (
k  +  1 )  <_  i )
307299, 301, 303, 304, 306ltletrd 9812 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  ( ( M  +  1 )..^ N )  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  k  <  i )
308307adantll 728 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  k  <  i )
309295, 297, 296, 298, 308lttrd 9813 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  M  <  i )
310295, 296, 309ltled 9800 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  M  <_  i )
311302adantl 473 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  i  e.  RR )
3126adantr 472 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  N  e.  RR )
313 1red 9676 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  1  e.  RR )
314312, 313resubcld 10068 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  ( N  -  1 )  e.  RR )
315 elfzle2 11829 . . . . . . . . . . . . . . . . . 18  |-  ( i  e.  ( ( k  +  1 ) ... ( N  -  1 ) )  ->  i  <_  ( N  -  1 ) )
316315adantl 473 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  i  <_  ( N  -  1 ) )
317312ltm1d 10561 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  ( N  -  1 )  <  N )
318311, 314, 312, 316, 317lelttrd 9810 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  i  <  N )
319311, 312, 318ltled 9800 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  i  <_  N )
320319adantlr 729 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  i  <_  N )
321292, 92, 1423syl 18 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  (
i  e.  ( M ... N )  <->  ( i  e.  ZZ  /\  M  <_ 
i  /\  i  <_  N ) ) )
322294, 310, 320, 321mpbir3and 1213 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  i  e.  ( M ... N
) )
323292, 322, 72syl2anc 673 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  ( P `  i )  e.  RR )
324294peano2zd 11066 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  (
i  +  1 )  e.  ZZ )
325324zred 11063 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  (
i  +  1 )  e.  RR )
326303, 300readdcld 9688 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  ( ( M  +  1 )..^ N )  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  (
i  +  1 )  e.  RR )
327299, 303, 307ltled 9800 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  ( ( M  +  1 )..^ N )  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  k  <_  i )
328299, 303, 300, 327leadd1dd 10248 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  ( ( M  +  1 )..^ N )  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  (
k  +  1 )  <_  ( i  +  1 ) )
329299, 301, 326, 304, 328ltletrd 9812 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  ( ( M  +  1 )..^ N )  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  k  <  ( i  +  1 ) )
330329adantll 728 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  k  <  ( i  +  1 ) )
331295, 297, 325, 298, 330lttrd 9813 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  M  <  ( i  +  1 ) )
332295, 325, 331ltled 9800 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  M  <_  ( i  +  1 ) )
333293, 3, 182syl2anr 486 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  (
i  <  N  <->  ( i  +  1 )  <_  N ) )
334318, 333mpbid 215 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  (
i  +  1 )  <_  N )
335334adantlr 729 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  (
i  +  1 )  <_  N )
336292, 92, 1853syl 18 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  (
( i  +  1 )  e.  ( M ... N )  <->  ( (
i  +  1 )  e.  ZZ  /\  M  <_  ( i  +  1 )  /\  ( i  +  1 )  <_  N ) ) )
337324, 332, 335, 336mpbir3and 1213 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  (
i  +  1 )  e.  ( M ... N ) )
338292, 337jca 541 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  ( ph  /\  ( i  +  1 )  e.  ( M ... N ) ) )
339337, 338, 194sylc 61 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  ( P `  ( i  +  1 ) )  e.  RR )
340292, 8syl 17 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  M  e.  ZZ )
341 eluz 11196 . . . . . . . . . . . . . . . 16  |-  ( ( M  e.  ZZ  /\  i  e.  ZZ )  ->  ( i  e.  (
ZZ>= `  M )  <->  M  <_  i ) )
342340, 294, 341syl2anc 673 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  (
i  e.  ( ZZ>= `  M )  <->  M  <_  i ) )
343310, 342mpbird 240 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  i  e.  ( ZZ>= `  M )
)
344292, 1, 23syl 18 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  N  e.  ZZ )
345318adantlr 729 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  i  <  N )
346343, 344, 345, 198syl3anbrc 1214 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  i  e.  ( M..^ N ) )
347292, 346, 200syl2anc 673 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  ( P `  i )  <  ( P `  (
i  +  1 ) ) )
348323, 339, 347ltled 9800 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  /\  i  e.  ( ( k  +  1 ) ... ( N  -  1 ) ) )  ->  ( P `  i )  <_  ( P `  (
i  +  1 ) ) )
349267, 291, 348monoord 12281 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  ( P `  ( k  +  1 ) )  <_  ( P `  N )
)
3503493adant3 1050 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N )  /\  t  e.  ( ( P `  M
) [,] ( P `
 ( k  +  1 ) ) ) )  ->  ( P `  ( k  +  1 ) )  <_  ( P `  N )
)
351244, 245, 257, 261, 350letrd 9809 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N )  /\  t  e.  ( ( P `  M
) [,] ( P `
 ( k  +  1 ) ) ) )  ->  t  <_  ( P `  N ) )
352257rexrd 9708 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N )  /\  t  e.  ( ( P `  M
) [,] ( P `
 ( k  +  1 ) ) ) )  ->  ( P `  N )  e.  RR* )
353 elicc1 11705 . . . . . . . . 9  |-  ( ( ( P `  M
)  e.  RR*  /\  ( P `  N )  e.  RR* )  ->  (
t  e.  ( ( P `  M ) [,] ( P `  N ) )  <->  ( t  e.  RR*  /\  ( P `
 M )  <_ 
t  /\  t  <_  ( P `  N ) ) ) )
354235, 352, 353syl2anc 673 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N )  /\  t  e.  ( ( P `  M
) [,] ( P `
 ( k  +  1 ) ) ) )  ->  ( t  e.  ( ( P `  M ) [,] ( P `  N )
)  <->  ( t  e. 
RR*  /\  ( P `  M )  <_  t  /\  t  <_  ( P `
 N ) ) ) )
355233, 239, 351, 354mpbir3and 1213 . . . . . . 7  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N )  /\  t  e.  ( ( P `  M
) [,] ( P `
 ( k  +  1 ) ) ) )  ->  t  e.  ( ( P `  M ) [,] ( P `  N )
) )
356 iblspltprt.6 . . . . . . 7  |-  ( (
ph  /\  t  e.  ( ( P `  M ) [,] ( P `  N )
) )  ->  A  e.  CC )
357231, 355, 356syl2anc 673 . . . . . 6  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N )  /\  t  e.  ( ( P `  M
) [,] ( P `
 ( k  +  1 ) ) ) )  ->  A  e.  CC )
358228, 229, 230, 357syl3anc 1292 . . . . 5  |-  ( ( ( k  e.  ( ( M  +  1 )..^ N )  /\  ( ph  ->  ( t  e.  ( ( P `  M ) [,] ( P `  k )
)  |->  A )  e.  L^1 )  /\  ph )  /\  t  e.  ( ( P `  M ) [,] ( P `  ( k  +  1 ) ) ) )  ->  A  e.  CC )
359 simp2 1031 . . . . . 6  |-  ( ( k  e.  ( ( M  +  1 )..^ N )  /\  ( ph  ->  ( t  e.  ( ( P `  M ) [,] ( P `  k )
)  |->  A )  e.  L^1 )  /\  ph )  ->  ( ph  ->  ( t  e.  ( ( P `  M
) [,] ( P `
 k ) ) 
|->  A )  e.  L^1 ) )
36060, 359mpd 15 . . . . 5  |-  ( ( k  e.  ( ( M  +  1 )..^ N )  /\  ( ph  ->  ( t  e.  ( ( P `  M ) [,] ( P `  k )
)  |->  A )  e.  L^1 )  /\  ph )  ->  ( t  e.  ( ( P `  M ) [,] ( P `  k )
)  |->  A )  e.  L^1 )
36160, 61jca 541 . . . . . 6  |-  ( ( k  e.  ( ( M  +  1 )..^ N )  /\  ( ph  ->  ( t  e.  ( ( P `  M ) [,] ( P `  k )
)  |->  A )  e.  L^1 )  /\  ph )  ->  ( ph  /\  k  e.  ( ( M  +  1 )..^ N ) ) )
36277, 206jca 541 . . . . . 6  |-  ( (
ph  /\  k  e.  ( ( M  + 
1 )..^ N ) )  ->  ( ph  /\  k  e.  ( M..^ N ) ) )
36399, 210oveq12d 6326 . . . . . . . . . 10  |-  ( i  =  k  ->  (
( P `  i
) [,] ( P `
 ( i  +  1 ) ) )  =  ( ( P `
 k ) [,] ( P `  (
k  +  1 ) ) ) )
364363mpteq1d 4477 . . . . . . . . 9  |-  ( i  =  k  ->  (
t  e.  ( ( P `  i ) [,] ( P `  ( i  +  1 ) ) )  |->  A )  =  ( t  e.  ( ( P `
 k ) [,] ( P `  (
k  +  1 ) ) )  |->  A ) )
365364eleq1d 2533 . . . . . . . 8  |-  ( i  =  k  ->  (
( t  e.  ( ( P `  i
) [,] ( P `
 ( i  +  1 ) ) ) 
|->  A )  e.  L^1 
<->  ( t  e.  ( ( P `  k
) [,] ( P `
 ( k  +  1 ) ) ) 
|->  A )  e.  L^1 ) )
366208, 365imbi12d 327 . . . . . . 7  |-  ( i  =  k  ->  (
( ( ph  /\  i  e.  ( M..^ N ) )  -> 
( t  e.  ( ( P `  i
) [,] ( P `
 ( i  +  1 ) ) ) 
|->  A )  e.  L^1 )  <->  ( ( ph  /\  k  e.  ( M..^ N ) )  -> 
( t  e.  ( ( P `  k
) [,] ( P `
 ( k  +  1 ) ) ) 
|->  A )  e.  L^1 ) ) )
367366, 49chvarv 2120 . . . . . 6  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( t  e.  ( ( P `  k ) [,] ( P `  ( k  +  1 ) ) )  |->  A )  e.  L^1 )
368361, 362, 3673syl 18 . . . . 5  |-  ( ( k  e.  ( ( M  +  1 )..^ N )  /\  ( ph  ->  ( t  e.  ( ( P `  M ) [,] ( P `  k )
)  |->  A )  e.  L^1 )  /\  ph )  ->  ( t  e.  ( ( P `  k ) [,] ( P `  ( k  +  1 ) ) )  |->  A )  e.  L^1 )
36959, 222, 227, 358, 360, 368iblsplitf 37944 . . . 4  |-  ( ( k  e.  ( ( M  +  1 )..^ N )  /\  ( ph  ->  ( t  e.  ( ( P `  M ) [,] ( P `  k )
)  |->  A )  e.  L^1 )  /\  ph )  ->  ( t  e.  ( ( P `  M ) [,] ( P `  ( k  +  1 ) ) )  |->  A )  e.  L^1 )
3703693exp 1230 . . 3  |-  ( k  e.  ( ( M  +  1 )..^ N
)  ->  ( ( ph  ->  ( t  e.  ( ( P `  M ) [,] ( P `  k )
)  |->  A )  e.  L^1 )  -> 
( ph  ->  ( t  e.  ( ( P `
 M ) [,] ( P `  (
k  +  1 ) ) )  |->  A )  e.  L^1 ) ) )
37117, 22, 27, 32, 53, 370fzind2 12054 . 2  |-  ( N  e.  ( ( M  +  1 ) ... N )  ->  ( ph  ->  ( t  e.  ( ( P `  M ) [,] ( P `  N )
)  |->  A )  e.  L^1 ) )
37212, 371mpcom 36 1  |-  ( ph  ->  ( t  e.  ( ( P `  M
) [,] ( P `
 N ) ) 
|->  A )  e.  L^1 )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 376    /\ w3a 1007    = wceq 1452   F/wnf 1675    e. wcel 1904    u. cun 3388    i^i cin 3389   {csn 3959   class class class wbr 4395    |-> cmpt 4454   ` cfv 5589  (class class class)co 6308   CCcc 9555   RRcr 9556   0cc0 9557   1c1 9558    + caddc 9560   RR*cxr 9692    < clt 9693    <_ cle 9694    - cmin 9880   ZZcz 10961   ZZ>=cuz 11182   [,]cicc 11663   ...cfz 11810  ..^cfzo 11942   vol*covol 22491   L^1cibl 22654
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-inf2 8164  ax-cnex 9613  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0 9634  ax-pre-sup 9635  ax-addf 9636
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-fal 1458  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-disj 4367  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-se 4799  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-isom 5598  df-riota 6270  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-of 6550  df-ofr 6551  df-om 6712  df-1st 6812  df-2nd 6813  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-2o 7201  df-oadd 7204  df-er 7381  df-map 7492  df-pm 7493  df-en 7588  df-dom 7589  df-sdom 7590  df-fin 7591  df-fi 7943  df-sup 7974  df-inf 7975  df-oi 8043  df-card 8391  df-cda 8616  df-pnf 9695  df-mnf 9696  df-xr 9697  df-ltxr 9698  df-le 9699  df-sub 9882  df-neg 9883  df-div 10292  df-nn 10632  df-2 10690  df-3 10691  df-n0 10894  df-z 10962  df-uz 11183  df-q 11288  df-rp 11326  df-xneg 11432  df-xadd 11433  df-xmul 11434  df-ioo 11664  df-ico 11666  df-icc 11667  df-fz 11811  df-fzo 11943  df-fl 12061  df-seq 12252  df-exp 12311  df-hash 12554  df-cj 13239  df-re 13240  df-im 13241  df-sqrt 13375  df-abs 13376  df-clim 13629  df-sum 13830  df-rest 15399  df-topgen 15420  df-psmet 19039  df-xmet 19040  df-met 19041  df-bl 19042  df-mopn 19043  df-top 19998  df-bases 19999  df-topon 20000  df-cmp 20479  df-ovol 22494  df-vol 22496  df-mbf 22656  df-itg1 22657  df-itg2 22658  df-ibl 22659
This theorem is referenced by:  itgspltprt  37953  fourierdlem69  38151
  Copyright terms: Public domain W3C validator