Metamath Proof Explorer

Theorem etransclem24

Description: P divides the I -th derivative of F applied to J . when J = 0 and I is not equal to P - 1 . This is the second part of case 2 proven in Juillerat p. 13 . (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem24.p 
|- ( ph -> P e. NN )
etransclem24.m 
|- ( ph -> M e. NN0 )
etransclem24.i 
|- ( ph -> I e. NN0 )
etransclem24.ip 
|- ( ph -> I =/= ( P - 1 ) )
etransclem24.j 
|- ( ph -> J = 0 )
etransclem24.c 
|- C = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = n } )
etransclem24.d 
|- ( ph -> D e. ( C ` I ) )
Assertion etransclem24 
|- ( ph -> P || ( ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. ( if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) ) / ( ! ` ( P - 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 etransclem24.p 
 |-  ( ph -> P e. NN )
2 etransclem24.m 
 |-  ( ph -> M e. NN0 )
3 etransclem24.i 
 |-  ( ph -> I e. NN0 )
4 etransclem24.ip 
 |-  ( ph -> I =/= ( P - 1 ) )
5 etransclem24.j 
 |-  ( ph -> J = 0 )
6 etransclem24.c 
 |-  C = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = n } )
7 etransclem24.d 
 |-  ( ph -> D e. ( C ` I ) )
8 6 3 etransclem12 
 |-  ( ph -> ( C ` I ) = { c e. ( ( 0 ... I ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = I } )
9 7 8 eleqtrd 
 |-  ( ph -> D e. { c e. ( ( 0 ... I ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = I } )
10 fveq1 
 |-  ( c = D -> ( c ` j ) = ( D ` j ) )
11 10 sumeq2sdv 
 |-  ( c = D -> sum_ j e. ( 0 ... M ) ( c ` j ) = sum_ j e. ( 0 ... M ) ( D ` j ) )
12 11 eqeq1d 
 |-  ( c = D -> ( sum_ j e. ( 0 ... M ) ( c ` j ) = I <-> sum_ j e. ( 0 ... M ) ( D ` j ) = I ) )
13 12 elrab 
 |-  ( D e. { c e. ( ( 0 ... I ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = I } <-> ( D e. ( ( 0 ... I ) ^m ( 0 ... M ) ) /\ sum_ j e. ( 0 ... M ) ( D ` j ) = I ) )
14 9 13 sylib 
 |-  ( ph -> ( D e. ( ( 0 ... I ) ^m ( 0 ... M ) ) /\ sum_ j e. ( 0 ... M ) ( D ` j ) = I ) )
15 14 simprd 
 |-  ( ph -> sum_ j e. ( 0 ... M ) ( D ` j ) = I )
16 15 ad2antrr 
 |-  ( ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) /\ -. E. k e. ( 1 ... M ) ( D ` k ) e. NN ) -> sum_ j e. ( 0 ... M ) ( D ` j ) = I )
17 ralnex 
 |-  ( A. k e. ( 1 ... M ) -. ( D ` k ) e. NN <-> -. E. k e. ( 1 ... M ) ( D ` k ) e. NN )
18 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
19 2 18 eleqtrdi 
 |-  ( ph -> M e. ( ZZ>= ` 0 ) )
20 19 ad2antrr 
 |-  ( ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) -> M e. ( ZZ>= ` 0 ) )
21 fzsscn 
 |-  ( 0 ... I ) C_ CC
22 ssrab2 
 |-  { c e. ( ( 0 ... I ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = I } C_ ( ( 0 ... I ) ^m ( 0 ... M ) )
23 8 22 eqsstrdi 
 |-  ( ph -> ( C ` I ) C_ ( ( 0 ... I ) ^m ( 0 ... M ) ) )
24 23 7 sseldd 
 |-  ( ph -> D e. ( ( 0 ... I ) ^m ( 0 ... M ) ) )
25 elmapi 
 |-  ( D e. ( ( 0 ... I ) ^m ( 0 ... M ) ) -> D : ( 0 ... M ) --> ( 0 ... I ) )
26 24 25 syl 
 |-  ( ph -> D : ( 0 ... M ) --> ( 0 ... I ) )
27 26 ffvelrnda 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( D ` j ) e. ( 0 ... I ) )
28 21 27 sseldi 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( D ` j ) e. CC )
29 28 ad4ant14 
 |-  ( ( ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) /\ j e. ( 0 ... M ) ) -> ( D ` j ) e. CC )
30 fveq2 
 |-  ( j = 0 -> ( D ` j ) = ( D ` 0 ) )
31 20 29 30 fsum1p 
 |-  ( ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) -> sum_ j e. ( 0 ... M ) ( D ` j ) = ( ( D ` 0 ) + sum_ j e. ( ( 0 + 1 ) ... M ) ( D ` j ) ) )
32 simplr 
 |-  ( ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) -> ( D ` 0 ) = ( P - 1 ) )
33 0p1e1 
 |-  ( 0 + 1 ) = 1
34 33 oveq1i 
 |-  ( ( 0 + 1 ) ... M ) = ( 1 ... M )
35 34 sumeq1i 
 |-  sum_ j e. ( ( 0 + 1 ) ... M ) ( D ` j ) = sum_ j e. ( 1 ... M ) ( D ` j )
36 35 a1i 
 |-  ( ( ph /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) -> sum_ j e. ( ( 0 + 1 ) ... M ) ( D ` j ) = sum_ j e. ( 1 ... M ) ( D ` j ) )
37 fveq2 
 |-  ( k = j -> ( D ` k ) = ( D ` j ) )
38 37 eleq1d 
 |-  ( k = j -> ( ( D ` k ) e. NN <-> ( D ` j ) e. NN ) )
39 38 notbid 
 |-  ( k = j -> ( -. ( D ` k ) e. NN <-> -. ( D ` j ) e. NN ) )
40 39 rspccva 
 |-  ( ( A. k e. ( 1 ... M ) -. ( D ` k ) e. NN /\ j e. ( 1 ... M ) ) -> -. ( D ` j ) e. NN )
41 40 adantll 
 |-  ( ( ( ph /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) /\ j e. ( 1 ... M ) ) -> -. ( D ` j ) e. NN )
42 fzssnn0 
 |-  ( 0 ... I ) C_ NN0
43 fz1ssfz0 
 |-  ( 1 ... M ) C_ ( 0 ... M )
44 43 sseli 
 |-  ( j e. ( 1 ... M ) -> j e. ( 0 ... M ) )
45 44 27 sylan2 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( D ` j ) e. ( 0 ... I ) )
46 42 45 sseldi 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( D ` j ) e. NN0 )
47 elnn0 
 |-  ( ( D ` j ) e. NN0 <-> ( ( D ` j ) e. NN \/ ( D ` j ) = 0 ) )
48 46 47 sylib 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( D ` j ) e. NN \/ ( D ` j ) = 0 ) )
49 48 adantlr 
 |-  ( ( ( ph /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) /\ j e. ( 1 ... M ) ) -> ( ( D ` j ) e. NN \/ ( D ` j ) = 0 ) )
50 orel1 
 |-  ( -. ( D ` j ) e. NN -> ( ( ( D ` j ) e. NN \/ ( D ` j ) = 0 ) -> ( D ` j ) = 0 ) )
51 41 49 50 sylc 
 |-  ( ( ( ph /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) /\ j e. ( 1 ... M ) ) -> ( D ` j ) = 0 )
52 51 sumeq2dv 
 |-  ( ( ph /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) -> sum_ j e. ( 1 ... M ) ( D ` j ) = sum_ j e. ( 1 ... M ) 0 )
53 fzfi 
 |-  ( 1 ... M ) e. Fin
54 53 olci 
 |-  ( ( 1 ... M ) C_ ( ZZ>= ` A ) \/ ( 1 ... M ) e. Fin )
55 sumz 
 |-  ( ( ( 1 ... M ) C_ ( ZZ>= ` A ) \/ ( 1 ... M ) e. Fin ) -> sum_ j e. ( 1 ... M ) 0 = 0 )
56 54 55 mp1i 
 |-  ( ( ph /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) -> sum_ j e. ( 1 ... M ) 0 = 0 )
57 36 52 56 3eqtrd 
 |-  ( ( ph /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) -> sum_ j e. ( ( 0 + 1 ) ... M ) ( D ` j ) = 0 )
58 57 adantlr 
 |-  ( ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) -> sum_ j e. ( ( 0 + 1 ) ... M ) ( D ` j ) = 0 )
59 32 58 oveq12d 
 |-  ( ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) -> ( ( D ` 0 ) + sum_ j e. ( ( 0 + 1 ) ... M ) ( D ` j ) ) = ( ( P - 1 ) + 0 ) )
60 nnm1nn0 
 |-  ( P e. NN -> ( P - 1 ) e. NN0 )
61 1 60 syl 
 |-  ( ph -> ( P - 1 ) e. NN0 )
62 61 nn0red 
 |-  ( ph -> ( P - 1 ) e. RR )
63 62 recnd 
 |-  ( ph -> ( P - 1 ) e. CC )
64 63 addid1d 
 |-  ( ph -> ( ( P - 1 ) + 0 ) = ( P - 1 ) )
65 64 ad2antrr 
 |-  ( ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) -> ( ( P - 1 ) + 0 ) = ( P - 1 ) )
66 31 59 65 3eqtrd 
 |-  ( ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) -> sum_ j e. ( 0 ... M ) ( D ` j ) = ( P - 1 ) )
67 4 necomd 
 |-  ( ph -> ( P - 1 ) =/= I )
68 67 ad2antrr 
 |-  ( ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) -> ( P - 1 ) =/= I )
69 66 68 eqnetrd 
 |-  ( ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) -> sum_ j e. ( 0 ... M ) ( D ` j ) =/= I )
70 69 neneqd 
 |-  ( ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) -> -. sum_ j e. ( 0 ... M ) ( D ` j ) = I )
71 17 70 sylan2br 
 |-  ( ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) /\ -. E. k e. ( 1 ... M ) ( D ` k ) e. NN ) -> -. sum_ j e. ( 0 ... M ) ( D ` j ) = I )
72 16 71 condan 
 |-  ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> E. k e. ( 1 ... M ) ( D ` k ) e. NN )
73 1 nnzd 
 |-  ( ph -> P e. ZZ )
74 15 eqcomd 
 |-  ( ph -> I = sum_ j e. ( 0 ... M ) ( D ` j ) )
75 74 fveq2d 
 |-  ( ph -> ( ! ` I ) = ( ! ` sum_ j e. ( 0 ... M ) ( D ` j ) ) )
76 75 oveq1d 
 |-  ( ph -> ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) = ( ( ! ` sum_ j e. ( 0 ... M ) ( D ` j ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) )
77 nfcv 
 |-  F/_ j D
78 fzfid 
 |-  ( ph -> ( 0 ... M ) e. Fin )
79 nn0ex 
 |-  NN0 e. _V
80 mapss 
 |-  ( ( NN0 e. _V /\ ( 0 ... I ) C_ NN0 ) -> ( ( 0 ... I ) ^m ( 0 ... M ) ) C_ ( NN0 ^m ( 0 ... M ) ) )
81 79 42 80 mp2an 
 |-  ( ( 0 ... I ) ^m ( 0 ... M ) ) C_ ( NN0 ^m ( 0 ... M ) )
82 81 24 sseldi 
 |-  ( ph -> D e. ( NN0 ^m ( 0 ... M ) ) )
83 77 78 82 mccl 
 |-  ( ph -> ( ( ! ` sum_ j e. ( 0 ... M ) ( D ` j ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) e. NN )
84 76 83 eqeltrd 
 |-  ( ph -> ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) e. NN )
85 84 nnzd 
 |-  ( ph -> ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) e. ZZ )
86 fzfid 
 |-  ( ph -> ( 1 ... M ) e. Fin )
87 1 adantr 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> P e. NN )
88 26 adantr 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> D : ( 0 ... M ) --> ( 0 ... I ) )
89 44 adantl 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> j e. ( 0 ... M ) )
90 0zd 
 |-  ( ph -> 0 e. ZZ )
91 5 90 eqeltrd 
 |-  ( ph -> J e. ZZ )
92 91 adantr 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> J e. ZZ )
93 87 88 89 92 etransclem3 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) e. ZZ )
94 86 93 fprodzcl 
 |-  ( ph -> prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) e. ZZ )
95 73 85 94 3jca 
 |-  ( ph -> ( P e. ZZ /\ ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) e. ZZ /\ prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) e. ZZ ) )
96 95 3ad2ant1 
 |-  ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) -> ( P e. ZZ /\ ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) e. ZZ /\ prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) e. ZZ ) )
97 73 adantr 
 |-  ( ( ph /\ k e. ( 1 ... M ) ) -> P e. ZZ )
98 1 adantr 
 |-  ( ( ph /\ k e. ( 1 ... M ) ) -> P e. NN )
99 26 adantr 
 |-  ( ( ph /\ k e. ( 1 ... M ) ) -> D : ( 0 ... M ) --> ( 0 ... I ) )
100 43 sseli 
 |-  ( k e. ( 1 ... M ) -> k e. ( 0 ... M ) )
101 100 adantl 
 |-  ( ( ph /\ k e. ( 1 ... M ) ) -> k e. ( 0 ... M ) )
102 91 adantr 
 |-  ( ( ph /\ k e. ( 1 ... M ) ) -> J e. ZZ )
103 98 99 101 102 etransclem3 
 |-  ( ( ph /\ k e. ( 1 ... M ) ) -> if ( P < ( D ` k ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) ) e. ZZ )
104 difss 
 |-  ( ( 1 ... M ) \ { k } ) C_ ( 1 ... M )
105 ssfi 
 |-  ( ( ( 1 ... M ) e. Fin /\ ( ( 1 ... M ) \ { k } ) C_ ( 1 ... M ) ) -> ( ( 1 ... M ) \ { k } ) e. Fin )
106 53 104 105 mp2an 
 |-  ( ( 1 ... M ) \ { k } ) e. Fin
107 106 a1i 
 |-  ( ph -> ( ( 1 ... M ) \ { k } ) e. Fin )
108 1 adantr 
 |-  ( ( ph /\ j e. ( ( 1 ... M ) \ { k } ) ) -> P e. NN )
109 26 adantr 
 |-  ( ( ph /\ j e. ( ( 1 ... M ) \ { k } ) ) -> D : ( 0 ... M ) --> ( 0 ... I ) )
110 104 43 sstri 
 |-  ( ( 1 ... M ) \ { k } ) C_ ( 0 ... M )
111 110 sseli 
 |-  ( j e. ( ( 1 ... M ) \ { k } ) -> j e. ( 0 ... M ) )
112 111 adantl 
 |-  ( ( ph /\ j e. ( ( 1 ... M ) \ { k } ) ) -> j e. ( 0 ... M ) )
113 91 adantr 
 |-  ( ( ph /\ j e. ( ( 1 ... M ) \ { k } ) ) -> J e. ZZ )
114 108 109 112 113 etransclem3 
 |-  ( ( ph /\ j e. ( ( 1 ... M ) \ { k } ) ) -> if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) e. ZZ )
115 107 114 fprodzcl 
 |-  ( ph -> prod_ j e. ( ( 1 ... M ) \ { k } ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) e. ZZ )
116 115 adantr 
 |-  ( ( ph /\ k e. ( 1 ... M ) ) -> prod_ j e. ( ( 1 ... M ) \ { k } ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) e. ZZ )
117 97 103 116 3jca 
 |-  ( ( ph /\ k e. ( 1 ... M ) ) -> ( P e. ZZ /\ if ( P < ( D ` k ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) ) e. ZZ /\ prod_ j e. ( ( 1 ... M ) \ { k } ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) e. ZZ ) )
118 117 3adant3 
 |-  ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) -> ( P e. ZZ /\ if ( P < ( D ` k ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) ) e. ZZ /\ prod_ j e. ( ( 1 ... M ) \ { k } ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) e. ZZ ) )
119 dvds0 
 |-  ( P e. ZZ -> P || 0 )
120 73 119 syl 
 |-  ( ph -> P || 0 )
121 120 adantr 
 |-  ( ( ph /\ P < ( D ` k ) ) -> P || 0 )
122 121 3ad2antl1 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ P < ( D ` k ) ) -> P || 0 )
123 iftrue 
 |-  ( P < ( D ` k ) -> if ( P < ( D ` k ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) ) = 0 )
124 123 eqcomd 
 |-  ( P < ( D ` k ) -> 0 = if ( P < ( D ` k ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) ) )
125 124 adantl 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ P < ( D ` k ) ) -> 0 = if ( P < ( D ` k ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) ) )
126 122 125 breqtrd 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ P < ( D ` k ) ) -> P || if ( P < ( D ` k ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) ) )
127 97 adantr 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> P e. ZZ )
128 0zd 
 |-  ( ( ph /\ k e. ( 1 ... M ) ) -> 0 e. ZZ )
129 99 101 ffvelrnd 
 |-  ( ( ph /\ k e. ( 1 ... M ) ) -> ( D ` k ) e. ( 0 ... I ) )
130 129 elfzelzd 
 |-  ( ( ph /\ k e. ( 1 ... M ) ) -> ( D ` k ) e. ZZ )
131 97 130 zsubcld 
 |-  ( ( ph /\ k e. ( 1 ... M ) ) -> ( P - ( D ` k ) ) e. ZZ )
132 128 97 131 3jca 
 |-  ( ( ph /\ k e. ( 1 ... M ) ) -> ( 0 e. ZZ /\ P e. ZZ /\ ( P - ( D ` k ) ) e. ZZ ) )
133 132 adantr 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( 0 e. ZZ /\ P e. ZZ /\ ( P - ( D ` k ) ) e. ZZ ) )
134 fzssre 
 |-  ( 0 ... I ) C_ RR
135 134 129 sseldi 
 |-  ( ( ph /\ k e. ( 1 ... M ) ) -> ( D ` k ) e. RR )
136 135 adantr 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( D ` k ) e. RR )
137 127 zred 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> P e. RR )
138 simpr 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> -. P < ( D ` k ) )
139 136 137 138 nltled 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( D ` k ) <_ P )
140 137 136 subge0d 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( 0 <_ ( P - ( D ` k ) ) <-> ( D ` k ) <_ P ) )
141 139 140 mpbird 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> 0 <_ ( P - ( D ` k ) ) )
142 elfzle1 
 |-  ( ( D ` k ) e. ( 0 ... I ) -> 0 <_ ( D ` k ) )
143 129 142 syl 
 |-  ( ( ph /\ k e. ( 1 ... M ) ) -> 0 <_ ( D ` k ) )
144 143 adantr 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> 0 <_ ( D ` k ) )
145 137 136 subge02d 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( 0 <_ ( D ` k ) <-> ( P - ( D ` k ) ) <_ P ) )
146 144 145 mpbid 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( P - ( D ` k ) ) <_ P )
147 133 141 146 jca32 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( ( 0 e. ZZ /\ P e. ZZ /\ ( P - ( D ` k ) ) e. ZZ ) /\ ( 0 <_ ( P - ( D ` k ) ) /\ ( P - ( D ` k ) ) <_ P ) ) )
148 elfz2 
 |-  ( ( P - ( D ` k ) ) e. ( 0 ... P ) <-> ( ( 0 e. ZZ /\ P e. ZZ /\ ( P - ( D ` k ) ) e. ZZ ) /\ ( 0 <_ ( P - ( D ` k ) ) /\ ( P - ( D ` k ) ) <_ P ) ) )
149 147 148 sylibr 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( P - ( D ` k ) ) e. ( 0 ... P ) )
150 permnn 
 |-  ( ( P - ( D ` k ) ) e. ( 0 ... P ) -> ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) e. NN )
151 149 150 syl 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) e. NN )
152 151 nnzd 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) e. ZZ )
153 101 elfzelzd 
 |-  ( ( ph /\ k e. ( 1 ... M ) ) -> k e. ZZ )
154 102 153 zsubcld 
 |-  ( ( ph /\ k e. ( 1 ... M ) ) -> ( J - k ) e. ZZ )
155 154 adantr 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( J - k ) e. ZZ )
156 131 adantr 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( P - ( D ` k ) ) e. ZZ )
157 elnn0z 
 |-  ( ( P - ( D ` k ) ) e. NN0 <-> ( ( P - ( D ` k ) ) e. ZZ /\ 0 <_ ( P - ( D ` k ) ) ) )
158 156 141 157 sylanbrc 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( P - ( D ` k ) ) e. NN0 )
159 zexpcl 
 |-  ( ( ( J - k ) e. ZZ /\ ( P - ( D ` k ) ) e. NN0 ) -> ( ( J - k ) ^ ( P - ( D ` k ) ) ) e. ZZ )
160 155 158 159 syl2anc 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( ( J - k ) ^ ( P - ( D ` k ) ) ) e. ZZ )
161 127 152 160 3jca 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( P e. ZZ /\ ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) e. ZZ /\ ( ( J - k ) ^ ( P - ( D ` k ) ) ) e. ZZ ) )
162 161 3adantl3 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ -. P < ( D ` k ) ) -> ( P e. ZZ /\ ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) e. ZZ /\ ( ( J - k ) ^ ( P - ( D ` k ) ) ) e. ZZ ) )
163 127 3adantl3 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ -. P < ( D ` k ) ) -> P e. ZZ )
164 61 nn0zd 
 |-  ( ph -> ( P - 1 ) e. ZZ )
165 164 adantr 
 |-  ( ( ph /\ k e. ( 1 ... M ) ) -> ( P - 1 ) e. ZZ )
166 128 165 131 3jca 
 |-  ( ( ph /\ k e. ( 1 ... M ) ) -> ( 0 e. ZZ /\ ( P - 1 ) e. ZZ /\ ( P - ( D ` k ) ) e. ZZ ) )
167 166 3adant3 
 |-  ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) -> ( 0 e. ZZ /\ ( P - 1 ) e. ZZ /\ ( P - ( D ` k ) ) e. ZZ ) )
168 167 adantr 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ -. P < ( D ` k ) ) -> ( 0 e. ZZ /\ ( P - 1 ) e. ZZ /\ ( P - ( D ` k ) ) e. ZZ ) )
169 141 3adantl3 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ -. P < ( D ` k ) ) -> 0 <_ ( P - ( D ` k ) ) )
170 1red 
 |-  ( ( ph /\ ( D ` k ) e. NN ) -> 1 e. RR )
171 nnre 
 |-  ( ( D ` k ) e. NN -> ( D ` k ) e. RR )
172 171 adantl 
 |-  ( ( ph /\ ( D ` k ) e. NN ) -> ( D ` k ) e. RR )
173 1 nnred 
 |-  ( ph -> P e. RR )
174 173 adantr 
 |-  ( ( ph /\ ( D ` k ) e. NN ) -> P e. RR )
175 nnge1 
 |-  ( ( D ` k ) e. NN -> 1 <_ ( D ` k ) )
176 175 adantl 
 |-  ( ( ph /\ ( D ` k ) e. NN ) -> 1 <_ ( D ` k ) )
177 170 172 174 176 lesub2dd 
 |-  ( ( ph /\ ( D ` k ) e. NN ) -> ( P - ( D ` k ) ) <_ ( P - 1 ) )
178 177 3adant2 
 |-  ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) -> ( P - ( D ` k ) ) <_ ( P - 1 ) )
179 178 adantr 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ -. P < ( D ` k ) ) -> ( P - ( D ` k ) ) <_ ( P - 1 ) )
180 168 169 179 jca32 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ -. P < ( D ` k ) ) -> ( ( 0 e. ZZ /\ ( P - 1 ) e. ZZ /\ ( P - ( D ` k ) ) e. ZZ ) /\ ( 0 <_ ( P - ( D ` k ) ) /\ ( P - ( D ` k ) ) <_ ( P - 1 ) ) ) )
181 elfz2 
 |-  ( ( P - ( D ` k ) ) e. ( 0 ... ( P - 1 ) ) <-> ( ( 0 e. ZZ /\ ( P - 1 ) e. ZZ /\ ( P - ( D ` k ) ) e. ZZ ) /\ ( 0 <_ ( P - ( D ` k ) ) /\ ( P - ( D ` k ) ) <_ ( P - 1 ) ) ) )
182 180 181 sylibr 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ -. P < ( D ` k ) ) -> ( P - ( D ` k ) ) e. ( 0 ... ( P - 1 ) ) )
183 permnn 
 |-  ( ( P - ( D ` k ) ) e. ( 0 ... ( P - 1 ) ) -> ( ( ! ` ( P - 1 ) ) / ( ! ` ( P - ( D ` k ) ) ) ) e. NN )
184 182 183 syl 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ -. P < ( D ` k ) ) -> ( ( ! ` ( P - 1 ) ) / ( ! ` ( P - ( D ` k ) ) ) ) e. NN )
185 184 nnzd 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ -. P < ( D ` k ) ) -> ( ( ! ` ( P - 1 ) ) / ( ! ` ( P - ( D ` k ) ) ) ) e. ZZ )
186 dvdsmul1 
 |-  ( ( P e. ZZ /\ ( ( ! ` ( P - 1 ) ) / ( ! ` ( P - ( D ` k ) ) ) ) e. ZZ ) -> P || ( P x. ( ( ! ` ( P - 1 ) ) / ( ! ` ( P - ( D ` k ) ) ) ) ) )
187 163 185 186 syl2anc 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ -. P < ( D ` k ) ) -> P || ( P x. ( ( ! ` ( P - 1 ) ) / ( ! ` ( P - ( D ` k ) ) ) ) ) )
188 1 nncnd 
 |-  ( ph -> P e. CC )
189 1cnd 
 |-  ( ph -> 1 e. CC )
190 188 189 npcand 
 |-  ( ph -> ( ( P - 1 ) + 1 ) = P )
191 190 eqcomd 
 |-  ( ph -> P = ( ( P - 1 ) + 1 ) )
192 191 fveq2d 
 |-  ( ph -> ( ! ` P ) = ( ! ` ( ( P - 1 ) + 1 ) ) )
193 facp1 
 |-  ( ( P - 1 ) e. NN0 -> ( ! ` ( ( P - 1 ) + 1 ) ) = ( ( ! ` ( P - 1 ) ) x. ( ( P - 1 ) + 1 ) ) )
194 61 193 syl 
 |-  ( ph -> ( ! ` ( ( P - 1 ) + 1 ) ) = ( ( ! ` ( P - 1 ) ) x. ( ( P - 1 ) + 1 ) ) )
195 190 oveq2d 
 |-  ( ph -> ( ( ! ` ( P - 1 ) ) x. ( ( P - 1 ) + 1 ) ) = ( ( ! ` ( P - 1 ) ) x. P ) )
196 61 faccld 
 |-  ( ph -> ( ! ` ( P - 1 ) ) e. NN )
197 196 nncnd 
 |-  ( ph -> ( ! ` ( P - 1 ) ) e. CC )
198 197 188 mulcomd 
 |-  ( ph -> ( ( ! ` ( P - 1 ) ) x. P ) = ( P x. ( ! ` ( P - 1 ) ) ) )
199 195 198 eqtrd 
 |-  ( ph -> ( ( ! ` ( P - 1 ) ) x. ( ( P - 1 ) + 1 ) ) = ( P x. ( ! ` ( P - 1 ) ) ) )
200 192 194 199 3eqtrd 
 |-  ( ph -> ( ! ` P ) = ( P x. ( ! ` ( P - 1 ) ) ) )
201 200 oveq1d 
 |-  ( ph -> ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) = ( ( P x. ( ! ` ( P - 1 ) ) ) / ( ! ` ( P - ( D ` k ) ) ) ) )
202 201 adantr 
 |-  ( ( ph /\ -. P < ( D ` k ) ) -> ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) = ( ( P x. ( ! ` ( P - 1 ) ) ) / ( ! ` ( P - ( D ` k ) ) ) ) )
203 202 3ad2antl1 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ -. P < ( D ` k ) ) -> ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) = ( ( P x. ( ! ` ( P - 1 ) ) ) / ( ! ` ( P - ( D ` k ) ) ) ) )
204 188 ad2antrr 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> P e. CC )
205 197 ad2antrr 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( ! ` ( P - 1 ) ) e. CC )
206 158 faccld 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( ! ` ( P - ( D ` k ) ) ) e. NN )
207 206 nncnd 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( ! ` ( P - ( D ` k ) ) ) e. CC )
208 206 nnne0d 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( ! ` ( P - ( D ` k ) ) ) =/= 0 )
209 204 205 207 208 divassd 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( ( P x. ( ! ` ( P - 1 ) ) ) / ( ! ` ( P - ( D ` k ) ) ) ) = ( P x. ( ( ! ` ( P - 1 ) ) / ( ! ` ( P - ( D ` k ) ) ) ) ) )
210 209 3adantl3 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ -. P < ( D ` k ) ) -> ( ( P x. ( ! ` ( P - 1 ) ) ) / ( ! ` ( P - ( D ` k ) ) ) ) = ( P x. ( ( ! ` ( P - 1 ) ) / ( ! ` ( P - ( D ` k ) ) ) ) ) )
211 203 210 eqtr2d 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ -. P < ( D ` k ) ) -> ( P x. ( ( ! ` ( P - 1 ) ) / ( ! ` ( P - ( D ` k ) ) ) ) ) = ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) )
212 187 211 breqtrd 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ -. P < ( D ` k ) ) -> P || ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) )
213 dvdsmultr1 
 |-  ( ( P e. ZZ /\ ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) e. ZZ /\ ( ( J - k ) ^ ( P - ( D ` k ) ) ) e. ZZ ) -> ( P || ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) -> P || ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) ) )
214 162 212 213 sylc 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ -. P < ( D ` k ) ) -> P || ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) )
215 iffalse 
 |-  ( -. P < ( D ` k ) -> if ( P < ( D ` k ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) ) = ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) )
216 215 adantl 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ -. P < ( D ` k ) ) -> if ( P < ( D ` k ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) ) = ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) )
217 214 216 breqtrrd 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ -. P < ( D ` k ) ) -> P || if ( P < ( D ` k ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) ) )
218 126 217 pm2.61dan 
 |-  ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) -> P || if ( P < ( D ` k ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) ) )
219 dvdsmultr1 
 |-  ( ( P e. ZZ /\ if ( P < ( D ` k ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) ) e. ZZ /\ prod_ j e. ( ( 1 ... M ) \ { k } ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) e. ZZ ) -> ( P || if ( P < ( D ` k ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) ) -> P || ( if ( P < ( D ` k ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) ) x. prod_ j e. ( ( 1 ... M ) \ { k } ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) ) )
220 118 218 219 sylc 
 |-  ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) -> P || ( if ( P < ( D ` k ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) ) x. prod_ j e. ( ( 1 ... M ) \ { k } ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) )
221 fzfid 
 |-  ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) -> ( 1 ... M ) e. Fin )
222 93 zcnd 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) e. CC )
223 222 3ad2antl1 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ j e. ( 1 ... M ) ) -> if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) e. CC )
224 simp2 
 |-  ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) -> k e. ( 1 ... M ) )
225 fveq2 
 |-  ( j = k -> ( D ` j ) = ( D ` k ) )
226 225 breq2d 
 |-  ( j = k -> ( P < ( D ` j ) <-> P < ( D ` k ) ) )
227 225 oveq2d 
 |-  ( j = k -> ( P - ( D ` j ) ) = ( P - ( D ` k ) ) )
228 227 fveq2d 
 |-  ( j = k -> ( ! ` ( P - ( D ` j ) ) ) = ( ! ` ( P - ( D ` k ) ) ) )
229 228 oveq2d 
 |-  ( j = k -> ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) = ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) )
230 oveq2 
 |-  ( j = k -> ( J - j ) = ( J - k ) )
231 230 227 oveq12d 
 |-  ( j = k -> ( ( J - j ) ^ ( P - ( D ` j ) ) ) = ( ( J - k ) ^ ( P - ( D ` k ) ) ) )
232 229 231 oveq12d 
 |-  ( j = k -> ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) = ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) )
233 226 232 ifbieq2d 
 |-  ( j = k -> if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) = if ( P < ( D ` k ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) ) )
234 233 adantl 
 |-  ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ j = k ) -> if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) = if ( P < ( D ` k ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) ) )
235 221 223 224 234 fprodsplit1 
 |-  ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) -> prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) = ( if ( P < ( D ` k ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) ) x. prod_ j e. ( ( 1 ... M ) \ { k } ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) )
236 220 235 breqtrrd 
 |-  ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) -> P || prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) )
237 dvdsmultr2 
 |-  ( ( P e. ZZ /\ ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) e. ZZ /\ prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) e. ZZ ) -> ( P || prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) -> P || ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) ) )
238 96 236 237 sylc 
 |-  ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) -> P || ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) )
239 238 3adant1r 
 |-  ( ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) -> P || ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) )
240 simpr 
 |-  ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( D ` 0 ) = ( P - 1 ) )
241 eluzfz1 
 |-  ( M e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... M ) )
242 19 241 syl 
 |-  ( ph -> 0 e. ( 0 ... M ) )
243 26 242 ffvelrnd 
 |-  ( ph -> ( D ` 0 ) e. ( 0 ... I ) )
244 134 243 sseldi 
 |-  ( ph -> ( D ` 0 ) e. RR )
245 244 adantr 
 |-  ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( D ` 0 ) e. RR )
246 62 adantr 
 |-  ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( P - 1 ) e. RR )
247 245 246 lttri3d 
 |-  ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( ( D ` 0 ) = ( P - 1 ) <-> ( -. ( D ` 0 ) < ( P - 1 ) /\ -. ( P - 1 ) < ( D ` 0 ) ) ) )
248 240 247 mpbid 
 |-  ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( -. ( D ` 0 ) < ( P - 1 ) /\ -. ( P - 1 ) < ( D ` 0 ) ) )
249 248 simprd 
 |-  ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> -. ( P - 1 ) < ( D ` 0 ) )
250 249 iffalsed 
 |-  ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) = ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) )
251 oveq2 
 |-  ( ( D ` 0 ) = ( P - 1 ) -> ( ( P - 1 ) - ( D ` 0 ) ) = ( ( P - 1 ) - ( P - 1 ) ) )
252 63 subidd 
 |-  ( ph -> ( ( P - 1 ) - ( P - 1 ) ) = 0 )
253 251 252 sylan9eqr 
 |-  ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( ( P - 1 ) - ( D ` 0 ) ) = 0 )
254 253 fveq2d 
 |-  ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) = ( ! ` 0 ) )
255 fac0 
 |-  ( ! ` 0 ) = 1
256 254 255 eqtrdi 
 |-  ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) = 1 )
257 256 oveq2d 
 |-  ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) = ( ( ! ` ( P - 1 ) ) / 1 ) )
258 197 div1d 
 |-  ( ph -> ( ( ! ` ( P - 1 ) ) / 1 ) = ( ! ` ( P - 1 ) ) )
259 258 adantr 
 |-  ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( ( ! ` ( P - 1 ) ) / 1 ) = ( ! ` ( P - 1 ) ) )
260 257 259 eqtrd 
 |-  ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) = ( ! ` ( P - 1 ) ) )
261 253 oveq2d 
 |-  ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) = ( J ^ 0 ) )
262 91 zcnd 
 |-  ( ph -> J e. CC )
263 262 exp0d 
 |-  ( ph -> ( J ^ 0 ) = 1 )
264 263 adantr 
 |-  ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( J ^ 0 ) = 1 )
265 261 264 eqtrd 
 |-  ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) = 1 )
266 260 265 oveq12d 
 |-  ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) = ( ( ! ` ( P - 1 ) ) x. 1 ) )
267 197 mulid1d 
 |-  ( ph -> ( ( ! ` ( P - 1 ) ) x. 1 ) = ( ! ` ( P - 1 ) ) )
268 267 adantr 
 |-  ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( ( ! ` ( P - 1 ) ) x. 1 ) = ( ! ` ( P - 1 ) ) )
269 250 266 268 3eqtrd 
 |-  ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) = ( ! ` ( P - 1 ) ) )
270 269 oveq1d 
 |-  ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) = ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) )
271 270 oveq2d 
 |-  ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. ( if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) ) = ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) ) )
272 271 oveq1d 
 |-  ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. ( if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) ) / ( ! ` ( P - 1 ) ) ) = ( ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) ) / ( ! ` ( P - 1 ) ) ) )
273 84 nncnd 
 |-  ( ph -> ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) e. CC )
274 94 zcnd 
 |-  ( ph -> prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) e. CC )
275 197 274 mulcld 
 |-  ( ph -> ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) e. CC )
276 196 nnne0d 
 |-  ( ph -> ( ! ` ( P - 1 ) ) =/= 0 )
277 273 275 197 276 divassd 
 |-  ( ph -> ( ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) ) / ( ! ` ( P - 1 ) ) ) = ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. ( ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) / ( ! ` ( P - 1 ) ) ) ) )
278 277 adantr 
 |-  ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) ) / ( ! ` ( P - 1 ) ) ) = ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. ( ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) / ( ! ` ( P - 1 ) ) ) ) )
279 274 197 276 divcan3d 
 |-  ( ph -> ( ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) / ( ! ` ( P - 1 ) ) ) = prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) )
280 279 oveq2d 
 |-  ( ph -> ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. ( ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) / ( ! ` ( P - 1 ) ) ) ) = ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) )
281 280 adantr 
 |-  ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. ( ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) / ( ! ` ( P - 1 ) ) ) ) = ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) )
282 272 278 281 3eqtrd 
 |-  ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. ( if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) ) / ( ! ` ( P - 1 ) ) ) = ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) )
283 282 3ad2ant1 
 |-  ( ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) -> ( ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. ( if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) ) / ( ! ` ( P - 1 ) ) ) = ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) )
284 239 283 breqtrrd 
 |-  ( ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) -> P || ( ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. ( if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) ) / ( ! ` ( P - 1 ) ) ) )
285 284 rexlimdv3a 
 |-  ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( E. k e. ( 1 ... M ) ( D ` k ) e. NN -> P || ( ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. ( if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) ) / ( ! ` ( P - 1 ) ) ) ) )
286 72 285 mpd 
 |-  ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> P || ( ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. ( if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) ) / ( ! ` ( P - 1 ) ) ) )
287 120 adantr 
 |-  ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) -> P || 0 )
288 simpr 
 |-  ( ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) /\ ( P - 1 ) < ( D ` 0 ) ) -> ( P - 1 ) < ( D ` 0 ) )
289 288 iftrued 
 |-  ( ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) /\ ( P - 1 ) < ( D ` 0 ) ) -> if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) = 0 )
290 simpr 
 |-  ( ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) /\ -. ( P - 1 ) < ( D ` 0 ) ) -> -. ( P - 1 ) < ( D ` 0 ) )
291 290 iffalsed 
 |-  ( ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) /\ -. ( P - 1 ) < ( D ` 0 ) ) -> if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) = ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) )
292 simpll 
 |-  ( ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) /\ -. ( P - 1 ) < ( D ` 0 ) ) -> ph )
293 244 ad2antrr 
 |-  ( ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) /\ -. ( P - 1 ) < ( D ` 0 ) ) -> ( D ` 0 ) e. RR )
294 62 ad2antrr 
 |-  ( ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) /\ -. ( P - 1 ) < ( D ` 0 ) ) -> ( P - 1 ) e. RR )
295 293 294 290 nltled 
 |-  ( ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) /\ -. ( P - 1 ) < ( D ` 0 ) ) -> ( D ` 0 ) <_ ( P - 1 ) )
296 id 
 |-  ( ( D ` 0 ) =/= ( P - 1 ) -> ( D ` 0 ) =/= ( P - 1 ) )
297 296 necomd 
 |-  ( ( D ` 0 ) =/= ( P - 1 ) -> ( P - 1 ) =/= ( D ` 0 ) )
298 297 ad2antlr 
 |-  ( ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) /\ -. ( P - 1 ) < ( D ` 0 ) ) -> ( P - 1 ) =/= ( D ` 0 ) )
299 293 294 295 298 leneltd 
 |-  ( ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) /\ -. ( P - 1 ) < ( D ` 0 ) ) -> ( D ` 0 ) < ( P - 1 ) )
300 5 oveq1d 
 |-  ( ph -> ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) = ( 0 ^ ( ( P - 1 ) - ( D ` 0 ) ) ) )
301 300 adantr 
 |-  ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) = ( 0 ^ ( ( P - 1 ) - ( D ` 0 ) ) ) )
302 243 elfzelzd 
 |-  ( ph -> ( D ` 0 ) e. ZZ )
303 164 302 zsubcld 
 |-  ( ph -> ( ( P - 1 ) - ( D ` 0 ) ) e. ZZ )
304 303 adantr 
 |-  ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> ( ( P - 1 ) - ( D ` 0 ) ) e. ZZ )
305 simpr 
 |-  ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> ( D ` 0 ) < ( P - 1 ) )
306 244 adantr 
 |-  ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> ( D ` 0 ) e. RR )
307 62 adantr 
 |-  ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> ( P - 1 ) e. RR )
308 306 307 posdifd 
 |-  ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> ( ( D ` 0 ) < ( P - 1 ) <-> 0 < ( ( P - 1 ) - ( D ` 0 ) ) ) )
309 305 308 mpbid 
 |-  ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> 0 < ( ( P - 1 ) - ( D ` 0 ) ) )
310 elnnz 
 |-  ( ( ( P - 1 ) - ( D ` 0 ) ) e. NN <-> ( ( ( P - 1 ) - ( D ` 0 ) ) e. ZZ /\ 0 < ( ( P - 1 ) - ( D ` 0 ) ) ) )
311 304 309 310 sylanbrc 
 |-  ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> ( ( P - 1 ) - ( D ` 0 ) ) e. NN )
312 311 0expd 
 |-  ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> ( 0 ^ ( ( P - 1 ) - ( D ` 0 ) ) ) = 0 )
313 301 312 eqtrd 
 |-  ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) = 0 )
314 313 oveq2d 
 |-  ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) = ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. 0 ) )
315 197 adantr 
 |-  ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> ( ! ` ( P - 1 ) ) e. CC )
316 311 nnnn0d 
 |-  ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> ( ( P - 1 ) - ( D ` 0 ) ) e. NN0 )
317 316 faccld 
 |-  ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) e. NN )
318 317 nncnd 
 |-  ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) e. CC )
319 317 nnne0d 
 |-  ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) =/= 0 )
320 315 318 319 divcld 
 |-  ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) e. CC )
321 320 mul01d 
 |-  ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. 0 ) = 0 )
322 314 321 eqtrd 
 |-  ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) = 0 )
323 292 299 322 syl2anc 
 |-  ( ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) /\ -. ( P - 1 ) < ( D ` 0 ) ) -> ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) = 0 )
324 291 323 eqtrd 
 |-  ( ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) /\ -. ( P - 1 ) < ( D ` 0 ) ) -> if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) = 0 )
325 289 324 pm2.61dan 
 |-  ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) -> if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) = 0 )
326 325 oveq1d 
 |-  ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) -> ( if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) = ( 0 x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) )
327 274 mul02d 
 |-  ( ph -> ( 0 x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) = 0 )
328 327 adantr 
 |-  ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) -> ( 0 x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) = 0 )
329 326 328 eqtrd 
 |-  ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) -> ( if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) = 0 )
330 329 oveq2d 
 |-  ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) -> ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. ( if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) ) = ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. 0 ) )
331 273 mul01d 
 |-  ( ph -> ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. 0 ) = 0 )
332 331 adantr 
 |-  ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) -> ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. 0 ) = 0 )
333 330 332 eqtrd 
 |-  ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) -> ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. ( if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) ) = 0 )
334 333 oveq1d 
 |-  ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) -> ( ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. ( if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) ) / ( ! ` ( P - 1 ) ) ) = ( 0 / ( ! ` ( P - 1 ) ) ) )
335 197 276 div0d 
 |-  ( ph -> ( 0 / ( ! ` ( P - 1 ) ) ) = 0 )
336 335 adantr 
 |-  ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) -> ( 0 / ( ! ` ( P - 1 ) ) ) = 0 )
337 334 336 eqtrd 
 |-  ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) -> ( ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. ( if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) ) / ( ! ` ( P - 1 ) ) ) = 0 )
338 287 337 breqtrrd 
 |-  ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) -> P || ( ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. ( if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) ) / ( ! ` ( P - 1 ) ) ) )
339 286 338 pm2.61dane 
 |-  ( ph -> P || ( ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. ( if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) ) / ( ! ` ( P - 1 ) ) ) )