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