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	ffvelcdmd	\|- ( ( 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	ffvelcdmd	\|- ( 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	ffvelcdmd	\|- ( 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	ffvelcdmd	\|- ( 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	ffvelcdmd	\|- ( ( 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	ffvelcdmd	\|- ( ( 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	ffvelcdmd	\|- ( ( 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	ffvelcdmd	\|- ( ( ( ( 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	ffvelcdmd	\|- ( ( ( ( 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	ffvelcdmd	\|- ( ( ( ( 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	ffvelcdmd	\|- ( ( ( ( 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	ffvelcdmd	\|- ( ( ( ( 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	ffvelcdmd	\|- ( ( ( ( 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	ffvelcdmd	\|- ( ( 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	ffvelcdmd	\|- ( ( 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	ffvelcdmd	\|- ( ( 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	ffvelcdmd	\|- ( ( 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	ffvelcdmd	\|- ( ( ( 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	ffvelcdmd	\|- ( ( ( 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	ffvelcdmd	\|- ( ( ( 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	ffvelcdmd	\|- ( ( ( 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	ffvelcdmd	\|- ( ( ( 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	ffvelcdmd	\|- ( ( ( 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	ffvelcdmd	\|- ( ( ( 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	ffvelcdmd	\|- ( ( ( 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	ffvelcdmd	\|- ( ( ( 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 )

Metamath Proof Explorer

Theorem itgspltprt

Proof