Theorem etransclem35 32218

Description: P does not divide the P-1 -th derivative of F applied to 0. This is case 2 of the proof in [Juillerat] p. 13 . (Contributed by Glauco Siliprandi, 5-Apr-2020.)

Hypotheses

Ref	Expression
etransclem35.p	|- ( ph -> P e. NN )
etransclem35.m	|- ( ph -> M e. NN0 )
etransclem35.f	|- F = ( x e. RR |-> ( ( x ^ ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( ( x - j ) ^ P ) ) )
etransclem35.c	|- C = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = n } )
etransclem35.d	|- D = ( j e. ( 0 ... M ) |-> if ( j = 0 , ( P - 1 ) , 0 ) )

Assertion

Ref	Expression
etransclem35	|- ( ph -> ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) = ( ( ! ` ( P - 1 ) ) x. ( prod_ j e. ( 1 ... M ) -u j ^ P ) ) )

Distinct variable groups:   C, c, j, x   D, c, j   M, c, j, n, x   P, c, j, n, x   ph, c, j, n, x

Allowed substitution hints:   C( n)   D( x, n)   F( x, j, n, c)

Proof of Theorem etransclem35

Dummy variables A k y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		reelprrecn 9495	. . . 4 |- RR e. { RR , CC }
2	1	a1i 11	. . 3 |- ( ph -> RR e. { RR , CC } )
3		reopn 31643	. . . . 5 |- RR e. ( topGen ` ran (,) )
4		eqid 2382	. . . . . 6 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
5	4	tgioo2 21393	. . . . 5 |- ( topGen ` ran (,) ) = ( ( TopOpen ` ℂfld ) ↾t RR )
6	3, 5	eleqtri 2468	. . . 4 |- RR e. ( ( TopOpen ` ℂfld ) ↾t RR )
7	6	a1i 11	. . 3 |- ( ph -> RR e. ( ( TopOpen ` ℂfld ) ↾t RR ) )
8		etransclem35.p	. . 3 |- ( ph -> P e. NN )
9		etransclem35.m	. . 3 |- ( ph -> M e. NN0 )
10		etransclem35.f	. . 3 |- F = ( x e. RR |-> ( ( x ^ ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( ( x - j ) ^ P ) ) )
11		nnm1nn0 10754	. . . 4 |- ( P e. NN -> ( P - 1 ) e. NN0 )
12	8, 11	syl 16	. . 3 |- ( ph -> ( P - 1 ) e. NN0 )
13		etransclem5 32188	. . 3 |- ( k e. ( 0 ... M ) |-> ( y e. RR |-> ( ( y - k ) ^ if ( k = 0 , ( P - 1 ) , P ) ) ) ) = ( j e. ( 0 ... M ) |-> ( x e. RR |-> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) )
14		etransclem35.c	. . 3 |- C = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = n } )
15		0red 9508	. . 3 |- ( ph -> 0 e. RR )
16	2, 7, 8, 9, 10, 12, 13, 14, 15	etransclem31 32214	. 2 |- ( ph -> ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) = sum_ c e. ( C ` ( P - 1 ) ) ( ( ( ! ` ( P - 1 ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) x. ( if ( ( P - 1 ) < ( c ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) ) x. ( 0 ^ ( ( P - 1 ) - ( c ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( c ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( c ` j ) ) ) ) x. ( ( 0 - j ) ^ ( P - ( c ` j ) ) ) ) ) ) ) )
17		nfv 1715	. . 3 |- F/ c ph
18		nfcv 2544	. . 3 |- F/_ c ( ( ( ! ` ( P - 1 ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. ( if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( 0 ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( 0 - j ) ^ ( P - ( D ` j ) ) ) ) ) ) )
19	14, 12	etransclem16 32199	. . 3 |- ( ph -> ( C ` ( P - 1 ) ) e. Fin )
20		simpr 459	. . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> c e. ( C ` ( P - 1 ) ) )
21	14, 12	etransclem12 32195	. . . . . . . . . . . . . 14 |- ( ph -> ( C ` ( P - 1 ) ) = { c e. ( ( 0 ... ( P - 1 ) ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = ( P - 1 ) } )
22	21	adantr 463	. . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> ( C ` ( P - 1 ) ) = { c e. ( ( 0 ... ( P - 1 ) ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = ( P - 1 ) } )
23	20, 22	eleqtrd 2472	. . . . . . . . . . . 12 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> c e. { c e. ( ( 0 ... ( P - 1 ) ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = ( P - 1 ) } )
24		rabid 2959	. . . . . . . . . . . 12 |- ( c e. { c e. ( ( 0 ... ( P - 1 ) ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = ( P - 1 ) } <-> ( c e. ( ( 0 ... ( P - 1 ) ) ^m ( 0 ... M ) ) /\ sum_ j e. ( 0 ... M ) ( c ` j ) = ( P - 1 ) ) )
25	23, 24	sylib 196	. . . . . . . . . . 11 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> ( c e. ( ( 0 ... ( P - 1 ) ) ^m ( 0 ... M ) ) /\ sum_ j e. ( 0 ... M ) ( c ` j ) = ( P - 1 ) ) )
26	25	simprd 461	. . . . . . . . . 10 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> sum_ j e. ( 0 ... M ) ( c ` j ) = ( P - 1 ) )
27	26	eqcomd 2390	. . . . . . . . 9 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> ( P - 1 ) = sum_ j e. ( 0 ... M ) ( c ` j ) )
28	27	fveq2d 5778	. . . . . . . 8 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> ( ! ` ( P - 1 ) ) = ( ! ` sum_ j e. ( 0 ... M ) ( c ` j ) ) )
29	28	oveq1d 6211	. . . . . . 7 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> ( ( ! ` ( P - 1 ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) = ( ( ! ` sum_ j e. ( 0 ... M ) ( c ` j ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) )
30		nfcv 2544	. . . . . . . 8 |- F/_ j c
31		fzfid 11986	. . . . . . . 8 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> ( 0 ... M ) e. Fin )
32		nn0ex 10718	. . . . . . . . . 10 |- NN0 e. _V
33		fzssnn0 31688	. . . . . . . . . 10 |- ( 0 ... ( P - 1 ) ) C_ NN0
34		mapss 7380	. . . . . . . . . 10 |- ( ( NN0 e. _V /\ ( 0 ... ( P - 1 ) ) C_ NN0 ) -> ( ( 0 ... ( P - 1 ) ) ^m ( 0 ... M ) ) C_ ( NN0 ^m ( 0 ... M ) ) )
35	32, 33, 34	mp2an 670	. . . . . . . . 9 |- ( ( 0 ... ( P - 1 ) ) ^m ( 0 ... M ) ) C_ ( NN0 ^m ( 0 ... M ) )
36	25	simpld 457	. . . . . . . . 9 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> c e. ( ( 0 ... ( P - 1 ) ) ^m ( 0 ... M ) ) )
37	35, 36	sseldi 3415	. . . . . . . 8 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> c e. ( NN0 ^m ( 0 ... M ) ) )
38	30, 31, 37	mccl 31772	. . . . . . 7 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> ( ( ! ` sum_ j e. ( 0 ... M ) ( c ` j ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) e. NN )
39	29, 38	eqeltrd 2470	. . . . . 6 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> ( ( ! ` ( P - 1 ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) e. NN )
40	39	nnzd 10883	. . . . 5 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> ( ( ! ` ( P - 1 ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) e. ZZ )
41	8	adantr 463	. . . . . . 7 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> P e. NN )
42	9	adantr 463	. . . . . . 7 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> M e. NN0 )
43		elmapi 7359	. . . . . . . 8 |- ( c e. ( ( 0 ... ( P - 1 ) ) ^m ( 0 ... M ) ) -> c : ( 0 ... M ) --> ( 0 ... ( P - 1 ) ) )
44	36, 43	syl 16	. . . . . . 7 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> c : ( 0 ... M ) --> ( 0 ... ( P - 1 ) ) )
45		0zd 10793	. . . . . . 7 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> 0 e. ZZ )
46	41, 42, 44, 45	etransclem10 32193	. . . . . 6 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> if ( ( P - 1 ) < ( c ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) ) x. ( 0 ^ ( ( P - 1 ) - ( c ` 0 ) ) ) ) ) e. ZZ )
47		fzfid 11986	. . . . . . 7 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> ( 1 ... M ) e. Fin )
48	8	ad2antrr 723	. . . . . . . 8 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 1 ... M ) ) -> P e. NN )
49	44	adantr 463	. . . . . . . 8 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 1 ... M ) ) -> c : ( 0 ... M ) --> ( 0 ... ( P - 1 ) ) )
50		fz1ssfz0 31676	. . . . . . . . . 10 |- ( 1 ... M ) C_ ( 0 ... M )
51	50	sseli 3413	. . . . . . . . 9 |- ( j e. ( 1 ... M ) -> j e. ( 0 ... M ) )
52	51	adantl 464	. . . . . . . 8 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 1 ... M ) ) -> j e. ( 0 ... M ) )
53		0zd 10793	. . . . . . . 8 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 1 ... M ) ) -> 0 e. ZZ )
54	48, 49, 52, 53	etransclem3 32186	. . . . . . 7 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 1 ... M ) ) -> if ( P < ( c ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( c ` j ) ) ) ) x. ( ( 0 - j ) ^ ( P - ( c ` j ) ) ) ) ) e. ZZ )
55	47, 54	fprodzcl 13763	. . . . . 6 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> prod_ j e. ( 1 ... M ) if ( P < ( c ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( c ` j ) ) ) ) x. ( ( 0 - j ) ^ ( P - ( c ` j ) ) ) ) ) e. ZZ )
56	46, 55	zmulcld 10890	. . . . 5 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> ( if ( ( P - 1 ) < ( c ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) ) x. ( 0 ^ ( ( P - 1 ) - ( c ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( c ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( c ` j ) ) ) ) x. ( ( 0 - j ) ^ ( P - ( c ` j ) ) ) ) ) ) e. ZZ )
57	40, 56	zmulcld 10890	. . . 4 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> ( ( ( ! ` ( P - 1 ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) x. ( if ( ( P - 1 ) < ( c ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) ) x. ( 0 ^ ( ( P - 1 ) - ( c ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( c ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( c ` j ) ) ) ) x. ( ( 0 - j ) ^ ( P - ( c ` j ) ) ) ) ) ) ) e. ZZ )
58	57	zcnd 10885	. . 3 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> ( ( ( ! ` ( P - 1 ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) x. ( if ( ( P - 1 ) < ( c ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) ) x. ( 0 ^ ( ( P - 1 ) - ( c ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( c ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( c ` j ) ) ) ) x. ( ( 0 - j ) ^ ( P - ( c ` j ) ) ) ) ) ) ) e. CC )
59		nn0uz 11035	. . . . . . . . . . 11 |- NN0 = ( ZZ>= ` 0 )
60	12, 59	syl6eleq 2480	. . . . . . . . . 10 |- ( ph -> ( P - 1 ) e. ( ZZ>= ` 0 ) )
61		eluzfz2 11615	. . . . . . . . . 10 |- ( ( P - 1 ) e. ( ZZ>= ` 0 ) -> ( P - 1 ) e. ( 0 ... ( P - 1 ) ) )
62	60, 61	syl 16	. . . . . . . . 9 |- ( ph -> ( P - 1 ) e. ( 0 ... ( P - 1 ) ) )
63		eluzfz1 11614	. . . . . . . . . 10 |- ( ( P - 1 ) e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... ( P - 1 ) ) )
64	60, 63	syl 16	. . . . . . . . 9 |- ( ph -> 0 e. ( 0 ... ( P - 1 ) ) )
65	62, 64	ifcld 3900	. . . . . . . 8 |- ( ph -> if ( j = 0 , ( P - 1 ) , 0 ) e. ( 0 ... ( P - 1 ) ) )
66	65	adantr 463	. . . . . . 7 |- ( ( ph /\ j e. ( 0 ... M ) ) -> if ( j = 0 , ( P - 1 ) , 0 ) e. ( 0 ... ( P - 1 ) ) )
67		etransclem35.d	. . . . . . 7 |- D = ( j e. ( 0 ... M ) |-> if ( j = 0 , ( P - 1 ) , 0 ) )
68	66, 67	fmptd 5957	. . . . . 6 |- ( ph -> D : ( 0 ... M ) --> ( 0 ... ( P - 1 ) ) )
69		ovex 6224	. . . . . . 7 |- ( 0 ... ( P - 1 ) ) e. _V
70		ovex 6224	. . . . . . 7 |- ( 0 ... M ) e. _V
71	69, 70	elmap 7366	. . . . . 6 |- ( D e. ( ( 0 ... ( P - 1 ) ) ^m ( 0 ... M ) ) <-> D : ( 0 ... M ) --> ( 0 ... ( P - 1 ) ) )
72	68, 71	sylibr 212	. . . . 5 |- ( ph -> D e. ( ( 0 ... ( P - 1 ) ) ^m ( 0 ... M ) ) )
73	9, 59	syl6eleq 2480	. . . . . . 7 |- ( ph -> M e. ( ZZ>= ` 0 ) )
74		fzsscn 31680	. . . . . . . 8 |- ( 0 ... ( P - 1 ) ) C_ CC
75	68	ffvelrnda 5933	. . . . . . . 8 |- ( ( ph /\ j e. ( 0 ... M ) ) -> ( D ` j ) e. ( 0 ... ( P - 1 ) ) )
76	74, 75	sseldi 3415	. . . . . . 7 |- ( ( ph /\ j e. ( 0 ... M ) ) -> ( D ` j ) e. CC )
77		fveq2 5774	. . . . . . 7 |- ( j = 0 -> ( D ` j ) = ( D ` 0 ) )
78	73, 76, 77	fsum1p 13570	. . . . . 6 |- ( ph -> sum_ j e. ( 0 ... M ) ( D ` j ) = ( ( D ` 0 ) + sum_ j e. ( ( 0 + 1 ) ... M ) ( D ` j ) ) )
79	67	a1i 11	. . . . . . . 8 |- ( ph -> D = ( j e. ( 0 ... M ) |-> if ( j = 0 , ( P - 1 ) , 0 ) ) )
80		simpr 459	. . . . . . . . 9 |- ( ( ph /\ j = 0 ) -> j = 0 )
81	80	iftrued 3865	. . . . . . . 8 |- ( ( ph /\ j = 0 ) -> if ( j = 0 , ( P - 1 ) , 0 ) = ( P - 1 ) )
82		eluzfz1 11614	. . . . . . . . 9 |- ( M e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... M ) )
83	73, 82	syl 16	. . . . . . . 8 |- ( ph -> 0 e. ( 0 ... M ) )
84	79, 81, 83, 12	fvmptd 5862	. . . . . . 7 |- ( ph -> ( D ` 0 ) = ( P - 1 ) )
85		0p1e1 10564	. . . . . . . . . . 11 |- ( 0 + 1 ) = 1
86	85	oveq1i 6206	. . . . . . . . . 10 |- ( ( 0 + 1 ) ... M ) = ( 1 ... M )
87	86	sumeq1i 13522	. . . . . . . . 9 |- sum_ j e. ( ( 0 + 1 ) ... M ) ( D ` j ) = sum_ j e. ( 1 ... M ) ( D ` j )
88	87	a1i 11	. . . . . . . 8 |- ( ph -> sum_ j e. ( ( 0 + 1 ) ... M ) ( D ` j ) = sum_ j e. ( 1 ... M ) ( D ` j ) )
89	67	fvmpt2 5865	. . . . . . . . . . 11 |- ( ( j e. ( 0 ... M ) /\ if ( j = 0 , ( P - 1 ) , 0 ) e. ( 0 ... ( P - 1 ) ) ) -> ( D ` j ) = if ( j = 0 , ( P - 1 ) , 0 ) )
90	51, 65, 89	syl2anr 476	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( D ` j ) = if ( j = 0 , ( P - 1 ) , 0 ) )
91		0red 9508	. . . . . . . . . . . . . 14 |- ( j e. ( 1 ... M ) -> 0 e. RR )
92		1red 9522	. . . . . . . . . . . . . . 15 |- ( j e. ( 1 ... M ) -> 1 e. RR )
93		elfzelz 11609	. . . . . . . . . . . . . . . 16 |- ( j e. ( 1 ... M ) -> j e. ZZ )
94	93	zred 10884	. . . . . . . . . . . . . . 15 |- ( j e. ( 1 ... M ) -> j e. RR )
95		0lt1 9992	. . . . . . . . . . . . . . . 16 |- 0 < 1
96	95	a1i 11	. . . . . . . . . . . . . . 15 |- ( j e. ( 1 ... M ) -> 0 < 1 )
97		elfzle1 11610	. . . . . . . . . . . . . . 15 |- ( j e. ( 1 ... M ) -> 1 <_ j )
98	91, 92, 94, 96, 97	ltletrd 9653	. . . . . . . . . . . . . 14 |- ( j e. ( 1 ... M ) -> 0 < j )
99	91, 98	gtned 9631	. . . . . . . . . . . . 13 |- ( j e. ( 1 ... M ) -> j =/= 0 )
100	99	neneqd 2584	. . . . . . . . . . . 12 |- ( j e. ( 1 ... M ) -> -. j = 0 )
101	100	iffalsed 3868	. . . . . . . . . . 11 |- ( j e. ( 1 ... M ) -> if ( j = 0 , ( P - 1 ) , 0 ) = 0 )
102	101	adantl 464	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 1 ... M ) ) -> if ( j = 0 , ( P - 1 ) , 0 ) = 0 )
103	90, 102	eqtrd 2423	. . . . . . . . 9 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( D ` j ) = 0 )
104	103	sumeq2dv 13527	. . . . . . . 8 |- ( ph -> sum_ j e. ( 1 ... M ) ( D ` j ) = sum_ j e. ( 1 ... M ) 0 )
105		fzfi 11985	. . . . . . . . . 10 |- ( 1 ... M ) e. Fin
106	105	olci 389	. . . . . . . . 9 |- ( ( 1 ... M ) C_ ( ZZ>= ` A ) \/ ( 1 ... M ) e. Fin )
107		sumz 13546	. . . . . . . . 9 |- ( ( ( 1 ... M ) C_ ( ZZ>= ` A ) \/ ( 1 ... M ) e. Fin ) -> sum_ j e. ( 1 ... M ) 0 = 0 )
108	106, 107	mp1i 12	. . . . . . . 8 |- ( ph -> sum_ j e. ( 1 ... M ) 0 = 0 )
109	88, 104, 108	3eqtrd 2427	. . . . . . 7 |- ( ph -> sum_ j e. ( ( 0 + 1 ) ... M ) ( D ` j ) = 0 )
110	84, 109	oveq12d 6214	. . . . . 6 |- ( ph -> ( ( D ` 0 ) + sum_ j e. ( ( 0 + 1 ) ... M ) ( D ` j ) ) = ( ( P - 1 ) + 0 ) )
111	8	nncnd 10468	. . . . . . . 8 |- ( ph -> P e. CC )
112		1cnd 9523	. . . . . . . 8 |- ( ph -> 1 e. CC )
113	111, 112	subcld 9844	. . . . . . 7 |- ( ph -> ( P - 1 ) e. CC )
114	113	addid1d 9691	. . . . . 6 |- ( ph -> ( ( P - 1 ) + 0 ) = ( P - 1 ) )
115	78, 110, 114	3eqtrd 2427	. . . . 5 |- ( ph -> sum_ j e. ( 0 ... M ) ( D ` j ) = ( P - 1 ) )
116		fveq1 5773	. . . . . . . 8 |- ( c = D -> ( c ` j ) = ( D ` j ) )
117	116	sumeq2ad 31732	. . . . . . 7 |- ( c = D -> sum_ j e. ( 0 ... M ) ( c ` j ) = sum_ j e. ( 0 ... M ) ( D ` j ) )
118	117	eqeq1d 2384	. . . . . 6 |- ( c = D -> ( sum_ j e. ( 0 ... M ) ( c ` j ) = ( P - 1 ) <-> sum_ j e. ( 0 ... M ) ( D ` j ) = ( P - 1 ) ) )
119	118	elrab 3182	. . . . 5 |- ( D e. { c e. ( ( 0 ... ( P - 1 ) ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = ( P - 1 ) } <-> ( D e. ( ( 0 ... ( P - 1 ) ) ^m ( 0 ... M ) ) /\ sum_ j e. ( 0 ... M ) ( D ` j ) = ( P - 1 ) ) )
120	72, 115, 119	sylanbrc 662	. . . 4 |- ( ph -> D e. { c e. ( ( 0 ... ( P - 1 ) ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = ( P - 1 ) } )
121	120, 21	eleqtrrd 2473	. . 3 |- ( ph -> D e. ( C ` ( P - 1 ) ) )
122	116	fveq2d 5778	. . . . . 6 |- ( c = D -> ( ! ` ( c ` j ) ) = ( ! ` ( D ` j ) ) )
123	122	prodeq2ad 31756	. . . . 5 |- ( c = D -> prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) = prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) )
124	123	oveq2d 6212	. . . 4 |- ( c = D -> ( ( ! ` ( P - 1 ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) = ( ( ! ` ( P - 1 ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) )
125		fveq1 5773	. . . . . . 7 |- ( c = D -> ( c ` 0 ) = ( D ` 0 ) )
126	125	breq2d 4379	. . . . . 6 |- ( c = D -> ( ( P - 1 ) < ( c ` 0 ) <-> ( P - 1 ) < ( D ` 0 ) ) )
127	125	oveq2d 6212	. . . . . . . . 9 |- ( c = D -> ( ( P - 1 ) - ( c ` 0 ) ) = ( ( P - 1 ) - ( D ` 0 ) ) )
128	127	fveq2d 5778	. . . . . . . 8 |- ( c = D -> ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) = ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) )
129	128	oveq2d 6212	. . . . . . 7 |- ( c = D -> ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) ) = ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) )
130	127	oveq2d 6212	. . . . . . 7 |- ( c = D -> ( 0 ^ ( ( P - 1 ) - ( c ` 0 ) ) ) = ( 0 ^ ( ( P - 1 ) - ( D ` 0 ) ) ) )
131	129, 130	oveq12d 6214	. . . . . 6 |- ( c = D -> ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) ) x. ( 0 ^ ( ( P - 1 ) - ( c ` 0 ) ) ) ) = ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( 0 ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) )
132	126, 131	ifbieq2d 3882	. . . . 5 |- ( c = D -> if ( ( P - 1 ) < ( c ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) ) x. ( 0 ^ ( ( P - 1 ) - ( c ` 0 ) ) ) ) ) = if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( 0 ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) )
133	116	breq2d 4379	. . . . . . 7 |- ( c = D -> ( P < ( c ` j ) <-> P < ( D ` j ) ) )
134	116	oveq2d 6212	. . . . . . . . . 10 |- ( c = D -> ( P - ( c ` j ) ) = ( P - ( D ` j ) ) )
135	134	fveq2d 5778	. . . . . . . . 9 |- ( c = D -> ( ! ` ( P - ( c ` j ) ) ) = ( ! ` ( P - ( D ` j ) ) ) )
136	135	oveq2d 6212	. . . . . . . 8 |- ( c = D -> ( ( ! ` P ) / ( ! ` ( P - ( c ` j ) ) ) ) = ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) )
137	134	oveq2d 6212	. . . . . . . 8 |- ( c = D -> ( ( 0 - j ) ^ ( P - ( c ` j ) ) ) = ( ( 0 - j ) ^ ( P - ( D ` j ) ) ) )
138	136, 137	oveq12d 6214	. . . . . . 7 |- ( c = D -> ( ( ( ! ` P ) / ( ! ` ( P - ( c ` j ) ) ) ) x. ( ( 0 - j ) ^ ( P - ( c ` j ) ) ) ) = ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( 0 - j ) ^ ( P - ( D ` j ) ) ) ) )
139	133, 138	ifbieq2d 3882	. . . . . 6 |- ( c = D -> if ( P < ( c ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( c ` j ) ) ) ) x. ( ( 0 - j ) ^ ( P - ( c ` j ) ) ) ) ) = if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( 0 - j ) ^ ( P - ( D ` j ) ) ) ) ) )
140	139	prodeq2ad 31756	. . . . 5 |- ( c = D -> prod_ j e. ( 1 ... M ) if ( P < ( c ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( c ` j ) ) ) ) x. ( ( 0 - j ) ^ ( P - ( c ` j ) ) ) ) ) = prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( 0 - j ) ^ ( P - ( D ` j ) ) ) ) ) )
141	132, 140	oveq12d 6214	. . . 4 |- ( c = D -> ( if ( ( P - 1 ) < ( c ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) ) x. ( 0 ^ ( ( P - 1 ) - ( c ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( c ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( c ` j ) ) ) ) x. ( ( 0 - j ) ^ ( P - ( c ` j ) ) ) ) ) ) = ( if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( 0 ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( 0 - j ) ^ ( P - ( D ` j ) ) ) ) ) ) )
142	124, 141	oveq12d 6214	. . 3 |- ( c = D -> ( ( ( ! ` ( P - 1 ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) x. ( if ( ( P - 1 ) < ( c ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) ) x. ( 0 ^ ( ( P - 1 ) - ( c ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( c ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( c ` j ) ) ) ) x. ( ( 0 - j ) ^ ( P - ( c ` j ) ) ) ) ) ) ) = ( ( ( ! ` ( P - 1 ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. ( if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( 0 ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( 0 - j ) ^ ( P - ( D ` j ) ) ) ) ) ) ) )
143	17, 18, 19, 58, 121, 142	fsumsplit1 31739	. 2 |- ( ph -> sum_ c e. ( C ` ( P - 1 ) ) ( ( ( ! ` ( P - 1 ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) x. ( if ( ( P - 1 ) < ( c ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) ) x. ( 0 ^ ( ( P - 1 ) - ( c ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( c ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( c ` j ) ) ) ) x. ( ( 0 - j ) ^ ( P - ( c ` j ) ) ) ) ) ) ) = ( ( ( ( ! ` ( P - 1 ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. ( if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( 0 ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( 0 - j ) ^ ( P - ( D ` j ) ) ) ) ) ) ) + sum_ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ( ( ( ! ` ( P - 1 ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) x. ( if ( ( P - 1 ) < ( c ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) ) x. ( 0 ^ ( ( P - 1 ) - ( c ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( c ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( c ` j ) ) ) ) x. ( ( 0 - j ) ^ ( P - ( c ` j ) ) ) ) ) ) ) ) )
144	33, 75	sseldi 3415	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0 ... M ) ) -> ( D ` j ) e. NN0 )
145	144	faccld 31682	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0 ... M ) ) -> ( ! ` ( D ` j ) ) e. NN )
146	145	nncnd 10468	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0 ... M ) ) -> ( ! ` ( D ` j ) ) e. CC )
147	77	fveq2d 5778	. . . . . . . . . 10 |- ( j = 0 -> ( ! ` ( D ` j ) ) = ( ! ` ( D ` 0 ) ) )
148	73, 146, 147	fprod1p 13774	. . . . . . . . 9 |- ( ph -> prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) = ( ( ! ` ( D ` 0 ) ) x. prod_ j e. ( ( 0 + 1 ) ... M ) ( ! ` ( D ` j ) ) ) )
149	84	fveq2d 5778	. . . . . . . . . 10 |- ( ph -> ( ! ` ( D ` 0 ) ) = ( ! ` ( P - 1 ) ) )
150	86	prodeq1i 13727	. . . . . . . . . . . 12 |- prod_ j e. ( ( 0 + 1 ) ... M ) ( ! ` ( D ` j ) ) = prod_ j e. ( 1 ... M ) ( ! ` ( D ` j ) )
151	150	a1i 11	. . . . . . . . . . 11 |- ( ph -> prod_ j e. ( ( 0 + 1 ) ... M ) ( ! ` ( D ` j ) ) = prod_ j e. ( 1 ... M ) ( ! ` ( D ` j ) ) )
152	103	fveq2d 5778	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ! ` ( D ` j ) ) = ( ! ` 0 ) )
153		fac0 12258	. . . . . . . . . . . . 13 |- ( ! ` 0 ) = 1
154	152, 153	syl6eq 2439	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ! ` ( D ` j ) ) = 1 )
155	154	prodeq2dv 13732	. . . . . . . . . . 11 |- ( ph -> prod_ j e. ( 1 ... M ) ( ! ` ( D ` j ) ) = prod_ j e. ( 1 ... M ) 1 )
156		prod1 13753	. . . . . . . . . . . 12 |- ( ( ( 1 ... M ) C_ ( ZZ>= ` A ) \/ ( 1 ... M ) e. Fin ) -> prod_ j e. ( 1 ... M ) 1 = 1 )
157	106, 156	mp1i 12	. . . . . . . . . . 11 |- ( ph -> prod_ j e. ( 1 ... M ) 1 = 1 )
158	151, 155, 157	3eqtrd 2427	. . . . . . . . . 10 |- ( ph -> prod_ j e. ( ( 0 + 1 ) ... M ) ( ! ` ( D ` j ) ) = 1 )
159	149, 158	oveq12d 6214	. . . . . . . . 9 |- ( ph -> ( ( ! ` ( D ` 0 ) ) x. prod_ j e. ( ( 0 + 1 ) ... M ) ( ! ` ( D ` j ) ) ) = ( ( ! ` ( P - 1 ) ) x. 1 ) )
160	12	faccld 31682	. . . . . . . . . . 11 |- ( ph -> ( ! ` ( P - 1 ) ) e. NN )
161	160	nncnd 10468	. . . . . . . . . 10 |- ( ph -> ( ! ` ( P - 1 ) ) e. CC )
162	161	mulid1d 9524	. . . . . . . . 9 |- ( ph -> ( ( ! ` ( P - 1 ) ) x. 1 ) = ( ! ` ( P - 1 ) ) )
163	148, 159, 162	3eqtrd 2427	. . . . . . . 8 |- ( ph -> prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) = ( ! ` ( P - 1 ) ) )
164	163	oveq2d 6212	. . . . . . 7 |- ( ph -> ( ( ! ` ( P - 1 ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) = ( ( ! ` ( P - 1 ) ) / ( ! ` ( P - 1 ) ) ) )
165	160	nnne0d 10497	. . . . . . . 8 |- ( ph -> ( ! ` ( P - 1 ) ) =/= 0 )
166	161, 165	dividd 10235	. . . . . . 7 |- ( ph -> ( ( ! ` ( P - 1 ) ) / ( ! ` ( P - 1 ) ) ) = 1 )
167	164, 166	eqtrd 2423	. . . . . 6 |- ( ph -> ( ( ! ` ( P - 1 ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) = 1 )
168	12	nn0red 10770	. . . . . . . . . . . . 13 |- ( ph -> ( P - 1 ) e. RR )
169	84, 168	eqeltrd 2470	. . . . . . . . . . . 12 |- ( ph -> ( D ` 0 ) e. RR )
170	169, 168	lttri3d 9636	. . . . . . . . . . 11 |- ( ph -> ( ( D ` 0 ) = ( P - 1 ) <-> ( -. ( D ` 0 ) < ( P - 1 ) /\ -. ( P - 1 ) < ( D ` 0 ) ) ) )
171	84, 170	mpbid 210	. . . . . . . . . 10 |- ( ph -> ( -. ( D ` 0 ) < ( P - 1 ) /\ -. ( P - 1 ) < ( D ` 0 ) ) )
172	171	simprd 461	. . . . . . . . 9 |- ( ph -> -. ( P - 1 ) < ( D ` 0 ) )
173	172	iffalsed 3868	. . . . . . . 8 |- ( ph -> if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( 0 ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) = ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( 0 ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) )
174	84	eqcomd 2390	. . . . . . . . . . . . . 14 |- ( ph -> ( P - 1 ) = ( D ` 0 ) )
175	113, 174	subeq0bd 9903	. . . . . . . . . . . . 13 |- ( ph -> ( ( P - 1 ) - ( D ` 0 ) ) = 0 )
176	175	fveq2d 5778	. . . . . . . . . . . 12 |- ( ph -> ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) = ( ! ` 0 ) )
177	176, 153	syl6eq 2439	. . . . . . . . . . 11 |- ( ph -> ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) = 1 )
178	177	oveq2d 6212	. . . . . . . . . 10 |- ( ph -> ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) = ( ( ! ` ( P - 1 ) ) / 1 ) )
179	161	div1d 10229	. . . . . . . . . 10 |- ( ph -> ( ( ! ` ( P - 1 ) ) / 1 ) = ( ! ` ( P - 1 ) ) )
180	178, 179	eqtrd 2423	. . . . . . . . 9 |- ( ph -> ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) = ( ! ` ( P - 1 ) ) )
181	175	oveq2d 6212	. . . . . . . . . 10 |- ( ph -> ( 0 ^ ( ( P - 1 ) - ( D ` 0 ) ) ) = ( 0 ^ 0 ) )
182		0cnd 9500	. . . . . . . . . . 11 |- ( ph -> 0 e. CC )
183	182	exp0d 12206	. . . . . . . . . 10 |- ( ph -> ( 0 ^ 0 ) = 1 )
184	181, 183	eqtrd 2423	. . . . . . . . 9 |- ( ph -> ( 0 ^ ( ( P - 1 ) - ( D ` 0 ) ) ) = 1 )
185	180, 184	oveq12d 6214	. . . . . . . 8 |- ( ph -> ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( 0 ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) = ( ( ! ` ( P - 1 ) ) x. 1 ) )
186	173, 185, 162	3eqtrd 2427	. . . . . . 7 |- ( ph -> if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( 0 ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) = ( ! ` ( P - 1 ) ) )
187		fzssre 31684	. . . . . . . . . . . 12 |- ( 0 ... ( P - 1 ) ) C_ RR
188	68	adantr 463	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 1 ... M ) ) -> D : ( 0 ... M ) --> ( 0 ... ( P - 1 ) ) )
189	51	adantl 464	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 1 ... M ) ) -> j e. ( 0 ... M ) )
190	188, 189	ffvelrnd 5934	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( D ` j ) e. ( 0 ... ( P - 1 ) ) )
191	187, 190	sseldi 3415	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( D ` j ) e. RR )
192	8	nnred 10467	. . . . . . . . . . . 12 |- ( ph -> P e. RR )
193	192	adantr 463	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> P e. RR )
194	8	nngt0d 10496	. . . . . . . . . . . . . 14 |- ( ph -> 0 < P )
195	15, 192, 194	ltled 9644	. . . . . . . . . . . . 13 |- ( ph -> 0 <_ P )
196	195	adantr 463	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 1 ... M ) ) -> 0 <_ P )
197	103, 196	eqbrtrd 4387	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( D ` j ) <_ P )
198	191, 193, 197	leimnltd 31639	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 1 ... M ) ) -> -. P < ( D ` j ) )
199	198	iffalsed 3868	. . . . . . . . 9 |- ( ( ph /\ j e. ( 1 ... M ) ) -> if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( 0 - j ) ^ ( P - ( D ` j ) ) ) ) ) = ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( 0 - j ) ^ ( P - ( D ` j ) ) ) ) )
200	103	oveq2d 6212	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( P - ( D ` j ) ) = ( P - 0 ) )
201	111	adantr 463	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. ( 1 ... M ) ) -> P e. CC )
202	201	subid1d 9833	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( P - 0 ) = P )
203	200, 202	eqtrd 2423	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( P - ( D ` j ) ) = P )
204	203	fveq2d 5778	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ! ` ( P - ( D ` j ) ) ) = ( ! ` P ) )
205	204	oveq2d 6212	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) = ( ( ! ` P ) / ( ! ` P ) ) )
206	8	nnnn0d 10769	. . . . . . . . . . . . . . 15 |- ( ph -> P e. NN0 )
207	206	faccld 31682	. . . . . . . . . . . . . 14 |- ( ph -> ( ! ` P ) e. NN )
208	207	nncnd 10468	. . . . . . . . . . . . 13 |- ( ph -> ( ! ` P ) e. CC )
209	207	nnne0d 10497	. . . . . . . . . . . . 13 |- ( ph -> ( ! ` P ) =/= 0 )
210	208, 209	dividd 10235	. . . . . . . . . . . 12 |- ( ph -> ( ( ! ` P ) / ( ! ` P ) ) = 1 )
211	210	adantr 463	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( ! ` P ) / ( ! ` P ) ) = 1 )
212	205, 211	eqtrd 2423	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) = 1 )
213		df-neg 9721	. . . . . . . . . . . . 13 |- -u j = ( 0 - j )
214	213	eqcomi 2395	. . . . . . . . . . . 12 |- ( 0 - j ) = -u j
215	214	a1i 11	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( 0 - j ) = -u j )
216	215, 203	oveq12d 6214	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( 0 - j ) ^ ( P - ( D ` j ) ) ) = ( -u j ^ P ) )
217	212, 216	oveq12d 6214	. . . . . . . . 9 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( 0 - j ) ^ ( P - ( D ` j ) ) ) ) = ( 1 x. ( -u j ^ P ) ) )
218	93	znegcld 10886	. . . . . . . . . . . . 13 |- ( j e. ( 1 ... M ) -> -u j e. ZZ )
219	218	zcnd 10885	. . . . . . . . . . . 12 |- ( j e. ( 1 ... M ) -> -u j e. CC )
220	219	adantl 464	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> -u j e. CC )
221	206	adantr 463	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> P e. NN0 )
222	220, 221	expcld 12212	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( -u j ^ P ) e. CC )
223	222	mulid2d 9525	. . . . . . . . 9 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( 1 x. ( -u j ^ P ) ) = ( -u j ^ P ) )
224	199, 217, 223	3eqtrd 2427	. . . . . . . 8 |- ( ( ph /\ j e. ( 1 ... M ) ) -> if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( 0 - j ) ^ ( P - ( D ` j ) ) ) ) ) = ( -u j ^ P ) )
225	224	prodeq2dv 13732	. . . . . . 7 |- ( ph -> prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( 0 - j ) ^ ( P - ( D ` j ) ) ) ) ) = prod_ j e. ( 1 ... M ) ( -u j ^ P ) )
226	186, 225	oveq12d 6214	. . . . . 6 |- ( ph -> ( if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( 0 ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( 0 - j ) ^ ( P - ( D ` j ) ) ) ) ) ) = ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( -u j ^ P ) ) )
227	167, 226	oveq12d 6214	. . . . 5 |- ( ph -> ( ( ( ! ` ( P - 1 ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. ( if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( 0 ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( 0 - j ) ^ ( P - ( D ` j ) ) ) ) ) ) ) = ( 1 x. ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( -u j ^ P ) ) ) )
228		fzfid 11986	. . . . . . . . 9 |- ( ph -> ( 1 ... M ) e. Fin )
229		zexpcl 12084	. . . . . . . . . 10 |- ( ( -u j e. ZZ /\ P e. NN0 ) -> ( -u j ^ P ) e. ZZ )
230	218, 206, 229	syl2anr 476	. . . . . . . . 9 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( -u j ^ P ) e. ZZ )
231	228, 230	fprodzcl 13763	. . . . . . . 8 |- ( ph -> prod_ j e. ( 1 ... M ) ( -u j ^ P ) e. ZZ )
232	231	zcnd 10885	. . . . . . 7 |- ( ph -> prod_ j e. ( 1 ... M ) ( -u j ^ P ) e. CC )
233	161, 232	mulcld 9527	. . . . . 6 |- ( ph -> ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( -u j ^ P ) ) e. CC )
234	233	mulid2d 9525	. . . . 5 |- ( ph -> ( 1 x. ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( -u j ^ P ) ) ) = ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( -u j ^ P ) ) )
235	227, 234	eqtrd 2423	. . . 4 |- ( ph -> ( ( ( ! ` ( P - 1 ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. ( if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( 0 ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( 0 - j ) ^ ( P - ( D ` j ) ) ) ) ) ) ) = ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( -u j ^ P ) ) )
236		eldifi 3540	. . . . . . . . . . . . . . 15 |- ( c e. ( ( C ` ( P - 1 ) ) \ { D } ) -> c e. ( C ` ( P - 1 ) ) )
237	83	adantr 463	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> 0 e. ( 0 ... M ) )
238	44, 237	ffvelrnd 5934	. . . . . . . . . . . . . . 15 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> ( c ` 0 ) e. ( 0 ... ( P - 1 ) ) )
239	236, 238	sylan2 472	. . . . . . . . . . . . . 14 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( c ` 0 ) e. ( 0 ... ( P - 1 ) ) )
240	187, 239	sseldi 3415	. . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( c ` 0 ) e. RR )
241	168	adantr 463	. . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( P - 1 ) e. RR )
242		elfzle2 11611	. . . . . . . . . . . . . 14 |- ( ( c ` 0 ) e. ( 0 ... ( P - 1 ) ) -> ( c ` 0 ) <_ ( P - 1 ) )
243	239, 242	syl 16	. . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( c ` 0 ) <_ ( P - 1 ) )
244	240, 241, 243	leimnltd 31639	. . . . . . . . . . . 12 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> -. ( P - 1 ) < ( c ` 0 ) )
245	244	iffalsed 3868	. . . . . . . . . . 11 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> if ( ( P - 1 ) < ( c ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) ) x. ( 0 ^ ( ( P - 1 ) - ( c ` 0 ) ) ) ) ) = ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) ) x. ( 0 ^ ( ( P - 1 ) - ( c ` 0 ) ) ) ) )
246	12	nn0zd 10882	. . . . . . . . . . . . . . . 16 |- ( ph -> ( P - 1 ) e. ZZ )
247	246	adantr 463	. . . . . . . . . . . . . . 15 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( P - 1 ) e. ZZ )
248	239	elfzelzd 31685	. . . . . . . . . . . . . . 15 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( c ` 0 ) e. ZZ )
249	247, 248	zsubcld 10889	. . . . . . . . . . . . . 14 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( ( P - 1 ) - ( c ` 0 ) ) e. ZZ )
250		ffn 5639	. . . . . . . . . . . . . . . . . . . . . 22 |- ( c : ( 0 ... M ) --> ( 0 ... ( P - 1 ) ) -> c Fn ( 0 ... M ) )
251	44, 250	syl 16	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> c Fn ( 0 ... M ) )
252	251	adantr 463	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) -> c Fn ( 0 ... M ) )
253		ffn 5639	. . . . . . . . . . . . . . . . . . . . . 22 |- ( D : ( 0 ... M ) --> ( 0 ... ( P - 1 ) ) -> D Fn ( 0 ... M ) )
254	68, 253	syl 16	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> D Fn ( 0 ... M ) )
255	254	ad2antrr 723	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) -> D Fn ( 0 ... M ) )
256		fveq2 5774	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( j = 0 -> ( c ` j ) = ( c ` 0 ) )
257	256	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ ( P - 1 ) = ( c ` 0 ) ) /\ j = 0 ) -> ( c ` j ) = ( c ` 0 ) )
258		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( P - 1 ) = ( c ` 0 ) -> ( P - 1 ) = ( c ` 0 ) )
259	258	eqcomd 2390	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( P - 1 ) = ( c ` 0 ) -> ( c ` 0 ) = ( P - 1 ) )
260	259	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ ( P - 1 ) = ( c ` 0 ) ) /\ j = 0 ) -> ( c ` 0 ) = ( P - 1 ) )
261	77	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ j = 0 ) -> ( D ` j ) = ( D ` 0 ) )
262	84	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ j = 0 ) -> ( D ` 0 ) = ( P - 1 ) )
263	261, 262	eqtr2d 2424	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ j = 0 ) -> ( P - 1 ) = ( D ` j ) )
264	263	adantlr 712	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ ( P - 1 ) = ( c ` 0 ) ) /\ j = 0 ) -> ( P - 1 ) = ( D ` j ) )
265	257, 260, 264	3eqtrd 2427	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ ( P - 1 ) = ( c ` 0 ) ) /\ j = 0 ) -> ( c ` j ) = ( D ` j ) )
266	265	adantllr 716	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) /\ j = 0 ) -> ( c ` j ) = ( D ` j ) )
267	266	adantlr 712	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) /\ j e. ( 0 ... M ) ) /\ j = 0 ) -> ( c ` j ) = ( D ` j ) )
268	26	ad4antr 729	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> sum_ j e. ( 0 ... M ) ( c ` j ) = ( P - 1 ) )
269	168	ad5antr 731	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> ( P - 1 ) e. RR )
270	168	ad4antr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> ( P - 1 ) e. RR )
271	44	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( 1 ... M ) ) -> c : ( 0 ... M ) --> ( 0 ... ( P - 1 ) ) )
272	50	sseli 3413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( k e. ( 1 ... M ) -> k e. ( 0 ... M ) )
273	272	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( 1 ... M ) ) -> k e. ( 0 ... M ) )
274	271, 273	ffvelrnd 5934	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( 1 ... M ) ) -> ( c ` k ) e. ( 0 ... ( P - 1 ) ) )
275	33, 274	sseldi 3415	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( 1 ... M ) ) -> ( c ` k ) e. NN0 )
276	47, 275	fsumnn0cl 13560	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> sum_ k e. ( 1 ... M ) ( c ` k ) e. NN0 )
277	276	nn0red 10770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> sum_ k e. ( 1 ... M ) ( c ` k ) e. RR )
278	277	ad3antrrr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> sum_ k e. ( 1 ... M ) ( c ` k ) e. RR )
279		0red 9508	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> 0 e. RR )
280	44	ffvelrnda 5933	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) -> ( c ` j ) e. ( 0 ... ( P - 1 ) ) )
281	187, 280	sseldi 3415	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) -> ( c ` j ) e. RR )
282	281	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> ( c ` j ) e. RR )
283		nfv 1715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- F/ k ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 )
284		nfcv 2544	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- F/_ k ( c ` j )
285		fzfid 11986	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> ( 1 ... M ) e. Fin )
286		simp-4l 765	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) /\ k e. ( 1 ... M ) ) -> ( ph /\ c e. ( C ` ( P - 1 ) ) ) )
287	74, 274	sseldi 3415	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( 1 ... M ) ) -> ( c ` k ) e. CC )
288	286, 287	sylancom 665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) /\ k e. ( 1 ... M ) ) -> ( c ` k ) e. CC )
289		1zzd 10812	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> 1 e. ZZ )
290		elfzel2 11607	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( j e. ( 0 ... M ) -> M e. ZZ )
291	290	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> M e. ZZ )
292		elfzelz 11609	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( j e. ( 0 ... M ) -> j e. ZZ )
293	292	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> j e. ZZ )
294	289, 291, 293	3jca 1174	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> ( 1 e. ZZ /\ M e. ZZ /\ j e. ZZ ) )
295		elfznn0 11693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( j e. ( 0 ... M ) -> j e. NN0 )
296	295	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> j e. NN0 )
297		neqne 31601	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( -. j = 0 -> j =/= 0 )
298	297	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> j =/= 0 )
299		elnnne0 10726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( j e. NN <-> ( j e. NN0 /\ j =/= 0 ) )
300	296, 298, 299	sylanbrc 662	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> j e. NN )
301	300	nnge1d 10495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> 1 <_ j )
302		elfzle2 11611	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( j e. ( 0 ... M ) -> j <_ M )
303	302	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> j <_ M )
304	294, 301, 303	jca32 533	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> ( ( 1 e. ZZ /\ M e. ZZ /\ j e. ZZ ) /\ ( 1 <_ j /\ j <_ M ) ) )
305		elfz2 11600	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( j e. ( 1 ... M ) <-> ( ( 1 e. ZZ /\ M e. ZZ /\ j e. ZZ ) /\ ( 1 <_ j /\ j <_ M ) ) )
306	304, 305	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> j e. ( 1 ... M ) )
307	306	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( j e. ( 0 ... M ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> j e. ( 1 ... M ) )
308	307	adantlll 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> j e. ( 1 ... M ) )
309		fveq2 5774	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( k = j -> ( c ` k ) = ( c ` j ) )
310	283, 284, 285, 288, 308, 309	fsumsplit1 31739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> sum_ k e. ( 1 ... M ) ( c ` k ) = ( ( c ` j ) + sum_ k e. ( ( 1 ... M ) \ { j } ) ( c ` k ) ) )
311	310	eqcomd 2390	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> ( ( c ` j ) + sum_ k e. ( ( 1 ... M ) \ { j } ) ( c ` k ) ) = sum_ k e. ( 1 ... M ) ( c ` k ) )
312	311, 278	eqeltrd 2470	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> ( ( c ` j ) + sum_ k e. ( ( 1 ... M ) \ { j } ) ( c ` k ) ) e. RR )
313		elfzle1 11610	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( c ` j ) e. ( 0 ... ( P - 1 ) ) -> 0 <_ ( c ` j ) )
314	280, 313	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) -> 0 <_ ( c ` j ) )
315	314	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> 0 <_ ( c ` j ) )
316		neqne 31601	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( -. ( c ` j ) = 0 -> ( c ` j ) =/= 0 )
317	316	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> ( c ` j ) =/= 0 )
318	279, 282, 315, 317	leneltd 31660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> 0 < ( c ` j ) )
319		diffi 7667	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( 1 ... M ) e. Fin -> ( ( 1 ... M ) \ { j } ) e. Fin )
320	105, 319	mp1i 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> ( ( 1 ... M ) \ { j } ) e. Fin )
321		eldifi 3540	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( k e. ( ( 1 ... M ) \ { j } ) -> k e. ( 1 ... M ) )
322	321	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( ( 1 ... M ) \ { j } ) ) -> k e. ( 1 ... M ) )
323	50, 322	sseldi 3415	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( ( 1 ... M ) \ { j } ) ) -> k e. ( 0 ... M ) )
324	44	ffvelrnda 5933	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( 0 ... M ) ) -> ( c ` k ) e. ( 0 ... ( P - 1 ) ) )
325	187, 324	sseldi 3415	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( 0 ... M ) ) -> ( c ` k ) e. RR )
326	323, 325	syldan 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( ( 1 ... M ) \ { j } ) ) -> ( c ` k ) e. RR )
327		elfzle1 11610	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( c ` k ) e. ( 0 ... ( P - 1 ) ) -> 0 <_ ( c ` k ) )
328	324, 327	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( 0 ... M ) ) -> 0 <_ ( c ` k ) )
329	323, 328	syldan 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( ( 1 ... M ) \ { j } ) ) -> 0 <_ ( c ` k ) )
330	320, 326, 329	fsumge0 13611	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> 0 <_ sum_ k e. ( ( 1 ... M ) \ { j } ) ( c ` k ) )
331	330	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) -> 0 <_ sum_ k e. ( ( 1 ... M ) \ { j } ) ( c ` k ) )
332	320, 326	fsumrecl 13558	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> sum_ k e. ( ( 1 ... M ) \ { j } ) ( c ` k ) e. RR )
333	332	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) -> sum_ k e. ( ( 1 ... M ) \ { j } ) ( c ` k ) e. RR )
334	281, 333	addge01d 10057	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) -> ( 0 <_ sum_ k e. ( ( 1 ... M ) \ { j } ) ( c ` k ) <-> ( c ` j ) <_ ( ( c ` j ) + sum_ k e. ( ( 1 ... M ) \ { j } ) ( c ` k ) ) ) )
335	331, 334	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) -> ( c ` j ) <_ ( ( c ` j ) + sum_ k e. ( ( 1 ... M ) \ { j } ) ( c ` k ) ) )
336	335	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> ( c ` j ) <_ ( ( c ` j ) + sum_ k e. ( ( 1 ... M ) \ { j } ) ( c ` k ) ) )
337	279, 282, 312, 318, 336	ltletrd 9653	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> 0 < ( ( c ` j ) + sum_ k e. ( ( 1 ... M ) \ { j } ) ( c ` k ) ) )
338	337, 311	breqtrd 4391	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> 0 < sum_ k e. ( 1 ... M ) ( c ` k ) )
339	278, 338	elrpd 11174	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> sum_ k e. ( 1 ... M ) ( c ` k ) e. RR+ )
340	270, 339	ltaddrpd 11206	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> ( P - 1 ) < ( ( P - 1 ) + sum_ k e. ( 1 ... M ) ( c ` k ) ) )
341	340	adantlllr 31583	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> ( P - 1 ) < ( ( P - 1 ) + sum_ k e. ( 1 ... M ) ( c ` k ) ) )
342		fveq2 5774	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( j = k -> ( c ` j ) = ( c ` k ) )
343	342	cbvsumv 13520	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- sum_ j e. ( 0 ... M ) ( c ` j ) = sum_ k e. ( 0 ... M ) ( c ` k )
344	343	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> sum_ j e. ( 0 ... M ) ( c ` j ) = sum_ k e. ( 0 ... M ) ( c ` k ) )
345	73	ad5antr 731	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> M e. ( ZZ>= ` 0 ) )
346		simp-5l 767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) /\ k e. ( 0 ... M ) ) -> ( ph /\ c e. ( C ` ( P - 1 ) ) ) )
347	74, 324	sseldi 3415	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( 0 ... M ) ) -> ( c ` k ) e. CC )
348	346, 347	sylancom 665	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) /\ k e. ( 0 ... M ) ) -> ( c ` k ) e. CC )
349		fveq2 5774	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( k = 0 -> ( c ` k ) = ( c ` 0 ) )
350	345, 348, 349	fsum1p 13570	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> sum_ k e. ( 0 ... M ) ( c ` k ) = ( ( c ` 0 ) + sum_ k e. ( ( 0 + 1 ) ... M ) ( c ` k ) ) )
351	259	ad4antlr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> ( c ` 0 ) = ( P - 1 ) )
352	86	sumeq1i 13522	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- sum_ k e. ( ( 0 + 1 ) ... M ) ( c ` k ) = sum_ k e. ( 1 ... M ) ( c ` k )
353	352	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> sum_ k e. ( ( 0 + 1 ) ... M ) ( c ` k ) = sum_ k e. ( 1 ... M ) ( c ` k ) )
354	351, 353	oveq12d 6214	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> ( ( c ` 0 ) + sum_ k e. ( ( 0 + 1 ) ... M ) ( c ` k ) ) = ( ( P - 1 ) + sum_ k e. ( 1 ... M ) ( c ` k ) ) )
355	344, 350, 354	3eqtrrd 2428	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> ( ( P - 1 ) + sum_ k e. ( 1 ... M ) ( c ` k ) ) = sum_ j e. ( 0 ... M ) ( c ` j ) )
356	341, 355	breqtrd 4391	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> ( P - 1 ) < sum_ j e. ( 0 ... M ) ( c ` j ) )
357	269, 356	gtned 9631	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> sum_ j e. ( 0 ... M ) ( c ` j ) =/= ( P - 1 ) )
358	357	neneqd 2584	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> -. sum_ j e. ( 0 ... M ) ( c ` j ) = ( P - 1 ) )
359	268, 358	condan 792	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) -> ( c ` j ) = 0 )
360		simpr 459	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ j e. ( 0 ... M ) ) -> j e. ( 0 ... M ) )
361	33, 66	sseldi 3415	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ j e. ( 0 ... M ) ) -> if ( j = 0 , ( P - 1 ) , 0 ) e. NN0 )
362	67	fvmpt2 5865	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( j e. ( 0 ... M ) /\ if ( j = 0 , ( P - 1 ) , 0 ) e. NN0 ) -> ( D ` j ) = if ( j = 0 , ( P - 1 ) , 0 ) )
363	360, 361, 362	syl2anc 659	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ j e. ( 0 ... M ) ) -> ( D ` j ) = if ( j = 0 , ( P - 1 ) , 0 ) )
364	363	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) -> ( D ` j ) = if ( j = 0 , ( P - 1 ) , 0 ) )
365		simpr 459	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) -> -. j = 0 )
366	365	iffalsed 3868	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) -> if ( j = 0 , ( P - 1 ) , 0 ) = 0 )
367	364, 366	eqtr2d 2424	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) -> 0 = ( D ` j ) )
368	367	adantllr 716	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) -> 0 = ( D ` j ) )
369	368	adantllr 716	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) -> 0 = ( D ` j ) )
370	359, 369	eqtrd 2423	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) -> ( c ` j ) = ( D ` j ) )
371	267, 370	pm2.61dan 789	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) /\ j e. ( 0 ... M ) ) -> ( c ` j ) = ( D ` j ) )
372	252, 255, 371	eqfnfvd 5886	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) -> c = D )
373	236, 372	sylanl2 649	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) /\ ( P - 1 ) = ( c ` 0 ) ) -> c = D )
374		eldifsni 4070	. . . . . . . . . . . . . . . . . . . 20 |- ( c e. ( ( C ` ( P - 1 ) ) \ { D } ) -> c =/= D )
375	374	neneqd 2584	. . . . . . . . . . . . . . . . . . 19 |- ( c e. ( ( C ` ( P - 1 ) ) \ { D } ) -> -. c = D )
376	375	ad2antlr 724	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ c e. ( ( C ` ( P - 1 )