Metamath Proof Explorer

Theorem etransclem36

Description: The N -th derivative of F applied to J is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020)

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

Proof

Step Hyp Ref Expression
1 etransclem36.s 
 |-  ( ph -> S e. { RR , CC } )
2 etransclem36.x 
 |-  ( ph -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
3 etransclem36.p 
 |-  ( ph -> P e. NN )
4 etransclem36.m 
 |-  ( ph -> M e. NN0 )
5 etransclem36.f 
 |-  F = ( x e. X |-> ( ( x ^ ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( ( x - j ) ^ P ) ) )
6 etransclem36.n 
 |-  ( ph -> N e. NN0 )
7 etransclem36.h 
 |-  H = ( j e. ( 0 ... M ) |-> ( x e. X |-> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) )
8 etransclem36.jx 
 |-  ( ph -> J e. X )
9 etransclem36.jz 
 |-  ( ph -> J e. ZZ )
10 etransclem36.10 
 |-  C = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = n } )
11 1 2 3 4 5 6 7 10 8 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 ) ) ) ) ) ) ) )
12 10 6 etransclem16 
 |-  ( ph -> ( C ` N ) e. Fin )
13 3 adantr 
 |-  ( ( ph /\ c e. ( C ` N ) ) -> P e. NN )
14 4 adantr 
 |-  ( ( ph /\ c e. ( C ` N ) ) -> M e. NN0 )
15 6 adantr 
 |-  ( ( ph /\ c e. ( C ` N ) ) -> N e. NN0 )
16 9 adantr 
 |-  ( ( ph /\ c e. ( C ` N ) ) -> J e. ZZ )
17 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 } )
18 etransclem11 
 |-  ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) = ( n e. NN0 |-> { e e. ( ( 0 ... n ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( e ` j ) = n } )
19 10 17 18 3eqtri 
 |-  C = ( n e. NN0 |-> { e e. ( ( 0 ... n ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( e ` j ) = n } )
20 simpr 
 |-  ( ( ph /\ c e. ( C ` N ) ) -> c e. ( C ` N ) )
21 13 14 15 16 19 20 etransclem26 
 |-  ( ( 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 )
22 12 21 fsumzcl 
 |-  ( ph -> 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 ) ) ) ) ) ) ) e. ZZ )
23 11 22 eqeltrd 
 |-  ( ph -> ( ( ( S Dn F ) ` N ) ` J ) e. ZZ )