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 )`
` |-  ( ( ph /\ c e. ( C ` N ) ) -> P e. NN )`
` |-  ( ( ph /\ c e. ( C ` N ) ) -> M e. NN0 )`
` |-  ( ( ph /\ c e. ( C ` N ) ) -> N e. NN0 )`
` |-  ( ( 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 )`