Metamath Proof Explorer

Theorem etransclem26

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

Ref Expression
Hypotheses etransclem26.p 
|- ( ph -> P e. NN )
etransclem26.m 
|- ( ph -> M e. NN0 )
etransclem26.n 
|- ( ph -> N e. NN0 )
etransclem26.jz 
|- ( ph -> J e. ZZ )
etransclem26.c 
|- C = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = n } )
etransclem26.d 
|- ( ph -> D e. ( C ` N ) )
Assertion etransclem26 
|- ( ph -> ( ( ( ! ` N ) / 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 ) ) ) ) ) ) ) e. ZZ )

Proof

Step Hyp Ref Expression
1 etransclem26.p 
 |-  ( ph -> P e. NN )
2 etransclem26.m 
 |-  ( ph -> M e. NN0 )
3 etransclem26.n 
 |-  ( ph -> N e. NN0 )
4 etransclem26.jz 
 |-  ( ph -> J e. ZZ )
5 etransclem26.c 
 |-  C = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = n } )
6 etransclem26.d 
 |-  ( ph -> D e. ( C ` N ) )
7 5 3 etransclem12 
 |-  ( ph -> ( C ` N ) = { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } )
8 6 7 eleqtrd 
 |-  ( ph -> D e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } )
9 fveq1 
 |-  ( c = D -> ( c ` j ) = ( D ` j ) )
10 9 sumeq2sdv 
 |-  ( c = D -> sum_ j e. ( 0 ... M ) ( c ` j ) = sum_ j e. ( 0 ... M ) ( D ` j ) )
11 10 eqeq1d 
 |-  ( c = D -> ( sum_ j e. ( 0 ... M ) ( c ` j ) = N <-> sum_ j e. ( 0 ... M ) ( D ` j ) = N ) )
12 11 elrab 
 |-  ( D e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } <-> ( D e. ( ( 0 ... N ) ^m ( 0 ... M ) ) /\ sum_ j e. ( 0 ... M ) ( D ` j ) = N ) )
13 8 12 sylib 
 |-  ( ph -> ( D e. ( ( 0 ... N ) ^m ( 0 ... M ) ) /\ sum_ j e. ( 0 ... M ) ( D ` j ) = N ) )
14 13 simprd 
 |-  ( ph -> sum_ j e. ( 0 ... M ) ( D ` j ) = N )
15 14 eqcomd 
 |-  ( ph -> N = sum_ j e. ( 0 ... M ) ( D ` j ) )
16 15 fveq2d 
 |-  ( ph -> ( ! ` N ) = ( ! ` sum_ j e. ( 0 ... M ) ( D ` j ) ) )
17 16 oveq1d 
 |-  ( ph -> ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) = ( ( ! ` sum_ j e. ( 0 ... M ) ( D ` j ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) )
18 nfcv 
 |-  F/_ j D
19 fzfid 
 |-  ( ph -> ( 0 ... M ) e. Fin )
20 nn0ex 
 |-  NN0 e. _V
21 fzssnn0 
 |-  ( 0 ... N ) C_ NN0
22 mapss 
 |-  ( ( NN0 e. _V /\ ( 0 ... N ) C_ NN0 ) -> ( ( 0 ... N ) ^m ( 0 ... M ) ) C_ ( NN0 ^m ( 0 ... M ) ) )
23 20 21 22 mp2an 
 |-  ( ( 0 ... N ) ^m ( 0 ... M ) ) C_ ( NN0 ^m ( 0 ... M ) )
24 13 simpld 
 |-  ( ph -> D e. ( ( 0 ... N ) ^m ( 0 ... M ) ) )
25 23 24 sseldi 
 |-  ( ph -> D e. ( NN0 ^m ( 0 ... M ) ) )
26 18 19 25 mccl 
 |-  ( ph -> ( ( ! ` sum_ j e. ( 0 ... M ) ( D ` j ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) e. NN )
27 17 26 eqeltrd 
 |-  ( ph -> ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) e. NN )
28 27 nnzd 
 |-  ( ph -> ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) e. ZZ )
29 elmapi 
 |-  ( D e. ( ( 0 ... N ) ^m ( 0 ... M ) ) -> D : ( 0 ... M ) --> ( 0 ... N ) )
30 24 29 syl 
 |-  ( ph -> D : ( 0 ... M ) --> ( 0 ... N ) )
31 1 2 30 4 etransclem10 
 |-  ( ph -> if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) e. ZZ )
32 fzfid 
 |-  ( ph -> ( 1 ... M ) e. Fin )
33 1 adantr 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> P e. NN )
34 30 adantr 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> D : ( 0 ... M ) --> ( 0 ... N ) )
35 0z 
 |-  0 e. ZZ
36 fzp1ss 
 |-  ( 0 e. ZZ -> ( ( 0 + 1 ) ... M ) C_ ( 0 ... M ) )
37 35 36 ax-mp 
 |-  ( ( 0 + 1 ) ... M ) C_ ( 0 ... M )
38 1e0p1 
 |-  1 = ( 0 + 1 )
39 38 oveq1i 
 |-  ( 1 ... M ) = ( ( 0 + 1 ) ... M )
40 39 eleq2i 
 |-  ( j e. ( 1 ... M ) <-> j e. ( ( 0 + 1 ) ... M ) )
41 40 biimpi 
 |-  ( j e. ( 1 ... M ) -> j e. ( ( 0 + 1 ) ... M ) )
42 37 41 sseldi 
 |-  ( j e. ( 1 ... M ) -> j e. ( 0 ... M ) )
43 42 adantl 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> j e. ( 0 ... M ) )
44 4 adantr 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> J e. ZZ )
45 33 34 43 44 etransclem3 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) e. ZZ )
46 32 45 fprodzcl 
 |-  ( ph -> prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) e. ZZ )
47 31 46 zmulcld 
 |-  ( ph -> ( 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 ) ) ) ) ) ) e. ZZ )
48 28 47 zmulcld 
 |-  ( ph -> ( ( ( ! ` N ) / 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 ) ) ) ) ) ) ) e. ZZ )