Theorem etransclem35 38246

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 9649	. . . 4 |- RR e. { RR , CC }
2	1	a1i 11	. . 3 |- ( ph -> RR e. { RR , CC } )
3		reopn 37591	. . . . 5 |- RR e. ( topGen ` ran (,) )
4		eqid 2471	. . . . . 6 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
5	4	tgioo2 21899	. . . . 5 |- ( topGen ` ran (,) ) = ( ( TopOpen ` ℂfld ) ↾t RR )
6	3, 5	eleqtri 2547	. . . 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 10935	. . . 4 |- ( P e. NN -> ( P - 1 ) e. NN0 )
12	8, 11	syl 17	. . 3 |- ( ph -> ( P - 1 ) e. NN0 )
13		etransclem5 38216	. . 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 9662	. . 3 |- ( ph -> 0 e. RR )
16	2, 7, 8, 9, 10, 12, 13, 14, 15	etransclem31 38242	. 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 1769	. . 3 |- F/ c ph
18		nfcv 2612	. . 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 38227	. . 3 |- ( ph -> ( C ` ( P - 1 ) ) e. Fin )
20		simpr 468	. . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> c e. ( C ` ( P - 1 ) ) )
21	14, 12	etransclem12 38223	. . . . . . . . . . . . . 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 472	. . . . . . . . . . . . 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 2551	. . . . . . . . . . . 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 2953	. . . . . . . . . . . 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 201	. . . . . . . . . . 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 470	. . . . . . . . . 10 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> sum_ j e. ( 0 ... M ) ( c ` j ) = ( P - 1 ) )
27	26	eqcomd 2477	. . . . . . . . 9 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> ( P - 1 ) = sum_ j e. ( 0 ... M ) ( c ` j ) )
28	27	fveq2d 5883	. . . . . . . 8 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> ( ! ` ( P - 1 ) ) = ( ! ` sum_ j e. ( 0 ... M ) ( c ` j ) ) )
29	28	oveq1d 6323	. . . . . . 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 2612	. . . . . . . 8 |- F/_ j c
31		fzfid 12224	. . . . . . . 8 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> ( 0 ... M ) e. Fin )
32		nn0ex 10899	. . . . . . . . . 10 |- NN0 e. _V
33		fzssnn0 37627	. . . . . . . . . 10 |- ( 0 ... ( P - 1 ) ) C_ NN0
34		mapss 7532	. . . . . . . . . 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 686	. . . . . . . . 9 |- ( ( 0 ... ( P - 1 ) ) ^m ( 0 ... M ) ) C_ ( NN0 ^m ( 0 ... M ) )
36	25	simpld 466	. . . . . . . . 9 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> c e. ( ( 0 ... ( P - 1 ) ) ^m ( 0 ... M ) ) )
37	35, 36	sseldi 3416	. . . . . . . 8 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> c e. ( NN0 ^m ( 0 ... M ) ) )
38	30, 31, 37	mccl 37775	. . . . . . 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 2549	. . . . . 6 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> ( ( ! ` ( P - 1 ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) e. NN )
40	39	nnzd 11062	. . . . 5 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> ( ( ! ` ( P - 1 ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) e. ZZ )
41	8	adantr 472	. . . . . . 7 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> P e. NN )
42	9	adantr 472	. . . . . . 7 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> M e. NN0 )
43		elmapi 7511	. . . . . . . 8 |- ( c e. ( ( 0 ... ( P - 1 ) ) ^m ( 0 ... M ) ) -> c : ( 0 ... M ) --> ( 0 ... ( P - 1 ) ) )
44	36, 43	syl 17	. . . . . . 7 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> c : ( 0 ... M ) --> ( 0 ... ( P - 1 ) ) )
45		0zd 10973	. . . . . . 7 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> 0 e. ZZ )
46	41, 42, 44, 45	etransclem10 38221	. . . . . 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 12224	. . . . . . 7 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> ( 1 ... M ) e. Fin )
48	8	ad2antrr 740	. . . . . . . 8 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 1 ... M ) ) -> P e. NN )
49	44	adantr 472	. . . . . . . 8 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 1 ... M ) ) -> c : ( 0 ... M ) --> ( 0 ... ( P - 1 ) ) )
50		fz1ssfz0 37616	. . . . . . . . . 10 |- ( 1 ... M ) C_ ( 0 ... M )
51	50	sseli 3414	. . . . . . . . 9 |- ( j e. ( 1 ... M ) -> j e. ( 0 ... M ) )
52	51	adantl 473	. . . . . . . 8 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 1 ... M ) ) -> j e. ( 0 ... M ) )
53		0zd 10973	. . . . . . . 8 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 1 ... M ) ) -> 0 e. ZZ )
54	48, 49, 52, 53	etransclem3 38214	. . . . . . 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 14085	. . . . . 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 11069	. . . . 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 11069	. . . 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 11064	. . 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 11217	. . . . . . . . . . 11 |- NN0 = ( ZZ>= ` 0 )
60	12, 59	syl6eleq 2559	. . . . . . . . . 10 |- ( ph -> ( P - 1 ) e. ( ZZ>= ` 0 ) )
61		eluzfz2 11833	. . . . . . . . . 10 |- ( ( P - 1 ) e. ( ZZ>= ` 0 ) -> ( P - 1 ) e. ( 0 ... ( P - 1 ) ) )
62	60, 61	syl 17	. . . . . . . . 9 |- ( ph -> ( P - 1 ) e. ( 0 ... ( P - 1 ) ) )
63		eluzfz1 11832	. . . . . . . . . 10 |- ( ( P - 1 ) e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... ( P - 1 ) ) )
64	60, 63	syl 17	. . . . . . . . 9 |- ( ph -> 0 e. ( 0 ... ( P - 1 ) ) )
65	62, 64	ifcld 3915	. . . . . . . 8 |- ( ph -> if ( j = 0 , ( P - 1 ) , 0 ) e. ( 0 ... ( P - 1 ) ) )
66	65	adantr 472	. . . . . . 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 6061	. . . . . 6 |- ( ph -> D : ( 0 ... M ) --> ( 0 ... ( P - 1 ) ) )
69		ovex 6336	. . . . . . 7 |- ( 0 ... ( P - 1 ) ) e. _V
70		ovex 6336	. . . . . . 7 |- ( 0 ... M ) e. _V
71	69, 70	elmap 7518	. . . . . 6 |- ( D e. ( ( 0 ... ( P - 1 ) ) ^m ( 0 ... M ) ) <-> D : ( 0 ... M ) --> ( 0 ... ( P - 1 ) ) )
72	68, 71	sylibr 217	. . . . 5 |- ( ph -> D e. ( ( 0 ... ( P - 1 ) ) ^m ( 0 ... M ) ) )
73	9, 59	syl6eleq 2559	. . . . . . 7 |- ( ph -> M e. ( ZZ>= ` 0 ) )
74		fzsscn 37619	. . . . . . . 8 |- ( 0 ... ( P - 1 ) ) C_ CC
75	68	ffvelrnda 6037	. . . . . . . 8 |- ( ( ph /\ j e. ( 0 ... M ) ) -> ( D ` j ) e. ( 0 ... ( P - 1 ) ) )
76	74, 75	sseldi 3416	. . . . . . 7 |- ( ( ph /\ j e. ( 0 ... M ) ) -> ( D ` j ) e. CC )
77		fveq2 5879	. . . . . . 7 |- ( j = 0 -> ( D ` j ) = ( D ` 0 ) )
78	73, 76, 77	fsum1p 13891	. . . . . 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 468	. . . . . . . . 9 |- ( ( ph /\ j = 0 ) -> j = 0 )
81	80	iftrued 3880	. . . . . . . 8 |- ( ( ph /\ j = 0 ) -> if ( j = 0 , ( P - 1 ) , 0 ) = ( P - 1 ) )
82		eluzfz1 11832	. . . . . . . . 9 |- ( M e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... M ) )
83	73, 82	syl 17	. . . . . . . 8 |- ( ph -> 0 e. ( 0 ... M ) )
84	79, 81, 83, 12	fvmptd 5969	. . . . . . 7 |- ( ph -> ( D ` 0 ) = ( P - 1 ) )
85		0p1e1 10743	. . . . . . . . . . 11 |- ( 0 + 1 ) = 1
86	85	oveq1i 6318	. . . . . . . . . 10 |- ( ( 0 + 1 ) ... M ) = ( 1 ... M )
87	86	sumeq1i 13841	. . . . . . . . 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 5972	. . . . . . . . . . 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 486	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( D ` j ) = if ( j = 0 , ( P - 1 ) , 0 ) )
91		0red 9662	. . . . . . . . . . . . . 14 |- ( j e. ( 1 ... M ) -> 0 e. RR )
92		1red 9676	. . . . . . . . . . . . . . 15 |- ( j e. ( 1 ... M ) -> 1 e. RR )
93		elfzelz 11826	. . . . . . . . . . . . . . . 16 |- ( j e. ( 1 ... M ) -> j e. ZZ )
94	93	zred 11063	. . . . . . . . . . . . . . 15 |- ( j e. ( 1 ... M ) -> j e. RR )
95		0lt1 10157	. . . . . . . . . . . . . . . 16 |- 0 < 1
96	95	a1i 11	. . . . . . . . . . . . . . 15 |- ( j e. ( 1 ... M ) -> 0 < 1 )
97		elfzle1 11828	. . . . . . . . . . . . . . 15 |- ( j e. ( 1 ... M ) -> 1 <_ j )
98	91, 92, 94, 96, 97	ltletrd 9812	. . . . . . . . . . . . . 14 |- ( j e. ( 1 ... M ) -> 0 < j )
99	91, 98	gtned 9787	. . . . . . . . . . . . 13 |- ( j e. ( 1 ... M ) -> j =/= 0 )
100	99	neneqd 2648	. . . . . . . . . . . 12 |- ( j e. ( 1 ... M ) -> -. j = 0 )
101	100	iffalsed 3883	. . . . . . . . . . 11 |- ( j e. ( 1 ... M ) -> if ( j = 0 , ( P - 1 ) , 0 ) = 0 )
102	101	adantl 473	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 1 ... M ) ) -> if ( j = 0 , ( P - 1 ) , 0 ) = 0 )
103	90, 102	eqtrd 2505	. . . . . . . . 9 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( D ` j ) = 0 )
104	103	sumeq2dv 13846	. . . . . . . 8 |- ( ph -> sum_ j e. ( 1 ... M ) ( D ` j ) = sum_ j e. ( 1 ... M ) 0 )
105		fzfi 12223	. . . . . . . . . 10 |- ( 1 ... M ) e. Fin
106	105	olci 398	. . . . . . . . 9 |- ( ( 1 ... M ) C_ ( ZZ>= ` A ) \/ ( 1 ... M ) e. Fin )
107		sumz 13865	. . . . . . . . 9 |- ( ( ( 1 ... M ) C_ ( ZZ>= ` A ) \/ ( 1 ... M ) e. Fin ) -> sum_ j e. ( 1 ... M ) 0 = 0 )
108	106, 107	mp1i 13	. . . . . . . 8 |- ( ph -> sum_ j e. ( 1 ... M ) 0 = 0 )
109	88, 104, 108	3eqtrd 2509	. . . . . . 7 |- ( ph -> sum_ j e. ( ( 0 + 1 ) ... M ) ( D ` j ) = 0 )
110	84, 109	oveq12d 6326	. . . . . 6 |- ( ph -> ( ( D ` 0 ) + sum_ j e. ( ( 0 + 1 ) ... M ) ( D ` j ) ) = ( ( P - 1 ) + 0 ) )
111	8	nncnd 10647	. . . . . . . 8 |- ( ph -> P e. CC )
112		1cnd 9677	. . . . . . . 8 |- ( ph -> 1 e. CC )
113	111, 112	subcld 10005	. . . . . . 7 |- ( ph -> ( P - 1 ) e. CC )
114	113	addid1d 9851	. . . . . 6 |- ( ph -> ( ( P - 1 ) + 0 ) = ( P - 1 ) )
115	78, 110, 114	3eqtrd 2509	. . . . 5 |- ( ph -> sum_ j e. ( 0 ... M ) ( D ` j ) = ( P - 1 ) )
116		fveq1 5878	. . . . . . . 8 |- ( c = D -> ( c ` j ) = ( D ` j ) )
117	116	sumeq2ad 37740	. . . . . . 7 |- ( c = D -> sum_ j e. ( 0 ... M ) ( c ` j ) = sum_ j e. ( 0 ... M ) ( D ` j ) )
118	117	eqeq1d 2473	. . . . . 6 |- ( c = D -> ( sum_ j e. ( 0 ... M ) ( c ` j ) = ( P - 1 ) <-> sum_ j e. ( 0 ... M ) ( D ` j ) = ( P - 1 ) ) )
119	118	elrab 3184	. . . . 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 677	. . . 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 2552	. . 3 |- ( ph -> D e. ( C ` ( P - 1 ) ) )
122	116	fveq2d 5883	. . . . . 6 |- ( c = D -> ( ! ` ( c ` j ) ) = ( ! ` ( D ` j ) ) )
123	122	prodeq2ad 37769	. . . . 5 |- ( c = D -> prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) = prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) )
124	123	oveq2d 6324	. . . 4 |- ( c = D -> ( ( ! ` ( P - 1 ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) = ( ( ! ` ( P - 1 ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) )
125		fveq1 5878	. . . . . . 7 |- ( c = D -> ( c ` 0 ) = ( D ` 0 ) )
126	125	breq2d 4407	. . . . . 6 |- ( c = D -> ( ( P - 1 ) < ( c ` 0 ) <-> ( P - 1 ) < ( D ` 0 ) ) )
127	125	oveq2d 6324	. . . . . . . . 9 |- ( c = D -> ( ( P - 1 ) - ( c ` 0 ) ) = ( ( P - 1 ) - ( D ` 0 ) ) )
128	127	fveq2d 5883	. . . . . . . 8 |- ( c = D -> ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) = ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) )
129	128	oveq2d 6324	. . . . . . 7 |- ( c = D -> ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) ) = ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) )
130	127	oveq2d 6324	. . . . . . 7 |- ( c = D -> ( 0 ^ ( ( P - 1 ) - ( c ` 0 ) ) ) = ( 0 ^ ( ( P - 1 ) - ( D ` 0 ) ) ) )
131	129, 130	oveq12d 6326	. . . . . 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 3897	. . . . 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 4407	. . . . . . 7 |- ( c = D -> ( P < ( c ` j ) <-> P < ( D ` j ) ) )
134	116	oveq2d 6324	. . . . . . . . . 10 |- ( c = D -> ( P - ( c ` j ) ) = ( P - ( D ` j ) ) )
135	134	fveq2d 5883	. . . . . . . . 9 |- ( c = D -> ( ! ` ( P - ( c ` j ) ) ) = ( ! ` ( P - ( D ` j ) ) ) )
136	135	oveq2d 6324	. . . . . . . 8 |- ( c = D -> ( ( ! ` P ) / ( ! ` ( P - ( c ` j ) ) ) ) = ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) )
137	134	oveq2d 6324	. . . . . . . 8 |- ( c = D -> ( ( 0 - j ) ^ ( P - ( c ` j ) ) ) = ( ( 0 - j ) ^ ( P - ( D ` j ) ) ) )
138	136, 137	oveq12d 6326	. . . . . . 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 3897	. . . . . 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 37769	. . . . 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 6326	. . . 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 6326	. . 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 37747	. 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 3416	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0 ... M ) ) -> ( D ` j ) e. NN0 )
145	144	faccld 37621	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0 ... M ) ) -> ( ! ` ( D ` j ) ) e. NN )
146	145	nncnd 10647	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0 ... M ) ) -> ( ! ` ( D ` j ) ) e. CC )
147	77	fveq2d 5883	. . . . . . . . . 10 |- ( j = 0 -> ( ! ` ( D ` j ) ) = ( ! ` ( D ` 0 ) ) )
148	73, 146, 147	fprod1p 14099	. . . . . . . . 9 |- ( ph -> prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) = ( ( ! ` ( D ` 0 ) ) x. prod_ j e. ( ( 0 + 1 ) ... M ) ( ! ` ( D ` j ) ) ) )
149	84	fveq2d 5883	. . . . . . . . . 10 |- ( ph -> ( ! ` ( D ` 0 ) ) = ( ! ` ( P - 1 ) ) )
150	86	prodeq1i 14049	. . . . . . . . . . . 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 5883	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ! ` ( D ` j ) ) = ( ! ` 0 ) )
153		fac0 12500	. . . . . . . . . . . . 13 |- ( ! ` 0 ) = 1
154	152, 153	syl6eq 2521	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ! ` ( D ` j ) ) = 1 )
155	154	prodeq2dv 14054	. . . . . . . . . . 11 |- ( ph -> prod_ j e. ( 1 ... M ) ( ! ` ( D ` j ) ) = prod_ j e. ( 1 ... M ) 1 )
156		prod1 14075	. . . . . . . . . . . 12 |- ( ( ( 1 ... M ) C_ ( ZZ>= ` A ) \/ ( 1 ... M ) e. Fin ) -> prod_ j e. ( 1 ... M ) 1 = 1 )
157	106, 156	mp1i 13	. . . . . . . . . . 11 |- ( ph -> prod_ j e. ( 1 ... M ) 1 = 1 )
158	151, 155, 157	3eqtrd 2509	. . . . . . . . . 10 |- ( ph -> prod_ j e. ( ( 0 + 1 ) ... M ) ( ! ` ( D ` j ) ) = 1 )
159	149, 158	oveq12d 6326	. . . . . . . . 9 |- ( ph -> ( ( ! ` ( D ` 0 ) ) x. prod_ j e. ( ( 0 + 1 ) ... M ) ( ! ` ( D ` j ) ) ) = ( ( ! ` ( P - 1 ) ) x. 1 ) )
160	12	faccld 37621	. . . . . . . . . . 11 |- ( ph -> ( ! ` ( P - 1 ) ) e. NN )
161	160	nncnd 10647	. . . . . . . . . 10 |- ( ph -> ( ! ` ( P - 1 ) ) e. CC )
162	161	mulid1d 9678	. . . . . . . . 9 |- ( ph -> ( ( ! ` ( P - 1 ) ) x. 1 ) = ( ! ` ( P - 1 ) ) )
163	148, 159, 162	3eqtrd 2509	. . . . . . . 8 |- ( ph -> prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) = ( ! ` ( P - 1 ) ) )
164	163	oveq2d 6324	. . . . . . 7 |- ( ph -> ( ( ! ` ( P - 1 ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) = ( ( ! ` ( P - 1 ) ) / ( ! ` ( P - 1 ) ) ) )
165	160	nnne0d 10676	. . . . . . . 8 |- ( ph -> ( ! ` ( P - 1 ) ) =/= 0 )
166	161, 165	dividd 10403	. . . . . . 7 |- ( ph -> ( ( ! ` ( P - 1 ) ) / ( ! ` ( P - 1 ) ) ) = 1 )
167	164, 166	eqtrd 2505	. . . . . 6 |- ( ph -> ( ( ! ` ( P - 1 ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) = 1 )
168	12	nn0red 10950	. . . . . . . . . . . . 13 |- ( ph -> ( P - 1 ) e. RR )
169	84, 168	eqeltrd 2549	. . . . . . . . . . . 12 |- ( ph -> ( D ` 0 ) e. RR )
170	169, 168	lttri3d 9792	. . . . . . . . . . 11 |- ( ph -> ( ( D ` 0 ) = ( P - 1 ) <-> ( -. ( D ` 0 ) < ( P - 1 ) /\ -. ( P - 1 ) < ( D ` 0 ) ) ) )
171	84, 170	mpbid 215	. . . . . . . . . 10 |- ( ph -> ( -. ( D ` 0 ) < ( P - 1 ) /\ -. ( P - 1 ) < ( D ` 0 ) ) )
172	171	simprd 470	. . . . . . . . 9 |- ( ph -> -. ( P - 1 ) < ( D ` 0 ) )
173	172	iffalsed 3883	. . . . . . . 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 2477	. . . . . . . . . . . . . 14 |- ( ph -> ( P - 1 ) = ( D ` 0 ) )
175	113, 174	subeq0bd 10066	. . . . . . . . . . . . 13 |- ( ph -> ( ( P - 1 ) - ( D ` 0 ) ) = 0 )
176	175	fveq2d 5883	. . . . . . . . . . . 12 |- ( ph -> ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) = ( ! ` 0 ) )
177	176, 153	syl6eq 2521	. . . . . . . . . . 11 |- ( ph -> ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) = 1 )
178	177	oveq2d 6324	. . . . . . . . . 10 |- ( ph -> ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) = ( ( ! ` ( P - 1 ) ) / 1 ) )
179	161	div1d 10397	. . . . . . . . . 10 |- ( ph -> ( ( ! ` ( P - 1 ) ) / 1 ) = ( ! ` ( P - 1 ) ) )
180	178, 179	eqtrd 2505	. . . . . . . . 9 |- ( ph -> ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) = ( ! ` ( P - 1 ) ) )
181	175	oveq2d 6324	. . . . . . . . . 10 |- ( ph -> ( 0 ^ ( ( P - 1 ) - ( D ` 0 ) ) ) = ( 0 ^ 0 ) )
182		0cnd 9654	. . . . . . . . . . 11 |- ( ph -> 0 e. CC )
183	182	exp0d 12448	. . . . . . . . . 10 |- ( ph -> ( 0 ^ 0 ) = 1 )
184	181, 183	eqtrd 2505	. . . . . . . . 9 |- ( ph -> ( 0 ^ ( ( P - 1 ) - ( D ` 0 ) ) ) = 1 )
185	180, 184	oveq12d 6326	. . . . . . . 8 |- ( ph -> ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( 0 ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) = ( ( ! ` ( P - 1 ) ) x. 1 ) )
186	173, 185, 162	3eqtrd 2509	. . . . . . 7 |- ( ph -> if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( 0 ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) = ( ! ` ( P - 1 ) ) )
187		fzssre 37623	. . . . . . . . . . . 12 |- ( 0 ... ( P - 1 ) ) C_ RR
188	68	adantr 472	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 1 ... M ) ) -> D : ( 0 ... M ) --> ( 0 ... ( P - 1 ) ) )
189	51	adantl 473	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 1 ... M ) ) -> j e. ( 0 ... M ) )
190	188, 189	ffvelrnd 6038	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( D ` j ) e. ( 0 ... ( P - 1 ) ) )
191	187, 190	sseldi 3416	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( D ` j ) e. RR )
192	8	nnred 10646	. . . . . . . . . . . 12 |- ( ph -> P e. RR )
193	192	adantr 472	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> P e. RR )
194	8	nngt0d 10675	. . . . . . . . . . . . . 14 |- ( ph -> 0 < P )
195	15, 192, 194	ltled 9800	. . . . . . . . . . . . 13 |- ( ph -> 0 <_ P )
196	195	adantr 472	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 1 ... M ) ) -> 0 <_ P )
197	103, 196	eqbrtrd 4416	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( D ` j ) <_ P )
198	191, 193, 197	lensymd 9803	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 1 ... M ) ) -> -. P < ( D ` j ) )
199	198	iffalsed 3883	. . . . . . . . 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 6324	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( P - ( D ` j ) ) = ( P - 0 ) )
201	111	adantr 472	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. ( 1 ... M ) ) -> P e. CC )
202	201	subid1d 9994	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( P - 0 ) = P )
203	200, 202	eqtrd 2505	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( P - ( D ` j ) ) = P )
204	203	fveq2d 5883	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ! ` ( P - ( D ` j ) ) ) = ( ! ` P ) )
205	204	oveq2d 6324	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) = ( ( ! ` P ) / ( ! ` P ) ) )
206	8	nnnn0d 10949	. . . . . . . . . . . . . . 15 |- ( ph -> P e. NN0 )
207	206	faccld 37621	. . . . . . . . . . . . . 14 |- ( ph -> ( ! ` P ) e. NN )
208	207	nncnd 10647	. . . . . . . . . . . . 13 |- ( ph -> ( ! ` P ) e. CC )
209	207	nnne0d 10676	. . . . . . . . . . . . 13 |- ( ph -> ( ! ` P ) =/= 0 )
210	208, 209	dividd 10403	. . . . . . . . . . . 12 |- ( ph -> ( ( ! ` P ) / ( ! ` P ) ) = 1 )
211	210	adantr 472	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( ! ` P ) / ( ! ` P ) ) = 1 )
212	205, 211	eqtrd 2505	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) = 1 )
213		df-neg 9883	. . . . . . . . . . . . 13 |- -u j = ( 0 - j )
214	213	eqcomi 2480	. . . . . . . . . . . 12 |- ( 0 - j ) = -u j
215	214	a1i 11	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( 0 - j ) = -u j )
216	215, 203	oveq12d 6326	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( 0 - j ) ^ ( P - ( D ` j ) ) ) = ( -u j ^ P ) )
217	212, 216	oveq12d 6326	. . . . . . . . 9 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( 0 - j ) ^ ( P - ( D ` j ) ) ) ) = ( 1 x. ( -u j ^ P ) ) )
218	93	znegcld 11065	. . . . . . . . . . . . 13 |- ( j e. ( 1 ... M ) -> -u j e. ZZ )
219	218	zcnd 11064	. . . . . . . . . . . 12 |- ( j e. ( 1 ... M ) -> -u j e. CC )
220	219	adantl 473	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> -u j e. CC )
221	206	adantr 472	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> P e. NN0 )
222	220, 221	expcld 12454	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( -u j ^ P ) e. CC )
223	222	mulid2d 9679	. . . . . . . . 9 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( 1 x. ( -u j ^ P ) ) = ( -u j ^ P ) )
224	199, 217, 223	3eqtrd 2509	. . . . . . . 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 14054	. . . . . . 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 6326	. . . . . 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 6326	. . . . 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 12224	. . . . . . . . 9 |- ( ph -> ( 1 ... M ) e. Fin )
229		zexpcl 12325	. . . . . . . . . 10 |- ( ( -u j e. ZZ /\ P e. NN0 ) -> ( -u j ^ P ) e. ZZ )
230	218, 206, 229	syl2anr 486	. . . . . . . . 9 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( -u j ^ P ) e. ZZ )
231	228, 230	fprodzcl 14085	. . . . . . . 8 |- ( ph -> prod_ j e. ( 1 ... M ) ( -u j ^ P ) e. ZZ )
232	231	zcnd 11064	. . . . . . 7 |- ( ph -> prod_ j e. ( 1 ... M ) ( -u j ^ P ) e. CC )
233	161, 232	mulcld 9681	. . . . . 6 |- ( ph -> ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( -u j ^ P ) ) e. CC )
234	233	mulid2d 9679	. . . . 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 2505	. . . 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 3544	. . . . . . . . . . . . . . 15 |- ( c e. ( ( C ` ( P - 1 ) ) \ { D } ) -> c e. ( C ` ( P - 1 ) ) )
237	83	adantr 472	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> 0 e. ( 0 ... M ) )
238	44, 237	ffvelrnd 6038	. . . . . . . . . . . . . . 15 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> ( c ` 0 ) e. ( 0 ... ( P - 1 ) ) )
239	236, 238	sylan2 482	. . . . . . . . . . . . . 14 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( c ` 0 ) e. ( 0 ... ( P - 1 ) ) )
240	187, 239	sseldi 3416	. . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( c ` 0 ) e. RR )
241	168	adantr 472	. . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( P - 1 ) e. RR )
242		elfzle2 11829	. . . . . . . . . . . . . 14 |- ( ( c ` 0 ) e. ( 0 ... ( P - 1 ) ) -> ( c ` 0 ) <_ ( P - 1 ) )
243	239, 242	syl 17	. . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( c ` 0 ) <_ ( P - 1 ) )
244	240, 241, 243	lensymd 9803	. . . . . . . . . . . 12 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> -. ( P - 1 ) < ( c ` 0 ) )
245	244	iffalsed 3883	. . . . . . . . . . 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 11061	. . . . . . . . . . . . . . . 16 |- ( ph -> ( P - 1 ) e. ZZ )
247	246	adantr 472	. . . . . . . . . . . . . . 15 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( P - 1 ) e. ZZ )
248	239	elfzelzd 37624	. . . . . . . . . . . . . . 15 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( c ` 0 ) e. ZZ )
249	247, 248	zsubcld 11068	. . . . . . . . . . . . . 14 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( ( P - 1 ) - ( c ` 0 ) ) e. ZZ )
250		ffn 5739	. . . . . . . . . . . . . . . . . . . . . 22 |- ( c : ( 0 ... M ) --> ( 0 ... ( P - 1 ) ) -> c Fn ( 0 ... M ) )
251	44, 250	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> c Fn ( 0 ... M ) )
252	251	adantr 472	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) -> c Fn ( 0 ... M ) )
253		ffn 5739	. . . . . . . . . . . . . . . . . . . . . 22 |- ( D : ( 0 ... M ) --> ( 0 ... ( P - 1 ) ) -> D Fn ( 0 ... M ) )
254	68, 253	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> D Fn ( 0 ... M ) )
255	254	ad2antrr 740	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) -> D Fn ( 0 ... M ) )
256		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( j = 0 -> ( c ` j ) = ( c ` 0 ) )
257	256	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . 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 2477	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( P - 1 ) = ( c ` 0 ) -> ( c ` 0 ) = ( P - 1 ) )
260	259	ad2antlr 741	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ ( P - 1 ) = ( c ` 0 ) ) /\ j = 0 ) -> ( c ` 0 ) = ( P - 1 ) )
261	77	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ j = 0 ) -> ( D ` j ) = ( D ` 0 ) )
262	84	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ j = 0 ) -> ( D ` 0 ) = ( P - 1 ) )
263	261, 262	eqtr2d 2506	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ j = 0 ) -> ( P - 1 ) = ( D ` j ) )
264	263	adantlr 729	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ ( P - 1 ) = ( c ` 0 ) ) /\ j = 0 ) -> ( P - 1 ) = ( D ` j ) )
265	257, 260, 264	3eqtrd 2509	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ ( P - 1 ) = ( c ` 0 ) ) /\ j = 0 ) -> ( c ` j ) = ( D ` j ) )
266	265	adantllr 733	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) /\ j = 0 ) -> ( c ` j ) = ( D ` j ) )
267	266	adantlr 729	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) /\ j e. ( 0 ... M ) ) /\ j = 0 ) -> ( c ` j ) = ( D ` j ) )
268	26	ad4antr 746	. . . . . . . . . . . . . . . . . . . . . . 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 748	. . . . . . . . . . . . . . . . . . . . . . . . 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 746	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> ( P - 1 ) e. RR )
271	44	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( 1 ... M ) ) -> c : ( 0 ... M ) --> ( 0 ... ( P - 1 ) ) )
272	50	sseli 3414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( k e. ( 1 ... M ) -> k e. ( 0 ... M ) )
273	272	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( 1 ... M ) ) -> k e. ( 0 ... M ) )
274	271, 273	ffvelrnd 6038	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( 1 ... M ) ) -> ( c ` k ) e. ( 0 ... ( P - 1 ) ) )
275	33, 274	sseldi 3416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( 1 ... M ) ) -> ( c ` k ) e. NN0 )
276	47, 275	fsumnn0cl 13879	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> sum_ k e. ( 1 ... M ) ( c ` k ) e. NN0 )
277	276	nn0red 10950	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> sum_ k e. ( 1 ... M ) ( c ` k ) e. RR )
278	277	ad3antrrr 744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9662	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> 0 e. RR )
280	44	ffvelrnda 6037	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) -> ( c ` j ) e. ( 0 ... ( P - 1 ) ) )
281	187, 280	sseldi 3416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) -> ( c ` j ) e. RR )
282	281	ad2antrr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> ( c ` j ) e. RR )
283		nfv 1769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- F/ k ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 )
284		nfcv 2612	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- F/_ k ( c ` j )
285		fzfid 12224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> ( 1 ... M ) e. Fin )
286		simp-4l 784	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( 1 ... M ) ) -> ( c ` k ) e. CC )
288	286, 287	sylancom 680	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10992	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> 1 e. ZZ )
290		elfzel2 11824	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( j e. ( 0 ... M ) -> M e. ZZ )
291	290	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> M e. ZZ )
292		elfzelz 11826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( j e. ( 0 ... M ) -> j e. ZZ )
293	292	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> j e. ZZ )
294	289, 291, 293	3jca 1210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> ( 1 e. ZZ /\ M e. ZZ /\ j e. ZZ ) )
295		elfznn0 11913	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( j e. ( 0 ... M ) -> j e. NN0 )
296	295	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> j e. NN0 )
297		neqne 2651	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( -. j = 0 -> j =/= 0 )
298	297	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> j =/= 0 )
299		elnnne0 10907	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( j e. NN <-> ( j e. NN0 /\ j =/= 0 ) )
300	296, 298, 299	sylanbrc 677	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> j e. NN )
301	300	nnge1d 10674	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> 1 <_ j )
302		elfzle2 11829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( j e. ( 0 ... M ) -> j <_ M )
303	302	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> j <_ M )
304	294, 301, 303	jca32 544	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> ( ( 1 e. ZZ /\ M e. ZZ /\ j e. ZZ ) /\ ( 1 <_ j /\ j <_ M ) ) )
305		elfz2 11817	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( j e. ( 1 ... M ) <-> ( ( 1 e. ZZ /\ M e. ZZ /\ j e. ZZ ) /\ ( 1 <_ j /\ j <_ M ) ) )
306	304, 305	sylibr 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> j e. ( 1 ... M ) )
307	306	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( j e. ( 0 ... M ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> j e. ( 1 ... M ) )
308	307	adantlll 732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> j e. ( 1 ... M ) )
309		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( k = j -> ( c ` k ) = ( c ` j ) )
310	283, 284, 285, 288, 308, 309	fsumsplit1 37747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2549	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11828	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( c ` j ) e. ( 0 ... ( P - 1 ) ) -> 0 <_ ( c ` j ) )
314	280, 313	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) -> 0 <_ ( c ` j ) )
315	314	ad2antrr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> 0 <_ ( c ` j ) )
316		neqne 2651	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( -. ( c ` j ) = 0 -> ( c ` j ) =/= 0 )
317	316	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9806	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> 0 < ( c ` j ) )
319		diffi 7821	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( 1 ... M ) e. Fin -> ( ( 1 ... M ) \ { j } ) e. Fin )
320	105, 319	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> ( ( 1 ... M ) \ { j } ) e. Fin )
321		eldifi 3544	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( k e. ( ( 1 ... M ) \ { j } ) -> k e. ( 1 ... M ) )
322	321	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( ( 1 ... M ) \ { j } ) ) -> k e. ( 1 ... M ) )
323	50, 322	sseldi 3416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( ( 1 ... M ) \ { j } ) ) -> k e. ( 0 ... M ) )
324	44	ffvelrnda 6037	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( 0 ... M ) ) -> ( c ` k ) e. ( 0 ... ( P - 1 ) ) )
325	187, 324	sseldi 3416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( 0 ... M ) ) -> ( c ` k ) e. RR )
326	323, 325	syldan 478	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( ( 1 ... M ) \ { j } ) ) -> ( c ` k ) e. RR )
327		elfzle1 11828	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( c ` k ) e. ( 0 ... ( P - 1 ) ) -> 0 <_ ( c ` k ) )
328	324, 327	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( 0 ... M ) ) -> 0 <_ ( c ` k ) )
329	323, 328	syldan 478	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( ( 1 ... M ) \ { j } ) ) -> 0 <_ ( c ` k ) )
330	320, 326, 329	fsumge0 13932	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> 0 <_ sum_ k e. ( ( 1 ... M ) \ { j } ) ( c ` k ) )
331	330	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) -> 0 <_ sum_ k e. ( ( 1 ... M ) \ { j } ) ( c ` k ) )
332	320, 326	fsumrecl 13877	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> sum_ k e. ( ( 1 ... M ) \ { j } ) ( c ` k ) e. RR )
333	332	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10222	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9812	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4420	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11361	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11394	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 37424	. . . . . . . . . . . . . . . . . . . . . . . . . 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 5879	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( j = k -> ( c ` j ) = ( c ` k ) )
343	342	cbvsumv 13839	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 748	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 786	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( 0 ... M ) ) -> ( c ` k ) e. CC )
348	346, 347	sylancom 680	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5879	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( k = 0 -> ( c ` k ) = ( c ` 0 ) )
350	345, 348, 349	fsum1p 13891	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 747	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 13841	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6326	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 2510	. . . . . . . . . . . . . . . . . . . . . . . . . 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 4420	. . . . . . . . . . . . . . . . . . . . . . . . 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 9787	. . . . . . . . . . . . . . . . . . . . . . . 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 2648	. . . . . . . . . . . . . . . . . . . . . . 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 811	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) -> ( c ` j ) = 0 )
360		simpr 468	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ j e. ( 0 ... M ) ) -> j e. ( 0 ... M ) )
361	33, 66	sseldi 3416	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ j e. ( 0 ... M ) ) -> if ( j = 0 , ( P - 1 ) , 0 ) e. NN0 )
362	67	fvmpt2 5972	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 673	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ j e. ( 0 ... M ) ) -> ( D ` j ) = if ( j = 0 , ( P - 1 ) , 0 ) )
364	363	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) -> ( D ` j ) = if ( j = 0 , ( P - 1 ) , 0 ) )
365		simpr 468	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) -> -. j = 0 )
366	365	iffalsed 3883	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) -> if ( j = 0 , ( P - 1 ) , 0 ) = 0 )
367	364, 366	eqtr2d 2506	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) -> 0 = ( D ` j ) )
368	367	adantllr 733	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) -> 0 = ( D ` j ) )
369	368	adantllr 733	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) -> 0 = ( D ` j ) )
370	359, 369	eqtrd 2505	. . . . . . . . . . . . . . . . . . . . 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 808	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) /\ j e. ( 0 ... M ) ) -> ( c ` j ) = ( D ` j ) )
372	252, 255, 371	eqfnfvd 5994	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) -> c = D )
373	236, 372	sylanl2 663	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) /\ ( P - 1 ) = ( c ` 0 ) ) -> c = D )
374		eldifsni 4089	. . . . . . . . . . . . . . . . . . . 20 |- ( c e. ( ( C ` ( P - 1 ) ) \ { D } ) -> c =/= D )
375	374	neneqd 2648	. . . . . . . . . . . . . . . . . . 19 |- ( c e. ( ( C ` ( P - 1 ) ) \ { D } ) -> -. c = D )
376	375	ad2antlr 741	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ c e. ( ( C ` ( P -