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 ) } )`
` |-  ( ( 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 )`
` |-  ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) -> P e. NN )`
` |-  ( ( 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 )`
` |-  ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 1 ... M ) ) -> P e. NN )`
` |-  ( ( ( 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 ) )`
` |-  ( ( ( 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 ) ) )`
` |-  ( ( 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 )`
` |-  ( ( 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 )`
` |-  ( 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 ) ) )`
` |-  ( 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 ) ) ) ) ) )`
` |-  ( 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 syl6eq
` |-  ( ( 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 syl6eq
` |-  ( 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`
` |-  ( ( ph /\ j e. ( 1 ... M ) ) -> D : ( 0 ... M ) --> ( 0 ... ( P - 1 ) ) )`
` |-  ( ( 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 )`
` |-  ( ( ph /\ j e. ( 1 ... M ) ) -> P e. RR )`
194 1 nngt0d
` |-  ( ph -> 0 < P )`
195 16 192 194 ltled
` |-  ( ph -> 0 <_ P )`
` |-  ( ( 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 ) )`
` |-  ( ( 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 )`
` |-  ( ( 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 )`
` |-  ( ( ph /\ j e. ( 1 ... M ) ) -> -u j e. CC )`
` |-  ( ( 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 ) ) )`
` |-  ( ( 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 )`
` |-  ( ( 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 )`
` |-  ( ( 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 ) )`
` |-  ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) -> c Fn ( 0 ... M ) )`
252 68 ffnd
` |-  ( ph -> D Fn ( 0 ... M ) )`
` |-  ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) -> D Fn ( 0 ... M ) )`
254 fveq2
` |-  ( j = 0 -> ( c ` j ) = ( c ` 0 ) )`
` |-  ( ( ( 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 ) )`
` |-  ( ( ( ph /\ ( P - 1 ) = ( c ` 0 ) ) /\ j = 0 ) -> ( c ` 0 ) = ( P - 1 ) )`
` |-  ( ( ph /\ j = 0 ) -> ( D ` j ) = ( D ` 0 ) )`
` |-  ( ( ph /\ j = 0 ) -> ( D ` 0 ) = ( P - 1 ) )`
261 259 260 eqtr2d
` |-  ( ( ph /\ j = 0 ) -> ( P - 1 ) = ( D ` j ) )`
` |-  ( ( ( 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 ) )`
` |-  ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) /\ j = 0 ) -> ( c ` j ) = ( D ` j ) )`
` |-  ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) /\ j e. ( 0 ... M ) ) /\ j = 0 ) -> ( c ` j ) = ( D ` j ) )`
` |-  ( ( ( ( ( ( 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 ) )`
` |-  ( ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ ( P - 1 ) = ( c ` 0 ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> ( P - 1 ) e. RR )`
` |-  ( ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> ( P - 1 ) e. RR )`
` |-  ( ( ( 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 ) )`
` |-  ( ( ( 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 )`
` |-  ( ( ( ( ( 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 )`
` |-  ( ( ( ( ( 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 )`
` |-  ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> M e. ZZ )`
290 elfzelz
` |-  ( j e. ( 0 ... M ) -> j e. ZZ )`
` |-  ( ( 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 )`
` |-  ( ( j e. ( 0 ... M ) /\ -. j = 0 ) -> j e. NN0 )`
295 neqne
` |-  ( -. j = 0 -> j =/= 0 )`
` |-  ( ( 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 )`
` |-  ( ( 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 ) )`
` |-  ( ( ( j e. ( 0 ... M ) /\ -. j = 0 ) /\ -. ( c ` j ) = 0 ) -> j e. ( 1 ... M ) )`
` |-  ( ( ( ( ( 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 ) )`
` |-  ( ( ( ( ( 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 )`
` |-  ( ( ( ( ( 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 ) )`
` |-  ( ( ( 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 ) )`
` |-  ( ( ( 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 )`
` |-  ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) -> sum_ k e. ( ( 1 ... M ) \ { j } ) ( c ` k ) e. RR )`
` |-  ( ( ( 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 ) ) )`
` |-  ( ( ( ( ( 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+ )`
` |-  ( ( ( ( ( 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 ) ) )`
` |-  ( ( ( ( ( ( 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 ) )`
` |-  ( ( ( ( ( ( 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 ) ) )`
` |-  ( ( ( ( ( ( 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 ) )`
` |-  ( ( ( 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 ) )`
` |-  ( ( ( ( ph /\ c e. ( C ` ( P - 1 ) ) ) /\ j e. ( 0 ... M ) ) /\ -. j = 0 ) -> 0 = ( D ` j ) )`
` |-  ( ( ( ( ( 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 )`
` |-  ( ( ( 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 ) )`
` |-  ( ( 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 ) )`
` |-  ( ph -> ( ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( -u j ^ P ) ) + 0 ) = ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( -u j ^ P ) ) )`
` |-  F/ j ph`
` |-  ( ph -> prod_ j e. ( 1 ... M ) ( -u j ^ P ) = ( prod_ j e. ( 1 ... M ) -u j ^ P ) )`
` |-  ( ph -> ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( -u j ^ P ) ) = ( ( ! ` ( P - 1 ) ) x. ( prod_ j e. ( 1 ... M ) -u j ^ P ) ) )`
` |-  ( 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 ) ) )`
` |-  ( ph -> ( ( ( RR Dn F ) ` ( P - 1 ) ) ` 0 ) = ( ( ! ` ( P - 1 ) ) x. ( prod_ j e. ( 1 ... M ) -u j ^ P ) ) )`