Metamath Proof Explorer

Theorem itgspltprt

Description: The S. integral splits on a given partition P . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses itgspltprt.1 
|- ( ph -> M e. ZZ )
itgspltprt.2 
|- ( ph -> N e. ( ZZ>= ` ( M + 1 ) ) )
itgspltprt.3 
|- ( ph -> P : ( M ... N ) --> RR )
itgspltprt.4 
|- ( ( ph /\ i e. ( M ..^ N ) ) -> ( P ` i ) < ( P ` ( i + 1 ) ) )
itgspltprt.5 
|- ( ( ph /\ t e. ( ( P ` M ) [,] ( P ` N ) ) ) -> A e. CC )
itgspltprt.6 
|- ( ( ph /\ i e. ( M ..^ N ) ) -> ( t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) |-> A ) e. L^1 )
Assertion itgspltprt 
|- ( ph -> S. ( ( P ` M ) [,] ( P ` N ) ) A _d t = sum_ i e. ( M ..^ N ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t )

Proof

Step Hyp Ref Expression
1 itgspltprt.1 
 |-  ( ph -> M e. ZZ )
2 itgspltprt.2 
 |-  ( ph -> N e. ( ZZ>= ` ( M + 1 ) ) )
3 itgspltprt.3 
 |-  ( ph -> P : ( M ... N ) --> RR )
4 itgspltprt.4 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( P ` i ) < ( P ` ( i + 1 ) ) )
5 itgspltprt.5 
 |-  ( ( ph /\ t e. ( ( P ` M ) [,] ( P ` N ) ) ) -> A e. CC )
6 itgspltprt.6 
 |-  ( ( ph /\ i e. ( M ..^ N ) ) -> ( t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) |-> A ) e. L^1 )
7 1 peano2zd 
 |-  ( ph -> ( M + 1 ) e. ZZ )
8 eluzelz 
 |-  ( N e. ( ZZ>= ` ( M + 1 ) ) -> N e. ZZ )
9 2 8 syl 
 |-  ( ph -> N e. ZZ )
10 eluzle 
 |-  ( N e. ( ZZ>= ` ( M + 1 ) ) -> ( M + 1 ) <_ N )
11 2 10 syl 
 |-  ( ph -> ( M + 1 ) <_ N )
12 eluzelre 
 |-  ( N e. ( ZZ>= ` ( M + 1 ) ) -> N e. RR )
13 2 12 syl 
 |-  ( ph -> N e. RR )
14 13 leidd 
 |-  ( ph -> N <_ N )
15 7 9 9 11 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 itgeq1d 
 |-  ( j = ( M + 1 ) -> S. ( ( P ` M ) [,] ( P ` j ) ) A _d t = S. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) A _d t )
19 oveq2 
 |-  ( j = ( M + 1 ) -> ( M ..^ j ) = ( M ..^ ( M + 1 ) ) )
20 19 sumeq1d 
 |-  ( j = ( M + 1 ) -> sum_ i e. ( M ..^ j ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t = sum_ i e. ( M ..^ ( M + 1 ) ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t )
21 18 20 eqeq12d 
 |-  ( j = ( M + 1 ) -> ( S. ( ( P ` M ) [,] ( P ` j ) ) A _d t = sum_ i e. ( M ..^ j ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t <-> S. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) A _d t = sum_ i e. ( M ..^ ( M + 1 ) ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t ) )
22 21 imbi2d 
 |-  ( j = ( M + 1 ) -> ( ( ph -> S. ( ( P ` M ) [,] ( P ` j ) ) A _d t = sum_ i e. ( M ..^ j ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t ) <-> ( ph -> S. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) A _d t = sum_ i e. ( M ..^ ( M + 1 ) ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t ) ) )
23 fveq2 
 |-  ( j = k -> ( P ` j ) = ( P ` k ) )
24 23 oveq2d 
 |-  ( j = k -> ( ( P ` M ) [,] ( P ` j ) ) = ( ( P ` M ) [,] ( P ` k ) ) )
25 24 itgeq1d 
 |-  ( j = k -> S. ( ( P ` M ) [,] ( P ` j ) ) A _d t = S. ( ( P ` M ) [,] ( P ` k ) ) A _d t )
26 oveq2 
 |-  ( j = k -> ( M ..^ j ) = ( M ..^ k ) )
27 26 sumeq1d 
 |-  ( j = k -> sum_ i e. ( M ..^ j ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t = sum_ i e. ( M ..^ k ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t )
28 25 27 eqeq12d 
 |-  ( j = k -> ( S. ( ( P ` M ) [,] ( P ` j ) ) A _d t = sum_ i e. ( M ..^ j ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t <-> S. ( ( P ` M ) [,] ( P ` k ) ) A _d t = sum_ i e. ( M ..^ k ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t ) )
29 28 imbi2d 
 |-  ( j = k -> ( ( ph -> S. ( ( P ` M ) [,] ( P ` j ) ) A _d t = sum_ i e. ( M ..^ j ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t ) <-> ( ph -> S. ( ( P ` M ) [,] ( P ` k ) ) A _d t = sum_ i e. ( M ..^ k ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t ) ) )
30 fveq2 
 |-  ( j = ( k + 1 ) -> ( P ` j ) = ( P ` ( k + 1 ) ) )
31 30 oveq2d 
 |-  ( j = ( k + 1 ) -> ( ( P ` M ) [,] ( P ` j ) ) = ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) )
32 31 itgeq1d 
 |-  ( j = ( k + 1 ) -> S. ( ( P ` M ) [,] ( P ` j ) ) A _d t = S. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) A _d t )
33 oveq2 
 |-  ( j = ( k + 1 ) -> ( M ..^ j ) = ( M ..^ ( k + 1 ) ) )
34 33 sumeq1d 
 |-  ( j = ( k + 1 ) -> sum_ i e. ( M ..^ j ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t = sum_ i e. ( M ..^ ( k + 1 ) ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t )
35 32 34 eqeq12d 
 |-  ( j = ( k + 1 ) -> ( S. ( ( P ` M ) [,] ( P ` j ) ) A _d t = sum_ i e. ( M ..^ j ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t <-> S. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) A _d t = sum_ i e. ( M ..^ ( k + 1 ) ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t ) )
36 35 imbi2d 
 |-  ( j = ( k + 1 ) -> ( ( ph -> S. ( ( P ` M ) [,] ( P ` j ) ) A _d t = sum_ i e. ( M ..^ j ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t ) <-> ( ph -> S. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) A _d t = sum_ i e. ( M ..^ ( k + 1 ) ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t ) ) )
37 fveq2 
 |-  ( j = N -> ( P ` j ) = ( P ` N ) )
38 37 oveq2d 
 |-  ( j = N -> ( ( P ` M ) [,] ( P ` j ) ) = ( ( P ` M ) [,] ( P ` N ) ) )
39 38 itgeq1d 
 |-  ( j = N -> S. ( ( P ` M ) [,] ( P ` j ) ) A _d t = S. ( ( P ` M ) [,] ( P ` N ) ) A _d t )
40 oveq2 
 |-  ( j = N -> ( M ..^ j ) = ( M ..^ N ) )
41 40 sumeq1d 
 |-  ( j = N -> sum_ i e. ( M ..^ j ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t = sum_ i e. ( M ..^ N ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t )
42 39 41 eqeq12d 
 |-  ( j = N -> ( S. ( ( P ` M ) [,] ( P ` j ) ) A _d t = sum_ i e. ( M ..^ j ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t <-> S. ( ( P ` M ) [,] ( P ` N ) ) A _d t = sum_ i e. ( M ..^ N ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t ) )
43 42 imbi2d 
 |-  ( j = N -> ( ( ph -> S. ( ( P ` M ) [,] ( P ` j ) ) A _d t = sum_ i e. ( M ..^ j ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t ) <-> ( ph -> S. ( ( P ` M ) [,] ( P ` N ) ) A _d t = sum_ i e. ( M ..^ N ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t ) ) )
44 1 adantl 
 |-  ( ( N e. ( ZZ>= ` ( M + 1 ) ) /\ ph ) -> M e. ZZ )
45 fzval3 
 |-  ( M e. ZZ -> ( M ... M ) = ( M ..^ ( M + 1 ) ) )
46 44 45 syl 
 |-  ( ( N e. ( ZZ>= ` ( M + 1 ) ) /\ ph ) -> ( M ... M ) = ( M ..^ ( M + 1 ) ) )
47 46 eqcomd 
 |-  ( ( N e. ( ZZ>= ` ( M + 1 ) ) /\ ph ) -> ( M ..^ ( M + 1 ) ) = ( M ... M ) )
48 47 sumeq1d 
 |-  ( ( N e. ( ZZ>= ` ( M + 1 ) ) /\ ph ) -> sum_ i e. ( M ..^ ( M + 1 ) ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t = sum_ i e. ( M ... M ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t )
49 3 adantr 
 |-  ( ( ph /\ t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) ) -> P : ( M ... N ) --> RR )
50 1 zred 
 |-  ( ph -> M e. RR )
51 1red 
 |-  ( ph -> 1 e. RR )
52 50 51 readdcld 
 |-  ( ph -> ( M + 1 ) e. RR )
53 50 ltp1d 
 |-  ( ph -> M < ( M + 1 ) )
54 50 52 13 53 11 ltletrd 
 |-  ( ph -> M < N )
55 50 13 54 ltled 
 |-  ( ph -> M <_ N )
56 eluz 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( N e. ( ZZ>= ` M ) <-> M <_ N ) )
57 1 9 56 syl2anc 
 |-  ( ph -> ( N e. ( ZZ>= ` M ) <-> M <_ N ) )
58 55 57 mpbird 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
59 eluzfz1 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ( M ... N ) )
60 58 59 syl 
 |-  ( ph -> M e. ( M ... N ) )
61 60 adantr 
 |-  ( ( ph /\ t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) ) -> M e. ( M ... N ) )
62 49 61 ffvelrnd 
 |-  ( ( ph /\ t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) ) -> ( P ` M ) e. RR )
63 1 9 9 55 14 elfzd 
 |-  ( ph -> N e. ( M ... N ) )
64 3 63 ffvelrnd 
 |-  ( ph -> ( P ` N ) e. RR )
65 64 adantr 
 |-  ( ( ph /\ t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) ) -> ( P ` N ) e. RR )
66 50 lep1d 
 |-  ( ph -> M <_ ( M + 1 ) )
67 1 9 7 66 11 elfzd 
 |-  ( ph -> ( M + 1 ) e. ( M ... N ) )
68 3 67 ffvelrnd 
 |-  ( ph -> ( P ` ( M + 1 ) ) e. RR )
69 68 adantr 
 |-  ( ( ph /\ t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) ) -> ( P ` ( M + 1 ) ) e. RR )
70 simpr 
 |-  ( ( ph /\ t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) ) -> t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) )
71 eliccre 
 |-  ( ( ( P ` M ) e. RR /\ ( P ` ( M + 1 ) ) e. RR /\ t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) ) -> t e. RR )
72 62 69 70 71 syl3anc 
 |-  ( ( ph /\ t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) ) -> t e. RR )
73 3 60 ffvelrnd 
 |-  ( ph -> ( P ` M ) e. RR )
74 73 rexrd 
 |-  ( ph -> ( P ` M ) e. RR* )
75 74 adantr 
 |-  ( ( ph /\ t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) ) -> ( P ` M ) e. RR* )
76 69 rexrd 
 |-  ( ( ph /\ t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) ) -> ( P ` ( M + 1 ) ) e. RR* )
77 iccgelb 
 |-  ( ( ( P ` M ) e. RR* /\ ( P ` ( M + 1 ) ) e. RR* /\ t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) ) -> ( P ` M ) <_ t )
78 75 76 70 77 syl3anc 
 |-  ( ( ph /\ t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) ) -> ( P ` M ) <_ t )
79 iccleub 
 |-  ( ( ( P ` M ) e. RR* /\ ( P ` ( M + 1 ) ) e. RR* /\ t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) ) -> t <_ ( P ` ( M + 1 ) ) )
80 75 76 70 79 syl3anc 
 |-  ( ( ph /\ t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) ) -> t <_ ( P ` ( M + 1 ) ) )
81 3 adantr 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... N ) ) -> P : ( M ... N ) --> RR )
82 elfzelz 
 |-  ( i e. ( ( M + 1 ) ... N ) -> i e. ZZ )
83 82 adantl 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... N ) ) -> i e. ZZ )
84 50 adantr 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... N ) ) -> M e. RR )
85 83 zred 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... N ) ) -> i e. RR )
86 52 adantr 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... N ) ) -> ( M + 1 ) e. RR )
87 53 adantr 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... N ) ) -> M < ( M + 1 ) )
88 elfzle1 
 |-  ( i e. ( ( M + 1 ) ... N ) -> ( M + 1 ) <_ i )
89 88 adantl 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... N ) ) -> ( M + 1 ) <_ i )
90 84 86 85 87 89 ltletrd 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... N ) ) -> M < i )
91 84 85 90 ltled 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... N ) ) -> M <_ i )
92 elfzle2 
 |-  ( i e. ( ( M + 1 ) ... N ) -> i <_ N )
93 92 adantl 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... N ) ) -> i <_ N )
94 1 9 jca 
 |-  ( ph -> ( M e. ZZ /\ N e. ZZ ) )
95 94 adantr 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... N ) ) -> ( M e. ZZ /\ N e. ZZ ) )
96 elfz1 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( i e. ( M ... N ) <-> ( i e. ZZ /\ M <_ i /\ i <_ N ) ) )
97 95 96 syl 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... N ) ) -> ( i e. ( M ... N ) <-> ( i e. ZZ /\ M <_ i /\ i <_ N ) ) )
98 83 91 93 97 mpbir3and 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... N ) ) -> i e. ( M ... N ) )
99 81 98 ffvelrnd 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... N ) ) -> ( P ` i ) e. RR )
100 3 adantr 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> P : ( M ... N ) --> RR )
101 elfzelz 
 |-  ( i e. ( ( M + 1 ) ... ( N - 1 ) ) -> i e. ZZ )
102 101 adantl 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> i e. ZZ )
103 50 adantr 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> M e. RR )
104 102 zred 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> i e. RR )
105 52 adantr 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> ( M + 1 ) e. RR )
106 53 adantr 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> M < ( M + 1 ) )
107 elfzle1 
 |-  ( i e. ( ( M + 1 ) ... ( N - 1 ) ) -> ( M + 1 ) <_ i )
108 107 adantl 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> ( M + 1 ) <_ i )
109 103 105 104 106 108 ltletrd 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> M < i )
110 103 104 109 ltled 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> M <_ i )
111 13 adantr 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> N e. RR )
112 1red 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> 1 e. RR )
113 111 112 resubcld 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> ( N - 1 ) e. RR )
114 elfzle2 
 |-  ( i e. ( ( M + 1 ) ... ( N - 1 ) ) -> i <_ ( N - 1 ) )
115 114 adantl 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> i <_ ( N - 1 ) )
116 111 ltm1d 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> ( N - 1 ) < N )
117 104 113 111 115 116 lelttrd 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> i < N )
118 104 111 117 ltled 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> i <_ N )
119 94 adantr 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> ( M e. ZZ /\ N e. ZZ ) )
120 119 96 syl 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> ( i e. ( M ... N ) <-> ( i e. ZZ /\ M <_ i /\ i <_ N ) ) )
121 102 110 118 120 mpbir3and 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> i e. ( M ... N ) )
122 100 121 ffvelrnd 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> ( P ` i ) e. RR )
123 102 peano2zd 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> ( i + 1 ) e. ZZ )
124 104 112 readdcld 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> ( i + 1 ) e. RR )
125 103 104 112 109 ltadd1dd 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> ( M + 1 ) < ( i + 1 ) )
126 103 105 124 106 125 lttrd 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> M < ( i + 1 ) )
127 103 124 126 ltled 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> M <_ ( i + 1 ) )
128 zltp1le 
 |-  ( ( i e. ZZ /\ N e. ZZ ) -> ( i < N <-> ( i + 1 ) <_ N ) )
129 101 9 128 syl2anr 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> ( i < N <-> ( i + 1 ) <_ N ) )
130 117 129 mpbid 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> ( i + 1 ) <_ N )
131 elfz1 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( i + 1 ) e. ( M ... N ) <-> ( ( i + 1 ) e. ZZ /\ M <_ ( i + 1 ) /\ ( i + 1 ) <_ N ) ) )
132 119 131 syl 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> ( ( i + 1 ) e. ( M ... N ) <-> ( ( i + 1 ) e. ZZ /\ M <_ ( i + 1 ) /\ ( i + 1 ) <_ N ) ) )
133 123 127 130 132 mpbir3and 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> ( i + 1 ) e. ( M ... N ) )
134 100 133 ffvelrnd 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> ( P ` ( i + 1 ) ) e. RR )
135 eluz 
 |-  ( ( M e. ZZ /\ i e. ZZ ) -> ( i e. ( ZZ>= ` M ) <-> M <_ i ) )
136 1 101 135 syl2an 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> ( i e. ( ZZ>= ` M ) <-> M <_ i ) )
137 110 136 mpbird 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> i e. ( ZZ>= ` M ) )
138 9 adantr 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> N e. ZZ )
139 elfzo2 
 |-  ( i e. ( M ..^ N ) <-> ( i e. ( ZZ>= ` M ) /\ N e. ZZ /\ i < N ) )
140 137 138 117 139 syl3anbrc 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> i e. ( M ..^ N ) )
141 140 4 syldan 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> ( P ` i ) < ( P ` ( i + 1 ) ) )
142 122 134 141 ltled 
 |-  ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> ( P ` i ) <_ ( P ` ( i + 1 ) ) )
143 2 99 142 monoord 
 |-  ( ph -> ( P ` ( M + 1 ) ) <_ ( P ` N ) )
144 143 adantr 
 |-  ( ( ph /\ t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) ) -> ( P ` ( M + 1 ) ) <_ ( P ` N ) )
145 72 69 65 80 144 letrd 
 |-  ( ( ph /\ t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) ) -> t <_ ( P ` N ) )
146 62 65 72 78 145 eliccd 
 |-  ( ( ph /\ t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) ) -> t e. ( ( P ` M ) [,] ( P ` N ) ) )
147 146 5 syldan 
 |-  ( ( ph /\ t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) ) -> A e. CC )
148 id 
 |-  ( ph -> ph )
149 fzolb 
 |-  ( M e. ( M ..^ N ) <-> ( M e. ZZ /\ N e. ZZ /\ M < N ) )
150 1 9 54 149 syl3anbrc 
 |-  ( ph -> M e. ( M ..^ N ) )
151 148 150 jca 
 |-  ( ph -> ( ph /\ M e. ( M ..^ N ) ) )
152 eleq1 
 |-  ( i = M -> ( i e. ( M ..^ N ) <-> M e. ( M ..^ N ) ) )
153 152 anbi2d 
 |-  ( i = M -> ( ( ph /\ i e. ( M ..^ N ) ) <-> ( ph /\ M e. ( M ..^ N ) ) ) )
154 fveq2 
 |-  ( i = M -> ( P ` i ) = ( P ` M ) )
155 fvoveq1 
 |-  ( i = M -> ( P ` ( i + 1 ) ) = ( P ` ( M + 1 ) ) )
156 154 155 oveq12d 
 |-  ( i = M -> ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) = ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) )
157 156 mpteq1d 
 |-  ( i = M -> ( t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) |-> A ) = ( t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) |-> A ) )
158 157 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 ) )
159 153 158 imbi12d 
 |-  ( i = M -> ( ( ( ph /\ i e. ( M ..^ N ) ) -> ( t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) |-> A ) e. L^1 ) <-> ( ( ph /\ M e. ( M ..^ N ) ) -> ( t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) |-> A ) e. L^1 ) ) )
160 159 6 vtoclg 
 |-  ( M e. ZZ -> ( ( ph /\ M e. ( M ..^ N ) ) -> ( t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) |-> A ) e. L^1 ) )
161 1 151 160 sylc 
 |-  ( ph -> ( t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) |-> A ) e. L^1 )
162 147 161 itgcl 
 |-  ( ph -> S. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) A _d t e. CC )
163 156 itgeq1d 
 |-  ( i = M -> S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t = S. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) A _d t )
164 163 fsum1 
 |-  ( ( M e. ZZ /\ S. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) A _d t e. CC ) -> sum_ i e. ( M ... M ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t = S. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) A _d t )
165 1 162 164 syl2anc 
 |-  ( ph -> sum_ i e. ( M ... M ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t = S. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) A _d t )
166 165 adantl 
 |-  ( ( N e. ( ZZ>= ` ( M + 1 ) ) /\ ph ) -> sum_ i e. ( M ... M ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t = S. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) A _d t )
167 48 166 eqtr2d 
 |-  ( ( N e. ( ZZ>= ` ( M + 1 ) ) /\ ph ) -> S. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) A _d t = sum_ i e. ( M ..^ ( M + 1 ) ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t )
168 167 ex 
 |-  ( N e. ( ZZ>= ` ( M + 1 ) ) -> ( ph -> S. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) A _d t = sum_ i e. ( M ..^ ( M + 1 ) ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t ) )
169 simp3 
 |-  ( ( k e. ( ( M + 1 ) ..^ N ) /\ ( ph -> S. ( ( P ` M ) [,] ( P ` k ) ) A _d t = sum_ i e. ( M ..^ k ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t ) /\ ph ) -> ph )
170 simp1 
 |-  ( ( k e. ( ( M + 1 ) ..^ N ) /\ ( ph -> S. ( ( P ` M ) [,] ( P ` k ) ) A _d t = sum_ i e. ( M ..^ k ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t ) /\ ph ) -> k e. ( ( M + 1 ) ..^ N ) )
171 simp2 
 |-  ( ( k e. ( ( M + 1 ) ..^ N ) /\ ( ph -> S. ( ( P ` M ) [,] ( P ` k ) ) A _d t = sum_ i e. ( M ..^ k ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t ) /\ ph ) -> ( ph -> S. ( ( P ` M ) [,] ( P ` k ) ) A _d t = sum_ i e. ( M ..^ k ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t ) )
172 169 171 mpd 
 |-  ( ( k e. ( ( M + 1 ) ..^ N ) /\ ( ph -> S. ( ( P ` M ) [,] ( P ` k ) ) A _d t = sum_ i e. ( M ..^ k ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t ) /\ ph ) -> S. ( ( P ` M ) [,] ( P ` k ) ) A _d t = sum_ i e. ( M ..^ k ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t )
173 50 adantr 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> M e. RR )
174 elfzoelz 
 |-  ( k e. ( ( M + 1 ) ..^ N ) -> k e. ZZ )
175 174 zred 
 |-  ( k e. ( ( M + 1 ) ..^ N ) -> k e. RR )
176 175 adantl 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> k e. RR )
177 52 adantr 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( M + 1 ) e. RR )
178 53 adantr 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> M < ( M + 1 ) )
179 elfzole1 
 |-  ( k e. ( ( M + 1 ) ..^ N ) -> ( M + 1 ) <_ k )
180 179 adantl 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( M + 1 ) <_ k )
181 173 177 176 178 180 ltletrd 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> M < k )
182 173 176 181 ltled 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> M <_ k )
183 eluz 
 |-  ( ( M e. ZZ /\ k e. ZZ ) -> ( k e. ( ZZ>= ` M ) <-> M <_ k ) )
184 1 174 183 syl2an 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( k e. ( ZZ>= ` M ) <-> M <_ k ) )
185 182 184 mpbird 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> k e. ( ZZ>= ` M ) )
186 simplll 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> ph )
187 eliccxr 
 |-  ( t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) -> t e. RR* )
188 187 adantl 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> t e. RR* )
189 186 73 syl 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> ( P ` M ) e. RR )
190 186 3 syl 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> P : ( M ... N ) --> RR )
191 elfzelz 
 |-  ( i e. ( M ... k ) -> i e. ZZ )
192 191 adantl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> i e. ZZ )
193 elfzle1 
 |-  ( i e. ( M ... k ) -> M <_ i )
194 193 adantl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> M <_ i )
195 192 zred 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> i e. RR )
196 13 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> N e. RR )
197 176 adantr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> k e. RR )
198 elfzle2 
 |-  ( i e. ( M ... k ) -> i <_ k )
199 198 adantl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> i <_ k )
200 elfzolt2 
 |-  ( k e. ( ( M + 1 ) ..^ N ) -> k < N )
201 200 ad2antlr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> k < N )
202 195 197 196 199 201 lelttrd 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> i < N )
203 195 196 202 ltled 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> i <_ N )
204 94 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> ( M e. ZZ /\ N e. ZZ ) )
205 204 96 syl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> ( i e. ( M ... N ) <-> ( i e. ZZ /\ M <_ i /\ i <_ N ) ) )
206 192 194 203 205 mpbir3and 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> i e. ( M ... N ) )
207 206 adantr 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> i e. ( M ... N ) )
208 190 207 ffvelrnd 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> ( P ` i ) e. RR )
209 192 peano2zd 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> ( i + 1 ) e. ZZ )
210 50 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> M e. RR )
211 209 zred 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> ( i + 1 ) e. RR )
212 50 adantr 
 |-  ( ( ph /\ i e. ( M ... k ) ) -> M e. RR )
213 191 zred 
 |-  ( i e. ( M ... k ) -> i e. RR )
214 213 adantl 
 |-  ( ( ph /\ i e. ( M ... k ) ) -> i e. RR )
215 1red 
 |-  ( ( ph /\ i e. ( M ... k ) ) -> 1 e. RR )
216 214 215 readdcld 
 |-  ( ( ph /\ i e. ( M ... k ) ) -> ( i + 1 ) e. RR )
217 193 adantl 
 |-  ( ( ph /\ i e. ( M ... k ) ) -> M <_ i )
218 214 ltp1d 
 |-  ( ( ph /\ i e. ( M ... k ) ) -> i < ( i + 1 ) )
219 212 214 216 217 218 lelttrd 
 |-  ( ( ph /\ i e. ( M ... k ) ) -> M < ( i + 1 ) )
220 219 adantlr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> M < ( i + 1 ) )
221 210 211 220 ltled 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> M <_ ( i + 1 ) )
222 9 191 anim12ci 
 |-  ( ( ph /\ i e. ( M ... k ) ) -> ( i e. ZZ /\ N e. ZZ ) )
223 222 adantlr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> ( i e. ZZ /\ N e. ZZ ) )
224 223 128 syl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> ( i < N <-> ( i + 1 ) <_ N ) )
225 202 224 mpbid 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> ( i + 1 ) <_ N )
226 204 131 syl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> ( ( i + 1 ) e. ( M ... N ) <-> ( ( i + 1 ) e. ZZ /\ M <_ ( i + 1 ) /\ ( i + 1 ) <_ N ) ) )
227 209 221 225 226 mpbir3and 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> ( i + 1 ) e. ( M ... N ) )
228 227 adantr 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> ( i + 1 ) e. ( M ... N ) )
229 190 228 ffvelrnd 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> ( P ` ( i + 1 ) ) e. RR )
230 simpr 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) )
231 eliccre 
 |-  ( ( ( P ` i ) e. RR /\ ( P ` ( i + 1 ) ) e. RR /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> t e. RR )
232 208 229 230 231 syl3anc 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> t e. RR )
233 elfzuz 
 |-  ( i e. ( M ... k ) -> i e. ( ZZ>= ` M ) )
234 233 adantl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> i e. ( ZZ>= ` M ) )
235 3 ad3antrrr 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... i ) ) -> P : ( M ... N ) --> RR )
236 elfzelz 
 |-  ( j e. ( M ... i ) -> j e. ZZ )
237 236 adantl 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... i ) ) -> j e. ZZ )
238 elfzle1 
 |-  ( j e. ( M ... i ) -> M <_ j )
239 238 adantl 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... i ) ) -> M <_ j )
240 237 zred 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... i ) ) -> j e. RR )
241 196 adantr 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... i ) ) -> N e. RR )
242 195 adantr 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... i ) ) -> i e. RR )
243 elfzle2 
 |-  ( j e. ( M ... i ) -> j <_ i )
244 243 adantl 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... i ) ) -> j <_ i )
245 202 adantr 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... i ) ) -> i < N )
246 240 242 241 244 245 lelttrd 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... i ) ) -> j < N )
247 240 241 246 ltled 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... i ) ) -> j <_ N )
248 204 adantr 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... i ) ) -> ( M e. ZZ /\ N e. ZZ ) )
249 elfz1 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( j e. ( M ... N ) <-> ( j e. ZZ /\ M <_ j /\ j <_ N ) ) )
250 248 249 syl 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... i ) ) -> ( j e. ( M ... N ) <-> ( j e. ZZ /\ M <_ j /\ j <_ N ) ) )
251 237 239 247 250 mpbir3and 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... i ) ) -> j e. ( M ... N ) )
252 235 251 ffvelrnd 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... i ) ) -> ( P ` j ) e. RR )
253 3 ad3antrrr 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> P : ( M ... N ) --> RR )
254 elfzelz 
 |-  ( j e. ( M ... ( i - 1 ) ) -> j e. ZZ )
255 254 adantl 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> j e. ZZ )
256 elfzle1 
 |-  ( j e. ( M ... ( i - 1 ) ) -> M <_ j )
257 256 adantl 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> M <_ j )
258 255 zred 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> j e. RR )
259 196 adantr 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> N e. RR )
260 195 adantr 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> i e. RR )
261 1red 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> 1 e. RR )
262 260 261 resubcld 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> ( i - 1 ) e. RR )
263 elfzle2 
 |-  ( j e. ( M ... ( i - 1 ) ) -> j <_ ( i - 1 ) )
264 263 adantl 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> j <_ ( i - 1 ) )
265 260 ltm1d 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> ( i - 1 ) < i )
266 258 262 260 264 265 lelttrd 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> j < i )
267 202 adantr 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> i < N )
268 258 260 259 266 267 lttrd 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> j < N )
269 258 259 268 ltled 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> j <_ N )
270 204 adantr 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> ( M e. ZZ /\ N e. ZZ ) )
271 270 249 syl 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> ( j e. ( M ... N ) <-> ( j e. ZZ /\ M <_ j /\ j <_ N ) ) )
272 255 257 269 271 mpbir3and 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> j e. ( M ... N ) )
273 253 272 ffvelrnd 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> ( P ` j ) e. RR )
274 255 peano2zd 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> ( j + 1 ) e. ZZ )
275 173 ad2antrr 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> M e. RR )
276 258 261 readdcld 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> ( j + 1 ) e. RR )
277 50 adantr 
 |-  ( ( ph /\ j e. ( M ... ( i - 1 ) ) ) -> M e. RR )
278 254 zred 
 |-  ( j e. ( M ... ( i - 1 ) ) -> j e. RR )
279 278 adantl 
 |-  ( ( ph /\ j e. ( M ... ( i - 1 ) ) ) -> j e. RR )
280 1red 
 |-  ( ( ph /\ j e. ( M ... ( i - 1 ) ) ) -> 1 e. RR )
281 279 280 readdcld 
 |-  ( ( ph /\ j e. ( M ... ( i - 1 ) ) ) -> ( j + 1 ) e. RR )
282 256 adantl 
 |-  ( ( ph /\ j e. ( M ... ( i - 1 ) ) ) -> M <_ j )
283 279 ltp1d 
 |-  ( ( ph /\ j e. ( M ... ( i - 1 ) ) ) -> j < ( j + 1 ) )
284 277 279 281 282 283 lelttrd 
 |-  ( ( ph /\ j e. ( M ... ( i - 1 ) ) ) -> M < ( j + 1 ) )
285 284 ad4ant14 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> M < ( j + 1 ) )
286 275 276 285 ltled 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> M <_ ( j + 1 ) )
287 zltp1le 
 |-  ( ( j e. ZZ /\ i e. ZZ ) -> ( j < i <-> ( j + 1 ) <_ i ) )
288 254 192 287 syl2anr 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> ( j < i <-> ( j + 1 ) <_ i ) )
289 266 288 mpbid 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> ( j + 1 ) <_ i )
290 276 260 259 289 267 lelttrd 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> ( j + 1 ) < N )
291 276 259 290 ltled 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> ( j + 1 ) <_ N )
292 elfz1 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( j + 1 ) e. ( M ... N ) <-> ( ( j + 1 ) e. ZZ /\ M <_ ( j + 1 ) /\ ( j + 1 ) <_ N ) ) )
293 270 292 syl 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> ( ( j + 1 ) e. ( M ... N ) <-> ( ( j + 1 ) e. ZZ /\ M <_ ( j + 1 ) /\ ( j + 1 ) <_ N ) ) )
294 274 286 291 293 mpbir3and 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> ( j + 1 ) e. ( M ... N ) )
295 253 294 ffvelrnd 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> ( P ` ( j + 1 ) ) e. RR )
296 simplll 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> ph )
297 elfzuz 
 |-  ( j e. ( M ... ( i - 1 ) ) -> j e. ( ZZ>= ` M ) )
298 297 adantl 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> j e. ( ZZ>= ` M ) )
299 296 9 syl 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> N e. ZZ )
300 elfzo2 
 |-  ( j e. ( M ..^ N ) <-> ( j e. ( ZZ>= ` M ) /\ N e. ZZ /\ j < N ) )
301 298 299 268 300 syl3anbrc 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> j e. ( M ..^ N ) )
302 eleq1 
 |-  ( i = j -> ( i e. ( M ..^ N ) <-> j e. ( M ..^ N ) ) )
303 302 anbi2d 
 |-  ( i = j -> ( ( ph /\ i e. ( M ..^ N ) ) <-> ( ph /\ j e. ( M ..^ N ) ) ) )
304 fveq2 
 |-  ( i = j -> ( P ` i ) = ( P ` j ) )
305 fvoveq1 
 |-  ( i = j -> ( P ` ( i + 1 ) ) = ( P ` ( j + 1 ) ) )
306 304 305 breq12d 
 |-  ( i = j -> ( ( P ` i ) < ( P ` ( i + 1 ) ) <-> ( P ` j ) < ( P ` ( j + 1 ) ) ) )
307 303 306 imbi12d 
 |-  ( i = j -> ( ( ( ph /\ i e. ( M ..^ N ) ) -> ( P ` i ) < ( P ` ( i + 1 ) ) ) <-> ( ( ph /\ j e. ( M ..^ N ) ) -> ( P ` j ) < ( P ` ( j + 1 ) ) ) ) )
308 307 4 chvarvv 
 |-  ( ( ph /\ j e. ( M ..^ N ) ) -> ( P ` j ) < ( P ` ( j + 1 ) ) )
309 296 301 308 syl2anc 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> ( P ` j ) < ( P ` ( j + 1 ) ) )
310 273 295 309 ltled 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> ( P ` j ) <_ ( P ` ( j + 1 ) ) )
311 234 252 310 monoord 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> ( P ` M ) <_ ( P ` i ) )
312 311 adantr 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> ( P ` M ) <_ ( P ` i ) )
313 208 rexrd 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> ( P ` i ) e. RR* )
314 229 rexrd 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> ( P ` ( i + 1 ) ) e. RR* )
315 iccgelb 
 |-  ( ( ( P ` i ) e. RR* /\ ( P ` ( i + 1 ) ) e. RR* /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> ( P ` i ) <_ t )
316 313 314 230 315 syl3anc 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> ( P ` i ) <_ t )
317 189 208 232 312 316 letrd 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> ( P ` M ) <_ t )
318 186 64 syl 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> ( P ` N ) e. RR )
319 iccleub 
 |-  ( ( ( P ` i ) e. RR* /\ ( P ` ( i + 1 ) ) e. RR* /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> t <_ ( P ` ( i + 1 ) ) )
320 313 314 230 319 syl3anc 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> t <_ ( P ` ( i + 1 ) ) )
321 9 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> N e. ZZ )
322 eluz 
 |-  ( ( ( i + 1 ) e. ZZ /\ N e. ZZ ) -> ( N e. ( ZZ>= ` ( i + 1 ) ) <-> ( i + 1 ) <_ N ) )
323 209 321 322 syl2anc 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> ( N e. ( ZZ>= ` ( i + 1 ) ) <-> ( i + 1 ) <_ N ) )
324 225 323 mpbird 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> N e. ( ZZ>= ` ( i + 1 ) ) )
325 324 adantr 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> N e. ( ZZ>= ` ( i + 1 ) ) )
326 3 ad3antrrr 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( ( i + 1 ) ... N ) ) -> P : ( M ... N ) --> RR )
327 elfzelz 
 |-  ( j e. ( ( i + 1 ) ... N ) -> j e. ZZ )
328 327 adantl 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( ( i + 1 ) ... N ) ) -> j e. ZZ )
329 elfzel1 
 |-  ( i e. ( M ... k ) -> M e. ZZ )
330 329 zred 
 |-  ( i e. ( M ... k ) -> M e. RR )
331 330 adantr 
 |-  ( ( i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... N ) ) -> M e. RR )
332 327 zred 
 |-  ( j e. ( ( i + 1 ) ... N ) -> j e. RR )
333 332 adantl 
 |-  ( ( i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... N ) ) -> j e. RR )
334 213 adantr 
 |-  ( ( i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... N ) ) -> i e. RR )
335 1red 
 |-  ( ( i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... N ) ) -> 1 e. RR )
336 334 335 readdcld 
 |-  ( ( i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... N ) ) -> ( i + 1 ) e. RR )
337 193 adantr 
 |-  ( ( i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... N ) ) -> M <_ i )
338 334 ltp1d 
 |-  ( ( i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... N ) ) -> i < ( i + 1 ) )
339 331 334 336 337 338 lelttrd 
 |-  ( ( i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... N ) ) -> M < ( i + 1 ) )
340 elfzle1 
 |-  ( j e. ( ( i + 1 ) ... N ) -> ( i + 1 ) <_ j )
341 340 adantl 
 |-  ( ( i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... N ) ) -> ( i + 1 ) <_ j )
342 331 336 333 339 341 ltletrd 
 |-  ( ( i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... N ) ) -> M < j )
343 331 333 342 ltled 
 |-  ( ( i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... N ) ) -> M <_ j )
344 343 adantll 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( ( i + 1 ) ... N ) ) -> M <_ j )
345 elfzle2 
 |-  ( j e. ( ( i + 1 ) ... N ) -> j <_ N )
346 345 adantl 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( ( i + 1 ) ... N ) ) -> j <_ N )
347 204 adantr 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( ( i + 1 ) ... N ) ) -> ( M e. ZZ /\ N e. ZZ ) )
348 347 249 syl 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( ( i + 1 ) ... N ) ) -> ( j e. ( M ... N ) <-> ( j e. ZZ /\ M <_ j /\ j <_ N ) ) )
349 328 344 346 348 mpbir3and 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( ( i + 1 ) ... N ) ) -> j e. ( M ... N ) )
350 326 349 ffvelrnd 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( ( i + 1 ) ... N ) ) -> ( P ` j ) e. RR )
351 350 adantlr 
 |-  ( ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) /\ j e. ( ( i + 1 ) ... N ) ) -> ( P ` j ) e. RR )
352 simplll 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> ph )
353 simplr 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> i e. ( M ... k ) )
354 simpr 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> j e. ( ( i + 1 ) ... ( N - 1 ) ) )
355 3 3ad2ant1 
 |-  ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> P : ( M ... N ) --> RR )
356 elfzelz 
 |-  ( j e. ( ( i + 1 ) ... ( N - 1 ) ) -> j e. ZZ )
357 356 3ad2ant3 
 |-  ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> j e. ZZ )
358 50 3ad2ant1 
 |-  ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> M e. RR )
359 357 zred 
 |-  ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> j e. RR )
360 216 3adant3 
 |-  ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> ( i + 1 ) e. RR )
361 219 3adant3 
 |-  ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> M < ( i + 1 ) )
362 elfzle1 
 |-  ( j e. ( ( i + 1 ) ... ( N - 1 ) ) -> ( i + 1 ) <_ j )
363 362 3ad2ant3 
 |-  ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> ( i + 1 ) <_ j )
364 358 360 359 361 363 ltletrd 
 |-  ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> M < j )
365 358 359 364 ltled 
 |-  ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> M <_ j )
366 356 adantl 
 |-  ( ( ph /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> j e. ZZ )
367 366 zred 
 |-  ( ( ph /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> j e. RR )
368 13 adantr 
 |-  ( ( ph /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> N e. RR )
369 1red 
 |-  ( ( ph /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> 1 e. RR )
370 368 369 resubcld 
 |-  ( ( ph /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> ( N - 1 ) e. RR )
371 elfzle2 
 |-  ( j e. ( ( i + 1 ) ... ( N - 1 ) ) -> j <_ ( N - 1 ) )
372 371 adantl 
 |-  ( ( ph /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> j <_ ( N - 1 ) )
373 368 ltm1d 
 |-  ( ( ph /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> ( N - 1 ) < N )
374 367 370 368 372 373 lelttrd 
 |-  ( ( ph /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> j < N )
375 367 368 374 ltled 
 |-  ( ( ph /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> j <_ N )
376 375 3adant2 
 |-  ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> j <_ N )
377 94 3ad2ant1 
 |-  ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> ( M e. ZZ /\ N e. ZZ ) )
378 377 249 syl 
 |-  ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> ( j e. ( M ... N ) <-> ( j e. ZZ /\ M <_ j /\ j <_ N ) ) )
379 357 365 376 378 mpbir3and 
 |-  ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> j e. ( M ... N ) )
380 355 379 ffvelrnd 
 |-  ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> ( P ` j ) e. RR )
381 357 peano2zd 
 |-  ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> ( j + 1 ) e. ZZ )
382 381 zred 
 |-  ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> ( j + 1 ) e. RR )
383 213 3ad2ant2 
 |-  ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> i e. RR )
384 1red 
 |-  ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> 1 e. RR )
385 218 3adant3 
 |-  ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> i < ( i + 1 ) )
386 383 360 359 385 363 ltletrd 
 |-  ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> i < j )
387 383 359 386 ltled 
 |-  ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> i <_ j )
388 383 359 384 387 leadd1dd 
 |-  ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> ( i + 1 ) <_ ( j + 1 ) )
389 358 360 382 361 388 ltletrd 
 |-  ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> M < ( j + 1 ) )
390 358 382 389 ltled 
 |-  ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> M <_ ( j + 1 ) )
391 zltp1le 
 |-  ( ( j e. ZZ /\ N e. ZZ ) -> ( j < N <-> ( j + 1 ) <_ N ) )
392 356 9 391 syl2anr 
 |-  ( ( ph /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> ( j < N <-> ( j + 1 ) <_ N ) )
393 374 392 mpbid 
 |-  ( ( ph /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> ( j + 1 ) <_ N )
394 393 3adant2 
 |-  ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> ( j + 1 ) <_ N )
395 377 292 syl 
 |-  ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> ( ( j + 1 ) e. ( M ... N ) <-> ( ( j + 1 ) e. ZZ /\ M <_ ( j + 1 ) /\ ( j + 1 ) <_ N ) ) )
396 381 390 394 395 mpbir3and 
 |-  ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> ( j + 1 ) e. ( M ... N ) )
397 355 396 ffvelrnd 
 |-  ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> ( P ` ( j + 1 ) ) e. RR )
398 simp1 
 |-  ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> ph )
399 1 3ad2ant1 
 |-  ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> M e. ZZ )
400 eluz 
 |-  ( ( M e. ZZ /\ j e. ZZ ) -> ( j e. ( ZZ>= ` M ) <-> M <_ j ) )
401 399 357 400 syl2anc 
 |-  ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> ( j e. ( ZZ>= ` M ) <-> M <_ j ) )
402 365 401 mpbird 
 |-  ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> j e. ( ZZ>= ` M ) )
403 9 3ad2ant1 
 |-  ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> N e. ZZ )
404 374 3adant2 
 |-  ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> j < N )
405 402 403 404 300 syl3anbrc 
 |-  ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> j e. ( M ..^ N ) )
406 398 405 308 syl2anc 
 |-  ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> ( P ` j ) < ( P ` ( j + 1 ) ) )
407 380 397 406 ltled 
 |-  ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> ( P ` j ) <_ ( P ` ( j + 1 ) ) )
408 352 353 354 407 syl3anc 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> ( P ` j ) <_ ( P ` ( j + 1 ) ) )
409 408 adantlr 
 |-  ( ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> ( P ` j ) <_ ( P ` ( j + 1 ) ) )
410 325 351 409 monoord 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> ( P ` ( i + 1 ) ) <_ ( P ` N ) )
411 232 229 318 320 410 letrd 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> t <_ ( P ` N ) )
412 64 rexrd 
 |-  ( ph -> ( P ` N ) e. RR* )
413 74 412 jca 
 |-  ( ph -> ( ( P ` M ) e. RR* /\ ( P ` N ) e. RR* ) )
414 186 413 syl 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> ( ( P ` M ) e. RR* /\ ( P ` N ) e. RR* ) )
415 elicc1 
 |-  ( ( ( P ` M ) e. RR* /\ ( P ` N ) e. RR* ) -> ( t e. ( ( P ` M ) [,] ( P ` N ) ) <-> ( t e. RR* /\ ( P ` M ) <_ t /\ t <_ ( P ` N ) ) ) )
416 414 415 syl 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> ( t e. ( ( P ` M ) [,] ( P ` N ) ) <-> ( t e. RR* /\ ( P ` M ) <_ t /\ t <_ ( P ` N ) ) ) )
417 188 317 411 416 mpbir3and 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> t e. ( ( P ` M ) [,] ( P ` N ) ) )
418 186 417 5 syl2anc 
 |-  ( ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> A e. CC )
419 simpll 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> ph )
420 234 321 202 139 syl3anbrc 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> i e. ( M ..^ N ) )
421 419 420 6 syl2anc 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> ( t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) |-> A ) e. L^1 )
422 418 421 itgcl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t e. CC )
423 fveq2 
 |-  ( i = k -> ( P ` i ) = ( P ` k ) )
424 fvoveq1 
 |-  ( i = k -> ( P ` ( i + 1 ) ) = ( P ` ( k + 1 ) ) )
425 423 424 oveq12d 
 |-  ( i = k -> ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) = ( ( P ` k ) [,] ( P ` ( k + 1 ) ) ) )
426 425 itgeq1d 
 |-  ( i = k -> S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t = S. ( ( P ` k ) [,] ( P ` ( k + 1 ) ) ) A _d t )
427 185 422 426 fzosump1 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> sum_ i e. ( M ..^ ( k + 1 ) ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t = ( sum_ i e. ( M ..^ k ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t + S. ( ( P ` k ) [,] ( P ` ( k + 1 ) ) ) A _d t ) )
428 427 3adant3 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) /\ S. ( ( P ` M ) [,] ( P ` k ) ) A _d t = sum_ i e. ( M ..^ k ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t ) -> sum_ i e. ( M ..^ ( k + 1 ) ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t = ( sum_ i e. ( M ..^ k ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t + S. ( ( P ` k ) [,] ( P ` ( k + 1 ) ) ) A _d t ) )
429 oveq1 
 |-  ( S. ( ( P ` M ) [,] ( P ` k ) ) A _d t = sum_ i e. ( M ..^ k ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t -> ( S. ( ( P ` M ) [,] ( P ` k ) ) A _d t + S. ( ( P ` k ) [,] ( P ` ( k + 1 ) ) ) A _d t ) = ( sum_ i e. ( M ..^ k ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t + S. ( ( P ` k ) [,] ( P ` ( k + 1 ) ) ) A _d t ) )
430 429 eqcomd 
 |-  ( S. ( ( P ` M ) [,] ( P ` k ) ) A _d t = sum_ i e. ( M ..^ k ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t -> ( sum_ i e. ( M ..^ k ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t + S. ( ( P ` k ) [,] ( P ` ( k + 1 ) ) ) A _d t ) = ( S. ( ( P ` M ) [,] ( P ` k ) ) A _d t + S. ( ( P ` k ) [,] ( P ` ( k + 1 ) ) ) A _d t ) )
431 430 3ad2ant3 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) /\ S. ( ( P ` M ) [,] ( P ` k ) ) A _d t = sum_ i e. ( M ..^ k ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t ) -> ( sum_ i e. ( M ..^ k ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t + S. ( ( P ` k ) [,] ( P ` ( k + 1 ) ) ) A _d t ) = ( S. ( ( P ` M ) [,] ( P ` k ) ) A _d t + S. ( ( P ` k ) [,] ( P ` ( k + 1 ) ) ) A _d t ) )
432 73 adantr 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( P ` M ) e. RR )
433 3 adantr 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> P : ( M ... N ) --> RR )
434 174 adantl 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> k e. ZZ )
435 434 peano2zd 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( k + 1 ) e. ZZ )
436 435 zred 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( k + 1 ) e. RR )
437 176 ltp1d 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> k < ( k + 1 ) )
438 173 176 436 181 437 lttrd 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> M < ( k + 1 ) )
439 173 436 438 ltled 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> M <_ ( k + 1 ) )
440 200 adantl 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> k < N )
441 zltp1le 
 |-  ( ( k e. ZZ /\ N e. ZZ ) -> ( k < N <-> ( k + 1 ) <_ N ) )
442 174 9 441 syl2anr 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( k < N <-> ( k + 1 ) <_ N ) )
443 440 442 mpbid 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( k + 1 ) <_ N )
444 94 adantr 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( M e. ZZ /\ N e. ZZ ) )
445 elfz1 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( k + 1 ) e. ( M ... N ) <-> ( ( k + 1 ) e. ZZ /\ M <_ ( k + 1 ) /\ ( k + 1 ) <_ N ) ) )
446 444 445 syl 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( ( k + 1 ) e. ( M ... N ) <-> ( ( k + 1 ) e. ZZ /\ M <_ ( k + 1 ) /\ ( k + 1 ) <_ N ) ) )
447 435 439 443 446 mpbir3and 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( k + 1 ) e. ( M ... N ) )
448 433 447 ffvelrnd 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( P ` ( k + 1 ) ) e. RR )
449 13 adantr 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> N e. RR )
450 176 449 440 ltled 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> k <_ N )
451 elfz1 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( k e. ( M ... N ) <-> ( k e. ZZ /\ M <_ k /\ k <_ N ) ) )
452 444 451 syl 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( k e. ( M ... N ) <-> ( k e. ZZ /\ M <_ k /\ k <_ N ) ) )
453 434 182 450 452 mpbir3and 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> k e. ( M ... N ) )
454 433 453 ffvelrnd 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( P ` k ) e. RR )
455 454 rexrd 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( P ` k ) e. RR* )
456 3 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> P : ( M ... N ) --> RR )
457 456 206 ffvelrnd 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... k ) ) -> ( P ` i ) e. RR )
458 3 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> P : ( M ... N ) --> RR )
459 elfzelz 
 |-  ( i e. ( M ... ( k - 1 ) ) -> i e. ZZ )
460 459 adantl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> i e. ZZ )
461 elfzle1 
 |-  ( i e. ( M ... ( k - 1 ) ) -> M <_ i )
462 461 adantl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> M <_ i )
463 460 zred 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> i e. RR )
464 13 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> N e. RR )
465 176 adantr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> k e. RR )
466 1red 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> 1 e. RR )
467 465 466 resubcld 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> ( k - 1 ) e. RR )
468 elfzle2 
 |-  ( i e. ( M ... ( k - 1 ) ) -> i <_ ( k - 1 ) )
469 468 adantl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> i <_ ( k - 1 ) )
470 465 ltm1d 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> ( k - 1 ) < k )
471 463 467 465 469 470 lelttrd 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> i < k )
472 440 adantr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> k < N )
473 463 465 464 471 472 lttrd 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> i < N )
474 463 464 473 ltled 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> i <_ N )
475 94 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> ( M e. ZZ /\ N e. ZZ ) )
476 475 96 syl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> ( i e. ( M ... N ) <-> ( i e. ZZ /\ M <_ i /\ i <_ N ) ) )
477 460 462 474 476 mpbir3and 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> i e. ( M ... N ) )
478 458 477 ffvelrnd 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> ( P ` i ) e. RR )
479 460 peano2zd 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> ( i + 1 ) e. ZZ )
480 50 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> M e. RR )
481 463 466 readdcld 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> ( i + 1 ) e. RR )
482 463 ltp1d 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> i < ( i + 1 ) )
483 480 463 481 462 482 lelttrd 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> M < ( i + 1 ) )
484 480 481 483 ltled 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> M <_ ( i + 1 ) )
485 zltp1le 
 |-  ( ( i e. ZZ /\ k e. ZZ ) -> ( i < k <-> ( i + 1 ) <_ k ) )
486 459 434 485 syl2anr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> ( i < k <-> ( i + 1 ) <_ k ) )
487 471 486 mpbid 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> ( i + 1 ) <_ k )
488 481 465 464 487 472 lelttrd 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> ( i + 1 ) < N )
489 481 464 488 ltled 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> ( i + 1 ) <_ N )
490 475 131 syl 
 |-  ( ( ( 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 ) ) )
491 479 484 489 490 mpbir3and 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> ( i + 1 ) e. ( M ... N ) )
492 458 491 ffvelrnd 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> ( P ` ( i + 1 ) ) e. RR )
493 simpll 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> ph )
494 elfzuz 
 |-  ( i e. ( M ... ( k - 1 ) ) -> i e. ( ZZ>= ` M ) )
495 494 adantl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> i e. ( ZZ>= ` M ) )
496 9 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> N e. ZZ )
497 495 496 473 139 syl3anbrc 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> i e. ( M ..^ N ) )
498 493 497 4 syl2anc 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> ( P ` i ) < ( P ` ( i + 1 ) ) )
499 478 492 498 ltled 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ... ( k - 1 ) ) ) -> ( P ` i ) <_ ( P ` ( i + 1 ) ) )
500 185 457 499 monoord 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( P ` M ) <_ ( P ` k ) )
501 9 adantr 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> N e. ZZ )
502 elfzo2 
 |-  ( k e. ( M ..^ N ) <-> ( k e. ( ZZ>= ` M ) /\ N e. ZZ /\ k < N ) )
503 185 501 440 502 syl3anbrc 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> k e. ( M ..^ N ) )
504 eleq1 
 |-  ( i = k -> ( i e. ( M ..^ N ) <-> k e. ( M ..^ N ) ) )
505 504 anbi2d 
 |-  ( i = k -> ( ( ph /\ i e. ( M ..^ N ) ) <-> ( ph /\ k e. ( M ..^ N ) ) ) )
506 423 424 breq12d 
 |-  ( i = k -> ( ( P ` i ) < ( P ` ( i + 1 ) ) <-> ( P ` k ) < ( P ` ( k + 1 ) ) ) )
507 505 506 imbi12d 
 |-  ( i = k -> ( ( ( ph /\ i e. ( M ..^ N ) ) -> ( P ` i ) < ( P ` ( i + 1 ) ) ) <-> ( ( ph /\ k e. ( M ..^ N ) ) -> ( P ` k ) < ( P ` ( k + 1 ) ) ) ) )
508 507 4 chvarvv 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( P ` k ) < ( P ` ( k + 1 ) ) )
509 503 508 syldan 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( P ` k ) < ( P ` ( k + 1 ) ) )
510 454 448 509 ltled 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( P ` k ) <_ ( P ` ( k + 1 ) ) )
511 74 adantr 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( P ` M ) e. RR* )
512 448 rexrd 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( P ` ( k + 1 ) ) e. RR* )
513 elicc1 
 |-  ( ( ( P ` M ) e. RR* /\ ( P ` ( k + 1 ) ) e. RR* ) -> ( ( P ` k ) e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) <-> ( ( P ` k ) e. RR* /\ ( P ` M ) <_ ( P ` k ) /\ ( P ` k ) <_ ( P ` ( k + 1 ) ) ) ) )
514 511 512 513 syl2anc 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( ( P ` k ) e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) <-> ( ( P ` k ) e. RR* /\ ( P ` M ) <_ ( P ` k ) /\ ( P ` k ) <_ ( P ` ( k + 1 ) ) ) ) )
515 455 500 510 514 mpbir3and 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( P ` k ) e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) )
516 simpll 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ t e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) ) -> ph )
517 eliccxr 
 |-  ( t e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) -> t e. RR* )
518 517 adantl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ t e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) ) -> t e. RR* )
519 74 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ t e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) ) -> ( P ` M ) e. RR* )
520 512 adantr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ t e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) ) -> ( P ` ( k + 1 ) ) e. RR* )
521 simpr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ t e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) ) -> t e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) )
522 iccgelb 
 |-  ( ( ( P ` M ) e. RR* /\ ( P ` ( k + 1 ) ) e. RR* /\ t e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) ) -> ( P ` M ) <_ t )
523 519 520 521 522 syl3anc 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ t e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) ) -> ( P ` M ) <_ t )
524 73 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ t e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) ) -> ( P ` M ) e. RR )
525 448 adantr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ t e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) ) -> ( P ` ( k + 1 ) ) e. RR )
526 eliccre 
 |-  ( ( ( P ` M ) e. RR /\ ( P ` ( k + 1 ) ) e. RR /\ t e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) ) -> t e. RR )
527 524 525 521 526 syl3anc 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ t e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) ) -> t e. RR )
528 64 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ t e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) ) -> ( P ` N ) e. RR )
529 iccleub 
 |-  ( ( ( P ` M ) e. RR* /\ ( P ` ( k + 1 ) ) e. RR* /\ t e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) ) -> t <_ ( P ` ( k + 1 ) ) )
530 519 520 521 529 syl3anc 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ t e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) ) -> t <_ ( P ` ( k + 1 ) ) )
531 eluz2 
 |-  ( N e. ( ZZ>= ` ( k + 1 ) ) <-> ( ( k + 1 ) e. ZZ /\ N e. ZZ /\ ( k + 1 ) <_ N ) )
532 435 501 443 531 syl3anbrc 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> N e. ( ZZ>= ` ( k + 1 ) ) )
533 3 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... N ) ) -> P : ( M ... N ) --> RR )
534 1 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... N ) ) -> M e. ZZ )
535 9 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... N ) ) -> N e. ZZ )
536 elfzelz 
 |-  ( i e. ( ( k + 1 ) ... N ) -> i e. ZZ )
537 536 adantl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... N ) ) -> i e. ZZ )
538 50 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... N ) ) -> M e. RR )
539 537 zred 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... N ) ) -> i e. RR )
540 176 adantr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... N ) ) -> k e. RR )
541 181 adantr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... N ) ) -> M < k )
542 175 adantr 
 |-  ( ( k e. ( ( M + 1 ) ..^ N ) /\ i e. ( ( k + 1 ) ... N ) ) -> k e. RR )
543 1red 
 |-  ( ( k e. ( ( M + 1 ) ..^ N ) /\ i e. ( ( k + 1 ) ... N ) ) -> 1 e. RR )
544 542 543 readdcld 
 |-  ( ( k e. ( ( M + 1 ) ..^ N ) /\ i e. ( ( k + 1 ) ... N ) ) -> ( k + 1 ) e. RR )
545 536 zred 
 |-  ( i e. ( ( k + 1 ) ... N ) -> i e. RR )
546 545 adantl 
 |-  ( ( k e. ( ( M + 1 ) ..^ N ) /\ i e. ( ( k + 1 ) ... N ) ) -> i e. RR )
547 542 ltp1d 
 |-  ( ( k e. ( ( M + 1 ) ..^ N ) /\ i e. ( ( k + 1 ) ... N ) ) -> k < ( k + 1 ) )
548 elfzle1 
 |-  ( i e. ( ( k + 1 ) ... N ) -> ( k + 1 ) <_ i )
549 548 adantl 
 |-  ( ( k e. ( ( M + 1 ) ..^ N ) /\ i e. ( ( k + 1 ) ... N ) ) -> ( k + 1 ) <_ i )
550 542 544 546 547 549 ltletrd 
 |-  ( ( k e. ( ( M + 1 ) ..^ N ) /\ i e. ( ( k + 1 ) ... N ) ) -> k < i )
551 550 adantll 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... N ) ) -> k < i )
552 538 540 539 541 551 lttrd 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... N ) ) -> M < i )
553 538 539 552 ltled 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... N ) ) -> M <_ i )
554 elfzle2 
 |-  ( i e. ( ( k + 1 ) ... N ) -> i <_ N )
555 554 adantl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... N ) ) -> i <_ N )
556 534 535 537 553 555 elfzd 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... N ) ) -> i e. ( M ... N ) )
557 533 556 ffvelrnd 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... N ) ) -> ( P ` i ) e. RR )
558 3 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> P : ( M ... N ) --> RR )
559 1 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> M e. ZZ )
560 9 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> N e. ZZ )
561 elfzelz 
 |-  ( i e. ( ( k + 1 ) ... ( N - 1 ) ) -> i e. ZZ )
562 561 adantl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> i e. ZZ )
563 50 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> M e. RR )
564 562 zred 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> i e. RR )
565 176 adantr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> k e. RR )
566 181 adantr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> M < k )
567 175 adantr 
 |-  ( ( k e. ( ( M + 1 ) ..^ N ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> k e. RR )
568 1red 
 |-  ( ( k e. ( ( M + 1 ) ..^ N ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> 1 e. RR )
569 567 568 readdcld 
 |-  ( ( k e. ( ( M + 1 ) ..^ N ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> ( k + 1 ) e. RR )
570 561 zred 
 |-  ( i e. ( ( k + 1 ) ... ( N - 1 ) ) -> i e. RR )
571 570 adantl 
 |-  ( ( k e. ( ( M + 1 ) ..^ N ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> i e. RR )
572 567 ltp1d 
 |-  ( ( k e. ( ( M + 1 ) ..^ N ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> k < ( k + 1 ) )
573 elfzle1 
 |-  ( i e. ( ( k + 1 ) ... ( N - 1 ) ) -> ( k + 1 ) <_ i )
574 573 adantl 
 |-  ( ( k e. ( ( M + 1 ) ..^ N ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> ( k + 1 ) <_ i )
575 567 569 571 572 574 ltletrd 
 |-  ( ( k e. ( ( M + 1 ) ..^ N ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> k < i )
576 575 adantll 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> k < i )
577 563 565 564 566 576 lttrd 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> M < i )
578 563 564 577 ltled 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> M <_ i )
579 570 adantl 
 |-  ( ( ph /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> i e. RR )
580 13 adantr 
 |-  ( ( ph /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> N e. RR )
581 1red 
 |-  ( ( ph /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> 1 e. RR )
582 580 581 resubcld 
 |-  ( ( ph /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> ( N - 1 ) e. RR )
583 elfzle2 
 |-  ( i e. ( ( k + 1 ) ... ( N - 1 ) ) -> i <_ ( N - 1 ) )
584 583 adantl 
 |-  ( ( ph /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> i <_ ( N - 1 ) )
585 580 ltm1d 
 |-  ( ( ph /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> ( N - 1 ) < N )
586 579 582 580 584 585 lelttrd 
 |-  ( ( ph /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> i < N )
587 579 580 586 ltled 
 |-  ( ( ph /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> i <_ N )
588 587 adantlr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> i <_ N )
589 559 560 562 578 588 elfzd 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> i e. ( M ... N ) )
590 558 589 ffvelrnd 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> ( P ` i ) e. RR )
591 562 peano2zd 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> ( i + 1 ) e. ZZ )
592 591 zred 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> ( i + 1 ) e. RR )
593 564 ltp1d 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> i < ( i + 1 ) )
594 565 564 592 576 593 lttrd 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> k < ( i + 1 ) )
595 563 565 592 566 594 lttrd 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> M < ( i + 1 ) )
596 563 592 595 ltled 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> M <_ ( i + 1 ) )
597 586 adantlr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> i < N )
598 561 501 128 syl2anr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> ( i < N <-> ( i + 1 ) <_ N ) )
599 597 598 mpbid 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> ( i + 1 ) <_ N )
600 559 560 591 596 599 elfzd 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> ( i + 1 ) e. ( M ... N ) )
601 558 600 ffvelrnd 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> ( P ` ( i + 1 ) ) e. RR )
602 simpll 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> ph )
603 eluz2 
 |-  ( i e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ i e. ZZ /\ M <_ i ) )
604 559 562 578 603 syl3anbrc 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> i e. ( ZZ>= ` M ) )
605 604 560 597 139 syl3anbrc 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> i e. ( M ..^ N ) )
606 602 605 4 syl2anc 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> ( P ` i ) < ( P ` ( i + 1 ) ) )
607 590 601 606 ltled 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( ( k + 1 ) ... ( N - 1 ) ) ) -> ( P ` i ) <_ ( P ` ( i + 1 ) ) )
608 532 557 607 monoord 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( P ` ( k + 1 ) ) <_ ( P ` N ) )
609 608 adantr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ t e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) ) -> ( P ` ( k + 1 ) ) <_ ( P ` N ) )
610 527 525 528 530 609 letrd 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ t e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) ) -> t <_ ( P ` N ) )
611 413 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ t e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) ) -> ( ( P ` M ) e. RR* /\ ( P ` N ) e. RR* ) )
612 611 415 syl 
 |-  ( ( ( 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 ) ) ) )
613 518 523 610 612 mpbir3and 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ t e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) ) -> t e. ( ( P ` M ) [,] ( P ` N ) ) )
614 516 613 5 syl2anc 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ t e. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) ) -> A e. CC )
615 nfv 
 |-  F/ t ( ph /\ k e. ( ( M + 1 ) ..^ N ) )
616 1 adantr 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> M e. ZZ )
617 elfzouz 
 |-  ( k e. ( ( M + 1 ) ..^ N ) -> k e. ( ZZ>= ` ( M + 1 ) ) )
618 617 adantl 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> k e. ( ZZ>= ` ( M + 1 ) ) )
619 simpll 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ..^ k ) ) -> ph )
620 elfzouz 
 |-  ( i e. ( M ..^ k ) -> i e. ( ZZ>= ` M ) )
621 620 adantl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ..^ k ) ) -> i e. ( ZZ>= ` M ) )
622 9 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ..^ k ) ) -> N e. ZZ )
623 elfzoelz 
 |-  ( i e. ( M ..^ k ) -> i e. ZZ )
624 623 zred 
 |-  ( i e. ( M ..^ k ) -> i e. RR )
625 624 adantl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ..^ k ) ) -> i e. RR )
626 176 adantr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ..^ k ) ) -> k e. RR )
627 13 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ..^ k ) ) -> N e. RR )
628 elfzolt2 
 |-  ( i e. ( M ..^ k ) -> i < k )
629 628 adantl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ..^ k ) ) -> i < k )
630 440 adantr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ..^ k ) ) -> k < N )
631 625 626 627 629 630 lttrd 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ..^ k ) ) -> i < N )
632 621 622 631 139 syl3anbrc 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ..^ k ) ) -> i e. ( M ..^ N ) )
633 619 632 4 syl2anc 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ..^ k ) ) -> ( P ` i ) < ( P ` ( i + 1 ) ) )
634 simpll 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ t e. ( ( P ` M ) [,] ( P ` k ) ) ) -> ph )
635 73 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ t e. ( ( P ` M ) [,] ( P ` k ) ) ) -> ( P ` M ) e. RR )
636 64 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ t e. ( ( P ` M ) [,] ( P ` k ) ) ) -> ( P ` N ) e. RR )
637 454 adantr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ t e. ( ( P ` M ) [,] ( P ` k ) ) ) -> ( P ` k ) e. RR )
638 simpr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ t e. ( ( P ` M ) [,] ( P ` k ) ) ) -> t e. ( ( P ` M ) [,] ( P ` k ) ) )
639 eliccre 
 |-  ( ( ( P ` M ) e. RR /\ ( P ` k ) e. RR /\ t e. ( ( P ` M ) [,] ( P ` k ) ) ) -> t e. RR )
640 635 637 638 639 syl3anc 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ t e. ( ( P ` M ) [,] ( P ` k ) ) ) -> t e. RR )
641 74 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ t e. ( ( P ` M ) [,] ( P ` k ) ) ) -> ( P ` M ) e. RR* )
642 455 adantr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ t e. ( ( P ` M ) [,] ( P ` k ) ) ) -> ( P ` k ) e. RR* )
643 iccgelb 
 |-  ( ( ( P ` M ) e. RR* /\ ( P ` k ) e. RR* /\ t e. ( ( P ` M ) [,] ( P ` k ) ) ) -> ( P ` M ) <_ t )
644 641 642 638 643 syl3anc 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ t e. ( ( P ` M ) [,] ( P ` k ) ) ) -> ( P ` M ) <_ t )
645 iccleub 
 |-  ( ( ( P ` M ) e. RR* /\ ( P ` k ) e. RR* /\ t e. ( ( P ` M ) [,] ( P ` k ) ) ) -> t <_ ( P ` k ) )
646 641 642 638 645 syl3anc 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ t e. ( ( P ` M ) [,] ( P ` k ) ) ) -> t <_ ( P ` k ) )
647 elfzouz2 
 |-  ( k e. ( ( M + 1 ) ..^ N ) -> N e. ( ZZ>= ` k ) )
648 647 adantl 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> N e. ( ZZ>= ` k ) )
649 3 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( k ... N ) ) -> P : ( M ... N ) --> RR )
650 1 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( k ... N ) ) -> M e. ZZ )
651 9 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( k ... N ) ) -> N e. ZZ )
652 elfzelz 
 |-  ( i e. ( k ... N ) -> i e. ZZ )
653 652 adantl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( k ... N ) ) -> i e. ZZ )
654 50 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( k ... N ) ) -> M e. RR )
655 653 zred 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( k ... N ) ) -> i e. RR )
656 176 adantr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( k ... N ) ) -> k e. RR )
657 181 adantr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( k ... N ) ) -> M < k )
658 elfzle1 
 |-  ( i e. ( k ... N ) -> k <_ i )
659 658 adantl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( k ... N ) ) -> k <_ i )
660 654 656 655 657 659 ltletrd 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( k ... N ) ) -> M < i )
661 654 655 660 ltled 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( k ... N ) ) -> M <_ i )
662 elfzle2 
 |-  ( i e. ( k ... N ) -> i <_ N )
663 662 adantl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( k ... N ) ) -> i <_ N )
664 650 651 653 661 663 elfzd 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( k ... N ) ) -> i e. ( M ... N ) )
665 649 664 ffvelrnd 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( k ... N ) ) -> ( P ` i ) e. RR )
666 3 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( k ... ( N - 1 ) ) ) -> P : ( M ... N ) --> RR )
667 1 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( k ... ( N - 1 ) ) ) -> M e. ZZ )
668 9 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( k ... ( N - 1 ) ) ) -> N e. ZZ )
669 elfzelz 
 |-  ( i e. ( k ... ( N - 1 ) ) -> i e. ZZ )
670 669 adantl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( k ... ( N - 1 ) ) ) -> i e. ZZ )
671 50 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( k ... ( N - 1 ) ) ) -> M e. RR )
672 670 zred 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( k ... ( N - 1 ) ) ) -> i e. RR )
673 176 adantr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( k ... ( N - 1 ) ) ) -> k e. RR )
674 181 adantr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( k ... ( N - 1 ) ) ) -> M < k )
675 elfzle1 
 |-  ( i e. ( k ... ( N - 1 ) ) -> k <_ i )
676 675 adantl 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( k ... ( N - 1 ) ) ) -> k <_ i )
677 671 673 672 674 676 ltletrd 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( k ... ( N - 1 ) ) ) -> M < i )
678 671 672 677 ltled 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( k ... ( N - 1 ) ) ) -> M <_ i )
679 669 zred 
 |-  ( i e. ( k ... ( N - 1 ) ) -> i e. RR )
680 679 adantl 
 |-  ( ( ph /\ i e. ( k ... ( N - 1 ) ) ) -> i e. RR )
681 13 adantr 
 |-  ( ( ph /\ i e. ( k ... ( N - 1 ) ) ) -> N e. RR )
682 1red 
 |-  ( ( ph /\ i e. ( k ... ( N - 1 ) ) ) -> 1 e. RR )
683 681 682 resubcld 
 |-  ( ( ph /\ i e. ( k ... ( N - 1 ) ) ) -> ( N - 1 ) e. RR )
684 elfzle2 
 |-  ( i e. ( k ... ( N - 1 ) ) -> i <_ ( N - 1 ) )
685 684 adantl 
 |-  ( ( ph /\ i e. ( k ... ( N - 1 ) ) ) -> i <_ ( N - 1 ) )
686 681 ltm1d 
 |-  ( ( ph /\ i e. ( k ... ( N - 1 ) ) ) -> ( N - 1 ) < N )
687 680 683 681 685 686 lelttrd 
 |-  ( ( ph /\ i e. ( k ... ( N - 1 ) ) ) -> i < N )
688 680 681 687 ltled 
 |-  ( ( ph /\ i e. ( k ... ( N - 1 ) ) ) -> i <_ N )
689 688 adantlr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( k ... ( N - 1 ) ) ) -> i <_ N )
690 667 668 670 678 689 elfzd 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( k ... ( N - 1 ) ) ) -> i e. ( M ... N ) )
691 666 690 ffvelrnd 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( k ... ( N - 1 ) ) ) -> ( P ` i ) e. RR )
692 670 peano2zd 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( k ... ( N - 1 ) ) ) -> ( i + 1 ) e. ZZ )
693 692 zred 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( k ... ( N - 1 ) ) ) -> ( i + 1 ) e. RR )
694 672 ltp1d 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( k ... ( N - 1 ) ) ) -> i < ( i + 1 ) )
695 671 672 693 678 694 lelttrd 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( k ... ( N - 1 ) ) ) -> M < ( i + 1 ) )
696 671 693 695 ltled 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( k ... ( N - 1 ) ) ) -> M <_ ( i + 1 ) )
697 669 9 128 syl2anr 
 |-  ( ( ph /\ i e. ( k ... ( N - 1 ) ) ) -> ( i < N <-> ( i + 1 ) <_ N ) )
698 687 697 mpbid 
 |-  ( ( ph /\ i e. ( k ... ( N - 1 ) ) ) -> ( i + 1 ) <_ N )
699 698 adantlr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( k ... ( N - 1 ) ) ) -> ( i + 1 ) <_ N )
700 667 668 692 696 699 elfzd 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( k ... ( N - 1 ) ) ) -> ( i + 1 ) e. ( M ... N ) )
701 666 700 ffvelrnd 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( k ... ( N - 1 ) ) ) -> ( P ` ( i + 1 ) ) e. RR )
702 simpll 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( k ... ( N - 1 ) ) ) -> ph )
703 667 670 678 603 syl3anbrc 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( k ... ( N - 1 ) ) ) -> i e. ( ZZ>= ` M ) )
704 687 adantlr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( k ... ( N - 1 ) ) ) -> i < N )
705 703 668 704 139 syl3anbrc 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( k ... ( N - 1 ) ) ) -> i e. ( M ..^ N ) )
706 702 705 4 syl2anc 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( k ... ( N - 1 ) ) ) -> ( P ` i ) < ( P ` ( i + 1 ) ) )
707 691 701 706 ltled 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( k ... ( N - 1 ) ) ) -> ( P ` i ) <_ ( P ` ( i + 1 ) ) )
708 648 665 707 monoord 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( P ` k ) <_ ( P ` N ) )
709 708 adantr 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ t e. ( ( P ` M ) [,] ( P ` k ) ) ) -> ( P ` k ) <_ ( P ` N ) )
710 640 637 636 646 709 letrd 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ t e. ( ( P ` M ) [,] ( P ` k ) ) ) -> t <_ ( P ` N ) )
711 635 636 640 644 710 eliccd 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ t e. ( ( P ` M ) [,] ( P ` k ) ) ) -> t e. ( ( P ` M ) [,] ( P ` N ) ) )
712 634 711 5 syl2anc 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ t e. ( ( P ` M ) [,] ( P ` k ) ) ) -> A e. CC )
713 619 632 6 syl2anc 
 |-  ( ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) /\ i e. ( M ..^ k ) ) -> ( t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) |-> A ) e. L^1 )
714 615 616 618 457 633 712 713 iblspltprt 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( t e. ( ( P ` M ) [,] ( P ` k ) ) |-> A ) e. L^1 )
715 425 mpteq1d 
 |-  ( i = k -> ( t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) |-> A ) = ( t e. ( ( P ` k ) [,] ( P ` ( k + 1 ) ) ) |-> A ) )
716 715 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 ) )
717 505 716 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 ) ) )
718 717 6 chvarvv 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( t e. ( ( P ` k ) [,] ( P ` ( k + 1 ) ) ) |-> A ) e. L^1 )
719 503 718 syldan 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( t e. ( ( P ` k ) [,] ( P ` ( k + 1 ) ) ) |-> A ) e. L^1 )
720 432 448 515 614 714 719 itgspliticc 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> S. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) A _d t = ( S. ( ( P ` M ) [,] ( P ` k ) ) A _d t + S. ( ( P ` k ) [,] ( P ` ( k + 1 ) ) ) A _d t ) )
721 720 eqcomd 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> ( S. ( ( P ` M ) [,] ( P ` k ) ) A _d t + S. ( ( P ` k ) [,] ( P ` ( k + 1 ) ) ) A _d t ) = S. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) A _d t )
722 721 3adant3 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) /\ S. ( ( P ` M ) [,] ( P ` k ) ) A _d t = sum_ i e. ( M ..^ k ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t ) -> ( S. ( ( P ` M ) [,] ( P ` k ) ) A _d t + S. ( ( P ` k ) [,] ( P ` ( k + 1 ) ) ) A _d t ) = S. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) A _d t )
723 428 431 722 3eqtrrd 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) /\ S. ( ( P ` M ) [,] ( P ` k ) ) A _d t = sum_ i e. ( M ..^ k ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t ) -> S. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) A _d t = sum_ i e. ( M ..^ ( k + 1 ) ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t )
724 169 170 172 723 syl3anc 
 |-  ( ( k e. ( ( M + 1 ) ..^ N ) /\ ( ph -> S. ( ( P ` M ) [,] ( P ` k ) ) A _d t = sum_ i e. ( M ..^ k ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t ) /\ ph ) -> S. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) A _d t = sum_ i e. ( M ..^ ( k + 1 ) ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t )
725 724 3exp 
 |-  ( k e. ( ( M + 1 ) ..^ N ) -> ( ( ph -> S. ( ( P ` M ) [,] ( P ` k ) ) A _d t = sum_ i e. ( M ..^ k ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t ) -> ( ph -> S. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) A _d t = sum_ i e. ( M ..^ ( k + 1 ) ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t ) ) )
726 22 29 36 43 168 725 fzind2 
 |-  ( N e. ( ( M + 1 ) ... N ) -> ( ph -> S. ( ( P ` M ) [,] ( P ` N ) ) A _d t = sum_ i e. ( M ..^ N ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t ) )
727 15 726 mpcom 
 |-  ( ph -> S. ( ( P ` M ) [,] ( P ` N ) ) A _d t = sum_ i e. ( M ..^ N ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t )