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