Metamath Proof Explorer

Theorem etransclem37

Description: ( P - 1 ) factorial divides the N -th derivative of F applied to J . (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem37.s 
|- ( ph -> S e. { RR , CC } )
etransclem37.x 
|- ( ph -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
etransclem37.p 
|- ( ph -> P e. NN )
etransclem37.m 
|- ( ph -> M e. NN0 )
etransclem37.f 
|- F = ( x e. X |-> ( ( x ^ ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( ( x - j ) ^ P ) ) )
etransclem37.n 
|- ( ph -> N e. NN0 )
etransclem37.h 
|- H = ( j e. ( 0 ... M ) |-> ( x e. X |-> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) )
etransclem37.c 
|- C = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = n } )
etransclem37.9 
|- ( ph -> J e. ( 0 ... M ) )
etransclem37.j 
|- ( ph -> J e. X )
Assertion etransclem37 
|- ( ph -> ( ! ` ( P - 1 ) ) || ( ( ( S Dn F ) ` N ) ` J ) )

Proof

Step Hyp Ref Expression
1 etransclem37.s 
 |-  ( ph -> S e. { RR , CC } )
2 etransclem37.x 
 |-  ( ph -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
3 etransclem37.p 
 |-  ( ph -> P e. NN )
4 etransclem37.m 
 |-  ( ph -> M e. NN0 )
5 etransclem37.f 
 |-  F = ( x e. X |-> ( ( x ^ ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( ( x - j ) ^ P ) ) )
6 etransclem37.n 
 |-  ( ph -> N e. NN0 )
7 etransclem37.h 
 |-  H = ( j e. ( 0 ... M ) |-> ( x e. X |-> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) )
8 etransclem37.c 
 |-  C = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = n } )
9 etransclem37.9 
 |-  ( ph -> J e. ( 0 ... M ) )
10 etransclem37.j 
 |-  ( ph -> J e. X )
11 8 6 etransclem16 
 |-  ( ph -> ( C ` N ) e. Fin )
12 nnm1nn0 
 |-  ( P e. NN -> ( P - 1 ) e. NN0 )
13 3 12 syl 
 |-  ( ph -> ( P - 1 ) e. NN0 )
14 13 faccld 
 |-  ( ph -> ( ! ` ( P - 1 ) ) e. NN )
15 14 nnzd 
 |-  ( ph -> ( ! ` ( P - 1 ) ) e. ZZ )
16 8 6 etransclem12 
 |-  ( ph -> ( C ` N ) = { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } )
17 16 eleq2d 
 |-  ( ph -> ( c e. ( C ` N ) <-> c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) )
18 17 biimpa 
 |-  ( ( ph /\ c e. ( C ` N ) ) -> c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } )
19 rabid 
 |-  ( c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } <-> ( c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) /\ sum_ j e. ( 0 ... M ) ( c ` j ) = N ) )
20 19 biimpi 
 |-  ( c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } -> ( c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) /\ sum_ j e. ( 0 ... M ) ( c ` j ) = N ) )
21 20 simprd 
 |-  ( c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } -> sum_ j e. ( 0 ... M ) ( c ` j ) = N )
22 18 21 syl 
 |-  ( ( ph /\ c e. ( C ` N ) ) -> sum_ j e. ( 0 ... M ) ( c ` j ) = N )
23 22 eqcomd 
 |-  ( ( ph /\ c e. ( C ` N ) ) -> N = sum_ j e. ( 0 ... M ) ( c ` j ) )
24 23 fveq2d 
 |-  ( ( ph /\ c e. ( C ` N ) ) -> ( ! ` N ) = ( ! ` sum_ j e. ( 0 ... M ) ( c ` j ) ) )
25 24 oveq1d 
 |-  ( ( ph /\ c e. ( C ` N ) ) -> ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) = ( ( ! ` sum_ j e. ( 0 ... M ) ( c ` j ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) )
26 nfcv 
 |-  F/_ j c
27 fzfid 
 |-  ( ( ph /\ c e. ( C ` N ) ) -> ( 0 ... M ) e. Fin )
28 nn0ex 
 |-  NN0 e. _V
29 28 a1i 
 |-  ( c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } -> NN0 e. _V )
30 fzssnn0 
 |-  ( 0 ... N ) C_ NN0
31 mapss 
 |-  ( ( NN0 e. _V /\ ( 0 ... N ) C_ NN0 ) -> ( ( 0 ... N ) ^m ( 0 ... M ) ) C_ ( NN0 ^m ( 0 ... M ) ) )
32 29 30 31 sylancl 
 |-  ( c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } -> ( ( 0 ... N ) ^m ( 0 ... M ) ) C_ ( NN0 ^m ( 0 ... M ) ) )
33 20 simpld 
 |-  ( c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } -> c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) )
34 32 33 sseldd 
 |-  ( c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } -> c e. ( NN0 ^m ( 0 ... M ) ) )
35 18 34 syl 
 |-  ( ( ph /\ c e. ( C ` N ) ) -> c e. ( NN0 ^m ( 0 ... M ) ) )
36 26 27 35 mccl 
 |-  ( ( ph /\ c e. ( C ` N ) ) -> ( ( ! ` sum_ j e. ( 0 ... M ) ( c ` j ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) e. NN )
37 25 36 eqeltrd 
 |-  ( ( ph /\ c e. ( C ` N ) ) -> ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) e. NN )
38 37 nnzd 
 |-  ( ( ph /\ c e. ( C ` N ) ) -> ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) e. ZZ )
39 3 adantr 
 |-  ( ( ph /\ c e. ( C ` N ) ) -> P e. NN )
40 4 adantr 
 |-  ( ( ph /\ c e. ( C ` N ) ) -> M e. NN0 )
41 elmapi 
 |-  ( c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) -> c : ( 0 ... M ) --> ( 0 ... N ) )
42 18 33 41 3syl 
 |-  ( ( ph /\ c e. ( C ` N ) ) -> c : ( 0 ... M ) --> ( 0 ... N ) )
43 9 elfzelzd 
 |-  ( ph -> J e. ZZ )
44 43 adantr 
 |-  ( ( ph /\ c e. ( C ` N ) ) -> J e. ZZ )
45 39 40 42 44 etransclem10 
 |-  ( ( ph /\ c e. ( C ` N ) ) -> if ( ( P - 1 ) < ( c ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( c ` 0 ) ) ) ) ) e. ZZ )
46 fzfid 
 |-  ( ( ph /\ c e. ( C ` N ) ) -> ( 1 ... M ) e. Fin )
47 39 adantr 
 |-  ( ( ( ph /\ c e. ( C ` N ) ) /\ j e. ( 1 ... M ) ) -> P e. NN )
48 42 adantr 
 |-  ( ( ( ph /\ c e. ( C ` N ) ) /\ j e. ( 1 ... M ) ) -> c : ( 0 ... M ) --> ( 0 ... N ) )
49 0z 
 |-  0 e. ZZ
50 fzp1ss 
 |-  ( 0 e. ZZ -> ( ( 0 + 1 ) ... M ) C_ ( 0 ... M ) )
51 49 50 ax-mp 
 |-  ( ( 0 + 1 ) ... M ) C_ ( 0 ... M )
52 51 sseli 
 |-  ( j e. ( ( 0 + 1 ) ... M ) -> j e. ( 0 ... M ) )
53 1e0p1 
 |-  1 = ( 0 + 1 )
54 53 oveq1i 
 |-  ( 1 ... M ) = ( ( 0 + 1 ) ... M )
55 52 54 eleq2s 
 |-  ( j e. ( 1 ... M ) -> j e. ( 0 ... M ) )
56 55 adantl 
 |-  ( ( ( ph /\ c e. ( C ` N ) ) /\ j e. ( 1 ... M ) ) -> j e. ( 0 ... M ) )
57 44 adantr 
 |-  ( ( ( ph /\ c e. ( C ` N ) ) /\ j e. ( 1 ... M ) ) -> J e. ZZ )
58 47 48 56 57 etransclem3 
 |-  ( ( ( ph /\ c e. ( C ` N ) ) /\ j e. ( 1 ... M ) ) -> if ( P < ( c ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( c ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( c ` j ) ) ) ) ) e. ZZ )
59 46 58 fprodzcl 
 |-  ( ( ph /\ c e. ( C ` N ) ) -> prod_ j e. ( 1 ... M ) if ( P < ( c ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( c ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( c ` j ) ) ) ) ) e. ZZ )
60 45 59 zmulcld 
 |-  ( ( ph /\ c e. ( C ` N ) ) -> ( if ( ( P - 1 ) < ( c ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( c ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( c ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( c ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( c ` j ) ) ) ) ) ) e. ZZ )
61 38 60 zmulcld 
 |-  ( ( ph /\ c e. ( C ` N ) ) -> ( ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) x. ( if ( ( P - 1 ) < ( c ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( c ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( c ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( c ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( c ` j ) ) ) ) ) ) ) e. ZZ )
62 6 adantr 
 |-  ( ( ph /\ c e. ( C ` N ) ) -> N e. NN0 )
63 etransclem11 
 |-  ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = n } ) = ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } )
64 8 63 eqtri 
 |-  C = ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } )
65 simpr 
 |-  ( ( ph /\ c e. ( C ` N ) ) -> c e. ( C ` N ) )
66 9 adantr 
 |-  ( ( ph /\ c e. ( C ` N ) ) -> J e. ( 0 ... M ) )
67 fveq2 
 |-  ( j = k -> ( c ` j ) = ( c ` k ) )
68 67 fveq2d 
 |-  ( j = k -> ( ! ` ( c ` j ) ) = ( ! ` ( c ` k ) ) )
69 68 cbvprodv 
 |-  prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) = prod_ k e. ( 0 ... M ) ( ! ` ( c ` k ) )
70 69 oveq2i 
 |-  ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) = ( ( ! ` N ) / prod_ k e. ( 0 ... M ) ( ! ` ( c ` k ) ) )
71 67 breq2d 
 |-  ( j = k -> ( P < ( c ` j ) <-> P < ( c ` k ) ) )
72 67 oveq2d 
 |-  ( j = k -> ( P - ( c ` j ) ) = ( P - ( c ` k ) ) )
73 72 fveq2d 
 |-  ( j = k -> ( ! ` ( P - ( c ` j ) ) ) = ( ! ` ( P - ( c ` k ) ) ) )
74 73 oveq2d 
 |-  ( j = k -> ( ( ! ` P ) / ( ! ` ( P - ( c ` j ) ) ) ) = ( ( ! ` P ) / ( ! ` ( P - ( c ` k ) ) ) ) )
75 oveq2 
 |-  ( j = k -> ( J - j ) = ( J - k ) )
76 75 72 oveq12d 
 |-  ( j = k -> ( ( J - j ) ^ ( P - ( c ` j ) ) ) = ( ( J - k ) ^ ( P - ( c ` k ) ) ) )
77 74 76 oveq12d 
 |-  ( j = k -> ( ( ( ! ` P ) / ( ! ` ( P - ( c ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( c ` j ) ) ) ) = ( ( ( ! ` P ) / ( ! ` ( P - ( c ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( c ` k ) ) ) ) )
78 71 77 ifbieq2d 
 |-  ( j = k -> if ( P < ( c ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( c ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( c ` j ) ) ) ) ) = if ( P < ( c ` k ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( c ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( c ` k ) ) ) ) ) )
79 78 cbvprodv 
 |-  prod_ j e. ( 1 ... M ) if ( P < ( c ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( c ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( c ` j ) ) ) ) ) = prod_ k e. ( 1 ... M ) if ( P < ( c ` k ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( c ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( c ` k ) ) ) ) )
80 79 oveq2i 
 |-  ( if ( ( P - 1 ) < ( c ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( c ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( c ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( c ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( c ` j ) ) ) ) ) ) = ( if ( ( P - 1 ) < ( c ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( c ` 0 ) ) ) ) ) x. prod_ k e. ( 1 ... M ) if ( P < ( c ` k ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( c ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( c ` k ) ) ) ) ) )
81 70 80 oveq12i 
 |-  ( ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) x. ( if ( ( P - 1 ) < ( c ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( c ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( c ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( c ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( c ` j ) ) ) ) ) ) ) = ( ( ( ! ` N ) / prod_ k e. ( 0 ... M ) ( ! ` ( c ` k ) ) ) x. ( if ( ( P - 1 ) < ( c ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( c ` 0 ) ) ) ) ) x. prod_ k e. ( 1 ... M ) if ( P < ( c ` k ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( c ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( c ` k ) ) ) ) ) ) )
82 39 40 62 64 65 66 81 etransclem28 
 |-  ( ( ph /\ c e. ( C ` N ) ) -> ( ! ` ( P - 1 ) ) || ( ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) x. ( if ( ( P - 1 ) < ( c ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( c ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( c ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( c ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( c ` j ) ) ) ) ) ) ) )
83 11 15 61 82 fsumdvds 
 |-  ( ph -> ( ! ` ( P - 1 ) ) || sum_ c e. ( C ` N ) ( ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) x. ( if ( ( P - 1 ) < ( c ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( c ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( c ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( c ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( c ` j ) ) ) ) ) ) ) )
84 1 2 3 4 5 6 7 8 10 etransclem31 
 |-  ( ph -> ( ( ( S Dn F ) ` N ) ` J ) = sum_ c e. ( C ` N ) ( ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) x. ( if ( ( P - 1 ) < ( c ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( c ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( c ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( c ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( c ` j ) ) ) ) ) ) ) )
85 83 84 breqtrrd 
 |-  ( ph -> ( ! ` ( P - 1 ) ) || ( ( ( S Dn F ) ` N ) ` J ) )