Theorem etransclem35 40486

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 k A y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		reelprrecn 10028	. . . 4 |- RR e. { RR , CC }
2	1	a1i 11	. . 3 |- ( ph -> RR e. { RR , CC } )
3		reopn 39501	. . . . 5 |- RR e. ( topGen ` ran (,) )
4		eqid 2622	. . . . . 6 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
5	4	tgioo2 22606	. . . . 5 |- ( topGen ` ran (,) ) = ( ( TopOpen ` ℂfld ) ↾t RR )
6	3, 5	eleqtri 2699	. . . 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 11334	. . . 4 |- ( P e. NN -> ( P - 1 ) e. NN0 )
12	8, 11	syl 17	. . 3 |- ( ph -> ( P - 1 ) e. NN0 )
13		etransclem5 40456	. . 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 10041	. . 3 |- ( ph -> 0 e. RR )
16	2, 7, 8, 9, 10, 12, 13, 14, 15	etransclem31 40482	. 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 1843	. . 3 |- F/ c ph
18		nfcv 2764	. . 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 40467	. . 3 |- ( ph -> ( C ` ( P - 1 ) ) e. Fin )
20		simpr 477	. . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> c e. ( C ` ( P - 1 ) ) )
21	14, 12	etransclem12 40463	. . . . . . . . . . . . . 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 481	. . . . . . . . . . . . 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 2703	. . . . . . . . . . . 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 3116	. . . . . . . . . . . 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 208	. . . . . . . . . . 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 479	. . . . . . . . . 10 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> sum_ j e. ( 0 ... M ) ( c ` j ) = ( P - 1 ) )
27	26	eqcomd 2628	. . . . . . . . 9 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> ( P - 1 ) = sum_ j e. ( 0 ... M ) ( c ` j ) )
28	27	fveq2d 6195	. . . . . . . 8 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> ( ! ` ( P - 1 ) ) = ( ! ` sum_ j e. ( 0 ... M ) ( c ` j ) ) )
29	28	oveq1d 6665	. . . . . . 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 2764	. . . . . . . 8 |- F/_ j c
31		fzfid 12772	. . . . . . . 8 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> ( 0 ... M ) e. Fin )
32		nn0ex 11298	. . . . . . . . . 10 |- NN0 e. _V
33		fzssnn0 39533	. . . . . . . . . 10 |- ( 0 ... ( P - 1 ) ) C_ NN0
34		mapss 7900	. . . . . . . . . 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 708	. . . . . . . . 9 |- ( ( 0 ... ( P - 1 ) ) ^m ( 0 ... M ) ) C_ ( NN0 ^m ( 0 ... M ) )
36	25	simpld 475	. . . . . . . . 9 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> c e. ( ( 0 ... ( P - 1 ) ) ^m ( 0 ... M ) ) )
37	35, 36	sseldi 3601	. . . . . . . 8 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> c e. ( NN0 ^m ( 0 ... M ) ) )
38	30, 31, 37	mccl 39830	. . . . . . 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 2701	. . . . . 6 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> ( ( ! ` ( P - 1 ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) e. NN )
40	39	nnzd 11481	. . . . 5 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> ( ( ! ` ( P - 1 ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) e. ZZ )
41	8	adantr 481	. . . . . . 7 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> P e. NN )
42	9	adantr 481	. . . . . . 7 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> M e. NN0 )
43		elmapi 7879	. . . . . . . 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 11389	. . . . . . 7 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> 0 e. ZZ )
46	41, 42, 44, 45	etransclem10 40461	. . . . . 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 12772	. . . . . . 7 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> ( 1 ... M ) e. Fin )
48	8	ad2antrr 762	. . . . . . . 8 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 1 ... M ) ) -> P e. NN )
49	44	adantr 481	. . . . . . . 8 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 1 ... M ) ) -> c : ( 0 ... M ) --> ( 0 ... ( P - 1 ) ) )
50		fz1ssfz0 39524	. . . . . . . . . 10 |- ( 1 ... M ) C_ ( 0 ... M )
51	50	sseli 3599	. . . . . . . . 9 |- ( j e. ( 1 ... M ) -> j e. ( 0 ... M ) )
52	51	adantl 482	. . . . . . . 8 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 1 ... M ) ) -> j e. ( 0 ... M ) )
53		0zd 11389	. . . . . . . 8 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 1 ... M ) ) -> 0 e. ZZ )
54	48, 49, 52, 53	etransclem3 40454	. . . . . . 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 14684	. . . . . 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 11488	. . . . 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 11488	. . . 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 11483	. . 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 11722	. . . . . . . . . . 11 |- NN0 = ( ZZ>= ` 0 )
60	12, 59	syl6eleq 2711	. . . . . . . . . 10 |- ( ph -> ( P - 1 ) e. ( ZZ>= ` 0 ) )
61		eluzfz2 12349	. . . . . . . . . 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 12348	. . . . . . . . . 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 4131	. . . . . . . 8 |- ( ph -> if ( j = 0 , ( P - 1 ) , 0 ) e. ( 0 ... ( P - 1 ) ) )
66	65	adantr 481	. . . . . . 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 6385	. . . . . 6 |- ( ph -> D : ( 0 ... M ) --> ( 0 ... ( P - 1 ) ) )
69		ovex 6678	. . . . . . 7 |- ( 0 ... ( P - 1 ) ) e. _V
70		ovex 6678	. . . . . . 7 |- ( 0 ... M ) e. _V
71	69, 70	elmap 7886	. . . . . 6 |- ( D e. ( ( 0 ... ( P - 1 ) ) ^m ( 0 ... M ) ) <-> D : ( 0 ... M ) --> ( 0 ... ( P - 1 ) ) )
72	68, 71	sylibr 224	. . . . 5 |- ( ph -> D e. ( ( 0 ... ( P - 1 ) ) ^m ( 0 ... M ) ) )
73	9, 59	syl6eleq 2711	. . . . . . 7 |- ( ph -> M e. ( ZZ>= ` 0 ) )
74		fzsscn 39526	. . . . . . . 8 |- ( 0 ... ( P - 1 ) ) C_ CC
75	68	ffvelrnda 6359	. . . . . . . 8 |- ( ( ph /\ j e. ( 0 ... M ) ) -> ( D ` j ) e. ( 0 ... ( P - 1 ) ) )
76	74, 75	sseldi 3601	. . . . . . 7 |- ( ( ph /\ j e. ( 0 ... M ) ) -> ( D ` j ) e. CC )
77		fveq2 6191	. . . . . . 7 |- ( j = 0 -> ( D ` j ) = ( D ` 0 ) )
78	73, 76, 77	fsum1p 14482	. . . . . 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 477	. . . . . . . . 9 |- ( ( ph /\ j = 0 ) -> j = 0 )
81	80	iftrued 4094	. . . . . . . 8 |- ( ( ph /\ j = 0 ) -> if ( j = 0 , ( P - 1 ) , 0 ) = ( P - 1 ) )
82		eluzfz1 12348	. . . . . . . . 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 6288	. . . . . . 7 |- ( ph -> ( D ` 0 ) = ( P - 1 ) )
85		0p1e1 11132	. . . . . . . . . . 11 |- ( 0 + 1 ) = 1
86	85	oveq1i 6660	. . . . . . . . . 10 |- ( ( 0 + 1 ) ... M ) = ( 1 ... M )
87	86	sumeq1i 14428	. . . . . . . . 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 6291	. . . . . . . . . . 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 495	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( D ` j ) = if ( j = 0 , ( P - 1 ) , 0 ) )
91		0red 10041	. . . . . . . . . . . . . 14 |- ( j e. ( 1 ... M ) -> 0 e. RR )
92		1red 10055	. . . . . . . . . . . . . . 15 |- ( j e. ( 1 ... M ) -> 1 e. RR )
93		elfzelz 12342	. . . . . . . . . . . . . . . 16 |- ( j e. ( 1 ... M ) -> j e. ZZ )
94	93	zred 11482	. . . . . . . . . . . . . . 15 |- ( j e. ( 1 ... M ) -> j e. RR )
95		0lt1 10550	. . . . . . . . . . . . . . . 16 |- 0 < 1
96	95	a1i 11	. . . . . . . . . . . . . . 15 |- ( j e. ( 1 ... M ) -> 0 < 1 )
97		elfzle1 12344	. . . . . . . . . . . . . . 15 |- ( j e. ( 1 ... M ) -> 1 <_ j )
98	91, 92, 94, 96, 97	ltletrd 10197	. . . . . . . . . . . . . 14 |- ( j e. ( 1 ... M ) -> 0 < j )
99	91, 98	gtned 10172	. . . . . . . . . . . . 13 |- ( j e. ( 1 ... M ) -> j =/= 0 )
100	99	neneqd 2799	. . . . . . . . . . . 12 |- ( j e. ( 1 ... M ) -> -. j = 0 )
101	100	iffalsed 4097	. . . . . . . . . . 11 |- ( j e. ( 1 ... M ) -> if ( j = 0 , ( P - 1 ) , 0 ) = 0 )
102	101	adantl 482	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 1 ... M ) ) -> if ( j = 0 , ( P - 1 ) , 0 ) = 0 )
103	90, 102	eqtrd 2656	. . . . . . . . 9 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( D ` j ) = 0 )
104	103	sumeq2dv 14433	. . . . . . . 8 |- ( ph -> sum_ j e. ( 1 ... M ) ( D ` j ) = sum_ j e. ( 1 ... M ) 0 )
105		fzfi 12771	. . . . . . . . . 10 |- ( 1 ... M ) e. Fin
106	105	olci 406	. . . . . . . . 9 |- ( ( 1 ... M ) C_ ( ZZ>= ` A ) \/ ( 1 ... M ) e. Fin )
107		sumz 14453	. . . . . . . . 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 2660	. . . . . . 7 |- ( ph -> sum_ j e. ( ( 0 + 1 ) ... M ) ( D ` j ) = 0 )
110	84, 109	oveq12d 6668	. . . . . 6 |- ( ph -> ( ( D ` 0 ) + sum_ j e. ( ( 0 + 1 ) ... M ) ( D ` j ) ) = ( ( P - 1 ) + 0 ) )
111	8	nncnd 11036	. . . . . . . 8 |- ( ph -> P e. CC )
112		1cnd 10056	. . . . . . . 8 |- ( ph -> 1 e. CC )
113	111, 112	subcld 10392	. . . . . . 7 |- ( ph -> ( P - 1 ) e. CC )
114	113	addid1d 10236	. . . . . 6 |- ( ph -> ( ( P - 1 ) + 0 ) = ( P - 1 ) )
115	78, 110, 114	3eqtrd 2660	. . . . 5 |- ( ph -> sum_ j e. ( 0 ... M ) ( D ` j ) = ( P - 1 ) )
116		fveq1 6190	. . . . . . . 8 |- ( c = D -> ( c ` j ) = ( D ` j ) )
117	116	sumeq2ad 14434	. . . . . . 7 |- ( c = D -> sum_ j e. ( 0 ... M ) ( c ` j ) = sum_ j e. ( 0 ... M ) ( D ` j ) )
118	117	eqeq1d 2624	. . . . . 6 |- ( c = D -> ( sum_ j e. ( 0 ... M ) ( c ` j ) = ( P - 1 ) <-> sum_ j e. ( 0 ... M ) ( D ` j ) = ( P - 1 ) ) )
119	118	elrab 3363	. . . . 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 698	. . . 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 2704	. . 3 |- ( ph -> D e. ( C ` ( P - 1 ) ) )
122	116	fveq2d 6195	. . . . . 6 |- ( c = D -> ( ! ` ( c ` j ) ) = ( ! ` ( D ` j ) ) )
123	122	prodeq2ad 39824	. . . . 5 |- ( c = D -> prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) = prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) )
124	123	oveq2d 6666	. . . 4 |- ( c = D -> ( ( ! ` ( P - 1 ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) = ( ( ! ` ( P - 1 ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) )
125		fveq1 6190	. . . . . . 7 |- ( c = D -> ( c ` 0 ) = ( D ` 0 ) )
126	125	breq2d 4665	. . . . . 6 |- ( c = D -> ( ( P - 1 ) < ( c ` 0 ) <-> ( P - 1 ) < ( D ` 0 ) ) )
127	125	oveq2d 6666	. . . . . . . . 9 |- ( c = D -> ( ( P - 1 ) - ( c ` 0 ) ) = ( ( P - 1 ) - ( D ` 0 ) ) )
128	127	fveq2d 6195	. . . . . . . 8 |- ( c = D -> ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) = ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) )
129	128	oveq2d 6666	. . . . . . 7 |- ( c = D -> ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) ) = ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) )
130	127	oveq2d 6666	. . . . . . 7 |- ( c = D -> ( 0 ^ ( ( P - 1 ) - ( c ` 0 ) ) ) = ( 0 ^ ( ( P - 1 ) - ( D ` 0 ) ) ) )
131	129, 130	oveq12d 6668	. . . . . 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 4111	. . . . 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 4665	. . . . . . 7 |- ( c = D -> ( P < ( c ` j ) <-> P < ( D ` j ) ) )
134	116	oveq2d 6666	. . . . . . . . . 10 |- ( c = D -> ( P - ( c ` j ) ) = ( P - ( D ` j ) ) )
135	134	fveq2d 6195	. . . . . . . . 9 |- ( c = D -> ( ! ` ( P - ( c ` j ) ) ) = ( ! ` ( P - ( D ` j ) ) ) )
136	135	oveq2d 6666	. . . . . . . 8 |- ( c = D -> ( ( ! ` P ) / ( ! ` ( P - ( c ` j ) ) ) ) = ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) )
137	134	oveq2d 6666	. . . . . . . 8 |- ( c = D -> ( ( 0 - j ) ^ ( P - ( c ` j ) ) ) = ( ( 0 - j ) ^ ( P - ( D ` j ) ) ) )
138	136, 137	oveq12d 6668	. . . . . . 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 4111	. . . . . 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 39824	. . . . 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 6668	. . . 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 6668	. . 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 39804	. 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 3601	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0 ... M ) ) -> ( D ` j ) e. NN0 )
145	144	faccld 13071	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0 ... M ) ) -> ( ! ` ( D ` j ) ) e. NN )
146	145	nncnd 11036	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0 ... M ) ) -> ( ! ` ( D ` j ) ) e. CC )
147	77	fveq2d 6195	. . . . . . . . . 10 |- ( j = 0 -> ( ! ` ( D ` j ) ) = ( ! ` ( D ` 0 ) ) )
148	73, 146, 147	fprod1p 14698	. . . . . . . . 9 |- ( ph -> prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) = ( ( ! ` ( D ` 0 ) ) x. prod_ j e. ( ( 0 + 1 ) ... M ) ( ! ` ( D ` j ) ) ) )
149	84	fveq2d 6195	. . . . . . . . . 10 |- ( ph -> ( ! ` ( D ` 0 ) ) = ( ! ` ( P - 1 ) ) )
150	86	prodeq1i 14648	. . . . . . . . . . . 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 6195	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ! ` ( D ` j ) ) = ( ! ` 0 ) )
153		fac0 13063	. . . . . . . . . . . . 13 |- ( ! ` 0 ) = 1
154	152, 153	syl6eq 2672	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ! ` ( D ` j ) ) = 1 )
155	154	prodeq2dv 14653	. . . . . . . . . . 11 |- ( ph -> prod_ j e. ( 1 ... M ) ( ! ` ( D ` j ) ) = prod_ j e. ( 1 ... M ) 1 )
156		prod1 14674	. . . . . . . . . . . 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 2660	. . . . . . . . . 10 |- ( ph -> prod_ j e. ( ( 0 + 1 ) ... M ) ( ! ` ( D ` j ) ) = 1 )
159	149, 158	oveq12d 6668	. . . . . . . . 9 |- ( ph -> ( ( ! ` ( D ` 0 ) ) x. prod_ j e. ( ( 0 + 1 ) ... M ) ( ! ` ( D ` j ) ) ) = ( ( ! ` ( P - 1 ) ) x. 1 ) )
160	12	faccld 13071	. . . . . . . . . . 11 |- ( ph -> ( ! ` ( P - 1 ) ) e. NN )
161	160	nncnd 11036	. . . . . . . . . 10 |- ( ph -> ( ! ` ( P - 1 ) ) e. CC )
162	161	mulid1d 10057	. . . . . . . . 9 |- ( ph -> ( ( ! ` ( P - 1 ) ) x. 1 ) = ( ! ` ( P - 1 ) ) )
163	148, 159, 162	3eqtrd 2660	. . . . . . . 8 |- ( ph -> prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) = ( ! ` ( P - 1 ) ) )
164	163	oveq2d 6666	. . . . . . 7 |- ( ph -> ( ( ! ` ( P - 1 ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) = ( ( ! ` ( P - 1 ) ) / ( ! ` ( P - 1 ) ) ) )
165	160	nnne0d 11065	. . . . . . . 8 |- ( ph -> ( ! ` ( P - 1 ) ) =/= 0 )
166	161, 165	dividd 10799	. . . . . . 7 |- ( ph -> ( ( ! ` ( P - 1 ) ) / ( ! ` ( P - 1 ) ) ) = 1 )
167	164, 166	eqtrd 2656	. . . . . 6 |- ( ph -> ( ( ! ` ( P - 1 ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) = 1 )
168	12	nn0red 11352	. . . . . . . . . . . . 13 |- ( ph -> ( P - 1 ) e. RR )
169	84, 168	eqeltrd 2701	. . . . . . . . . . . 12 |- ( ph -> ( D ` 0 ) e. RR )
170	169, 168	lttri3d 10177	. . . . . . . . . . 11 |- ( ph -> ( ( D ` 0 ) = ( P - 1 ) <-> ( -. ( D ` 0 ) < ( P - 1 ) /\ -. ( P - 1 ) < ( D ` 0 ) ) ) )
171	84, 170	mpbid 222	. . . . . . . . . 10 |- ( ph -> ( -. ( D ` 0 ) < ( P - 1 ) /\ -. ( P - 1 ) < ( D ` 0 ) ) )
172	171	simprd 479	. . . . . . . . 9 |- ( ph -> -. ( P - 1 ) < ( D ` 0 ) )
173	172	iffalsed 4097	. . . . . . . 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 2628	. . . . . . . . . . . . . 14 |- ( ph -> ( P - 1 ) = ( D ` 0 ) )
175	113, 174	subeq0bd 10456	. . . . . . . . . . . . 13 |- ( ph -> ( ( P - 1 ) - ( D ` 0 ) ) = 0 )
176	175	fveq2d 6195	. . . . . . . . . . . 12 |- ( ph -> ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) = ( ! ` 0 ) )
177	176, 153	syl6eq 2672	. . . . . . . . . . 11 |- ( ph -> ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) = 1 )
178	177	oveq2d 6666	. . . . . . . . . 10 |- ( ph -> ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) = ( ( ! ` ( P - 1 ) ) / 1 ) )
179	161	div1d 10793	. . . . . . . . . 10 |- ( ph -> ( ( ! ` ( P - 1 ) ) / 1 ) = ( ! ` ( P - 1 ) ) )
180	178, 179	eqtrd 2656	. . . . . . . . 9 |- ( ph -> ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) = ( ! ` ( P - 1 ) ) )
181	175	oveq2d 6666	. . . . . . . . . 10 |- ( ph -> ( 0 ^ ( ( P - 1 ) - ( D ` 0 ) ) ) = ( 0 ^ 0 ) )
182		0cnd 10033	. . . . . . . . . . 11 |- ( ph -> 0 e. CC )
183	182	exp0d 13002	. . . . . . . . . 10 |- ( ph -> ( 0 ^ 0 ) = 1 )
184	181, 183	eqtrd 2656	. . . . . . . . 9 |- ( ph -> ( 0 ^ ( ( P - 1 ) - ( D ` 0 ) ) ) = 1 )
185	180, 184	oveq12d 6668	. . . . . . . 8 |- ( ph -> ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( 0 ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) = ( ( ! ` ( P - 1 ) ) x. 1 ) )
186	173, 185, 162	3eqtrd 2660	. . . . . . 7 |- ( ph -> if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( 0 ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) = ( ! ` ( P - 1 ) ) )
187		fzssre 39529	. . . . . . . . . . . 12 |- ( 0 ... ( P - 1 ) ) C_ RR
188	68	adantr 481	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 1 ... M ) ) -> D : ( 0 ... M ) --> ( 0 ... ( P - 1 ) ) )
189	51	adantl 482	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 1 ... M ) ) -> j e. ( 0 ... M ) )
190	188, 189	ffvelrnd 6360	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( D ` j ) e. ( 0 ... ( P - 1 ) ) )
191	187, 190	sseldi 3601	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( D ` j ) e. RR )
192	8	nnred 11035	. . . . . . . . . . . 12 |- ( ph -> P e. RR )
193	192	adantr 481	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> P e. RR )
194	8	nngt0d 11064	. . . . . . . . . . . . . 14 |- ( ph -> 0 < P )
195	15, 192, 194	ltled 10185	. . . . . . . . . . . . 13 |- ( ph -> 0 <_ P )
196	195	adantr 481	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 1 ... M ) ) -> 0 <_ P )
197	103, 196	eqbrtrd 4675	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( D ` j ) <_ P )
198	191, 193, 197	lensymd 10188	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 1 ... M ) ) -> -. P < ( D ` j ) )
199	198	iffalsed 4097	. . . . . . . . 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 6666	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( P - ( D ` j ) ) = ( P - 0 ) )
201	111	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. ( 1 ... M ) ) -> P e. CC )
202	201	subid1d 10381	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( P - 0 ) = P )
203	200, 202	eqtrd 2656	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( P - ( D ` j ) ) = P )
204	203	fveq2d 6195	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ! ` ( P - ( D ` j ) ) ) = ( ! ` P ) )
205	204	oveq2d 6666	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) = ( ( ! ` P ) / ( ! ` P ) ) )
206	8	nnnn0d 11351	. . . . . . . . . . . . . . 15 |- ( ph -> P e. NN0 )
207	206	faccld 13071	. . . . . . . . . . . . . 14 |- ( ph -> ( ! ` P ) e. NN )
208	207	nncnd 11036	. . . . . . . . . . . . 13 |- ( ph -> ( ! ` P ) e. CC )
209	207	nnne0d 11065	. . . . . . . . . . . . 13 |- ( ph -> ( ! ` P ) =/= 0 )
210	208, 209	dividd 10799	. . . . . . . . . . . 12 |- ( ph -> ( ( ! ` P ) / ( ! ` P ) ) = 1 )
211	210	adantr 481	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( ! ` P ) / ( ! ` P ) ) = 1 )
212	205, 211	eqtrd 2656	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) = 1 )
213		df-neg 10269	. . . . . . . . . . . . 13 |- -u j = ( 0 - j )
214	213	eqcomi 2631	. . . . . . . . . . . 12 |- ( 0 - j ) = -u j
215	214	a1i 11	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( 0 - j ) = -u j )
216	215, 203	oveq12d 6668	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( 0 - j ) ^ ( P - ( D ` j ) ) ) = ( -u j ^ P ) )
217	212, 216	oveq12d 6668	. . . . . . . . 9 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( 0 - j ) ^ ( P - ( D ` j ) ) ) ) = ( 1 x. ( -u j ^ P ) ) )
218	93	znegcld 11484	. . . . . . . . . . . . 13 |- ( j e. ( 1 ... M ) -> -u j e. ZZ )
219	218	zcnd 11483	. . . . . . . . . . . 12 |- ( j e. ( 1 ... M ) -> -u j e. CC )
220	219	adantl 482	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> -u j e. CC )
221	206	adantr 481	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> P e. NN0 )
222	220, 221	expcld 13008	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( -u j ^ P ) e. CC )
223	222	mulid2d 10058	. . . . . . . . 9 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( 1 x. ( -u j ^ P ) ) = ( -u j ^ P ) )
224	199, 217, 223	3eqtrd 2660	. . . . . . . 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 14653	. . . . . . 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 6668	. . . . . 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 6668	. . . . 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 12772	. . . . . . . . 9 |- ( ph -> ( 1 ... M ) e. Fin )
229		zexpcl 12875	. . . . . . . . . 10 |- ( ( -u j e. ZZ /\ P e. NN0 ) -> ( -u j ^ P ) e. ZZ )
230	218, 206, 229	syl2anr 495	. . . . . . . . 9 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( -u j ^ P ) e. ZZ )
231	228, 230	fprodzcl 14684	. . . . . . . 8 |- ( ph -> prod_ j e. ( 1 ... M ) ( -u j ^ P ) e. ZZ )
232	231	zcnd 11483	. . . . . . 7 |- ( ph -> prod_ j e. ( 1 ... M ) ( -u j ^ P ) e. CC )
233	161, 232	mulcld 10060	. . . . . 6 |- ( ph -> ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( -u j ^ P ) ) e. CC )
234	233	mulid2d 10058	. . . . 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 2656	. . . 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 3732	. . . . . . . . . . . . . . 15 |- ( c e. ( ( C ` ( P - 1 ) ) \ { D } ) -> c e. ( C ` ( P - 1 ) ) )
237	83	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> 0 e. ( 0 ... M ) )
238	44, 237	ffvelrnd 6360	. . . . . . . . . . . . . . 15 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> ( c ` 0 ) e. ( 0 ... ( P - 1 ) ) )
239	236, 238	sylan2 491	. . . . . . . . . . . . . 14 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( c ` 0 ) e. ( 0 ... ( P - 1 ) ) )
240	187, 239	sseldi 3601	. . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( c ` 0 ) e. RR )
241	168	adantr 481	. . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( P - 1 ) e. RR )
242		elfzle2 12345	. . . . . . . . . . . . . 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 10188	. . . . . . . . . . . 12 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> -. ( P - 1 ) < ( c ` 0 ) )
245	244	iffalsed 4097	. . . . . . . . . . 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 11480	. . . . . . . . . . . . . . . 16 |- ( ph -> ( P - 1 ) e. ZZ )
247	246	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( P - 1 ) e. ZZ )
248	239	elfzelzd 39530	. . . . . . . . . . . . . . 15 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( c ` 0 ) e. ZZ )
249	247, 248	zsubcld 11487	. . . . . . . . . . . . . 14 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( ( P - 1 ) - ( c ` 0 ) ) e. ZZ )
250		ffn 6045	. . . . . . . . . . . . . . . . . . . . . 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 481	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) -> c Fn ( 0 ... M ) )
253		ffn 6045	. . . . . . . . . . . . . . . . . . . . . 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 762	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) -> D Fn ( 0 ... M ) )
256		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( j = 0 -> ( c ` j ) = ( c ` 0 ) )
257	256	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 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 2628	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( P - 1 ) = ( c ` 0 ) -> ( c ` 0 ) = ( P - 1 ) )
260	259	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ ( P - 1 ) = ( c ` 0 ) ) /\ j = 0 ) -> ( c ` 0 ) = ( P - 1 ) )
261	77	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ j = 0 ) -> ( D ` j ) = ( D ` 0 ) )
262	84	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ j = 0 ) -> ( D ` 0 ) = ( P - 1 ) )
263	261, 262	eqtr2d 2657	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ j = 0 ) -> ( P - 1 ) = ( D ` j ) )
264	263	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ ( P - 1 ) = ( c ` 0 ) ) /\ j = 0 ) -> ( P - 1 ) = ( D ` j ) )
265	257, 260, 264	3eqtrd 2660	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ ( P - 1 ) = ( c ` 0 ) ) /\ j = 0 ) -> ( c ` j ) = ( D ` j ) )
266	265	adantllr 755	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) /\ j = 0 ) -> ( c ` j ) = ( D ` j ) )
267	266	adantlr 751	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) /\ j e. ( 0 ... M ) ) /\ j = 0 ) -> ( c ` j ) = ( D ` j ) )
268	26	ad4antr 768	. . . . . . . . . . . . . . . . . . . . . . 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 770	. . . . . . . . . . . . . . . . . . . . . . . . 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 768	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> ( P - 1 ) e. RR )
271	44	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( 1 ... M ) ) -> c : ( 0 ... M ) --> ( 0 ... ( P - 1 ) ) )
272	50	sseli 3599	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( k e. ( 1 ... M ) -> k e. ( 0 ... M ) )
273	272	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( 1 ... M ) ) -> k e. ( 0 ... M ) )
274	271, 273	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( 1 ... M ) ) -> ( c ` k ) e. ( 0 ... ( P - 1 ) ) )
275	33, 274	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( 1 ... M ) ) -> ( c ` k ) e. NN0 )
276	47, 275	fsumnn0cl 14467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> sum_ k e. ( 1 ... M ) ( c ` k ) e. NN0 )
277	276	nn0red 11352	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> sum_ k e. ( 1 ... M ) ( c ` k ) e. RR )
278	277	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10041	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> 0 e. RR )
280	44	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) -> ( c ` j ) e. ( 0 ... ( P - 1 ) ) )
281	187, 280	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) -> ( c ` j ) e. RR )
282	281	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> ( c ` j ) e. RR )
283		nfv 1843	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- F/ k ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 )
284		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- F/_ k ( c ` j )
285		fzfid 12772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> ( 1 ... M ) e. Fin )
286		simp-4l 806	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3601	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( 1 ... M ) ) -> ( c ` k ) e. CC )
288	286, 287	sylancom 701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> 1 e. ZZ )
290		elfzel2 12340	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( j e. ( 0 ... M ) -> M e. ZZ )
291	290	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> M e. ZZ )
292		elfzelz 12342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( j e. ( 0 ... M ) -> j e. ZZ )
293	292	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> j e. ZZ )
294	289, 291, 293	3jca 1242	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> ( 1 e. ZZ /\ M e. ZZ /\ j e. ZZ ) )
295		elfznn0 12433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( j e. ( 0 ... M ) -> j e. NN0 )
296	295	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> j e. NN0 )
297		neqne 2802	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( -. j = 0 -> j =/= 0 )
298	297	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> j =/= 0 )
299		elnnne0 11306	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( j e. NN <-> ( j e. NN0 /\ j =/= 0 ) )
300	296, 298, 299	sylanbrc 698	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> j e. NN )
301	300	nnge1d 11063	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> 1 <_ j )
302		elfzle2 12345	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( j e. ( 0 ... M ) -> j <_ M )
303	302	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> j <_ M )
304	294, 301, 303	jca32 558	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> ( ( 1 e. ZZ /\ M e. ZZ /\ j e. ZZ ) /\ ( 1 <_ j /\ j <_ M ) ) )
305		elfz2 12333	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( j e. ( 1 ... M ) <-> ( ( 1 e. ZZ /\ M e. ZZ /\ j e. ZZ ) /\ ( 1 <_ j /\ j <_ M ) ) )
306	304, 305	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> j e. ( 1 ... M ) )
307	306	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( j e. ( 0 ... M ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> j e. ( 1 ... M ) )
308	307	adantlll 754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> j e. ( 1 ... M ) )
309		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( k = j -> ( c ` k ) = ( c ` j ) )
310	283, 284, 285, 288, 308, 309	fsumsplit1 39804	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 12344	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> 0 <_ ( c ` j ) )
316		neqne 2802	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( -. ( c ` j ) = 0 -> ( c ` j ) =/= 0 )
317	316	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> 0 < ( c ` j ) )
319		diffi 8192	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( k e. ( ( 1 ... M ) \ { j } ) -> k e. ( 1 ... M ) )
322	321	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( ( 1 ... M ) \ { j } ) ) -> k e. ( 1 ... M ) )
323	50, 322	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( ( 1 ... M ) \ { j } ) ) -> k e. ( 0 ... M ) )
324	44	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( 0 ... M ) ) -> ( c ` k ) e. ( 0 ... ( P - 1 ) ) )
325	187, 324	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( 0 ... M ) ) -> ( c ` k ) e. RR )
326	323, 325	syldan 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( ( 1 ... M ) \ { j } ) ) -> ( c ` k ) e. RR )
327		elfzle1 12344	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( ( 1 ... M ) \ { j } ) ) -> 0 <_ ( c ` k ) )
330	320, 326, 329	fsumge0 14527	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> 0 <_ sum_ k e. ( ( 1 ... M ) \ { j } ) ( c ` k ) )
331	330	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) -> 0 <_ sum_ k e. ( ( 1 ... M ) \ { j } ) ( c ` k ) )
332	320, 326	fsumrecl 14465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> sum_ k e. ( ( 1 ... M ) \ { j } ) ( c ` k ) e. RR )
333	332	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10615	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 222	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10197	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11869	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11905	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 39199	. . . . . . . . . . . . . . . . . . . . . . . . . 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 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( j = k -> ( c ` j ) = ( c ` k ) )
343	342	cbvsumv 14426	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 770	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 808	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3601	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( 0 ... M ) ) -> ( c ` k ) e. CC )
348	346, 347	sylancom 701	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( k = 0 -> ( c ` k ) = ( c ` 0 ) )
350	345, 348, 349	fsum1p 14482	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 769	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 14428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 2661	. . . . . . . . . . . . . . . . . . . . . . . . . 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 4679	. . . . . . . . . . . . . . . . . . . . . . . . 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 10172	. . . . . . . . . . . . . . . . . . . . . . . 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 2799	. . . . . . . . . . . . . . . . . . . . . . 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 835	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) -> ( c ` j ) = 0 )
360		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ j e. ( 0 ... M ) ) -> j e. ( 0 ... M ) )
361	33, 66	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ j e. ( 0 ... M ) ) -> if ( j = 0 , ( P - 1 ) , 0 ) e. NN0 )
362	67	fvmpt2 6291	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 693	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ j e. ( 0 ... M ) ) -> ( D ` j ) = if ( j = 0 , ( P - 1 ) , 0 ) )
364	363	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) -> ( D ` j ) = if ( j = 0 , ( P - 1 ) , 0 ) )
365		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) -> -. j = 0 )
366	365	iffalsed 4097	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) -> if ( j = 0 , ( P - 1 ) , 0 ) = 0 )
367	364, 366	eqtr2d 2657	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) -> 0 = ( D ` j ) )
368	367	adantllr 755	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) -> 0 = ( D ` j ) )
369	368	adantllr 755	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) -> 0 = ( D ` j ) )
370	359, 369	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . 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 832	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) /\ j e. ( 0 ... M ) ) -> ( c ` j ) = ( D ` j ) )
372	252, 255, 371	eqfnfvd 6314	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) -> c = D )
373	236, 372	sylanl2 683	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) /\ ( P - 1 ) = ( c ` 0 ) ) -> c = D )
374		eldifsni 4320	. . . . . . . . . . . . . . . . . . . 20 |- ( c e. ( ( C ` ( P - 1 ) ) \ { D } ) -> c =/= D )
375	374	neneqd 2799	. . . . . . . . . . . . . . . . . . 19 |- ( c e. ( ( C ` ( P - 1 ) ) \ { D } ) -> -. c = D )
376	375	ad2antlr 763	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) /\ ( P - 1 ) = ( c ` 0 ) ) -> -. c = D )
377	373, 376	pm2.65da 600	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> -. ( P - 1 ) = ( c ` 0 ) )
378	377	neqned 2801	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( P - 1 ) =/= ( c ` 0 ) )
379	240, 241, 243, 378	leneltd 10191	. . . . . . . . . . . . . . 15 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( c ` 0 ) < ( P - 1 ) )
380	240, 241	posdifd 10614	. . . . . . . . . . . . . . 15 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( ( c ` 0 ) < ( P - 1 ) <-> 0 < ( ( P - 1 ) - ( c ` 0 ) ) ) )
381	379, 380	mpbid 222	. . . . . . . . . . . . . 14 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> 0 < ( ( P - 1 ) - ( c ` 0 ) ) )
382		elnnz 11387	. . . . . . . . . . . . . 14 |- ( ( ( P - 1 ) - ( c ` 0 ) ) e. NN <-> ( ( ( P - 1 ) - ( c ` 0 ) ) e. ZZ /\ 0 < ( ( P - 1 ) - ( c ` 0 ) ) ) )
383	249, 381, 382	sylanbrc 698	. . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( ( P - 1 ) - ( c ` 0 ) ) e. NN )
384	383	0expd 13024	. . . . . . . . . . . 12 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( 0 ^ ( ( P - 1 ) - ( c ` 0 ) ) ) = 0 )
385	384	oveq2d 6666	. . . . . . . . . . 11 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) ) x. ( 0 ^ ( ( P - 1 ) - ( c ` 0 ) ) ) ) = ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) ) x. 0 ) )
386	161	adantr 481	. . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( ! ` ( P - 1 ) ) e. CC )
387	383	nnnn0d 11351	. . . . . . . . . . . . . . 15 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( ( P - 1 ) - ( c ` 0 ) ) e. NN0 )
388	387	faccld 13071	. . . . . . . . . . . . . 14 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) e. NN )
389	388	nncnd 11036	. . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) e. CC )
390	388	nnne0d 11065	. . . . . . . . . . . . 13 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) =/= 0 )
391	386, 389, 390	divcld 10801	. . . . . . . . . . . 12 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) ) e. CC )
392	391	mul01d 10235	. . . . . . . . . . 11 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) ) x. 0 ) = 0 )
393	245, 385, 392	3eqtrd 2660	. . . . . . . . . 10 |- ( ( 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 ) ) ) ) ) = 0 )
394	393	oveq1d 6665	. . . . . . . . 9 |- ( ( 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 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( c ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( c ` j ) ) ) ) x. ( ( 0 - j ) ^ ( P - ( c ` j ) ) ) ) ) ) = ( 0 x. prod_ j e. ( 1 ... M ) if ( P < ( c ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( c ` j ) ) ) ) x. ( ( 0 - j ) ^ ( P - ( c ` j ) ) ) ) ) ) )
395	236, 55	sylan2 491	. . . . . . . . . . 11 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> prod_ j e. ( 1 ... M ) if ( P < ( c ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( c ` j ) ) ) ) x. ( ( 0 - j ) ^ ( P - ( c ` j ) ) ) ) ) e. ZZ )
396	395	zcnd 11483	. . . . . . . . . 10 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> prod_ j e. ( 1 ... M ) if ( P < ( c ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( c ` j ) ) ) ) x. ( ( 0 - j ) ^ ( P - ( c ` j ) ) ) ) ) e. CC )
397	396	mul02d 10234	. . . . . . . . 9 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( 0 x. prod_ j e. ( 1 ... M ) if ( P < ( c ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( c ` j ) ) ) ) x. ( ( 0 - j ) ^ ( P - ( c ` j ) ) ) ) ) ) = 0 )
398	394, 397	eqtrd 2656	. . . . . . . 8 |- ( ( 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 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( c ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( c ` j ) ) ) ) x. ( ( 0 - j ) ^ ( P - ( c ` j ) ) ) ) ) ) = 0 )
399	398	oveq2d 6666	. . . . . . 7 |- ( ( ph /\ 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 ) ) ) ) ) ) ) = ( ( ( ! ` ( P - 1 ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) x. 0 ) )
400		fzfid 12772	. . . . . . . . . . 11 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( 0 ... M ) e. Fin )
401	33, 280	sseldi 3601	. . . . . . . . . . . . 13 |- ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) -> ( c ` j ) e. NN0 )
402	236, 401	sylanl2 683	. . . . . . . . . . . 12 |- ( ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) /\ j e. ( 0 ... M ) ) -> ( c ` j ) e. NN0 )
403	402	faccld 13071	. . . . . . . . . . 11 |- ( ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) /\ j e. ( 0 ... M ) ) -> ( ! ` ( c ` j ) ) e. NN )
404	400, 403	fprodnncl 14685	. . . . . . . . . 10 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) e. NN )
405	404	nncnd 11036	. . . . . . . . 9 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) e. CC )
406	404	nnne0d 11065	. . . . . . . . 9 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) =/= 0 )
407	386, 405, 406	divcld 10801	. . . . . . . 8 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( ( ! ` ( P - 1 ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) e. CC )
408	407	mul01d 10235	. . . . . . 7 |- ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( ( ( ! ` ( P - 1 ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) x. 0 ) = 0 )
409	399, 408	eqtrd 2656	. . . . . 6 |- ( ( ph /\ 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 ) ) ) ) ) ) ) = 0 )
410	409	sumeq2dv 14433	. . . . 5 |- ( ph -> 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 ) ) ) ) ) ) ) = sum_ c e. ( ( C ` ( P - 1 ) ) \ { D } ) 0 )
411		diffi 8192	. . . . . . . 8 |- ( ( C ` ( P - 1 ) ) e. Fin -> ( ( C ` ( P - 1 ) ) \ { D } ) e. Fin )
412	19, 411	syl 17	. . . . . . 7 |- ( ph -> ( ( C ` ( P - 1 ) ) \ { D } ) e. Fin )
413	412	olcd 408	. . . . . 6 |- ( ph -> ( ( ( C ` ( P - 1 ) ) \ { D } ) C_ ( ZZ>= ` 0 ) \/ ( ( C ` ( P - 1 ) ) \ { D } ) e. Fin ) )
414		sumz 14453	. . . . . 6 |- ( ( ( ( C ` ( P - 1 ) ) \ { D } ) C_ ( ZZ>= ` 0 ) \/ ( ( C ` ( P - 1 ) ) \ { D } ) e. Fin ) -> sum_ c e. ( ( C ` ( P - 1 ) ) \ { D } ) 0 = 0 )
415	413, 414	syl 17	. . . . 5 |- ( ph -> sum_ c e. ( ( C ` ( P - 1 ) ) \ { D } ) 0 = 0 )
416	410, 415	eqtrd 2656	. . . 4 |- ( ph -> 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 ) ) ) ) ) ) ) = 0 )
417	235, 416	oveq12d 6668	. . 3 |- ( 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 ) ) ) ) ) ) ) + 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 ) ) ) ) ) ) ) ) = ( ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( -u j ^ P ) ) + 0 ) )
418	233	addid1d 10236	. . 3 |- ( ph -> ( ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( -u j ^ P ) ) + 0 ) = ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( -u j ^ P ) ) )
419		nfv 1843	. . . . 5 |- F/ j ph
420	419, 206, 228, 220	fprodexp 39826	. . . 4 |- ( ph -> prod_ j e. ( 1 ... M ) ( -u j ^ P ) = ( prod_ j e. ( 1 ... M ) -u j ^ P ) )
421	420	oveq2d 6666	. . 3 |- ( ph -> ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( -u j ^ P ) ) = ( ( ! ` ( P - 1 ) ) x. ( prod_ j e. ( 1 ... M ) -u j ^ P ) ) )
422	417, 418, 421	3eqtrd 2660	. 2 |- ( 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 ) ) ) ) ) ) ) + 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 ) ) ) ) ) ) ) ) = ( ( ! ` ( P - 1 ) ) x. ( prod_ j e. ( 1 ... M ) -u j ^ P ) ) )
423	16, 143, 422	3eqtrd 2660	1 |- ( ph -> ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) = ( ( ! ` ( P - 1 ) ) x. ( prod_ j e. ( 1 ... M ) -u j ^ P ) ) )

Syntax hints:   -. wn 3   -> wi 4   \/ wo 383   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   =/= wne 2794   {crab 2916   _Vcvv 3200   \ cdif 3571   C_ wss 3574   ifcif 4086   {csn 4177   {cpr 4179   class class class wbr 4653   |-> cmpt 4729   ran crn 5115   Fn wfn 5883   -->wf 5884   ` cfv 5888  (class class class)co 6650   ^m cmap 7857   Fincfn 7955   CCcc 9934   RRcr 9935   0cc0 9936   1c1 9937   + caddc 9939   x. cmul 9941   < clt 10074   <_ cle 10075   - cmin 10266   -ucneg 10267   / cdiv 10684   NNcn 11020   NN0cn0 11292   ZZcz 11377   ZZ>=cuz 11687   (,)cioo 12175   ...cfz 12326   ^cexp 12860   !cfa 13060   sum_csu 14416   prod_cprod 14635   ↾_t crest 16081   TopOpenctopn 16082   topGenctg 16098  ℂ_fldccnfld 19746   Dncdvn 23628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014  ax-addf 10015  ax-mulf 10016

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-of 6897  df-om 7066  df-1st 7168  df-2nd 7169  df-supp 7296  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-oadd 7564  df-er 7742  df-map 7859  df-pm 7860  df-ixp 7909  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fsupp 8276  df-fi 8317  df-sup 8348  df-inf 8349  df-oi 8415  df-card 8765  df-cda 8990  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-z 11378  df-dec 11494  df-uz 11688  df-q 11789  df-rp 11833  df-xneg 11946  df-xadd 11947  df-xmul 11948  df-ioo 12179  df-ico 12181  df-icc 12182  df-fz 12327  df-fzo 12466  df-seq 12802  df-exp 12861  df-fac 13061  df-bc 13090  df-hash 13118  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-clim 14219  df-sum 14417  df-prod 14636  df-struct 15859  df-ndx 15860  df-slot 15861  df-base 15863  df-sets 15864  df-ress 15865  df-plusg 15954  df-mulr 15955  df-starv 15956  df-sca 15957  df-vsca 15958  df-ip 15959  df-tset 15960  df-ple 15961  df-ds 15964  df-unif 15965  df-hom 15966  df-cco 15967  df-rest 16083  df-topn 16084  df-0g 16102  df-gsum 16103  df-topgen 16104  df-pt 16105  df-prds 16108  df-xrs 16162  df-qtop 16167  df-imas 16168  df-xps 16170  df-mre 16246  df-mrc 16247  df-acs 16249  df-mgm 17242  df-sgrp 17284  df-mnd 17295  df-submnd 17336  df-mulg 17541  df-cntz 17750  df-cmn 18195  df-psmet 19738  df-xmet 19739  df-met 19740  df-bl 19741  df-mopn 19742  df-fbas 19743  df-fg 19744  df-cnfld 19747  df-top 20699  df-topon 20716  df-topsp 20737  df-bases 20750  df-cld 20823  df-ntr 20824  df-cls 20825  df-nei 20902  df-lp 20940  df-perf 20941  df-cn 21031  df-cnp 21032  df-haus 21119  df-tx 21365  df-hmeo 21558  df-fil 21650  df-fm 21742  df-flim 21743  df-flf 21744  df-xms 22125  df-ms 22126  df-tms 22127  df-cncf 22681  df-limc 23630  df-dv 23631  df-dvn 23632

This theorem is referenced by:  etransclem41  40492