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