Theorem itgspltprt 32020

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

Hypotheses

Ref	Expression
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

Ref	Expression
itgspltprt	|- ( ph -> S. ( ( P ` M ) [,] ( P ` N ) ) A _d t = sum_ i e. ( M..^ N ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t )

Distinct variable groups:   A, i   i, M, t   i, N, t   P, i, t   ph, i, t

Allowed substitution hint:   A( t)

Proof of Theorem itgspltprt

Dummy variables j k are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		itgspltprt.1	. . . . . 6 |- ( ph -> M e. ZZ )
2	1	peano2zd 10968	. . . . 5 |- ( ph -> ( M + 1 ) e. ZZ )
3		itgspltprt.2	. . . . . 6 |- ( ph -> N e. ( ZZ>= ` ( M + 1 ) ) )
4		eluzelz 11091	. . . . . 6 |- ( N e. ( ZZ>= ` ( M + 1 ) ) -> N e. ZZ )
5	3, 4	syl 16	. . . . 5 |- ( ph -> N e. ZZ )
6	2, 5, 5	3jca 1174	. . . 4 |- ( ph -> ( ( M + 1 ) e. ZZ /\ N e. ZZ /\ N e. ZZ ) )
7		eluzle 11094	. . . . 5 |- ( N e. ( ZZ>= ` ( M + 1 ) ) -> ( M + 1 ) <_ N )
8	3, 7	syl 16	. . . 4 |- ( ph -> ( M + 1 ) <_ N )
9		eluzelre 11092	. . . . . 6 |- ( N e. ( ZZ>= ` ( M + 1 ) ) -> N e. RR )
10	3, 9	syl 16	. . . . 5 |- ( ph -> N e. RR )
11	10	leidd 10115	. . . 4 |- ( ph -> N <_ N )
12	6, 8, 11	jca32 533	. . 3 |- ( ph -> ( ( ( M + 1 ) e. ZZ /\ N e. ZZ /\ N e. ZZ ) /\ ( ( M + 1 ) <_ N /\ N <_ N ) ) )
13		elfz2 11682	. . 3 |- ( N e. ( ( M + 1 ) ... N ) <-> ( ( ( M + 1 ) e. ZZ /\ N e. ZZ /\ N e. ZZ ) /\ ( ( M + 1 ) <_ N /\ N <_ N ) ) )
14	12, 13	sylibr 212	. 2 |- ( ph -> N e. ( ( M + 1 ) ... N ) )
15		fveq2 5848	. . . . . . 7 |- ( j = ( M + 1 ) -> ( P ` j ) = ( P ` ( M + 1 ) ) )
16	15	oveq2d 6286	. . . . . 6 |- ( j = ( M + 1 ) -> ( ( P ` M ) [,] ( P ` j ) ) = ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) )
17	16	itgeq1d 31997	. . . . 5 |- ( j = ( M + 1 ) -> S. ( ( P ` M ) [,] ( P ` j ) ) A _d t = S. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) A _d t )
18		oveq2 6278	. . . . . 6 |- ( j = ( M + 1 ) -> ( M..^ j ) = ( M..^ ( M + 1 ) ) )
19	18	sumeq1d 13608	. . . . 5 |- ( 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 )
20	17, 19	eqeq12d 2476	. . . 4 |- ( 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 ) )
21	20	imbi2d 314	. . 3 |- ( 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 ) ) )
22		fveq2 5848	. . . . . . 7 |- ( j = k -> ( P ` j ) = ( P ` k ) )
23	22	oveq2d 6286	. . . . . 6 |- ( j = k -> ( ( P ` M ) [,] ( P ` j ) ) = ( ( P ` M ) [,] ( P ` k ) ) )
24	23	itgeq1d 31997	. . . . 5 |- ( j = k -> S. ( ( P ` M ) [,] ( P ` j ) ) A _d t = S. ( ( P ` M ) [,] ( P ` k ) ) A _d t )
25		oveq2 6278	. . . . . 6 |- ( j = k -> ( M..^ j ) = ( M..^ k ) )
26	25	sumeq1d 13608	. . . . 5 |- ( 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 )
27	24, 26	eqeq12d 2476	. . . 4 |- ( 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 ) )
28	27	imbi2d 314	. . 3 |- ( 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 ) ) )
29		fveq2 5848	. . . . . . 7 |- ( j = ( k + 1 ) -> ( P ` j ) = ( P ` ( k + 1 ) ) )
30	29	oveq2d 6286	. . . . . 6 |- ( j = ( k + 1 ) -> ( ( P ` M ) [,] ( P ` j ) ) = ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) )
31	30	itgeq1d 31997	. . . . 5 |- ( j = ( k + 1 ) -> S. ( ( P ` M ) [,] ( P ` j ) ) A _d t = S. ( ( P ` M ) [,] ( P ` ( k + 1 ) ) ) A _d t )
32		oveq2 6278	. . . . . 6 |- ( j = ( k + 1 ) -> ( M..^ j ) = ( M..^ ( k + 1 ) ) )
33	32	sumeq1d 13608	. . . . 5 |- ( 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 )
34	31, 33	eqeq12d 2476	. . . 4 |- ( 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 ) )
35	34	imbi2d 314	. . 3 |- ( 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 ) ) )
36		fveq2 5848	. . . . . . 7 |- ( j = N -> ( P ` j ) = ( P ` N ) )
37	36	oveq2d 6286	. . . . . 6 |- ( j = N -> ( ( P ` M ) [,] ( P ` j ) ) = ( ( P ` M ) [,] ( P ` N ) ) )
38	37	itgeq1d 31997	. . . . 5 |- ( j = N -> S. ( ( P ` M ) [,] ( P ` j ) ) A _d t = S. ( ( P ` M ) [,] ( P ` N ) ) A _d t )
39		oveq2 6278	. . . . . 6 |- ( j = N -> ( M..^ j ) = ( M..^ N ) )
40	39	sumeq1d 13608	. . . . 5 |- ( 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 )
41	38, 40	eqeq12d 2476	. . . 4 |- ( 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 ) )
42	41	imbi2d 314	. . 3 |- ( 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 ) ) )
43	1	adantl 464	. . . . . . . 8 |- ( ( N e. ( ZZ>= ` ( M + 1 ) ) /\ ph ) -> M e. ZZ )
44		fzval3 11866	. . . . . . . 8 |- ( M e. ZZ -> ( M ... M ) = ( M..^ ( M + 1 ) ) )
45	43, 44	syl 16	. . . . . . 7 |- ( ( N e. ( ZZ>= ` ( M + 1 ) ) /\ ph ) -> ( M ... M ) = ( M..^ ( M + 1 ) ) )
46	45	eqcomd 2462	. . . . . 6 |- ( ( N e. ( ZZ>= ` ( M + 1 ) ) /\ ph ) -> ( M..^ ( M + 1 ) ) = ( M ... M ) )
47	46	sumeq1d 13608	. . . . 5 |- ( ( 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 )
48		itgspltprt.3	. . . . . . . . . . . 12 |- ( ph -> P : ( M ... N ) --> RR )
49	48	adantr 463	. . . . . . . . . . 11 |- ( ( ph /\ t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) ) -> P : ( M ... N ) --> RR )
50	1	zred 10965	. . . . . . . . . . . . . . 15 |- ( ph -> M e. RR )
51		1red 9600	. . . . . . . . . . . . . . . . 17 |- ( ph -> 1 e. RR )
52	50, 51	readdcld 9612	. . . . . . . . . . . . . . . 16 |- ( ph -> ( M + 1 ) e. RR )
53	50	ltp1d 10471	. . . . . . . . . . . . . . . 16 |- ( ph -> M < ( M + 1 ) )
54	50, 52, 10, 53, 8	ltletrd 9731	. . . . . . . . . . . . . . 15 |- ( ph -> M < N )
55	50, 10, 54	ltled 9722	. . . . . . . . . . . . . 14 |- ( ph -> M <_ N )
56		eluz 11095	. . . . . . . . . . . . . . 15 |- ( ( M e. ZZ /\ N e. ZZ ) -> ( N e. ( ZZ>= ` M ) <-> M <_ N ) )
57	1, 5, 56	syl2anc 659	. . . . . . . . . . . . . 14 |- ( ph -> ( N e. ( ZZ>= ` M ) <-> M <_ N ) )
58	55, 57	mpbird 232	. . . . . . . . . . . . 13 |- ( ph -> N e. ( ZZ>= ` M ) )
59		eluzfz1 11696	. . . . . . . . . . . . 13 |- ( N e. ( ZZ>= ` M ) -> M e. ( M ... N ) )
60	58, 59	syl 16	. . . . . . . . . . . 12 |- ( ph -> M e. ( M ... N ) )
61	60	adantr 463	. . . . . . . . . . 11 |- ( ( ph /\ t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) ) -> M e. ( M ... N ) )
62	49, 61	ffvelrnd 6008	. . . . . . . . . 10 |- ( ( ph /\ t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) ) -> ( P ` M ) e. RR )
63		elfz1 11680	. . . . . . . . . . . . . 14 |- ( ( M e. ZZ /\ N e. ZZ ) -> ( N e. ( M ... N ) <-> ( N e. ZZ /\ M <_ N /\ N <_ N ) ) )
64	1, 5, 63	syl2anc 659	. . . . . . . . . . . . 13 |- ( ph -> ( N e. ( M ... N ) <-> ( N e. ZZ /\ M <_ N /\ N <_ N ) ) )
65	5, 55, 11, 64	mpbir3and 1177	. . . . . . . . . . . 12 |- ( ph -> N e. ( M ... N ) )
66	48, 65	ffvelrnd 6008	. . . . . . . . . . 11 |- ( ph -> ( P ` N ) e. RR )
67	66	adantr 463	. . . . . . . . . 10 |- ( ( ph /\ t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) ) -> ( P ` N ) e. RR )
68	50	lep1d 10472	. . . . . . . . . . . . . 14 |- ( ph -> M <_ ( M + 1 ) )
69		elfz1 11680	. . . . . . . . . . . . . . 15 |- ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M + 1 ) e. ( M ... N ) <-> ( ( M + 1 ) e. ZZ /\ M <_ ( M + 1 ) /\ ( M + 1 ) <_ N ) ) )
70	1, 5, 69	syl2anc 659	. . . . . . . . . . . . . 14 |- ( ph -> ( ( M + 1 ) e. ( M ... N ) <-> ( ( M + 1 ) e. ZZ /\ M <_ ( M + 1 ) /\ ( M + 1 ) <_ N ) ) )
71	2, 68, 8, 70	mpbir3and 1177	. . . . . . . . . . . . 13 |- ( ph -> ( M + 1 ) e. ( M ... N ) )
72	48, 71	ffvelrnd 6008	. . . . . . . . . . . 12 |- ( ph -> ( P ` ( M + 1 ) ) e. RR )
73	72	adantr 463	. . . . . . . . . . 11 |- ( ( ph /\ t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) ) -> ( P ` ( M + 1 ) ) e. RR )
74		simpr 459	. . . . . . . . . . 11 |- ( ( ph /\ t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) ) -> t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) )
75		eliccre 31782	. . . . . . . . . . 11 |- ( ( ( P ` M ) e. RR /\ ( P ` ( M + 1 ) ) e. RR /\ t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) ) -> t e. RR )
76	62, 73, 74, 75	syl3anc 1226	. . . . . . . . . 10 |- ( ( ph /\ t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) ) -> t e. RR )
77	48, 60	ffvelrnd 6008	. . . . . . . . . . . . 13 |- ( ph -> ( P ` M ) e. RR )
78	77	rexrd 9632	. . . . . . . . . . . 12 |- ( ph -> ( P ` M ) e. RR* )
79	78	adantr 463	. . . . . . . . . . 11 |- ( ( ph /\ t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) ) -> ( P ` M ) e. RR* )
80	73	rexrd 9632	. . . . . . . . . . 11 |- ( ( ph /\ t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) ) -> ( P ` ( M + 1 ) ) e. RR* )
81		iccgelb 11584	. . . . . . . . . . 11 |- ( ( ( P ` M ) e. RR* /\ ( P ` ( M + 1 ) ) e. RR* /\ t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) ) -> ( P ` M ) <_ t )
82	79, 80, 74, 81	syl3anc 1226	. . . . . . . . . 10 |- ( ( ph /\ t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) ) -> ( P ` M ) <_ t )
83		iccleub 11583	. . . . . . . . . . . 12 |- ( ( ( P ` M ) e. RR* /\ ( P ` ( M + 1 ) ) e. RR* /\ t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) ) -> t <_ ( P ` ( M + 1 ) ) )
84	79, 80, 74, 83	syl3anc 1226	. . . . . . . . . . 11 |- ( ( ph /\ t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) ) -> t <_ ( P ` ( M + 1 ) ) )
85	48	adantr 463	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( ( M + 1 ) ... N ) ) -> P : ( M ... N ) --> RR )
86		elfzelz 11691	. . . . . . . . . . . . . . . 16 |- ( i e. ( ( M + 1 ) ... N ) -> i e. ZZ )
87	86	adantl 464	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( ( M + 1 ) ... N ) ) -> i e. ZZ )
88	50	adantr 463	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( ( M + 1 ) ... N ) ) -> M e. RR )
89	87	zred 10965	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( ( M + 1 ) ... N ) ) -> i e. RR )
90	52	adantr 463	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( ( M + 1 ) ... N ) ) -> ( M + 1 ) e. RR )
91	53	adantr 463	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( ( M + 1 ) ... N ) ) -> M < ( M + 1 ) )
92		elfzle1 11692	. . . . . . . . . . . . . . . . . 18 |- ( i e. ( ( M + 1 ) ... N ) -> ( M + 1 ) <_ i )
93	92	adantl 464	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( ( M + 1 ) ... N ) ) -> ( M + 1 ) <_ i )
94	88, 90, 89, 91, 93	ltletrd 9731	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( ( M + 1 ) ... N ) ) -> M < i )
95	88, 89, 94	ltled 9722	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( ( M + 1 ) ... N ) ) -> M <_ i )
96		elfzle2 11693	. . . . . . . . . . . . . . . 16 |- ( i e. ( ( M + 1 ) ... N ) -> i <_ N )
97	96	adantl 464	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( ( M + 1 ) ... N ) ) -> i <_ N )
98	1, 5	jca 530	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( M e. ZZ /\ N e. ZZ ) )
99	98	adantr 463	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( ( M + 1 ) ... N ) ) -> ( M e. ZZ /\ N e. ZZ ) )
100		elfz1 11680	. . . . . . . . . . . . . . . 16 |- ( ( M e. ZZ /\ N e. ZZ ) -> ( i e. ( M ... N ) <-> ( i e. ZZ /\ M <_ i /\ i <_ N ) ) )
101	99, 100	syl 16	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( ( M + 1 ) ... N ) ) -> ( i e. ( M ... N ) <-> ( i e. ZZ /\ M <_ i /\ i <_ N ) ) )
102	87, 95, 97, 101	mpbir3and 1177	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( ( M + 1 ) ... N ) ) -> i e. ( M ... N ) )
103	85, 102	ffvelrnd 6008	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( ( M + 1 ) ... N ) ) -> ( P ` i ) e. RR )
104	48	adantr 463	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> P : ( M ... N ) --> RR )
105		elfzelz 11691	. . . . . . . . . . . . . . . . 17 |- ( i e. ( ( M + 1 ) ... ( N - 1 ) ) -> i e. ZZ )
106	105	adantl 464	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> i e. ZZ )
107	50	adantr 463	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> M e. RR )
108	106	zred 10965	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> i e. RR )
109	52	adantr 463	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> ( M + 1 ) e. RR )
110	53	adantr 463	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> M < ( M + 1 ) )
111		elfzle1 11692	. . . . . . . . . . . . . . . . . . 19 |- ( i e. ( ( M + 1 ) ... ( N - 1 ) ) -> ( M + 1 ) <_ i )
112	111	adantl 464	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> ( M + 1 ) <_ i )
113	107, 109, 108, 110, 112	ltletrd 9731	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> M < i )
114	107, 108, 113	ltled 9722	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> M <_ i )
115	10	adantr 463	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> N e. RR )
116		1red 9600	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> 1 e. RR )
117	115, 116	resubcld 9983	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> ( N - 1 ) e. RR )
118		elfzle2 11693	. . . . . . . . . . . . . . . . . . 19 |- ( i e. ( ( M + 1 ) ... ( N - 1 ) ) -> i <_ ( N - 1 ) )
119	118	adantl 464	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> i <_ ( N - 1 ) )
120	115	ltm1d 10473	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> ( N - 1 ) < N )
121	108, 117, 115, 119, 120	lelttrd 9729	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> i < N )
122	108, 115, 121	ltled 9722	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> i <_ N )
123	98	adantr 463	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> ( M e. ZZ /\ N e. ZZ ) )
124	123, 100	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> ( i e. ( M ... N ) <-> ( i e. ZZ /\ M <_ i /\ i <_ N ) ) )
125	106, 114, 122, 124	mpbir3and 1177	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> i e. ( M ... N ) )
126	104, 125	ffvelrnd 6008	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> ( P ` i ) e. RR )
127	106	peano2zd 10968	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> ( i + 1 ) e. ZZ )
128	108, 116	readdcld 9612	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> ( i + 1 ) e. RR )
129	107, 108, 116, 113	ltadd1dd 10159	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> ( M + 1 ) < ( i + 1 ) )
130	107, 109, 128, 110, 129	lttrd 9732	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> M < ( i + 1 ) )
131	107, 128, 130	ltled 9722	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> M <_ ( i + 1 ) )
132		zltp1le 10909	. . . . . . . . . . . . . . . . . 18 |- ( ( i e. ZZ /\ N e. ZZ ) -> ( i < N <-> ( i + 1 ) <_ N ) )
133	105, 5, 132	syl2anr 476	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> ( i < N <-> ( i + 1 ) <_ N ) )
134	121, 133	mpbid 210	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> ( i + 1 ) <_ N )
135		elfz1 11680	. . . . . . . . . . . . . . . . 17 |- ( ( M e. ZZ /\ N e. ZZ ) -> ( ( i + 1 ) e. ( M ... N ) <-> ( ( i + 1 ) e. ZZ /\ M <_ ( i + 1 ) /\ ( i + 1 ) <_ N ) ) )
136	123, 135	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> ( ( i + 1 ) e. ( M ... N ) <-> ( ( i + 1 ) e. ZZ /\ M <_ ( i + 1 ) /\ ( i + 1 ) <_ N ) ) )
137	127, 131, 134, 136	mpbir3and 1177	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> ( i + 1 ) e. ( M ... N ) )
138	104, 137	ffvelrnd 6008	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> ( P ` ( i + 1 ) ) e. RR )
139		eluz 11095	. . . . . . . . . . . . . . . . . 18 |- ( ( M e. ZZ /\ i e. ZZ ) -> ( i e. ( ZZ>= ` M ) <-> M <_ i ) )
140	1, 105, 139	syl2an 475	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> ( i e. ( ZZ>= ` M ) <-> M <_ i ) )
141	114, 140	mpbird 232	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> i e. ( ZZ>= ` M ) )
142	5	adantr 463	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> N e. ZZ )
143		elfzo2 11807	. . . . . . . . . . . . . . . 16 |- ( i e. ( M..^ N ) <-> ( i e. ( ZZ>= ` M ) /\ N e. ZZ /\ i < N ) )
144	141, 142, 121, 143	syl3anbrc 1178	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> i e. ( M..^ N ) )
145		itgspltprt.4	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( M..^ N ) ) -> ( P ` i ) < ( P ` ( i + 1 ) ) )
146	144, 145	syldan 468	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> ( P ` i ) < ( P ` ( i + 1 ) ) )
147	126, 138, 146	ltled 9722	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( ( M + 1 ) ... ( N - 1 ) ) ) -> ( P ` i ) <_ ( P ` ( i + 1 ) ) )
148	3, 103, 147	monoord 12122	. . . . . . . . . . . 12 |- ( ph -> ( P ` ( M + 1 ) ) <_ ( P ` N ) )
149	148	adantr 463	. . . . . . . . . . 11 |- ( ( ph /\ t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) ) -> ( P ` ( M + 1 ) ) <_ ( P ` N ) )
150	76, 73, 67, 84, 149	letrd 9728	. . . . . . . . . 10 |- ( ( ph /\ t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) ) -> t <_ ( P ` N ) )
151	62, 67, 76, 82, 150	eliccd 31780	. . . . . . . . 9 |- ( ( ph /\ t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) ) -> t e. ( ( P ` M ) [,] ( P ` N ) ) )
152		itgspltprt.5	. . . . . . . . 9 |- ( ( ph /\ t e. ( ( P ` M ) [,] ( P ` N ) ) ) -> A e. CC )
153	151, 152	syldan 468	. . . . . . . 8 |- ( ( ph /\ t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) ) -> A e. CC )
154		id 22	. . . . . . . . . 10 |- ( ph -> ph )
155		fzolb 11810	. . . . . . . . . . 11 |- ( M e. ( M..^ N ) <-> ( M e. ZZ /\ N e. ZZ /\ M < N ) )
156	1, 5, 54, 155	syl3anbrc 1178	. . . . . . . . . 10 |- ( ph -> M e. ( M..^ N ) )
157	154, 156	jca 530	. . . . . . . . 9 |- ( ph -> ( ph /\ M e. ( M..^ N ) ) )
158		eleq1 2526	. . . . . . . . . . . 12 |- ( i = M -> ( i e. ( M..^ N ) <-> M e. ( M..^ N ) ) )
159	158	anbi2d 701	. . . . . . . . . . 11 |- ( i = M -> ( ( ph /\ i e. ( M..^ N ) ) <-> ( ph /\ M e. ( M..^ N ) ) ) )
160		fveq2 5848	. . . . . . . . . . . . . 14 |- ( i = M -> ( P ` i ) = ( P ` M ) )
161		oveq1 6277	. . . . . . . . . . . . . . 15 |- ( i = M -> ( i + 1 ) = ( M + 1 ) )
162	161	fveq2d 5852	. . . . . . . . . . . . . 14 |- ( i = M -> ( P ` ( i + 1 ) ) = ( P ` ( M + 1 ) ) )
163	160, 162	oveq12d 6288	. . . . . . . . . . . . 13 |- ( i = M -> ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) = ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) )
164	163	mpteq1d 4520	. . . . . . . . . . . 12 |- ( i = M -> ( t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) |-> A ) = ( t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) |-> A ) )
165	164	eleq1d 2523	. . . . . . . . . . 11 |- ( 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	159, 165	imbi12d 318	. . . . . . . . . 10 |- ( 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		itgspltprt.6	. . . . . . . . . 10 |- ( ( ph /\ i e. ( M..^ N ) ) -> ( t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) |-> A ) e. L^1 )
168	166, 167	vtoclg 3164	. . . . . . . . 9 |- ( M e. ZZ -> ( ( ph /\ M e. ( M..^ N ) ) -> ( t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) |-> A ) e. L^1 ) )
169	1, 157, 168	sylc 60	. . . . . . . 8 |- ( ph -> ( t e. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) |-> A ) e. L^1 )
170	153, 169	itgcl 22359	. . . . . . 7 |- ( ph -> S. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) A _d t e. CC )
171	163	itgeq1d 31997	. . . . . . . 8 |- ( i = M -> S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t = S. ( ( P ` M ) [,] ( P ` ( M + 1 ) ) ) A _d t )
172	171	fsum1 13649	. . . . . . 7 |- ( ( 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 )
173	1, 170, 172	syl2anc 659	. . . . . 6 |- ( 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	173	adantl 464	. . . . 5 |- ( ( 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 )
175	47, 174	eqtr2d 2496	. . . 4 |- ( ( 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	175	ex 432	. . 3 |- ( 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 ) )
177		simp3 996	. . . . 5 |- ( ( 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 )
178		simp1 994	. . . . 5 |- ( ( 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 ) )
179		simp2 995	. . . . . 6 |- ( ( 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 ) )
180	177, 179	mpd 15	. . . . 5 |- ( ( 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 )
181	50	adantr 463	. . . . . . . . . 10 |- ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) -> M e. RR )
182		elfzoelz 11804	. . . . . . . . . . . 12 |- ( k e. ( ( M + 1 )..^ N ) -> k e. ZZ )
183	182	zred 10965	. . . . . . . . . . 11 |- ( k e. ( ( M + 1 )..^ N ) -> k e. RR )
184	183	adantl 464	. . . . . . . . . 10 |- ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) -> k e. RR )
185	52	adantr 463	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) -> ( M + 1 ) e. RR )
186	53	adantr 463	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) -> M < ( M + 1 ) )
187		elfzole1 11812	. . . . . . . . . . . 12 |- ( k e. ( ( M + 1 )..^ N ) -> ( M + 1 ) <_ k )
188	187	adantl 464	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) -> ( M + 1 ) <_ k )
189	181, 185, 184, 186, 188	ltletrd 9731	. . . . . . . . . 10 |- ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) -> M < k )
190	181, 184, 189	ltled 9722	. . . . . . . . 9 |- ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) -> M <_ k )
191		eluz 11095	. . . . . . . . . 10 |- ( ( M e. ZZ /\ k e. ZZ ) -> ( k e. ( ZZ>= ` M ) <-> M <_ k ) )
192	1, 182, 191	syl2an 475	. . . . . . . . 9 |- ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) -> ( k e. ( ZZ>= ` M ) <-> M <_ k ) )
193	190, 192	mpbird 232	. . . . . . . 8 |- ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) -> k e. ( ZZ>= ` M ) )
194		simplll 757	. . . . . . . . . 10 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> ph )
195		eliccxr 31792	. . . . . . . . . . . 12 |- ( t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) -> t e. RR* )
196	195	adantl 464	. . . . . . . . . . 11 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> t e. RR* )
197	194, 77	syl 16	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> ( P ` M ) e. RR )
198	194, 48	syl 16	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> P : ( M ... N ) --> RR )
199		elfzelz 11691	. . . . . . . . . . . . . . . 16 |- ( i e. ( M ... k ) -> i e. ZZ )
200	199	adantl 464	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) -> i e. ZZ )
201		elfzle1 11692	. . . . . . . . . . . . . . . 16 |- ( i e. ( M ... k ) -> M <_ i )
202	201	adantl 464	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) -> M <_ i )
203	200	zred 10965	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) -> i e. RR )
204	10	ad2antrr 723	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) -> N e. RR )
205	184	adantr 463	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) -> k e. RR )
206		elfzle2 11693	. . . . . . . . . . . . . . . . . 18 |- ( i e. ( M ... k ) -> i <_ k )
207	206	adantl 464	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) -> i <_ k )
208		elfzolt2 11813	. . . . . . . . . . . . . . . . . 18 |- ( k e. ( ( M + 1 )..^ N ) -> k < N )
209	208	ad2antlr 724	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) -> k < N )
210	203, 205, 204, 207, 209	lelttrd 9729	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) -> i < N )
211	203, 204, 210	ltled 9722	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) -> i <_ N )
212	98	ad2antrr 723	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) -> ( M e. ZZ /\ N e. ZZ ) )
213	212, 100	syl 16	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) -> ( i e. ( M ... N ) <-> ( i e. ZZ /\ M <_ i /\ i <_ N ) ) )
214	200, 202, 211, 213	mpbir3and 1177	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) -> i e. ( M ... N ) )
215	214	adantr 463	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> i e. ( M ... N ) )
216	198, 215	ffvelrnd 6008	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> ( P ` i ) e. RR )
217	200	peano2zd 10968	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) -> ( i + 1 ) e. ZZ )
218	50	ad2antrr 723	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) -> M e. RR )
219	217	zred 10965	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) -> ( i + 1 ) e. RR )
220	50	adantr 463	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( M ... k ) ) -> M e. RR )
221	199	zred 10965	. . . . . . . . . . . . . . . . . . . 20 |- ( i e. ( M ... k ) -> i e. RR )
222	221	adantl 464	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( M ... k ) ) -> i e. RR )
223		1red 9600	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ i e. ( M ... k ) ) -> 1 e. RR )
224	222, 223	readdcld 9612	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( M ... k ) ) -> ( i + 1 ) e. RR )
225	201	adantl 464	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( M ... k ) ) -> M <_ i )
226	222	ltp1d 10471	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( M ... k ) ) -> i < ( i + 1 ) )
227	220, 222, 224, 225, 226	lelttrd 9729	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( M ... k ) ) -> M < ( i + 1 ) )
228	227	adantlr 712	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) -> M < ( i + 1 ) )
229	218, 219, 228	ltled 9722	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) -> M <_ ( i + 1 ) )
230	5, 199	anim12ci 565	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( M ... k ) ) -> ( i e. ZZ /\ N e. ZZ ) )
231	230	adantlr 712	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) -> ( i e. ZZ /\ N e. ZZ ) )
232	231, 132	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) -> ( i < N <-> ( i + 1 ) <_ N ) )
233	210, 232	mpbid 210	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) -> ( i + 1 ) <_ N )
234	212, 135	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( ( 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 ) ) )
235	217, 229, 233, 234	mpbir3and 1177	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) -> ( i + 1 ) e. ( M ... N ) )
236	235	adantr 463	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> ( i + 1 ) e. ( M ... N ) )
237	198, 236	ffvelrnd 6008	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> ( P ` ( i + 1 ) ) e. RR )
238		simpr 459	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) )
239		eliccre 31782	. . . . . . . . . . . . 13 |- ( ( ( P ` i ) e. RR /\ ( P ` ( i + 1 ) ) e. RR /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> t e. RR )
240	216, 237, 238, 239	syl3anc 1226	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> t e. RR )
241		elfzuz 11687	. . . . . . . . . . . . . . 15 |- ( i e. ( M ... k ) -> i e. ( ZZ>= ` M ) )
242	241	adantl 464	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) -> i e. ( ZZ>= ` M ) )
243	48	ad3antrrr 727	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... i ) ) -> P : ( M ... N ) --> RR )
244		elfzelz 11691	. . . . . . . . . . . . . . . . 17 |- ( j e. ( M ... i ) -> j e. ZZ )
245	244	adantl 464	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... i ) ) -> j e. ZZ )
246		elfzle1 11692	. . . . . . . . . . . . . . . . 17 |- ( j e. ( M ... i ) -> M <_ j )
247	246	adantl 464	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... i ) ) -> M <_ j )
248	245	zred 10965	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... i ) ) -> j e. RR )
249	204	adantr 463	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... i ) ) -> N e. RR )
250	203	adantr 463	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... i ) ) -> i e. RR )
251		elfzle2 11693	. . . . . . . . . . . . . . . . . . 19 |- ( j e. ( M ... i ) -> j <_ i )
252	251	adantl 464	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... i ) ) -> j <_ i )
253	210	adantr 463	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... i ) ) -> i < N )
254	248, 250, 249, 252, 253	lelttrd 9729	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... i ) ) -> j < N )
255	248, 249, 254	ltled 9722	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... i ) ) -> j <_ N )
256	212	adantr 463	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... i ) ) -> ( M e. ZZ /\ N e. ZZ ) )
257		elfz1 11680	. . . . . . . . . . . . . . . . 17 |- ( ( M e. ZZ /\ N e. ZZ ) -> ( j e. ( M ... N ) <-> ( j e. ZZ /\ M <_ j /\ j <_ N ) ) )
258	256, 257	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 ) ) )
259	245, 247, 255, 258	mpbir3and 1177	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... i ) ) -> j e. ( M ... N ) )
260	243, 259	ffvelrnd 6008	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... i ) ) -> ( P ` j ) e. RR )
261	48	ad3antrrr 727	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> P : ( M ... N ) --> RR )
262		elfzelz 11691	. . . . . . . . . . . . . . . . . 18 |- ( j e. ( M ... ( i - 1 ) ) -> j e. ZZ )
263	262	adantl 464	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> j e. ZZ )
264		elfzle1 11692	. . . . . . . . . . . . . . . . . 18 |- ( j e. ( M ... ( i - 1 ) ) -> M <_ j )
265	264	adantl 464	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> M <_ j )
266	263	zred 10965	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> j e. RR )
267	204	adantr 463	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> N e. RR )
268	203	adantr 463	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> i e. RR )
269		1red 9600	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> 1 e. RR )
270	268, 269	resubcld 9983	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> ( i - 1 ) e. RR )
271		elfzle2 11693	. . . . . . . . . . . . . . . . . . . . 21 |- ( j e. ( M ... ( i - 1 ) ) -> j <_ ( i - 1 ) )
272	271	adantl 464	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> j <_ ( i - 1 ) )
273	268	ltm1d 10473	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> ( i - 1 ) < i )
274	266, 270, 268, 272, 273	lelttrd 9729	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> j < i )
275	210	adantr 463	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> i < N )
276	266, 268, 267, 274, 275	lttrd 9732	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> j < N )
277	266, 267, 276	ltled 9722	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> j <_ N )
278	212	adantr 463	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> ( M e. ZZ /\ N e. ZZ ) )
279	278, 257	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( 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 ) ) )
280	263, 265, 277, 279	mpbir3and 1177	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> j e. ( M ... N ) )
281	261, 280	ffvelrnd 6008	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> ( P ` j ) e. RR )
282	263	peano2zd 10968	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> ( j + 1 ) e. ZZ )
283	181	ad2antrr 723	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> M e. RR )
284	266, 269	readdcld 9612	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> ( j + 1 ) e. RR )
285	50	adantr 463	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ j e. ( M ... ( i - 1 ) ) ) -> M e. RR )
286	262	zred 10965	. . . . . . . . . . . . . . . . . . . . 21 |- ( j e. ( M ... ( i - 1 ) ) -> j e. RR )
287	286	adantl 464	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ j e. ( M ... ( i - 1 ) ) ) -> j e. RR )
288		1red 9600	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ j e. ( M ... ( i - 1 ) ) ) -> 1 e. RR )
289	287, 288	readdcld 9612	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ j e. ( M ... ( i - 1 ) ) ) -> ( j + 1 ) e. RR )
290	264	adantl 464	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ j e. ( M ... ( i - 1 ) ) ) -> M <_ j )
291	287	ltp1d 10471	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ j e. ( M ... ( i - 1 ) ) ) -> j < ( j + 1 ) )
292	285, 287, 289, 290, 291	lelttrd 9729	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ j e. ( M ... ( i - 1 ) ) ) -> M < ( j + 1 ) )
293	292	adant423 31668	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> M < ( j + 1 ) )
294	283, 284, 293	ltled 9722	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> M <_ ( j + 1 ) )
295		zltp1le 10909	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( j e. ZZ /\ i e. ZZ ) -> ( j < i <-> ( j + 1 ) <_ i ) )
296	262, 200, 295	syl2anr 476	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> ( j < i <-> ( j + 1 ) <_ i ) )
297	274, 296	mpbid 210	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> ( j + 1 ) <_ i )
298	284, 268, 267, 297, 275	lelttrd 9729	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> ( j + 1 ) < N )
299	284, 267, 298	ltled 9722	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> ( j + 1 ) <_ N )
300		elfz1 11680	. . . . . . . . . . . . . . . . . 18 |- ( ( M e. ZZ /\ N e. ZZ ) -> ( ( j + 1 ) e. ( M ... N ) <-> ( ( j + 1 ) e. ZZ /\ M <_ ( j + 1 ) /\ ( j + 1 ) <_ N ) ) )
301	278, 300	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( 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 ) ) )
302	282, 294, 299, 301	mpbir3and 1177	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> ( j + 1 ) e. ( M ... N ) )
303	261, 302	ffvelrnd 6008	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> ( P ` ( j + 1 ) ) e. RR )
304		simplll 757	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> ph )
305		elfzuz 11687	. . . . . . . . . . . . . . . . . 18 |- ( j e. ( M ... ( i - 1 ) ) -> j e. ( ZZ>= ` M ) )
306	305	adantl 464	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> j e. ( ZZ>= ` M ) )
307	304, 5	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> N e. ZZ )
308		elfzo2 11807	. . . . . . . . . . . . . . . . 17 |- ( j e. ( M..^ N ) <-> ( j e. ( ZZ>= ` M ) /\ N e. ZZ /\ j < N ) )
309	306, 307, 276, 308	syl3anbrc 1178	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> j e. ( M..^ N ) )
310		eleq1 2526	. . . . . . . . . . . . . . . . . . 19 |- ( i = j -> ( i e. ( M..^ N ) <-> j e. ( M..^ N ) ) )
311	310	anbi2d 701	. . . . . . . . . . . . . . . . . 18 |- ( i = j -> ( ( ph /\ i e. ( M..^ N ) ) <-> ( ph /\ j e. ( M..^ N ) ) ) )
312		fveq2 5848	. . . . . . . . . . . . . . . . . . 19 |- ( i = j -> ( P ` i ) = ( P ` j ) )
313		oveq1 6277	. . . . . . . . . . . . . . . . . . . 20 |- ( i = j -> ( i + 1 ) = ( j + 1 ) )
314	313	fveq2d 5852	. . . . . . . . . . . . . . . . . . 19 |- ( i = j -> ( P ` ( i + 1 ) ) = ( P ` ( j + 1 ) ) )
315	312, 314	breq12d 4452	. . . . . . . . . . . . . . . . . 18 |- ( i = j -> ( ( P ` i ) < ( P ` ( i + 1 ) ) <-> ( P ` j ) < ( P ` ( j + 1 ) ) ) )
316	311, 315	imbi12d 318	. . . . . . . . . . . . . . . . 17 |- ( i = j -> ( ( ( ph /\ i e. ( M..^ N ) ) -> ( P ` i ) < ( P ` ( i + 1 ) ) ) <-> ( ( ph /\ j e. ( M..^ N ) ) -> ( P ` j ) < ( P ` ( j + 1 ) ) ) ) )
317	316, 145	chvarv 2019	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. ( M..^ N ) ) -> ( P ` j ) < ( P ` ( j + 1 ) ) )
318	304, 309, 317	syl2anc 659	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> ( P ` j ) < ( P ` ( j + 1 ) ) )
319	281, 303, 318	ltled 9722	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( M ... ( i - 1 ) ) ) -> ( P ` j ) <_ ( P ` ( j + 1 ) ) )
320	242, 260, 319	monoord 12122	. . . . . . . . . . . . 13 |- ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) -> ( P ` M ) <_ ( P ` i ) )
321	320	adantr 463	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> ( P ` M ) <_ ( P ` i ) )
322	216	rexrd 9632	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> ( P ` i ) e. RR* )
323	237	rexrd 9632	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> ( P ` ( i + 1 ) ) e. RR* )
324		iccgelb 11584	. . . . . . . . . . . . 13 |- ( ( ( P ` i ) e. RR* /\ ( P ` ( i + 1 ) ) e. RR* /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> ( P ` i ) <_ t )
325	322, 323, 238, 324	syl3anc 1226	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> ( P ` i ) <_ t )
326	197, 216, 240, 321, 325	letrd 9728	. . . . . . . . . . 11 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> ( P ` M ) <_ t )
327	194, 66	syl 16	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> ( P ` N ) e. RR )
328		iccleub 11583	. . . . . . . . . . . . 13 |- ( ( ( P ` i ) e. RR* /\ ( P ` ( i + 1 ) ) e. RR* /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> t <_ ( P ` ( i + 1 ) ) )
329	322, 323, 238, 328	syl3anc 1226	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> t <_ ( P ` ( i + 1 ) ) )
330	5	ad2antrr 723	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) -> N e. ZZ )
331		eluz 11095	. . . . . . . . . . . . . . . 16 |- ( ( ( i + 1 ) e. ZZ /\ N e. ZZ ) -> ( N e. ( ZZ>= ` ( i + 1 ) ) <-> ( i + 1 ) <_ N ) )
332	217, 330, 331	syl2anc 659	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) -> ( N e. ( ZZ>= ` ( i + 1 ) ) <-> ( i + 1 ) <_ N ) )
333	233, 332	mpbird 232	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) -> N e. ( ZZ>= ` ( i + 1 ) ) )
334	333	adantr 463	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) ) -> N e. ( ZZ>= ` ( i + 1 ) ) )
335	48	ad3antrrr 727	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( ( i + 1 ) ... N ) ) -> P : ( M ... N ) --> RR )
336		elfzelz 11691	. . . . . . . . . . . . . . . . 17 |- ( j e. ( ( i + 1 ) ... N ) -> j e. ZZ )
337	336	adantl 464	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( ( i + 1 ) ... N ) ) -> j e. ZZ )
338		elfzel1 11690	. . . . . . . . . . . . . . . . . . . 20 |- ( i e. ( M ... k ) -> M e. ZZ )
339	338	zred 10965	. . . . . . . . . . . . . . . . . . 19 |- ( i e. ( M ... k ) -> M e. RR )
340	339	adantr 463	. . . . . . . . . . . . . . . . . 18 |- ( ( i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... N ) ) -> M e. RR )
341	336	zred 10965	. . . . . . . . . . . . . . . . . . 19 |- ( j e. ( ( i + 1 ) ... N ) -> j e. RR )
342	341	adantl 464	. . . . . . . . . . . . . . . . . 18 |- ( ( i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... N ) ) -> j e. RR )
343	221	adantr 463	. . . . . . . . . . . . . . . . . . . 20 |- ( ( i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... N ) ) -> i e. RR )
344		1red 9600	. . . . . . . . . . . . . . . . . . . 20 |- ( ( i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... N ) ) -> 1 e. RR )
345	343, 344	readdcld 9612	. . . . . . . . . . . . . . . . . . 19 |- ( ( i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... N ) ) -> ( i + 1 ) e. RR )
346	201	adantr 463	. . . . . . . . . . . . . . . . . . . 20 |- ( ( i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... N ) ) -> M <_ i )
347	343	ltp1d 10471	. . . . . . . . . . . . . . . . . . . 20 |- ( ( i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... N ) ) -> i < ( i + 1 ) )
348	340, 343, 345, 346, 347	lelttrd 9729	. . . . . . . . . . . . . . . . . . 19 |- ( ( i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... N ) ) -> M < ( i + 1 ) )
349		elfzle1 11692	. . . . . . . . . . . . . . . . . . . 20 |- ( j e. ( ( i + 1 ) ... N ) -> ( i + 1 ) <_ j )
350	349	adantl 464	. . . . . . . . . . . . . . . . . . 19 |- ( ( i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... N ) ) -> ( i + 1 ) <_ j )
351	340, 345, 342, 348, 350	ltletrd 9731	. . . . . . . . . . . . . . . . . 18 |- ( ( i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... N ) ) -> M < j )
352	340, 342, 351	ltled 9722	. . . . . . . . . . . . . . . . 17 |- ( ( i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... N ) ) -> M <_ j )
353	352	adantll 711	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( ( i + 1 ) ... N ) ) -> M <_ j )
354		elfzle2 11693	. . . . . . . . . . . . . . . . 17 |- ( j e. ( ( i + 1 ) ... N ) -> j <_ N )
355	354	adantl 464	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( ( i + 1 ) ... N ) ) -> j <_ N )
356	212	adantr 463	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( ( i + 1 ) ... N ) ) -> ( M e. ZZ /\ N e. ZZ ) )
357	356, 257	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 ) ) )
358	337, 353, 355, 357	mpbir3and 1177	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( ( i + 1 ) ... N ) ) -> j e. ( M ... N ) )
359	335, 358	ffvelrnd 6008	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( ( i + 1 ) ... N ) ) -> ( P ` j ) e. RR )
360	359	adantlr 712	. . . . . . . . . . . . 13 |- ( ( ( ( ( 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 )
361		simplll 757	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> ph )
362		simplr 753	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> i e. ( M ... k ) )
363		simpr 459	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> j e. ( ( i + 1 ) ... ( N - 1 ) ) )
364	48	3ad2ant1 1015	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> P : ( M ... N ) --> RR )
365		elfzelz 11691	. . . . . . . . . . . . . . . . . . 19 |- ( j e. ( ( i + 1 ) ... ( N - 1 ) ) -> j e. ZZ )
366	365	3ad2ant3 1017	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> j e. ZZ )
367	50	3ad2ant1 1015	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> M e. RR )
368	366	zred 10965	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> j e. RR )
369	224	3adant3 1014	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> ( i + 1 ) e. RR )
370	227	3adant3 1014	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> M < ( i + 1 ) )
371		elfzle1 11692	. . . . . . . . . . . . . . . . . . . . 21 |- ( j e. ( ( i + 1 ) ... ( N - 1 ) ) -> ( i + 1 ) <_ j )
372	371	3ad2ant3 1017	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> ( i + 1 ) <_ j )
373	367, 369, 368, 370, 372	ltletrd 9731	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> M < j )
374	367, 368, 373	ltled 9722	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> M <_ j )
375	365	adantl 464	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> j e. ZZ )
376	375	zred 10965	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> j e. RR )
377	10	adantr 463	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> N e. RR )
378		1red 9600	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> 1 e. RR )
379	377, 378	resubcld 9983	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> ( N - 1 ) e. RR )
380		elfzle2 11693	. . . . . . . . . . . . . . . . . . . . . 22 |- ( j e. ( ( i + 1 ) ... ( N - 1 ) ) -> j <_ ( N - 1 ) )
381	380	adantl 464	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> j <_ ( N - 1 ) )
382	377	ltm1d 10473	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> ( N - 1 ) < N )
383	376, 379, 377, 381, 382	lelttrd 9729	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> j < N )
384	376, 377, 383	ltled 9722	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> j <_ N )
385	384	3adant2 1013	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> j <_ N )
386	98	3ad2ant1 1015	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> ( M e. ZZ /\ N e. ZZ ) )
387	386, 257	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> ( j e. ( M ... N ) <-> ( j e. ZZ /\ M <_ j /\ j <_ N ) ) )
388	366, 374, 385, 387	mpbir3and 1177	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> j e. ( M ... N ) )
389	364, 388	ffvelrnd 6008	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> ( P ` j ) e. RR )
390	366	peano2zd 10968	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> ( j + 1 ) e. ZZ )
391	390	zred 10965	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> ( j + 1 ) e. RR )
392	221	3ad2ant2 1016	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> i e. RR )
393		1red 9600	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> 1 e. RR )
394	226	3adant3 1014	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> i < ( i + 1 ) )
395	392, 369, 368, 394, 372	ltletrd 9731	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> i < j )
396	392, 368, 395	ltled 9722	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> i <_ j )
397	392, 368, 393, 396	leadd1dd 10162	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> ( i + 1 ) <_ ( j + 1 ) )
398	367, 369, 391, 370, 397	ltletrd 9731	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> M < ( j + 1 ) )
399	367, 391, 398	ltled 9722	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> M <_ ( j + 1 ) )
400		zltp1le 10909	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( j e. ZZ /\ N e. ZZ ) -> ( j < N <-> ( j + 1 ) <_ N ) )
401	365, 5, 400	syl2anr 476	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> ( j < N <-> ( j + 1 ) <_ N ) )
402	383, 401	mpbid 210	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> ( j + 1 ) <_ N )
403	402	3adant2 1013	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> ( j + 1 ) <_ N )
404	386, 300	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ( 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 ) ) )
405	390, 399, 403, 404	mpbir3and 1177	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> ( j + 1 ) e. ( M ... N ) )
406	364, 405	ffvelrnd 6008	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> ( P ` ( j + 1 ) ) e. RR )
407		simp1 994	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> ph )
408	1	3ad2ant1 1015	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> M e. ZZ )
409		eluz 11095	. . . . . . . . . . . . . . . . . . . 20 |- ( ( M e. ZZ /\ j e. ZZ ) -> ( j e. ( ZZ>= ` M ) <-> M <_ j ) )
410	408, 366, 409	syl2anc 659	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> ( j e. ( ZZ>= ` M ) <-> M <_ j ) )
411	374, 410	mpbird 232	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> j e. ( ZZ>= ` M ) )
412	5	3ad2ant1 1015	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> N e. ZZ )
413	383	3adant2 1013	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> j < N )
414	411, 412, 413, 308	syl3anbrc 1178	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> j e. ( M..^ N ) )
415	407, 414, 317	syl2anc 659	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> ( P ` j ) < ( P ` ( j + 1 ) ) )
416	389, 406, 415	ltled 9722	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( M ... k ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> ( P ` j ) <_ ( P ` ( j + 1 ) ) )
417	361, 362, 363, 416	syl3anc 1226	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ k e. ( ( M + 1 )..^ N ) ) /\ i e. ( M ... k ) ) /\ j e. ( ( i + 1 ) ... ( N - 1 ) ) ) -> ( P ` j ) <_ ( P ` ( j + 1 ) ) )
418	417	adantlr 712	. . . . . . . . . . . . 13 |- ( ( ( ( ( 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 ) ) )
419	334, 360, 418	monoord 12122	. . . . . . . . . . . 12 |- (