Metamath Proof Explorer

Theorem etransclem35

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)

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

Proof

Step Hyp Ref Expression
1 etransclem35.p 
 |-  ( ph -> P e. NN )
2 etransclem35.m 
 |-  ( ph -> M e. NN0 )
3 etransclem35.f 
 |-  F = ( x e. RR |-> ( ( x ^ ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( ( x - j ) ^ P ) ) )
4 etransclem35.c 
 |-  C = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = n } )
5 etransclem35.d 
 |-  D = ( j e. ( 0 ... M ) |-> if ( j = 0 , ( P - 1 ) , 0 ) )
6 reelprrecn 
 |-  RR e. { RR , CC }
7 6 a1i 
 |-  ( ph -> RR e. { RR , CC } )
8 reopn 
 |-  RR e. ( topGen ` ran (,) )
9 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
10 9 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
11 8 10 eleqtri 
 |-  RR e. ( ( TopOpen ` CCfld ) |`t RR )
12 11 a1i 
 |-  ( ph -> RR e. ( ( TopOpen ` CCfld ) |`t RR ) )
13 nnm1nn0 
 |-  ( P e. NN -> ( P - 1 ) e. NN0 )
14 1 13 syl 
 |-  ( ph -> ( P - 1 ) e. NN0 )
15 etransclem5 
 |-  ( 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 ) ) ) )
16 0red 
 |-  ( ph -> 0 e. RR )
17 7 12 1 2 3 14 15 4 16 etransclem31 
 |-  ( 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 ) ) ) ) ) ) ) )
18 nfv 
 |-  F/ c ph
19 nfcv 
 |-  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 ) ) ) ) ) ) )
20 4 14 etransclem16 
 |-  ( ph -> ( C ` ( P - 1 ) ) e. Fin )
21 simpr 
 |-  ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> c e. ( C ` ( P - 1 ) ) )
22 4 14 etransclem12 
 |-  ( ph -> ( C ` ( P - 1 ) ) = { c e. ( ( 0 ... ( P - 1 ) ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = ( P - 1 ) } )
23 22 adantr 
 |-  ( ( 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 ) } )
24 21 23 eleqtrd 
 |-  ( ( 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 ) } )
25 rabid 
 |-  ( 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 ) ) )
26 24 25 sylib 
 |-  ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> ( c e. ( ( 0 ... ( P - 1 ) ) ^m ( 0 ... M ) ) /\ sum_ j e. ( 0 ... M ) ( c ` j ) = ( P - 1 ) ) )
27 26 simprd 
 |-  ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> sum_ j e. ( 0 ... M ) ( c ` j ) = ( P - 1 ) )
28 27 eqcomd 
 |-  ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> ( P - 1 ) = sum_ j e. ( 0 ... M ) ( c ` j ) )
29 28 fveq2d 
 |-  ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> ( ! ` ( P - 1 ) ) = ( ! ` sum_ j e. ( 0 ... M ) ( c ` j ) ) )
30 29 oveq1d 
 |-  ( ( 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 ) ) ) )
31 nfcv 
 |-  F/_ j c
32 fzfid 
 |-  ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> ( 0 ... M ) e. Fin )
33 nn0ex 
 |-  NN0 e. _V
34 fzssnn0 
 |-  ( 0 ... ( P - 1 ) ) C_ NN0
35 mapss 
 |-  ( ( NN0 e. _V /\ ( 0 ... ( P - 1 ) ) C_ NN0 ) -> ( ( 0 ... ( P - 1 ) ) ^m ( 0 ... M ) ) C_ ( NN0 ^m ( 0 ... M ) ) )
36 33 34 35 mp2an 
 |-  ( ( 0 ... ( P - 1 ) ) ^m ( 0 ... M ) ) C_ ( NN0 ^m ( 0 ... M ) )
37 26 simpld 
 |-  ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> c e. ( ( 0 ... ( P - 1 ) ) ^m ( 0 ... M ) ) )
38 36 37 sseldi 
 |-  ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> c e. ( NN0 ^m ( 0 ... M ) ) )
39 31 32 38 mccl 
 |-  ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> ( ( ! ` sum_ j e. ( 0 ... M ) ( c ` j ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) e. NN )
40 30 39 eqeltrd 
 |-  ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> ( ( ! ` ( P - 1 ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) e. NN )
41 40 nnzd 
 |-  ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> ( ( ! ` ( P - 1 ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) e. ZZ )
42 1 adantr 
 |-  ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> P e. NN )
43 2 adantr 
 |-  ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> M e. NN0 )
44 elmapi 
 |-  ( c e. ( ( 0 ... ( P - 1 ) ) ^m ( 0 ... M ) ) -> c : ( 0 ... M ) --> ( 0 ... ( P - 1 ) ) )
45 37 44 syl 
 |-  ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> c : ( 0 ... M ) --> ( 0 ... ( P - 1 ) ) )
46 0zd 
 |-  ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> 0 e. ZZ )
47 42 43 45 46 etransclem10 
 |-  ( ( 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 )
48 fzfid 
 |-  ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> ( 1 ... M ) e. Fin )
49 1 ad2antrr 
 |-  ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 1 ... M ) ) -> P e. NN )
50 45 adantr 
 |-  ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 1 ... M ) ) -> c : ( 0 ... M ) --> ( 0 ... ( P - 1 ) ) )
51 fz1ssfz0 
 |-  ( 1 ... M ) C_ ( 0 ... M )
52 51 sseli 
 |-  ( j e. ( 1 ... M ) -> j e. ( 0 ... M ) )
53 52 adantl 
 |-  ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 1 ... M ) ) -> j e. ( 0 ... M ) )
54 0zd 
 |-  ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 1 ... M ) ) -> 0 e. ZZ )
55 49 50 53 54 etransclem3 
 |-  ( ( ( 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 )
56 48 55 fprodzcl 
 |-  ( ( 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 )
57 47 56 zmulcld 
 |-  ( ( 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 )
58 41 57 zmulcld 
 |-  ( ( 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 )
59 58 zcnd 
 |-  ( ( 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 )
60 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
61 14 60 eleqtrdi 
 |-  ( ph -> ( P - 1 ) e. ( ZZ>= ` 0 ) )
62 eluzfz2 
 |-  ( ( P - 1 ) e. ( ZZ>= ` 0 ) -> ( P - 1 ) e. ( 0 ... ( P - 1 ) ) )
63 61 62 syl 
 |-  ( ph -> ( P - 1 ) e. ( 0 ... ( P - 1 ) ) )
64 eluzfz1 
 |-  ( ( P - 1 ) e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... ( P - 1 ) ) )
65 61 64 syl 
 |-  ( ph -> 0 e. ( 0 ... ( P - 1 ) ) )
66 63 65 ifcld 
 |-  ( ph -> if ( j = 0 , ( P - 1 ) , 0 ) e. ( 0 ... ( P - 1 ) ) )
67 66 adantr 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> if ( j = 0 , ( P - 1 ) , 0 ) e. ( 0 ... ( P - 1 ) ) )
68 67 5 fmptd 
 |-  ( ph -> D : ( 0 ... M ) --> ( 0 ... ( P - 1 ) ) )
69 ovex 
 |-  ( 0 ... ( P - 1 ) ) e. _V
70 ovex 
 |-  ( 0 ... M ) e. _V
71 69 70 elmap 
 |-  ( D e. ( ( 0 ... ( P - 1 ) ) ^m ( 0 ... M ) ) <-> D : ( 0 ... M ) --> ( 0 ... ( P - 1 ) ) )
72 68 71 sylibr 
 |-  ( ph -> D e. ( ( 0 ... ( P - 1 ) ) ^m ( 0 ... M ) ) )
73 2 60 eleqtrdi 
 |-  ( ph -> M e. ( ZZ>= ` 0 ) )
74 fzsscn 
 |-  ( 0 ... ( P - 1 ) ) C_ CC
75 68 ffvelrnda 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( D ` j ) e. ( 0 ... ( P - 1 ) ) )
76 74 75 sseldi 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( D ` j ) e. CC )
77 fveq2 
 |-  ( j = 0 -> ( D ` j ) = ( D ` 0 ) )
78 73 76 77 fsum1p 
 |-  ( ph -> sum_ j e. ( 0 ... M ) ( D ` j ) = ( ( D ` 0 ) + sum_ j e. ( ( 0 + 1 ) ... M ) ( D ` j ) ) )
79 5 a1i 
 |-  ( ph -> D = ( j e. ( 0 ... M ) |-> if ( j = 0 , ( P - 1 ) , 0 ) ) )
80 simpr 
 |-  ( ( ph /\ j = 0 ) -> j = 0 )
81 80 iftrued 
 |-  ( ( ph /\ j = 0 ) -> if ( j = 0 , ( P - 1 ) , 0 ) = ( P - 1 ) )
82 eluzfz1 
 |-  ( M e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... M ) )
83 73 82 syl 
 |-  ( ph -> 0 e. ( 0 ... M ) )
84 79 81 83 14 fvmptd 
 |-  ( ph -> ( D ` 0 ) = ( P - 1 ) )
85 0p1e1 
 |-  ( 0 + 1 ) = 1
86 85 oveq1i 
 |-  ( ( 0 + 1 ) ... M ) = ( 1 ... M )
87 86 sumeq1i 
 |-  sum_ j e. ( ( 0 + 1 ) ... M ) ( D ` j ) = sum_ j e. ( 1 ... M ) ( D ` j )
88 87 a1i 
 |-  ( ph -> sum_ j e. ( ( 0 + 1 ) ... M ) ( D ` j ) = sum_ j e. ( 1 ... M ) ( D ` j ) )
89 5 fvmpt2 
 |-  ( ( j e. ( 0 ... M ) /\ if ( j = 0 , ( P - 1 ) , 0 ) e. ( 0 ... ( P - 1 ) ) ) -> ( D ` j ) = if ( j = 0 , ( P - 1 ) , 0 ) )
90 52 66 89 syl2anr 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( D ` j ) = if ( j = 0 , ( P - 1 ) , 0 ) )
91 0red 
 |-  ( j e. ( 1 ... M ) -> 0 e. RR )
92 1red 
 |-  ( j e. ( 1 ... M ) -> 1 e. RR )
93 elfzelz 
 |-  ( j e. ( 1 ... M ) -> j e. ZZ )
94 93 zred 
 |-  ( j e. ( 1 ... M ) -> j e. RR )
95 0lt1 
 |-  0 < 1
96 95 a1i 
 |-  ( j e. ( 1 ... M ) -> 0 < 1 )
97 elfzle1 
 |-  ( j e. ( 1 ... M ) -> 1 <_ j )
98 91 92 94 96 97 ltletrd 
 |-  ( j e. ( 1 ... M ) -> 0 < j )
99 91 98 gtned 
 |-  ( j e. ( 1 ... M ) -> j =/= 0 )
100 99 neneqd 
 |-  ( j e. ( 1 ... M ) -> -. j = 0 )
101 100 iffalsed 
 |-  ( j e. ( 1 ... M ) -> if ( j = 0 , ( P - 1 ) , 0 ) = 0 )
102 101 adantl 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> if ( j = 0 , ( P - 1 ) , 0 ) = 0 )
103 90 102 eqtrd 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( D ` j ) = 0 )
104 103 sumeq2dv 
 |-  ( ph -> sum_ j e. ( 1 ... M ) ( D ` j ) = sum_ j e. ( 1 ... M ) 0 )
105 fzfi 
 |-  ( 1 ... M ) e. Fin
106 105 olci 
 |-  ( ( 1 ... M ) C_ ( ZZ>= ` A ) \/ ( 1 ... M ) e. Fin )
107 sumz 
 |-  ( ( ( 1 ... M ) C_ ( ZZ>= ` A ) \/ ( 1 ... M ) e. Fin ) -> sum_ j e. ( 1 ... M ) 0 = 0 )
108 106 107 mp1i 
 |-  ( ph -> sum_ j e. ( 1 ... M ) 0 = 0 )
109 88 104 108 3eqtrd 
 |-  ( ph -> sum_ j e. ( ( 0 + 1 ) ... M ) ( D ` j ) = 0 )
110 84 109 oveq12d 
 |-  ( ph -> ( ( D ` 0 ) + sum_ j e. ( ( 0 + 1 ) ... M ) ( D ` j ) ) = ( ( P - 1 ) + 0 ) )
111 1 nncnd 
 |-  ( ph -> P e. CC )
112 1cnd 
 |-  ( ph -> 1 e. CC )
113 111 112 subcld 
 |-  ( ph -> ( P - 1 ) e. CC )
114 113 addid1d 
 |-  ( ph -> ( ( P - 1 ) + 0 ) = ( P - 1 ) )
115 78 110 114 3eqtrd 
 |-  ( ph -> sum_ j e. ( 0 ... M ) ( D ` j ) = ( P - 1 ) )
116 fveq1 
 |-  ( c = D -> ( c ` j ) = ( D ` j ) )
117 116 sumeq2sdv 
 |-  ( c = D -> sum_ j e. ( 0 ... M ) ( c ` j ) = sum_ j e. ( 0 ... M ) ( D ` j ) )
118 117 eqeq1d 
 |-  ( c = D -> ( sum_ j e. ( 0 ... M ) ( c ` j ) = ( P - 1 ) <-> sum_ j e. ( 0 ... M ) ( D ` j ) = ( P - 1 ) ) )
119 118 elrab 
 |-  ( 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 
 |-  ( ph -> D e. { c e. ( ( 0 ... ( P - 1 ) ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = ( P - 1 ) } )
121 120 22 eleqtrrd 
 |-  ( ph -> D e. ( C ` ( P - 1 ) ) )
122 116 fveq2d 
 |-  ( c = D -> ( ! ` ( c ` j ) ) = ( ! ` ( D ` j ) ) )
123 122 prodeq2ad 
 |-  ( c = D -> prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) = prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) )
124 123 oveq2d 
 |-  ( c = D -> ( ( ! ` ( P - 1 ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) = ( ( ! ` ( P - 1 ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) )
125 fveq1 
 |-  ( c = D -> ( c ` 0 ) = ( D ` 0 ) )
126 125 breq2d 
 |-  ( c = D -> ( ( P - 1 ) < ( c ` 0 ) <-> ( P - 1 ) < ( D ` 0 ) ) )
127 125 oveq2d 
 |-  ( c = D -> ( ( P - 1 ) - ( c ` 0 ) ) = ( ( P - 1 ) - ( D ` 0 ) ) )
128 127 fveq2d 
 |-  ( c = D -> ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) = ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) )
129 128 oveq2d 
 |-  ( c = D -> ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) ) = ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) )
130 127 oveq2d 
 |-  ( c = D -> ( 0 ^ ( ( P - 1 ) - ( c ` 0 ) ) ) = ( 0 ^ ( ( P - 1 ) - ( D ` 0 ) ) ) )
131 129 130 oveq12d 
 |-  ( 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 
 |-  ( 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 
 |-  ( c = D -> ( P < ( c ` j ) <-> P < ( D ` j ) ) )
134 116 oveq2d 
 |-  ( c = D -> ( P - ( c ` j ) ) = ( P - ( D ` j ) ) )
135 134 fveq2d 
 |-  ( c = D -> ( ! ` ( P - ( c ` j ) ) ) = ( ! ` ( P - ( D ` j ) ) ) )
136 135 oveq2d 
 |-  ( c = D -> ( ( ! ` P ) / ( ! ` ( P - ( c ` j ) ) ) ) = ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) )
137 134 oveq2d 
 |-  ( c = D -> ( ( 0 - j ) ^ ( P - ( c ` j ) ) ) = ( ( 0 - j ) ^ ( P - ( D ` j ) ) ) )
138 136 137 oveq12d 
 |-  ( 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( 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 18 19 20 59 121 142 fsumsplit1 
 |-  ( 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 34 75 sseldi 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( D ` j ) e. NN0 )
145 144 faccld 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( ! ` ( D ` j ) ) e. NN )
146 145 nncnd 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( ! ` ( D ` j ) ) e. CC )
147 77 fveq2d 
 |-  ( j = 0 -> ( ! ` ( D ` j ) ) = ( ! ` ( D ` 0 ) ) )
148 73 146 147 fprod1p 
 |-  ( ph -> prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) = ( ( ! ` ( D ` 0 ) ) x. prod_ j e. ( ( 0 + 1 ) ... M ) ( ! ` ( D ` j ) ) ) )
149 84 fveq2d 
 |-  ( ph -> ( ! ` ( D ` 0 ) ) = ( ! ` ( P - 1 ) ) )
150 86 prodeq1i 
 |-  prod_ j e. ( ( 0 + 1 ) ... M ) ( ! ` ( D ` j ) ) = prod_ j e. ( 1 ... M ) ( ! ` ( D ` j ) )
151 150 a1i 
 |-  ( ph -> prod_ j e. ( ( 0 + 1 ) ... M ) ( ! ` ( D ` j ) ) = prod_ j e. ( 1 ... M ) ( ! ` ( D ` j ) ) )
152 103 fveq2d 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( ! ` ( D ` j ) ) = ( ! ` 0 ) )
153 fac0 
 |-  ( ! ` 0 ) = 1
154 152 153 eqtrdi 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( ! ` ( D ` j ) ) = 1 )
155 154 prodeq2dv 
 |-  ( ph -> prod_ j e. ( 1 ... M ) ( ! ` ( D ` j ) ) = prod_ j e. ( 1 ... M ) 1 )
156 prod1 
 |-  ( ( ( 1 ... M ) C_ ( ZZ>= ` A ) \/ ( 1 ... M ) e. Fin ) -> prod_ j e. ( 1 ... M ) 1 = 1 )
157 106 156 mp1i 
 |-  ( ph -> prod_ j e. ( 1 ... M ) 1 = 1 )
158 151 155 157 3eqtrd 
 |-  ( ph -> prod_ j e. ( ( 0 + 1 ) ... M ) ( ! ` ( D ` j ) ) = 1 )
159 149 158 oveq12d 
 |-  ( ph -> ( ( ! ` ( D ` 0 ) ) x. prod_ j e. ( ( 0 + 1 ) ... M ) ( ! ` ( D ` j ) ) ) = ( ( ! ` ( P - 1 ) ) x. 1 ) )
160 14 faccld 
 |-  ( ph -> ( ! ` ( P - 1 ) ) e. NN )
161 160 nncnd 
 |-  ( ph -> ( ! ` ( P - 1 ) ) e. CC )
162 161 mulid1d 
 |-  ( ph -> ( ( ! ` ( P - 1 ) ) x. 1 ) = ( ! ` ( P - 1 ) ) )
163 148 159 162 3eqtrd 
 |-  ( ph -> prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) = ( ! ` ( P - 1 ) ) )
164 163 oveq2d 
 |-  ( ph -> ( ( ! ` ( P - 1 ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) = ( ( ! ` ( P - 1 ) ) / ( ! ` ( P - 1 ) ) ) )
165 160 nnne0d 
 |-  ( ph -> ( ! ` ( P - 1 ) ) =/= 0 )
166 161 165 dividd 
 |-  ( ph -> ( ( ! ` ( P - 1 ) ) / ( ! ` ( P - 1 ) ) ) = 1 )
167 164 166 eqtrd 
 |-  ( ph -> ( ( ! ` ( P - 1 ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) = 1 )
168 14 nn0red 
 |-  ( ph -> ( P - 1 ) e. RR )
169 84 168 eqeltrd 
 |-  ( ph -> ( D ` 0 ) e. RR )
170 169 168 lttri3d 
 |-  ( ph -> ( ( D ` 0 ) = ( P - 1 ) <-> ( -. ( D ` 0 ) < ( P - 1 ) /\ -. ( P - 1 ) < ( D ` 0 ) ) ) )
171 84 170 mpbid 
 |-  ( ph -> ( -. ( D ` 0 ) < ( P - 1 ) /\ -. ( P - 1 ) < ( D ` 0 ) ) )
172 171 simprd 
 |-  ( ph -> -. ( P - 1 ) < ( D ` 0 ) )
173 172 iffalsed 
 |-  ( 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 
 |-  ( ph -> ( P - 1 ) = ( D ` 0 ) )
175 113 174 subeq0bd 
 |-  ( ph -> ( ( P - 1 ) - ( D ` 0 ) ) = 0 )
176 175 fveq2d 
 |-  ( ph -> ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) = ( ! ` 0 ) )
177 176 153 eqtrdi 
 |-  ( ph -> ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) = 1 )
178 177 oveq2d 
 |-  ( ph -> ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) = ( ( ! ` ( P - 1 ) ) / 1 ) )
179 161 div1d 
 |-  ( ph -> ( ( ! ` ( P - 1 ) ) / 1 ) = ( ! ` ( P - 1 ) ) )
180 178 179 eqtrd 
 |-  ( ph -> ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) = ( ! ` ( P - 1 ) ) )
181 175 oveq2d 
 |-  ( ph -> ( 0 ^ ( ( P - 1 ) - ( D ` 0 ) ) ) = ( 0 ^ 0 ) )
182 0cnd 
 |-  ( ph -> 0 e. CC )
183 182 exp0d 
 |-  ( ph -> ( 0 ^ 0 ) = 1 )
184 181 183 eqtrd 
 |-  ( ph -> ( 0 ^ ( ( P - 1 ) - ( D ` 0 ) ) ) = 1 )
185 180 184 oveq12d 
 |-  ( ph -> ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( 0 ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) = ( ( ! ` ( P - 1 ) ) x. 1 ) )
186 173 185 162 3eqtrd 
 |-  ( ph -> if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( 0 ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) = ( ! ` ( P - 1 ) ) )
187 fzssre 
 |-  ( 0 ... ( P - 1 ) ) C_ RR
188 68 adantr 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> D : ( 0 ... M ) --> ( 0 ... ( P - 1 ) ) )
189 52 adantl 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> j e. ( 0 ... M ) )
190 188 189 ffvelrnd 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( D ` j ) e. ( 0 ... ( P - 1 ) ) )
191 187 190 sseldi 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( D ` j ) e. RR )
192 1 nnred 
 |-  ( ph -> P e. RR )
193 192 adantr 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> P e. RR )
194 1 nngt0d 
 |-  ( ph -> 0 < P )
195 16 192 194 ltled 
 |-  ( ph -> 0 <_ P )
196 195 adantr 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> 0 <_ P )
197 103 196 eqbrtrd 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( D ` j ) <_ P )
198 191 193 197 lensymd 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> -. P < ( D ` j ) )
199 198 iffalsed 
 |-  ( ( 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 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( P - ( D ` j ) ) = ( P - 0 ) )
201 111 adantr 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> P e. CC )
202 201 subid1d 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( P - 0 ) = P )
203 200 202 eqtrd 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( P - ( D ` j ) ) = P )
204 203 fveq2d 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( ! ` ( P - ( D ` j ) ) ) = ( ! ` P ) )
205 204 oveq2d 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) = ( ( ! ` P ) / ( ! ` P ) ) )
206 1 nnnn0d 
 |-  ( ph -> P e. NN0 )
207 206 faccld 
 |-  ( ph -> ( ! ` P ) e. NN )
208 207 nncnd 
 |-  ( ph -> ( ! ` P ) e. CC )
209 207 nnne0d 
 |-  ( ph -> ( ! ` P ) =/= 0 )
210 208 209 dividd 
 |-  ( ph -> ( ( ! ` P ) / ( ! ` P ) ) = 1 )
211 210 adantr 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( ! ` P ) / ( ! ` P ) ) = 1 )
212 205 211 eqtrd 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) = 1 )
213 df-neg 
 |-  -u j = ( 0 - j )
214 213 eqcomi 
 |-  ( 0 - j ) = -u j
215 214 a1i 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( 0 - j ) = -u j )
216 215 203 oveq12d 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( 0 - j ) ^ ( P - ( D ` j ) ) ) = ( -u j ^ P ) )
217 212 216 oveq12d 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( 0 - j ) ^ ( P - ( D ` j ) ) ) ) = ( 1 x. ( -u j ^ P ) ) )
218 93 znegcld 
 |-  ( j e. ( 1 ... M ) -> -u j e. ZZ )
219 218 zcnd 
 |-  ( j e. ( 1 ... M ) -> -u j e. CC )
220 219 adantl 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> -u j e. CC )
221 206 adantr 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> P e. NN0 )
222 220 221 expcld 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( -u j ^ P ) e. CC )
223 222 mulid2d 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( 1 x. ( -u j ^ P ) ) = ( -u j ^ P ) )
224 199 217 223 3eqtrd 
 |-  ( ( 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( ph -> ( 1 ... M ) e. Fin )
229 zexpcl 
 |-  ( ( -u j e. ZZ /\ P e. NN0 ) -> ( -u j ^ P ) e. ZZ )
230 218 206 229 syl2anr 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( -u j ^ P ) e. ZZ )
231 228 230 fprodzcl 
 |-  ( ph -> prod_ j e. ( 1 ... M ) ( -u j ^ P ) e. ZZ )
232 231 zcnd 
 |-  ( ph -> prod_ j e. ( 1 ... M ) ( -u j ^ P ) e. CC )
233 161 232 mulcld 
 |-  ( ph -> ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( -u j ^ P ) ) e. CC )
234 233 mulid2d 
 |-  ( 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 
 |-  ( 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 
 |-  ( c e. ( ( C ` ( P - 1 ) ) \ { D } ) -> c e. ( C ` ( P - 1 ) ) )
237 83 adantr 
 |-  ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> 0 e. ( 0 ... M ) )
238 45 237 ffvelrnd 
 |-  ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> ( c ` 0 ) e. ( 0 ... ( P - 1 ) ) )
239 236 238 sylan2 
 |-  ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( c ` 0 ) e. ( 0 ... ( P - 1 ) ) )
240 187 239 sseldi 
 |-  ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( c ` 0 ) e. RR )
241 168 adantr 
 |-  ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( P - 1 ) e. RR )
242 elfzle2 
 |-  ( ( c ` 0 ) e. ( 0 ... ( P - 1 ) ) -> ( c ` 0 ) <_ ( P - 1 ) )
243 239 242 syl 
 |-  ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( c ` 0 ) <_ ( P - 1 ) )
244 240 241 243 lensymd 
 |-  ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> -. ( P - 1 ) < ( c ` 0 ) )
245 244 iffalsed 
 |-  ( ( 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 14 nn0zd 
 |-  ( ph -> ( P - 1 ) e. ZZ )
247 246 adantr 
 |-  ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( P - 1 ) e. ZZ )
248 239 elfzelzd 
 |-  ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( c ` 0 ) e. ZZ )
249 247 248 zsubcld 
 |-  ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( ( P - 1 ) - ( c ` 0 ) ) e. ZZ )
250 45 ffnd 
 |-  ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> c Fn ( 0 ... M ) )
251 250 adantr 
 |-  ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) -> c Fn ( 0 ... M ) )
252 68 ffnd 
 |-  ( ph -> D Fn ( 0 ... M ) )
253 252 ad2antrr 
 |-  ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) -> D Fn ( 0 ... M ) )
254 fveq2 
 |-  ( j = 0 -> ( c ` j ) = ( c ` 0 ) )
255 254 adantl 
 |-  ( ( ( ph /\ ( P - 1 ) = ( c ` 0 ) ) /\ j = 0 ) -> ( c ` j ) = ( c ` 0 ) )
256 id 
 |-  ( ( P - 1 ) = ( c ` 0 ) -> ( P - 1 ) = ( c ` 0 ) )
257 256 eqcomd 
 |-  ( ( P - 1 ) = ( c ` 0 ) -> ( c ` 0 ) = ( P - 1 ) )
258 257 ad2antlr 
 |-  ( ( ( ph /\ ( P - 1 ) = ( c ` 0 ) ) /\ j = 0 ) -> ( c ` 0 ) = ( P - 1 ) )
259 77 adantl 
 |-  ( ( ph /\ j = 0 ) -> ( D ` j ) = ( D ` 0 ) )
260 84 adantr 
 |-  ( ( ph /\ j = 0 ) -> ( D ` 0 ) = ( P - 1 ) )
261 259 260 eqtr2d 
 |-  ( ( ph /\ j = 0 ) -> ( P - 1 ) = ( D ` j ) )
262 261 adantlr 
 |-  ( ( ( ph /\ ( P - 1 ) = ( c ` 0 ) ) /\ j = 0 ) -> ( P - 1 ) = ( D ` j ) )
263 255 258 262 3eqtrd 
 |-  ( ( ( ph /\ ( P - 1 ) = ( c ` 0 ) ) /\ j = 0 ) -> ( c ` j ) = ( D ` j ) )
264 263 adantllr 
 |-  ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) /\ j = 0 ) -> ( c ` j ) = ( D ` j ) )
265 264 adantlr 
 |-  ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) /\ j e. ( 0 ... M ) ) /\ j = 0 ) -> ( c ` j ) = ( D ` j ) )
266 27 ad4antr 
 |-  ( ( ( ( ( ( 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 ) )
267 168 ad5antr 
 |-  ( ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> ( P - 1 ) e. RR )
268 168 ad4antr 
 |-  ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> ( P - 1 ) e. RR )
269 45 adantr 
 |-  ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( 1 ... M ) ) -> c : ( 0 ... M ) --> ( 0 ... ( P - 1 ) ) )
270 51 sseli 
 |-  ( k e. ( 1 ... M ) -> k e. ( 0 ... M ) )
271 270 adantl 
 |-  ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( 1 ... M ) ) -> k e. ( 0 ... M ) )
272 269 271 ffvelrnd 
 |-  ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( 1 ... M ) ) -> ( c ` k ) e. ( 0 ... ( P - 1 ) ) )
273 34 272 sseldi 
 |-  ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( 1 ... M ) ) -> ( c ` k ) e. NN0 )
274 48 273 fsumnn0cl 
 |-  ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> sum_ k e. ( 1 ... M ) ( c ` k ) e. NN0 )
275 274 nn0red 
 |-  ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> sum_ k e. ( 1 ... M ) ( c ` k ) e. RR )
276 275 ad3antrrr 
 |-  ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> sum_ k e. ( 1 ... M ) ( c ` k ) e. RR )
277 0red 
 |-  ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> 0 e. RR )
278 45 ffvelrnda 
 |-  ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) -> ( c ` j ) e. ( 0 ... ( P - 1 ) ) )
279 187 278 sseldi 
 |-  ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) -> ( c ` j ) e. RR )
280 279 ad2antrr 
 |-  ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> ( c ` j ) e. RR )
281 nfv 
 |-  F/ k ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 )
282 nfcv 
 |-  F/_ k ( c ` j )
283 fzfid 
 |-  ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> ( 1 ... M ) e. Fin )
284 simp-4l 
 |-  ( ( ( ( ( ( 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 ) ) ) )
285 74 272 sseldi 
 |-  ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( 1 ... M ) ) -> ( c ` k ) e. CC )
286 284 285 sylancom 
 |-  ( ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) /\ k e. ( 1 ... M ) ) -> ( c ` k ) e. CC )
287 1zzd 
 |-  ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> 1 e. ZZ )
288 elfzel2 
 |-  ( j e. ( 0 ... M ) -> M e. ZZ )
289 288 adantr 
 |-  ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> M e. ZZ )
290 elfzelz 
 |-  ( j e. ( 0 ... M ) -> j e. ZZ )
291 290 adantr 
 |-  ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> j e. ZZ )
292 287 289 291 3jca 
 |-  ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> ( 1 e. ZZ /\ M e. ZZ /\ j e. ZZ ) )
293 elfznn0 
 |-  ( j e. ( 0 ... M ) -> j e. NN0 )
294 293 adantr 
 |-  ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> j e. NN0 )
295 neqne 
 |-  ( -. j = 0 -> j =/= 0 )
296 295 adantl 
 |-  ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> j =/= 0 )
297 elnnne0 
 |-  ( j e. NN <-> ( j e. NN0 /\ j =/= 0 ) )
298 294 296 297 sylanbrc 
 |-  ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> j e. NN )
299 298 nnge1d 
 |-  ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> 1 <_ j )
300 elfzle2 
 |-  ( j e. ( 0 ... M ) -> j <_ M )
301 300 adantr 
 |-  ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> j <_ M )
302 292 299 301 jca32 
 |-  ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> ( ( 1 e. ZZ /\ M e. ZZ /\ j e. ZZ ) /\ ( 1 <_ j /\ j <_ M ) ) )
303 elfz2 
 |-  ( j e. ( 1 ... M ) <-> ( ( 1 e. ZZ /\ M e. ZZ /\ j e. ZZ ) /\ ( 1 <_ j /\ j <_ M ) ) )
304 302 303 sylibr 
 |-  ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> j e. ( 1 ... M ) )
305 304 adantr 
 |-  ( ( ( j e. ( 0 ... M ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> j e. ( 1 ... M ) )
306 305 adantlll 
 |-  ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> j e. ( 1 ... M ) )
307 fveq2 
 |-  ( k = j -> ( c ` k ) = ( c ` j ) )
308 281 282 283 286 306 307 fsumsplit1 
 |-  ( ( ( ( ( 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 ) ) )
309 308 eqcomd 
 |-  ( ( ( ( ( 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 ) )
310 309 276 eqeltrd 
 |-  ( ( ( ( ( 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 )
311 elfzle1 
 |-  ( ( c ` j ) e. ( 0 ... ( P - 1 ) ) -> 0 <_ ( c ` j ) )
312 278 311 syl 
 |-  ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) -> 0 <_ ( c ` j ) )
313 312 ad2antrr 
 |-  ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> 0 <_ ( c ` j ) )
314 neqne 
 |-  ( -. ( c ` j ) = 0 -> ( c ` j ) =/= 0 )
315 314 adantl 
 |-  ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> ( c ` j ) =/= 0 )
316 277 280 313 315 leneltd 
 |-  ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> 0 < ( c ` j ) )
317 diffi 
 |-  ( ( 1 ... M ) e. Fin -> ( ( 1 ... M ) \ { j } ) e. Fin )
318 105 317 mp1i 
 |-  ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> ( ( 1 ... M ) \ { j } ) e. Fin )
319 eldifi 
 |-  ( k e. ( ( 1 ... M ) \ { j } ) -> k e. ( 1 ... M ) )
320 319 adantl 
 |-  ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( ( 1 ... M ) \ { j } ) ) -> k e. ( 1 ... M ) )
321 51 320 sseldi 
 |-  ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( ( 1 ... M ) \ { j } ) ) -> k e. ( 0 ... M ) )
322 45 ffvelrnda 
 |-  ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( 0 ... M ) ) -> ( c ` k ) e. ( 0 ... ( P - 1 ) ) )
323 187 322 sseldi 
 |-  ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( 0 ... M ) ) -> ( c ` k ) e. RR )
324 321 323 syldan 
 |-  ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( ( 1 ... M ) \ { j } ) ) -> ( c ` k ) e. RR )
325 elfzle1 
 |-  ( ( c ` k ) e. ( 0 ... ( P - 1 ) ) -> 0 <_ ( c ` k ) )
326 322 325 syl 
 |-  ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( 0 ... M ) ) -> 0 <_ ( c ` k ) )
327 321 326 syldan 
 |-  ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( ( 1 ... M ) \ { j } ) ) -> 0 <_ ( c ` k ) )
328 318 324 327 fsumge0 
 |-  ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> 0 <_ sum_ k e. ( ( 1 ... M ) \ { j } ) ( c ` k ) )
329 328 adantr 
 |-  ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) -> 0 <_ sum_ k e. ( ( 1 ... M ) \ { j } ) ( c ` k ) )
330 318 324 fsumrecl 
 |-  ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> sum_ k e. ( ( 1 ... M ) \ { j } ) ( c ` k ) e. RR )
331 330 adantr 
 |-  ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) -> sum_ k e. ( ( 1 ... M ) \ { j } ) ( c ` k ) e. RR )
332 279 331 addge01d 
 |-  ( ( ( 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 ) ) ) )
333 329 332 mpbid 
 |-  ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) -> ( c ` j ) <_ ( ( c ` j ) + sum_ k e. ( ( 1 ... M ) \ { j } ) ( c ` k ) ) )
334 333 ad2antrr 
 |-  ( ( ( ( ( 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 ) ) )
335 277 280 310 316 334 ltletrd 
 |-  ( ( ( ( ( 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 ) ) )
336 335 309 breqtrd 
 |-  ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> 0 < sum_ k e. ( 1 ... M ) ( c ` k ) )
337 276 336 elrpd 
 |-  ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> sum_ k e. ( 1 ... M ) ( c ` k ) e. RR+ )
338 268 337 ltaddrpd 
 |-  ( ( ( ( ( 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 ) ) )
339 338 adantl3r 
 |-  ( ( ( ( ( ( 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 ) ) )
340 fveq2 
 |-  ( j = k -> ( c ` j ) = ( c ` k ) )
341 340 cbvsumv 
 |-  sum_ j e. ( 0 ... M ) ( c ` j ) = sum_ k e. ( 0 ... M ) ( c ` k )
342 341 a1i 
 |-  ( ( ( ( ( ( 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 ) )
343 73 ad5antr 
 |-  ( ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> M e. ( ZZ>= ` 0 ) )
344 simp-5l 
 |-  ( ( ( ( ( ( ( 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 ) ) ) )
345 74 322 sseldi 
 |-  ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ k e. ( 0 ... M ) ) -> ( c ` k ) e. CC )
346 344 345 sylancom 
 |-  ( ( ( ( ( ( ( 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 )
347 fveq2 
 |-  ( k = 0 -> ( c ` k ) = ( c ` 0 ) )
348 343 346 347 fsum1p 
 |-  ( ( ( ( ( ( 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 ) ) )
349 257 ad4antlr 
 |-  ( ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> ( c ` 0 ) = ( P - 1 ) )
350 86 sumeq1i 
 |-  sum_ k e. ( ( 0 + 1 ) ... M ) ( c ` k ) = sum_ k e. ( 1 ... M ) ( c ` k )
351 350 a1i 
 |-  ( ( ( ( ( ( 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 ) )
352 349 351 oveq12d 
 |-  ( ( ( ( ( ( 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 ) ) )
353 342 348 352 3eqtrrd 
 |-  ( ( ( ( ( ( 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 ) )
354 339 353 breqtrd 
 |-  ( ( ( ( ( ( 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 ) )
355 267 354 gtned 
 |-  ( ( ( ( ( ( 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 ) )
356 355 neneqd 
 |-  ( ( ( ( ( ( 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 ) )
357 266 356 condan 
 |-  ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) -> ( c ` j ) = 0 )
358 simpr 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> j e. ( 0 ... M ) )
359 34 67 sseldi 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> if ( j = 0 , ( P - 1 ) , 0 ) e. NN0 )
360 5 fvmpt2 
 |-  ( ( j e. ( 0 ... M ) /\ if ( j = 0 , ( P - 1 ) , 0 ) e. NN0 ) -> ( D ` j ) = if ( j = 0 , ( P - 1 ) , 0 ) )
361 358 359 360 syl2anc 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( D ` j ) = if ( j = 0 , ( P - 1 ) , 0 ) )
362 361 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) -> ( D ` j ) = if ( j = 0 , ( P - 1 ) , 0 ) )
363 simpr 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) -> -. j = 0 )
364 363 iffalsed 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) -> if ( j = 0 , ( P - 1 ) , 0 ) = 0 )
365 362 364 eqtr2d 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) -> 0 = ( D ` j ) )
366 365 adantllr 
 |-  ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) -> 0 = ( D ` j ) )
367 366 adantllr 
 |-  ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) -> 0 = ( D ` j ) )
368 357 367 eqtrd 
 |-  ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) -> ( c ` j ) = ( D ` j ) )
369 265 368 pm2.61dan 
 |-  ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) /\ j e. ( 0 ... M ) ) -> ( c ` j ) = ( D ` j ) )
370 251 253 369 eqfnfvd 
 |-  ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) -> c = D )
371 236 370 sylanl2 
 |-  ( ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) /\ ( P - 1 ) = ( c ` 0 ) ) -> c = D )
372 eldifsni 
 |-  ( c e. ( ( C ` ( P - 1 ) ) \ { D } ) -> c =/= D )
373 372 neneqd 
 |-  ( c e. ( ( C ` ( P - 1 ) ) \ { D } ) -> -. c = D )
374 373 ad2antlr 
 |-  ( ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) /\ ( P - 1 ) = ( c ` 0 ) ) -> -. c = D )
375 371 374 pm2.65da 
 |-  ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> -. ( P - 1 ) = ( c ` 0 ) )
376 375 neqned 
 |-  ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( P - 1 ) =/= ( c ` 0 ) )
377 240 241 243 376 leneltd 
 |-  ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( c ` 0 ) < ( P - 1 ) )
378 240 241 posdifd 
 |-  ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( ( c ` 0 ) < ( P - 1 ) <-> 0 < ( ( P - 1 ) - ( c ` 0 ) ) ) )
379 377 378 mpbid 
 |-  ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> 0 < ( ( P - 1 ) - ( c ` 0 ) ) )
380 elnnz 
 |-  ( ( ( P - 1 ) - ( c ` 0 ) ) e. NN <-> ( ( ( P - 1 ) - ( c ` 0 ) ) e. ZZ /\ 0 < ( ( P - 1 ) - ( c ` 0 ) ) ) )
381 249 379 380 sylanbrc 
 |-  ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( ( P - 1 ) - ( c ` 0 ) ) e. NN )
382 381 0expd 
 |-  ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( 0 ^ ( ( P - 1 ) - ( c ` 0 ) ) ) = 0 )
383 382 oveq2d 
 |-  ( ( 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 ) )
384 161 adantr 
 |-  ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( ! ` ( P - 1 ) ) e. CC )
385 381 nnnn0d 
 |-  ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( ( P - 1 ) - ( c ` 0 ) ) e. NN0 )
386 385 faccld 
 |-  ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) e. NN )
387 386 nncnd 
 |-  ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) e. CC )
388 386 nnne0d 
 |-  ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) =/= 0 )
389 384 387 388 divcld 
 |-  ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) ) e. CC )
390 389 mul01d 
 |-  ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) ) x. 0 ) = 0 )
391 245 383 390 3eqtrd 
 |-  ( ( 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 )
392 391 oveq1d 
 |-  ( ( 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 ) ) ) ) ) ) )
393 236 56 sylan2 
 |-  ( ( 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 )
394 393 zcnd 
 |-  ( ( 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 )
395 394 mul02d 
 |-  ( ( 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 )
396 392 395 eqtrd 
 |-  ( ( 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 )
397 396 oveq2d 
 |-  ( ( 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 ) )
398 fzfid 
 |-  ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( 0 ... M ) e. Fin )
399 34 278 sseldi 
 |-  ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) -> ( c ` j ) e. NN0 )
400 236 399 sylanl2 
 |-  ( ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) /\ j e. ( 0 ... M ) ) -> ( c ` j ) e. NN0 )
401 400 faccld 
 |-  ( ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) /\ j e. ( 0 ... M ) ) -> ( ! ` ( c ` j ) ) e. NN )
402 398 401 fprodnncl 
 |-  ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) e. NN )
403 402 nncnd 
 |-  ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) e. CC )
404 402 nnne0d 
 |-  ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) =/= 0 )
405 384 403 404 divcld 
 |-  ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( ( ! ` ( P - 1 ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) e. CC )
406 405 mul01d 
 |-  ( ( ph /\ c e. ( ( C ` ( P - 1 ) ) \ { D } ) ) -> ( ( ( ! ` ( P - 1 ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) x. 0 ) = 0 )
407 397 406 eqtrd 
 |-  ( ( 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 )
408 407 sumeq2dv 
 |-  ( 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 )
409 diffi 
 |-  ( ( C ` ( P - 1 ) ) e. Fin -> ( ( C ` ( P - 1 ) ) \ { D } ) e. Fin )
410 20 409 syl 
 |-  ( ph -> ( ( C ` ( P - 1 ) ) \ { D } ) e. Fin )
411 410 olcd 
 |-  ( ph -> ( ( ( C ` ( P - 1 ) ) \ { D } ) C_ ( ZZ>= ` 0 ) \/ ( ( C ` ( P - 1 ) ) \ { D } ) e. Fin ) )
412 sumz 
 |-  ( ( ( ( C ` ( P - 1 ) ) \ { D } ) C_ ( ZZ>= ` 0 ) \/ ( ( C ` ( P - 1 ) ) \ { D } ) e. Fin ) -> sum_ c e. ( ( C ` ( P - 1 ) ) \ { D } ) 0 = 0 )
413 411 412 syl 
 |-  ( ph -> sum_ c e. ( ( C ` ( P - 1 ) ) \ { D } ) 0 = 0 )
414 408 413 eqtrd 
 |-  ( 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 )
415 235 414 oveq12d 
 |-  ( 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 ) )
416 233 addid1d 
 |-  ( ph -> ( ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( -u j ^ P ) ) + 0 ) = ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( -u j ^ P ) ) )
417 nfv 
 |-  F/ j ph
418 417 206 228 220 fprodexp 
 |-  ( ph -> prod_ j e. ( 1 ... M ) ( -u j ^ P ) = ( prod_ j e. ( 1 ... M ) -u j ^ P ) )
419 418 oveq2d 
 |-  ( ph -> ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( -u j ^ P ) ) = ( ( ! ` ( P - 1 ) ) x. ( prod_ j e. ( 1 ... M ) -u j ^ P ) ) )
420 415 416 419 3eqtrd 
 |-  ( 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 ) ) )
421 17 143 420 3eqtrd 
 |-  ( ph -> ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) = ( ( ! ` ( P - 1 ) ) x. ( prod_ j e. ( 1 ... M ) -u j ^ P ) ) )