Metamath Proof Explorer

Theorem iblspltprt

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)

Ref Expression
Hypotheses 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 iblspltprt 
|- ( ph -> ( t e. ( ( P ` M ) [,] ( P ` N ) ) |-> A ) e. L^1 )

Proof

Step Hyp Ref Expression
1 iblspltprt.1 
 |-  F/ t ph
2 iblspltprt.2 
 |-  ( ph -> M e. ZZ )
3 iblspltprt.3 
 |-  ( ph -> N e. ( ZZ>= ` ( M + 1 ) ) )
4 iblspltprt.4 
 |-  ( ( ph /\ i e. ( M ... N ) ) -> ( P ` i ) e. RR )
5 iblspltprt.5 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( P ` i ) < ( P ` ( i + 1 ) ) )
6 iblspltprt.6 
 |-  ( ( ph /\ t e. ( ( P ` M ) [,] ( P ` N ) ) ) -> A e. CC )
7 iblspltprt.7 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) |-> A ) e. L^1 )
8 2 peano2zd 
 |-  ( ph -> ( M + 1 ) e. ZZ )
9 eluzelz 
 |-  ( N e. ( ZZ>= ` ( M + 1 ) ) -> N e. ZZ )
10 3 9 syl 
 |-  ( ph -> N e. ZZ )
11 eluzle 
 |-  ( N e. ( ZZ>= ` ( M + 1 ) ) -> ( M + 1 ) <_ N )
12 3 11 syl 
 |-  ( ph -> ( M + 1 ) <_ N )
13 10 zred 
 |-  ( ph -> N e. RR )
14 13 leidd 
 |-  ( ph -> N <_ N )
15 8 10 10 12 14 elfzd 
 |-  ( ph -> N e. ( ( M + 1 ) ... N ) )
16 fveq2 
 |-  ( j = ( M + 1 ) -> ( P ` j ) = ( P ` ( M + 1 ) ) )
17 16 oveq2d 
 |-  ( j = ( M + 1 ) -> ( ( P ` M ) [,] ( P ` j ) ) = ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) )
18 17 mpteq1d 
 |-  ( j = ( M + 1 ) -> ( t e. ( ( P ` M ) [,] ( P ` j ) ) |-> A ) = ( t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) |-> A ) )
19 18 eleq1d 
 |-  ( j = ( M + 1 ) -> ( ( t e. ( ( P ` M ) [,] ( P ` j ) ) |-> A ) e. L^1 <-> ( t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) |-> A ) e. L^1 ) )
20 19 imbi2d 
 |-  ( 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 ) ) )
21 fveq2 
 |-  ( j = k -> ( P ` j ) = ( P ` k ) )
22 21 oveq2d 
 |-  ( j = k -> ( ( P ` M ) [,] ( P ` j ) ) = ( ( P ` M ) [,] ( P ` k ) ) )
23 22 mpteq1d 
 |-  ( j = k -> ( t e. ( ( P ` M ) [,] ( P ` j ) ) |-> A ) = ( t e. ( ( P ` M ) [,] ( P ` k ) ) |-> A ) )
24 23 eleq1d 
 |-  ( j = k -> ( ( t e. ( ( P ` M ) [,] ( P ` j ) ) |-> A ) e. L^1 <-> ( t e. ( ( P ` M ) [,] ( P ` k ) ) |-> A ) e. L^1 ) )
25 24 imbi2d 
 |-  ( j = k -> ( ( ph -> ( t e. ( ( P ` M ) [,] ( P ` j ) ) |-> A ) e. L^1 ) <-> ( ph -> ( t e. ( ( P ` M ) [,] ( P ` k ) ) |-> A ) e. L^1 ) ) )
26 fveq2 
 |-  ( j = ( k + 1 ) -> ( P ` j ) = ( P ` ( k + 1 ) ) )
27 26 oveq2d 
 |-  ( j = ( k + 1 ) -> ( ( P ` M ) [,] ( P ` j ) ) = ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) )
28 27 mpteq1d 
 |-  ( j = ( k + 1 ) -> ( t e. ( ( P ` M ) [,] ( P ` j ) ) |-> A ) = ( t e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) |-> A ) )
29 28 eleq1d 
 |-  ( j = ( k + 1 ) -> ( ( t e. ( ( P ` M ) [,] ( P ` j ) ) |-> A ) e. L^1 <-> ( t e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) |-> A ) e. L^1 ) )
30 29 imbi2d 
 |-  ( 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 ) ) )
31 fveq2 
 |-  ( j = N -> ( P ` j ) = ( P ` N ) )
32 31 oveq2d 
 |-  ( j = N -> ( ( P ` M ) [,] ( P ` j ) ) = ( ( P ` M ) [,] ( P ` N ) ) )
33 32 mpteq1d 
 |-  ( j = N -> ( t e. ( ( P ` M ) [,] ( P ` j ) ) |-> A ) = ( t e. ( ( P ` M ) [,] ( P ` N ) ) |-> A ) )
34 33 eleq1d 
 |-  ( j = N -> ( ( t e. ( ( P ` M ) [,] ( P ` j ) ) |-> A ) e. L^1 <-> ( t e. ( ( P ` M ) [,] ( P ` N ) ) |-> A ) e. L^1 ) )
35 34 imbi2d 
 |-  ( j = N -> ( ( ph -> ( t e. ( ( P ` M ) [,] ( P ` j ) ) |-> A ) e. L^1 ) <-> ( ph -> ( t e. ( ( P ` M ) [,] ( P ` N ) ) |-> A ) e. L^1 ) ) )
36 uzid 
 |-  ( M e. ZZ -> M e. ( ZZ>= ` M ) )
37 2 36 syl 
 |-  ( ph -> M e. ( ZZ>= ` M ) )
38 2 zred 
 |-  ( ph -> M e. RR )
39 1red 
 |-  ( ph -> 1 e. RR )
40 38 39 readdcld 
 |-  ( ph -> ( M + 1 ) e. RR )
41 38 ltp1d 
 |-  ( ph -> M < ( M + 1 ) )
42 38 40 13 41 12 ltletrd 
 |-  ( ph -> M < N )
43 elfzo2 
 |-  ( M e. ( M ..^ N ) <-> ( M e. ( ZZ>= ` M ) /\ N e. ZZ /\ M < N ) )
44 37 10 42 43 syl3anbrc 
 |-  ( ph -> M e. ( M ..^ N ) )
45 fveq2 
 |-  ( i = M -> ( P ` i ) = ( P ` M ) )
46 fvoveq1 
 |-  ( i = M -> ( P ` ( i + 1 ) ) = ( P ` ( M + 1 ) ) )
47 45 46 oveq12d 
 |-  ( i = M -> ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) = ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) )
48 47 mpteq1d 
 |-  ( i = M -> ( t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) |-> A ) = ( t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) |-> A ) )
49 48 eleq1d 
 |-  ( i = M -> ( ( t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) |-> A ) e. L^1 <-> ( t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) |-> A ) e. L^1 ) )
50 49 imbi2d 
 |-  ( 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 ) ) )
51 7 expcom 
 |-  ( i e. ( M ..^ N ) -> ( ph -> ( t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) |-> A ) e. L^1 ) )
52 50 51 vtoclga 
 |-  ( M e. ( M ..^ N ) -> ( ph -> ( t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) |-> A ) e. L^1 ) )
53 44 52 mpcom 
 |-  ( ph -> ( t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) |-> A ) e. L^1 )
54 53 a1i 
 |-  ( N e. ( ZZ>= ` ( M + 1 ) ) -> ( ph -> ( t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) |-> A ) e. L^1 ) )
55 nfv 
 |-  F/ t k e. ( ( M + 1 ) ..^ N )
56 nfmpt1 
 |-  F/_ t ( t e. ( ( P ` M ) [,] ( P ` k ) ) |-> A )
57 56 nfel1 
 |-  F/ t ( t e. ( ( P ` M ) [,] ( P ` k ) ) |-> A ) e. L^1
58 1 57 nfim 
 |-  F/ t ( ph -> ( t e. ( ( P ` M ) [,] ( P ` k ) ) |-> A ) e. L^1 )
59 55 58 1 nf3an 
 |-  F/ t ( k e. ( ( M + 1 ) ..^ N ) /\ ( ph -> ( t e. ( ( P ` M ) [,] ( P ` k ) ) |-> A ) e. L^1 ) /\ ph )
60 simp3 
 |-  ( ( k e. ( ( M + 1 ) ..^ N ) /\ ( ph -> ( t e. ( ( P ` M ) [,] ( P ` k ) ) |-> A ) e. L^1 ) /\ ph ) -> ph )
61 simp1 
 |-  ( ( k e. ( ( M + 1 ) ..^ N ) /\ ( ph -> ( t e. ( ( P ` M ) [,] ( P ` k ) ) |-> A ) e. L^1 ) /\ ph ) -> k e. ( ( M + 1 ) ..^ N ) )
62 38 leidd 
 |-  ( ph -> M <_ M )
63 38 13 42 ltled 
 |-  ( ph -> M <_ N )
64 2 10 2 62 63 elfzd 
 |-  ( ph -> M e. ( M ... N ) )
65 64 ancli 
 |-  ( ph -> ( ph /\ M e. ( M ... N ) ) )
66 eleq1 
 |-  ( i = M -> ( i e. ( M ... N ) <-> M e. ( M ... N ) ) )
67 66 anbi2d 
 |-  ( i = M -> ( ( ph /\ i e. ( M ... N ) ) <-> ( ph /\ M e. ( M ... N ) ) ) )
68 45 eleq1d 
 |-  ( i = M -> ( ( P ` i ) e. RR <-> ( P ` M ) e. RR ) )
69 67 68 imbi12d 
 |-  ( i = M -> ( ( ( ph /\ i e. ( M ... N ) ) -> ( P ` i ) e. RR ) <-> ( ( ph /\ M e. ( M ... N ) ) -> ( P ` M ) e. RR ) ) )
70 69 4 vtoclg 
 |-  ( M e. ( M ... N ) -> ( ( ph /\ M e. ( M ... N ) ) -> ( P ` M ) e. RR ) )
71 64 65 70 sylc 
 |-  ( ph -> ( P ` M ) e. RR )
72 71 adantr 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( P ` M ) e. RR )
73 72 rexrd 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( P ` M ) e. RR* )
74 simpl 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ph )
75 elfzoelz 
 |-  ( k e. ( ( M + 1 ) ..^ N ) -> k e. ZZ )
76 75 adantl 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> k e. ZZ )
77 38 adantr 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> M e. RR )
78 76 zred 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> k e. RR )
79 40 adantr 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( M + 1 ) e. RR )
80 41 adantr 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> M < ( M + 1 ) )
81 elfzole1 
 |-  ( k e. ( ( M + 1 ) ..^ N ) -> ( M + 1 ) <_ k )
82 81 adantl 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( M + 1 ) <_ k )
83 77 79 78 80 82 ltletrd 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> M < k )
84 77 78 83 ltled 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> M <_ k )
85 13 adantr 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> N e. RR )
86 elfzolt2 
 |-  ( k e. ( ( M + 1 ) ..^ N ) -> k < N )
87 86 adantl 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> k < N )
88 78 85 87 ltled 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> k <_ N )
89 2 10 jca 
 |-  ( ph -> ( M e. ZZ /\ N e. ZZ ) )
90 89 adantr 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( M e. ZZ /\ N e. ZZ ) )
91 elfz1 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( k e. ( M ... N ) <-> ( k e. ZZ /\ M <_ k /\ k <_ N ) ) )
92 90 91 syl 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( k e. ( M ... N ) <-> ( k e. ZZ /\ M <_ k /\ k <_ N ) ) )
93 76 84 88 92 mpbir3and 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> k e. ( M ... N ) )
94 eleq1 
 |-  ( i = k -> ( i e. ( M ... N ) <-> k e. ( M ... N ) ) )
95 94 anbi2d 
 |-  ( i = k -> ( ( ph /\ i e. ( M ... N ) ) <-> ( ph /\ k e. ( M ... N ) ) ) )
96 fveq2 
 |-  ( i = k -> ( P ` i ) = ( P ` k ) )
97 96 eleq1d 
 |-  ( i = k -> ( ( P ` i ) e. RR <-> ( P ` k ) e. RR ) )
98 95 97 imbi12d 
 |-  ( i = k -> ( ( ( ph /\ i e. ( M ... N ) ) -> ( P ` i ) e. RR ) <-> ( ( ph /\ k e. ( M ... N ) ) -> ( P ` k ) e. RR ) ) )
99 98 4 chvarvv 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( P ` k ) e. RR )
100 74 93 99 syl2anc 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( P ` k ) e. RR )
101 100 rexrd 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( P ` k ) e. RR* )
102 76 peano2zd 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( k + 1 ) e. ZZ )
103 102 zred 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( k + 1 ) e. RR )
104 1red 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> 1 e. RR )
105 77 78 104 83 ltadd1dd 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( M + 1 ) < ( k + 1 ) )
106 77 79 103 80 105 lttrd 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> M < ( k + 1 ) )
107 77 103 106 ltled 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> M <_ ( k + 1 ) )
108 zltp1le 
 |-  ( ( k e. ZZ /\ N e. ZZ ) -> ( k < N <-> ( k + 1 ) <_ N ) )
109 75 10 108 syl2anr 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( k < N <-> ( k + 1 ) <_ N ) )
110 87 109 mpbid 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( k + 1 ) <_ N )
111 elfz1 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( k + 1 ) e. ( M ... N ) <-> ( ( k + 1 ) e. ZZ /\ M <_ ( k + 1 ) /\ ( k + 1 ) <_ N ) ) )
112 90 111 syl 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( ( k + 1 ) e. ( M ... N ) <-> ( ( k + 1 ) e. ZZ /\ M <_ ( k + 1 ) /\ ( k + 1 ) <_ N ) ) )
113 102 107 110 112 mpbir3and 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( k + 1 ) e. ( M ... N ) )
114 74 113 jca 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( ph /\ ( k + 1 ) e. ( M ... N ) ) )
115 eleq1 
 |-  ( i = ( k + 1 ) -> ( i e. ( M ... N ) <-> ( k + 1 ) e. ( M ... N ) ) )
116 115 anbi2d 
 |-  ( i = ( k + 1 ) -> ( ( ph /\ i e. ( M ... N ) ) <-> ( ph /\ ( k + 1 ) e. ( M ... N ) ) ) )
117 fveq2 
 |-  ( i = ( k + 1 ) -> ( P ` i ) = ( P ` ( k + 1 ) ) )
118 117 eleq1d 
 |-  ( i = ( k + 1 ) -> ( ( P ` i ) e. RR <-> ( P ` ( k + 1 ) ) e. RR ) )
119 116 118 imbi12d 
 |-  ( i = ( k + 1 ) -> ( ( ( ph /\ i e. ( M ... N ) ) -> ( P ` i ) e. RR ) <-> ( ( ph /\ ( k + 1 ) e. ( M ... N ) ) -> ( P ` ( k + 1 ) ) e. RR ) ) )
120 119 4 vtoclg 
 |-  ( ( k + 1 ) e. ( M ... N ) -> ( ( ph /\ ( k + 1 ) e. ( M ... N ) ) -> ( P ` ( k + 1 ) ) e. RR ) )
121 113 114 120 sylc 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( P ` ( k + 1 ) ) e. RR )
122 121 rexrd 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( P ` ( k + 1 ) ) e. RR* )
123 eluz 
 |-  ( ( M e. ZZ /\ k e. ZZ ) -> ( k e. ( ZZ>= ` M ) <-> M <_ k ) )
124 2 75 123 syl2an 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( k e. ( ZZ>= ` M ) <-> M <_ k ) )
125 84 124 mpbird 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> k e. ( ZZ>= ` M ) )
126 simpll 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> ph )
127 elfzelz 
 |-  ( i e. ( M ... k ) -> i e. ZZ )
128 127 adantl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> i e. ZZ )
129 elfzle1 
 |-  ( i e. ( M ... k ) -> M <_ i )
130 129 adantl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> M <_ i )
131 128 zred 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> i e. RR )
132 126 13 syl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> N e. RR )
133 78 adantr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> k e. RR )
134 elfzle2 
 |-  ( i e. ( M ... k ) -> i <_ k )
135 134 adantl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> i <_ k )
136 87 adantr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> k < N )
137 131 133 132 135 136 lelttrd 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> i < N )
138 131 132 137 ltled 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> i <_ N )
139 elfz1 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( i e. ( M ... N ) <-> ( i e. ZZ /\ M <_ i /\ i <_ N ) ) )
140 126 89 139 3syl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> ( i e. ( M ... N ) <-> ( i e. ZZ /\ M <_ i /\ i <_ N ) ) )
141 128 130 138 140 mpbir3and 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> i e. ( M ... N ) )
142 126 141 4 syl2anc 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> ( P ` i ) e. RR )
143 simpll 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> ph )
144 elfzelz 
 |-  ( i e. ( M ... ( k - 1 ) ) -> i e. ZZ )
145 144 adantl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> i e. ZZ )
146 elfzle1 
 |-  ( i e. ( M ... ( k - 1 ) ) -> M <_ i )
147 146 adantl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> M <_ i )
148 145 zred 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> i e. RR )
149 143 13 syl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> N e. RR )
150 78 adantr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> k e. RR )
151 1red 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> 1 e. RR )
152 150 151 resubcld 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> ( k - 1 ) e. RR )
153 elfzle2 
 |-  ( i e. ( M ... ( k - 1 ) ) -> i <_ ( k - 1 ) )
154 153 adantl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> i <_ ( k - 1 ) )
155 75 zred 
 |-  ( k e. ( ( M + 1 ) ..^ N ) -> k e. RR )
156 1red 
 |-  ( k e. ( ( M + 1 ) ..^ N ) -> 1 e. RR )
157 155 156 resubcld 
 |-  ( k e. ( ( M + 1 ) ..^ N ) -> ( k - 1 ) e. RR )
158 elfzoel2 
 |-  ( k e. ( ( M + 1 ) ..^ N ) -> N e. ZZ )
159 158 zred 
 |-  ( k e. ( ( M + 1 ) ..^ N ) -> N e. RR )
160 155 ltm1d 
 |-  ( k e. ( ( M + 1 ) ..^ N ) -> ( k - 1 ) < k )
161 157 155 159 160 86 lttrd 
 |-  ( k e. ( ( M + 1 ) ..^ N ) -> ( k - 1 ) < N )
162 161 ad2antlr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> ( k - 1 ) < N )
163 148 152 149 154 162 lelttrd 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> i < N )
164 148 149 163 ltled 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> i <_ N )
165 143 89 139 3syl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> ( i e. ( M ... N ) <-> ( i e. ZZ /\ M <_ i /\ i <_ N ) ) )
166 145 147 164 165 mpbir3and 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> i e. ( M ... N ) )
167 143 166 4 syl2anc 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> ( P ` i ) e. RR )
168 145 peano2zd 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> ( i + 1 ) e. ZZ )
169 elfzel1 
 |-  ( i e. ( M ... ( k - 1 ) ) -> M e. ZZ )
170 169 zred 
 |-  ( i e. ( M ... ( k - 1 ) ) -> M e. RR )
171 144 zred 
 |-  ( i e. ( M ... ( k - 1 ) ) -> i e. RR )
172 1red 
 |-  ( i e. ( M ... ( k - 1 ) ) -> 1 e. RR )
173 171 172 readdcld 
 |-  ( i e. ( M ... ( k - 1 ) ) -> ( i + 1 ) e. RR )
174 171 ltp1d 
 |-  ( i e. ( M ... ( k - 1 ) ) -> i < ( i + 1 ) )
175 170 171 173 146 174 lelttrd 
 |-  ( i e. ( M ... ( k - 1 ) ) -> M < ( i + 1 ) )
176 170 173 175 ltled 
 |-  ( i e. ( M ... ( k - 1 ) ) -> M <_ ( i + 1 ) )
177 176 adantl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> M <_ ( i + 1 ) )
178 143 3 9 3syl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> N e. ZZ )
179 zltp1le 
 |-  ( ( i e. ZZ /\ N e. ZZ ) -> ( i < N <-> ( i + 1 ) <_ N ) )
180 145 178 179 syl2anc 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> ( i < N <-> ( i + 1 ) <_ N ) )
181 163 180 mpbid 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> ( i + 1 ) <_ N )
182 elfz1 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( i + 1 ) e. ( M ... N ) <-> ( ( i + 1 ) e. ZZ /\ M <_ ( i + 1 ) /\ ( i + 1 ) <_ N ) ) )
183 143 89 182 3syl 
 |-  ( ( ( 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 ) ) )
184 168 177 181 183 mpbir3and 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> ( i + 1 ) e. ( M ... N ) )
185 143 184 jca 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> ( ph /\ ( i + 1 ) e. ( M ... N ) ) )
186 eleq1 
 |-  ( k = ( i + 1 ) -> ( k e. ( M ... N ) <-> ( i + 1 ) e. ( M ... N ) ) )
187 186 anbi2d 
 |-  ( k = ( i + 1 ) -> ( ( ph /\ k e. ( M ... N ) ) <-> ( ph /\ ( i + 1 ) e. ( M ... N ) ) ) )
188 fveq2 
 |-  ( k = ( i + 1 ) -> ( P ` k ) = ( P ` ( i + 1 ) ) )
189 188 eleq1d 
 |-  ( k = ( i + 1 ) -> ( ( P ` k ) e. RR <-> ( P ` ( i + 1 ) ) e. RR ) )
190 187 189 imbi12d 
 |-  ( k = ( i + 1 ) -> ( ( ( ph /\ k e. ( M ... N ) ) -> ( P ` k ) e. RR ) <-> ( ( ph /\ ( i + 1 ) e. ( M ... N ) ) -> ( P ` ( i + 1 ) ) e. RR ) ) )
191 190 99 vtoclg 
 |-  ( ( i + 1 ) e. ( M ... N ) -> ( ( ph /\ ( i + 1 ) e. ( M ... N ) ) -> ( P ` ( i + 1 ) ) e. RR ) )
192 184 185 191 sylc 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> ( P ` ( i + 1 ) ) e. RR )
193 elfzuz 
 |-  ( i e. ( M ... ( k - 1 ) ) -> i e. ( ZZ>= ` M ) )
194 193 adantl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> i e. ( ZZ>= ` M ) )
195 elfzo2 
 |-  ( i e. ( M ..^ N ) <-> ( i e. ( ZZ>= ` M ) /\ N e. ZZ /\ i < N ) )
196 194 178 163 195 syl3anbrc 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> i e. ( M ..^ N ) )
197 143 196 5 syl2anc 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> ( P ` i ) < ( P ` ( i + 1 ) ) )
198 167 192 197 ltled 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> ( P ` i ) <_ ( P ` ( i + 1 ) ) )
199 125 142 198 monoord 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( P ` M ) <_ ( P ` k ) )
200 158 adantl 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> N e. ZZ )
201 elfzo2 
 |-  ( k e. ( M ..^ N ) <-> ( k e. ( ZZ>= ` M ) /\ N e. ZZ /\ k < N ) )
202 125 200 87 201 syl3anbrc 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> k e. ( M ..^ N ) )
203 eleq1 
 |-  ( i = k -> ( i e. ( M ..^ N ) <-> k e. ( M ..^ N ) ) )
204 203 anbi2d 
 |-  ( i = k -> ( ( ph /\ i e. ( M ..^ N ) ) <-> ( ph /\ k e. ( M ..^ N ) ) ) )
205 fvoveq1 
 |-  ( i = k -> ( P ` ( i + 1 ) ) = ( P ` ( k + 1 ) ) )
206 96 205 breq12d 
 |-  ( i = k -> ( ( P ` i ) < ( P ` ( i + 1 ) ) <-> ( P ` k ) < ( P ` ( k + 1 ) ) ) )
207 204 206 imbi12d 
 |-  ( i = k -> ( ( ( ph /\ i e. ( M ..^ N ) ) -> ( P ` i ) < ( P ` ( i + 1 ) ) ) <-> ( ( ph /\ k e. ( M ..^ N ) ) -> ( P ` k ) < ( P ` ( k + 1 ) ) ) ) )
208 207 5 chvarvv 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( P ` k ) < ( P ` ( k + 1 ) ) )
209 74 202 208 syl2anc 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( P ` k ) < ( P ` ( k + 1 ) ) )
210 100 121 209 ltled 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( P ` k ) <_ ( P ` ( k + 1 ) ) )
211 iccintsng 
 |-  ( ( ( ( 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 ) } )
212 73 101 122 199 210 211 syl32anc 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( ( ( P ` M ) [,] ( P ` k ) ) i^i ( ( P ` k ) [,] ( P ` ( k + 1 ) ) ) ) = { ( P ` k ) } )
213 212 fveq2d 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( vol* ` ( ( ( P ` M ) [,] ( P ` k ) ) i^i ( ( P ` k ) [,] ( P ` ( k + 1 ) ) ) ) ) = ( vol* ` { ( P ` k ) } ) )
214 ovolsn 
 |-  ( ( P ` k ) e. RR -> ( vol* ` { ( P ` k ) } ) = 0 )
215 100 214 syl 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( vol* ` { ( P ` k ) } ) = 0 )
216 213 215 eqtrd 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( vol* ` ( ( ( P ` M ) [,] ( P ` k ) ) i^i ( ( P ` k ) [,] ( P ` ( k + 1 ) ) ) ) ) = 0 )
217 60 61 216 syl2anc 
 |-  ( ( 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 )
218 72 121 100 199 210 eliccd 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( P ` k ) e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) )
219 72 121 218 3jca 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( ( P ` M ) e. RR /\ ( P ` ( k + 1 ) ) e. RR /\ ( P ` k ) e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) ) )
220 60 61 219 syl2anc 
 |-  ( ( 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 ) ) ) ) )
221 iccsplit 
 |-  ( ( ( 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 ) ) ) ) )
222 220 221 syl 
 |-  ( ( 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 ) ) ) ) )
223 simpl3 
 |-  ( ( ( 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 )
224 simpl1 
 |-  ( ( ( 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 ) )
225 simpr 
 |-  ( ( ( 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 ) ) ) )
226 simp1 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) /\ t e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) ) -> ph )
227 eliccxr 
 |-  ( t e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) -> t e. RR* )
228 227 3ad2ant3 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) /\ t e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) ) -> t e. RR* )
229 71 rexrd 
 |-  ( ph -> ( P ` M ) e. RR* )
230 229 3ad2ant1 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) /\ t e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) ) -> ( P ` M ) e. RR* )
231 122 3adant3 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) /\ t e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) ) -> ( P ` ( k + 1 ) ) e. RR* )
232 simp3 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) /\ t e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) ) -> t e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) )
233 iccgelb 
 |-  ( ( ( P ` M ) e. RR* /\ ( P ` ( k + 1 ) ) e. RR* /\ t e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) ) -> ( P ` M ) <_ t )
234 230 231 232 233 syl3anc 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) /\ t e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) ) -> ( P ` M ) <_ t )
235 72 121 jca 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( ( P ` M ) e. RR /\ ( P ` ( k + 1 ) ) e. RR ) )
236 235 3adant3 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) /\ t e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) ) -> ( ( P ` M ) e. RR /\ ( P ` ( k + 1 ) ) e. RR ) )
237 iccssre 
 |-  ( ( ( P ` M ) e. RR /\ ( P ` ( k + 1 ) ) e. RR ) -> ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) C_ RR )
238 237 sseld 
 |-  ( ( ( P ` M ) e. RR /\ ( P ` ( k + 1 ) ) e. RR ) -> ( t e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) -> t e. RR ) )
239 236 232 238 sylc 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) /\ t e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) ) -> t e. RR )
240 121 3adant3 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) /\ t e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) ) -> ( P ` ( k + 1 ) ) e. RR )
241 2 10 10 63 14 elfzd 
 |-  ( ph -> N e. ( M ... N ) )
242 241 ancli 
 |-  ( ph -> ( ph /\ N e. ( M ... N ) ) )
243 eleq1 
 |-  ( i = N -> ( i e. ( M ... N ) <-> N e. ( M ... N ) ) )
244 243 anbi2d 
 |-  ( i = N -> ( ( ph /\ i e. ( M ... N ) ) <-> ( ph /\ N e. ( M ... N ) ) ) )
245 fveq2 
 |-  ( i = N -> ( P ` i ) = ( P ` N ) )
246 245 eleq1d 
 |-  ( i = N -> ( ( P ` i ) e. RR <-> ( P ` N ) e. RR ) )
247 244 246 imbi12d 
 |-  ( i = N -> ( ( ( ph /\ i e. ( M ... N ) ) -> ( P ` i ) e. RR ) <-> ( ( ph /\ N e. ( M ... N ) ) -> ( P ` N ) e. RR ) ) )
248 247 4 vtoclg 
 |-  ( N e. ZZ -> ( ( ph /\ N e. ( M ... N ) ) -> ( P ` N ) e. RR ) )
249 10 242 248 sylc 
 |-  ( ph -> ( P ` N ) e. RR )
250 249 3ad2ant1 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) /\ t e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) ) -> ( P ` N ) e. RR )
251 elicc1 
 |-  ( ( ( 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 ) ) ) ) )
252 230 231 251 syl2anc 
 |-  ( ( 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 ) ) ) ) )
253 232 252 mpbid 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) /\ t e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) ) -> ( t e. RR* /\ ( P ` M ) <_ t /\ t <_ ( P ` ( k + 1 ) ) ) )
254 253 simp3d 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) /\ t e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) ) -> t <_ ( P ` ( k + 1 ) ) )
255 elfzop1le2 
 |-  ( k e. ( ( M + 1 ) ..^ N ) -> ( k + 1 ) <_ N )
256 75 peano2zd 
 |-  ( k e. ( ( M + 1 ) ..^ N ) -> ( k + 1 ) e. ZZ )
257 eluz 
 |-  ( ( ( k + 1 ) e. ZZ /\ N e. ZZ ) -> ( N e. ( ZZ>= ` ( k + 1 ) ) <-> ( k + 1 ) <_ N ) )
258 256 158 257 syl2anc 
 |-  ( k e. ( ( M + 1 ) ..^ N ) -> ( N e. ( ZZ>= ` ( k + 1 ) ) <-> ( k + 1 ) <_ N ) )
259 255 258 mpbird 
 |-  ( k e. ( ( M + 1 ) ..^ N ) -> N e. ( ZZ>= ` ( k + 1 ) ) )
260 259 adantl 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> N e. ( ZZ>= ` ( k + 1 ) ) )
261 simpll 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... N ) ) -> ph )
262 elfzelz 
 |-  ( i e. ( ( k + 1 ) ... N ) -> i e. ZZ )
263 262 adantl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... N ) ) -> i e. ZZ )
264 261 38 syl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... N ) ) -> M e. RR )
265 263 zred 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... N ) ) -> i e. RR )
266 78 adantr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... N ) ) -> k e. RR )
267 83 adantr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... N ) ) -> M < k )
268 155 adantr 
 |-  ( ( k e. ( ( M + 1 ) ..^ N ) /\ i e. ( ( k + 1 ) ... N ) ) -> k e. RR )
269 1red 
 |-  ( ( k e. ( ( M + 1 ) ..^ N ) /\ i e. ( ( k + 1 ) ... N ) ) -> 1 e. RR )
270 268 269 readdcld 
 |-  ( ( k e. ( ( M + 1 ) ..^ N ) /\ i e. ( ( k + 1 ) ... N ) ) -> ( k + 1 ) e. RR )
271 262 zred 
 |-  ( i e. ( ( k + 1 ) ... N ) -> i e. RR )
272 271 adantl 
 |-  ( ( k e. ( ( M + 1 ) ..^ N ) /\ i e. ( ( k + 1 ) ... N ) ) -> i e. RR )
273 268 ltp1d 
 |-  ( ( k e. ( ( M + 1 ) ..^ N ) /\ i e. ( ( k + 1 ) ... N ) ) -> k < ( k + 1 ) )
274 elfzle1 
 |-  ( i e. ( ( k + 1 ) ... N ) -> ( k + 1 ) <_ i )
275 274 adantl 
 |-  ( ( k e. ( ( M + 1 ) ..^ N ) /\ i e. ( ( k + 1 ) ... N ) ) -> ( k + 1 ) <_ i )
276 268 270 272 273 275 ltletrd 
 |-  ( ( k e. ( ( M + 1 ) ..^ N ) /\ i e. ( ( k + 1 ) ... N ) ) -> k < i )
277 276 adantll 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... N ) ) -> k < i )
278 264 266 265 267 277 lttrd 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... N ) ) -> M < i )
279 264 265 278 ltled 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... N ) ) -> M <_ i )
280 elfzle2 
 |-  ( i e. ( ( k + 1 ) ... N ) -> i <_ N )
281 280 adantl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... N ) ) -> i <_ N )
282 261 89 139 3syl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... N ) ) -> ( i e. ( M ... N ) <-> ( i e. ZZ /\ M <_ i /\ i <_ N ) ) )
283 263 279 281 282 mpbir3and 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... N ) ) -> i e. ( M ... N ) )
284 261 283 4 syl2anc 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... N ) ) -> ( P ` i ) e. RR )
285 simpll 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> ph )
286 elfzelz 
 |-  ( i e. ( ( k + 1 ) ... ( N - 1 ) ) -> i e. ZZ )
287 286 adantl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> i e. ZZ )
288 285 38 syl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> M e. RR )
289 287 zred 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> i e. RR )
290 78 adantr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> k e. RR )
291 83 adantr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> M < k )
292 155 adantr 
 |-  ( ( k e. ( ( M + 1 ) ..^ N ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> k e. RR )
293 1red 
 |-  ( ( k e. ( ( M + 1 ) ..^ N ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> 1 e. RR )
294 292 293 readdcld 
 |-  ( ( k e. ( ( M + 1 ) ..^ N ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> ( k + 1 ) e. RR )
295 286 zred 
 |-  ( i e. ( ( k + 1 ) ... ( N - 1 ) ) -> i e. RR )
296 295 adantl 
 |-  ( ( k e. ( ( M + 1 ) ..^ N ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> i e. RR )
297 292 ltp1d 
 |-  ( ( k e. ( ( M + 1 ) ..^ N ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> k < ( k + 1 ) )
298 elfzle1 
 |-  ( i e. ( ( k + 1 ) ... ( N - 1 ) ) -> ( k + 1 ) <_ i )
299 298 adantl 
 |-  ( ( k e. ( ( M + 1 ) ..^ N ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> ( k + 1 ) <_ i )
300 292 294 296 297 299 ltletrd 
 |-  ( ( k e. ( ( M + 1 ) ..^ N ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> k < i )
301 300 adantll 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> k < i )
302 288 290 289 291 301 lttrd 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> M < i )
303 288 289 302 ltled 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> M <_ i )
304 295 adantl 
 |-  ( ( ph /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> i e. RR )
305 13 adantr 
 |-  ( ( ph /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> N e. RR )
306 1red 
 |-  ( ( ph /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> 1 e. RR )
307 305 306 resubcld 
 |-  ( ( ph /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> ( N - 1 ) e. RR )
308 elfzle2 
 |-  ( i e. ( ( k + 1 ) ... ( N - 1 ) ) -> i <_ ( N - 1 ) )
309 308 adantl 
 |-  ( ( ph /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> i <_ ( N - 1 ) )
310 305 ltm1d 
 |-  ( ( ph /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> ( N - 1 ) < N )
311 304 307 305 309 310 lelttrd 
 |-  ( ( ph /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> i < N )
312 304 305 311 ltled 
 |-  ( ( ph /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> i <_ N )
313 312 adantlr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> i <_ N )
314 285 89 139 3syl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> ( i e. ( M ... N ) <-> ( i e. ZZ /\ M <_ i /\ i <_ N ) ) )
315 287 303 313 314 mpbir3and 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> i e. ( M ... N ) )
316 285 315 4 syl2anc 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> ( P ` i ) e. RR )
317 287 peano2zd 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> ( i + 1 ) e. ZZ )
318 317 zred 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> ( i + 1 ) e. RR )
319 296 293 readdcld 
 |-  ( ( k e. ( ( M + 1 ) ..^ N ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> ( i + 1 ) e. RR )
320 292 296 300 ltled 
 |-  ( ( k e. ( ( M + 1 ) ..^ N ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> k <_ i )
321 292 296 293 320 leadd1dd 
 |-  ( ( k e. ( ( M + 1 ) ..^ N ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> ( k + 1 ) <_ ( i + 1 ) )
322 292 294 319 297 321 ltletrd 
 |-  ( ( k e. ( ( M + 1 ) ..^ N ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> k < ( i + 1 ) )
323 322 adantll 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> k < ( i + 1 ) )
324 288 290 318 291 323 lttrd 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> M < ( i + 1 ) )
325 288 318 324 ltled 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> M <_ ( i + 1 ) )
326 286 10 179 syl2anr 
 |-  ( ( ph /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> ( i < N <-> ( i + 1 ) <_ N ) )
327 311 326 mpbid 
 |-  ( ( ph /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> ( i + 1 ) <_ N )
328 327 adantlr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> ( i + 1 ) <_ N )
329 285 89 182 3syl 
 |-  ( ( ( 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 ) ) )
330 317 325 328 329 mpbir3and 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> ( i + 1 ) e. ( M ... N ) )
331 285 330 jca 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> ( ph /\ ( i + 1 ) e. ( M ... N ) ) )
332 330 331 191 sylc 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> ( P ` ( i + 1 ) ) e. RR )
333 285 2 syl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> M e. ZZ )
334 eluz 
 |-  ( ( M e. ZZ /\ i e. ZZ ) -> ( i e. ( ZZ>= ` M ) <-> M <_ i ) )
335 333 287 334 syl2anc 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> ( i e. ( ZZ>= ` M ) <-> M <_ i ) )
336 303 335 mpbird 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> i e. ( ZZ>= ` M ) )
337 285 3 9 3syl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> N e. ZZ )
338 311 adantlr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> i < N )
339 336 337 338 195 syl3anbrc 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> i e. ( M ..^ N ) )
340 285 339 5 syl2anc 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> ( P ` i ) < ( P ` ( i + 1 ) ) )
341 316 332 340 ltled 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> ( P ` i ) <_ ( P ` ( i + 1 ) ) )
342 260 284 341 monoord 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( P ` ( k + 1 ) ) <_ ( P ` N ) )
343 342 3adant3 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) /\ t e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) ) -> ( P ` ( k + 1 ) ) <_ ( P ` N ) )
344 239 240 250 254 343 letrd 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) /\ t e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) ) -> t <_ ( P ` N ) )
345 250 rexrd 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) /\ t e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) ) -> ( P ` N ) e. RR* )
346 elicc1 
 |-  ( ( ( P ` M ) e. RR* /\ ( P ` N ) e. RR* ) -> ( t e. ( ( P ` M ) [,] ( P ` N ) ) <-> ( t e. RR* /\ ( P ` M ) <_ t /\ t <_ ( P ` N ) ) ) )
347 230 345 346 syl2anc 
 |-  ( ( 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 ) ) ) )
348 228 234 344 347 mpbir3and 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) /\ t e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) ) -> t e. ( ( P ` M ) [,] ( P ` N ) ) )
349 226 348 6 syl2anc 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) /\ t e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) ) -> A e. CC )
350 223 224 225 349 syl3anc 
 |-  ( ( ( 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 )
351 simp2 
 |-  ( ( 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 ) )
352 60 351 mpd 
 |-  ( ( 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 )
353 60 61 jca 
 |-  ( ( k e. ( ( M + 1 ) ..^ N ) /\ ( ph -> ( t e. ( ( P ` M ) [,] ( P ` k ) ) |-> A ) e. L^1 ) /\ ph ) -> ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) )
354 74 202 jca 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( ph /\ k e. ( M ..^ N ) ) )
355 96 205 oveq12d 
 |-  ( i = k -> ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) = ( ( P ` k ) [,] ( P ` ( k + 1 ) ) ) )
356 355 mpteq1d 
 |-  ( i = k -> ( t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) |-> A ) = ( t e. ( ( P ` k ) [,] ( P ` ( k + 1 ) ) ) |-> A ) )
357 356 eleq1d 
 |-  ( i = k -> ( ( t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) |-> A ) e. L^1 <-> ( t e. ( ( P ` k ) [,] ( P ` ( k + 1 ) ) ) |-> A ) e. L^1 ) )
358 204 357 imbi12d 
 |-  ( 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 ) ) )
359 358 7 chvarvv 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( t e. ( ( P ` k ) [,] ( P ` ( k + 1 ) ) ) |-> A ) e. L^1 )
360 353 354 359 3syl 
 |-  ( ( 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 )
361 59 217 222 350 352 360 iblsplitf 
 |-  ( ( 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 )
362 361 3exp 
 |-  ( 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 ) ) )
363 20 25 30 35 54 362 fzind2 
 |-  ( N e. ( ( M + 1 ) ... N ) -> ( ph -> ( t e. ( ( P ` M ) [,] ( P ` N ) ) |-> A ) e. L^1 ) )
364 15 363 mpcom 
 |-  ( ph -> ( t e. ( ( P ` M ) [,] ( P ` N ) ) |-> A ) e. L^1 )