Metamath Proof Explorer

Theorem etransclem27

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

Ref Expression
Hypotheses etransclem27.s 
|- ( ph -> S e. { RR , CC } )
etransclem27.x 
|- ( ph -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
etransclem27.p 
|- ( ph -> P e. NN )
etransclem27.h 
|- H = ( j e. ( 0 ... M ) |-> ( x e. X |-> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) )
etransclem27.cfi 
|- ( ph -> C e. Fin )
etransclem27.cf 
|- ( ph -> C : dom C --> ( NN0 ^m ( 0 ... M ) ) )
etransclem27.g 
|- G = ( x e. X |-> sum_ l e. dom C prod_ j e. ( 0 ... M ) ( ( ( S Dn ( H ` j ) ) ` ( ( C ` l ) ` j ) ) ` x ) )
etransclem27.jx 
|- ( ph -> J e. X )
etransclem27.jz 
|- ( ph -> J e. ZZ )
Assertion etransclem27 
|- ( ph -> ( G ` J ) e. ZZ )

Proof

Step Hyp Ref Expression
1 etransclem27.s 
 |-  ( ph -> S e. { RR , CC } )
2 etransclem27.x 
 |-  ( ph -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
3 etransclem27.p 
 |-  ( ph -> P e. NN )
4 etransclem27.h 
 |-  H = ( j e. ( 0 ... M ) |-> ( x e. X |-> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) )
5 etransclem27.cfi 
 |-  ( ph -> C e. Fin )
6 etransclem27.cf 
 |-  ( ph -> C : dom C --> ( NN0 ^m ( 0 ... M ) ) )
7 etransclem27.g 
 |-  G = ( x e. X |-> sum_ l e. dom C prod_ j e. ( 0 ... M ) ( ( ( S Dn ( H ` j ) ) ` ( ( C ` l ) ` j ) ) ` x ) )
8 etransclem27.jx 
 |-  ( ph -> J e. X )
9 etransclem27.jz 
 |-  ( ph -> J e. ZZ )
10 fveq2 
 |-  ( x = J -> ( ( ( S Dn ( H ` j ) ) ` ( ( C ` l ) ` j ) ) ` x ) = ( ( ( S Dn ( H ` j ) ) ` ( ( C ` l ) ` j ) ) ` J ) )
11 10 prodeq2ad 
 |-  ( x = J -> prod_ j e. ( 0 ... M ) ( ( ( S Dn ( H ` j ) ) ` ( ( C ` l ) ` j ) ) ` x ) = prod_ j e. ( 0 ... M ) ( ( ( S Dn ( H ` j ) ) ` ( ( C ` l ) ` j ) ) ` J ) )
12 11 sumeq2sdv 
 |-  ( x = J -> sum_ l e. dom C prod_ j e. ( 0 ... M ) ( ( ( S Dn ( H ` j ) ) ` ( ( C ` l ) ` j ) ) ` x ) = sum_ l e. dom C prod_ j e. ( 0 ... M ) ( ( ( S Dn ( H ` j ) ) ` ( ( C ` l ) ` j ) ) ` J ) )
13 dmfi 
 |-  ( C e. Fin -> dom C e. Fin )
14 5 13 syl 
 |-  ( ph -> dom C e. Fin )
15 fzfid 
 |-  ( ( ph /\ l e. dom C ) -> ( 0 ... M ) e. Fin )
16 1 ad2antrr 
 |-  ( ( ( ph /\ l e. dom C ) /\ j e. ( 0 ... M ) ) -> S e. { RR , CC } )
17 2 ad2antrr 
 |-  ( ( ( ph /\ l e. dom C ) /\ j e. ( 0 ... M ) ) -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
18 3 ad2antrr 
 |-  ( ( ( ph /\ l e. dom C ) /\ j e. ( 0 ... M ) ) -> P e. NN )
19 etransclem5 
 |-  ( j e. ( 0 ... M ) |-> ( x e. X |-> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) ) = ( z e. ( 0 ... M ) |-> ( y e. X |-> ( ( y - z ) ^ if ( z = 0 , ( P - 1 ) , P ) ) ) )
20 4 19 eqtri 
 |-  H = ( z e. ( 0 ... M ) |-> ( y e. X |-> ( ( y - z ) ^ if ( z = 0 , ( P - 1 ) , P ) ) ) )
21 simpr 
 |-  ( ( ( ph /\ l e. dom C ) /\ j e. ( 0 ... M ) ) -> j e. ( 0 ... M ) )
22 6 ffvelrnda 
 |-  ( ( ph /\ l e. dom C ) -> ( C ` l ) e. ( NN0 ^m ( 0 ... M ) ) )
23 elmapi 
 |-  ( ( C ` l ) e. ( NN0 ^m ( 0 ... M ) ) -> ( C ` l ) : ( 0 ... M ) --> NN0 )
24 22 23 syl 
 |-  ( ( ph /\ l e. dom C ) -> ( C ` l ) : ( 0 ... M ) --> NN0 )
25 24 ffvelrnda 
 |-  ( ( ( ph /\ l e. dom C ) /\ j e. ( 0 ... M ) ) -> ( ( C ` l ) ` j ) e. NN0 )
26 16 17 18 20 21 25 etransclem20 
 |-  ( ( ( ph /\ l e. dom C ) /\ j e. ( 0 ... M ) ) -> ( ( S Dn ( H ` j ) ) ` ( ( C ` l ) ` j ) ) : X --> CC )
27 8 ad2antrr 
 |-  ( ( ( ph /\ l e. dom C ) /\ j e. ( 0 ... M ) ) -> J e. X )
28 26 27 ffvelrnd 
 |-  ( ( ( ph /\ l e. dom C ) /\ j e. ( 0 ... M ) ) -> ( ( ( S Dn ( H ` j ) ) ` ( ( C ` l ) ` j ) ) ` J ) e. CC )
29 15 28 fprodcl 
 |-  ( ( ph /\ l e. dom C ) -> prod_ j e. ( 0 ... M ) ( ( ( S Dn ( H ` j ) ) ` ( ( C ` l ) ` j ) ) ` J ) e. CC )
30 14 29 fsumcl 
 |-  ( ph -> sum_ l e. dom C prod_ j e. ( 0 ... M ) ( ( ( S Dn ( H ` j ) ) ` ( ( C ` l ) ` j ) ) ` J ) e. CC )
31 7 12 8 30 fvmptd3 
 |-  ( ph -> ( G ` J ) = sum_ l e. dom C prod_ j e. ( 0 ... M ) ( ( ( S Dn ( H ` j ) ) ` ( ( C ` l ) ` j ) ) ` J ) )
32 16 17 18 20 21 25 27 etransclem21 
 |-  ( ( ( ph /\ l e. dom C ) /\ j e. ( 0 ... M ) ) -> ( ( ( S Dn ( H ` j ) ) ` ( ( C ` l ) ` j ) ) ` J ) = if ( if ( j = 0 , ( P - 1 ) , P ) < ( ( C ` l ) ` j ) , 0 , ( ( ( ! ` if ( j = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( j = 0 , ( P - 1 ) , P ) - ( ( C ` l ) ` j ) ) ) ) x. ( ( J - j ) ^ ( if ( j = 0 , ( P - 1 ) , P ) - ( ( C ` l ) ` j ) ) ) ) ) )
33 iftrue 
 |-  ( if ( j = 0 , ( P - 1 ) , P ) < ( ( C ` l ) ` j ) -> if ( if ( j = 0 , ( P - 1 ) , P ) < ( ( C ` l ) ` j ) , 0 , ( ( ( ! ` if ( j = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( j = 0 , ( P - 1 ) , P ) - ( ( C ` l ) ` j ) ) ) ) x. ( ( J - j ) ^ ( if ( j = 0 , ( P - 1 ) , P ) - ( ( C ` l ) ` j ) ) ) ) ) = 0 )
34 0zd 
 |-  ( if ( j = 0 , ( P - 1 ) , P ) < ( ( C ` l ) ` j ) -> 0 e. ZZ )
35 33 34 eqeltrd 
 |-  ( if ( j = 0 , ( P - 1 ) , P ) < ( ( C ` l ) ` j ) -> if ( if ( j = 0 , ( P - 1 ) , P ) < ( ( C ` l ) ` j ) , 0 , ( ( ( ! ` if ( j = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( j = 0 , ( P - 1 ) , P ) - ( ( C ` l ) ` j ) ) ) ) x. ( ( J - j ) ^ ( if ( j = 0 , ( P - 1 ) , P ) - ( ( C ` l ) ` j ) ) ) ) ) e. ZZ )
36 35 adantl 
 |-  ( ( ( ( ph /\ l e. dom C ) /\ j e. ( 0 ... M ) ) /\ if ( j = 0 , ( P - 1 ) , P ) < ( ( C ` l ) ` j ) ) -> if ( if ( j = 0 , ( P - 1 ) , P ) < ( ( C ` l ) ` j ) , 0 , ( ( ( ! ` if ( j = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( j = 0 , ( P - 1 ) , P ) - ( ( C ` l ) ` j ) ) ) ) x. ( ( J - j ) ^ ( if ( j = 0 , ( P - 1 ) , P ) - ( ( C ` l ) ` j ) ) ) ) ) e. ZZ )
37 0zd 
 |-  ( ( ( ( ph /\ l e. dom C ) /\ j e. ( 0 ... M ) ) /\ -. if ( j = 0 , ( P - 1 ) , P ) < ( ( C ` l ) ` j ) ) -> 0 e. ZZ )
38 nnm1nn0 
 |-  ( P e. NN -> ( P - 1 ) e. NN0 )
39 3 38 syl 
 |-  ( ph -> ( P - 1 ) e. NN0 )
40 3 nnnn0d 
 |-  ( ph -> P e. NN0 )
41 39 40 ifcld 
 |-  ( ph -> if ( j = 0 , ( P - 1 ) , P ) e. NN0 )
42 41 nn0zd 
 |-  ( ph -> if ( j = 0 , ( P - 1 ) , P ) e. ZZ )
43 42 ad3antrrr 
 |-  ( ( ( ( ph /\ l e. dom C ) /\ j e. ( 0 ... M ) ) /\ -. if ( j = 0 , ( P - 1 ) , P ) < ( ( C ` l ) ` j ) ) -> if ( j = 0 , ( P - 1 ) , P ) e. ZZ )
44 25 nn0zd 
 |-  ( ( ( ph /\ l e. dom C ) /\ j e. ( 0 ... M ) ) -> ( ( C ` l ) ` j ) e. ZZ )
45 44 adantr 
 |-  ( ( ( ( ph /\ l e. dom C ) /\ j e. ( 0 ... M ) ) /\ -. if ( j = 0 , ( P - 1 ) , P ) < ( ( C ` l ) ` j ) ) -> ( ( C ` l ) ` j ) e. ZZ )
46 43 45 zsubcld 
 |-  ( ( ( ( ph /\ l e. dom C ) /\ j e. ( 0 ... M ) ) /\ -. if ( j = 0 , ( P - 1 ) , P ) < ( ( C ` l ) ` j ) ) -> ( if ( j = 0 , ( P - 1 ) , P ) - ( ( C ` l ) ` j ) ) e. ZZ )
47 45 zred 
 |-  ( ( ( ( ph /\ l e. dom C ) /\ j e. ( 0 ... M ) ) /\ -. if ( j = 0 , ( P - 1 ) , P ) < ( ( C ` l ) ` j ) ) -> ( ( C ` l ) ` j ) e. RR )
48 43 zred 
 |-  ( ( ( ( ph /\ l e. dom C ) /\ j e. ( 0 ... M ) ) /\ -. if ( j = 0 , ( P - 1 ) , P ) < ( ( C ` l ) ` j ) ) -> if ( j = 0 , ( P - 1 ) , P ) e. RR )
49 simpr 
 |-  ( ( ( ( ph /\ l e. dom C ) /\ j e. ( 0 ... M ) ) /\ -. if ( j = 0 , ( P - 1 ) , P ) < ( ( C ` l ) ` j ) ) -> -. if ( j = 0 , ( P - 1 ) , P ) < ( ( C ` l ) ` j ) )
50 47 48 49 nltled 
 |-  ( ( ( ( ph /\ l e. dom C ) /\ j e. ( 0 ... M ) ) /\ -. if ( j = 0 , ( P - 1 ) , P ) < ( ( C ` l ) ` j ) ) -> ( ( C ` l ) ` j ) <_ if ( j = 0 , ( P - 1 ) , P ) )
51 48 47 subge0d 
 |-  ( ( ( ( ph /\ l e. dom C ) /\ j e. ( 0 ... M ) ) /\ -. if ( j = 0 , ( P - 1 ) , P ) < ( ( C ` l ) ` j ) ) -> ( 0 <_ ( if ( j = 0 , ( P - 1 ) , P ) - ( ( C ` l ) ` j ) ) <-> ( ( C ` l ) ` j ) <_ if ( j = 0 , ( P - 1 ) , P ) ) )
52 50 51 mpbird 
 |-  ( ( ( ( ph /\ l e. dom C ) /\ j e. ( 0 ... M ) ) /\ -. if ( j = 0 , ( P - 1 ) , P ) < ( ( C ` l ) ` j ) ) -> 0 <_ ( if ( j = 0 , ( P - 1 ) , P ) - ( ( C ` l ) ` j ) ) )
53 0red 
 |-  ( ( ( ph /\ l e. dom C ) /\ j e. ( 0 ... M ) ) -> 0 e. RR )
54 25 nn0red 
 |-  ( ( ( ph /\ l e. dom C ) /\ j e. ( 0 ... M ) ) -> ( ( C ` l ) ` j ) e. RR )
55 41 nn0red 
 |-  ( ph -> if ( j = 0 , ( P - 1 ) , P ) e. RR )
56 55 ad2antrr 
 |-  ( ( ( ph /\ l e. dom C ) /\ j e. ( 0 ... M ) ) -> if ( j = 0 , ( P - 1 ) , P ) e. RR )
57 25 nn0ge0d 
 |-  ( ( ( ph /\ l e. dom C ) /\ j e. ( 0 ... M ) ) -> 0 <_ ( ( C ` l ) ` j ) )
58 53 54 56 57 lesub2dd 
 |-  ( ( ( ph /\ l e. dom C ) /\ j e. ( 0 ... M ) ) -> ( if ( j = 0 , ( P - 1 ) , P ) - ( ( C ` l ) ` j ) ) <_ ( if ( j = 0 , ( P - 1 ) , P ) - 0 ) )
59 56 recnd 
 |-  ( ( ( ph /\ l e. dom C ) /\ j e. ( 0 ... M ) ) -> if ( j = 0 , ( P - 1 ) , P ) e. CC )
60 59 subid1d 
 |-  ( ( ( ph /\ l e. dom C ) /\ j e. ( 0 ... M ) ) -> ( if ( j = 0 , ( P - 1 ) , P ) - 0 ) = if ( j = 0 , ( P - 1 ) , P ) )
61 58 60 breqtrd 
 |-  ( ( ( ph /\ l e. dom C ) /\ j e. ( 0 ... M ) ) -> ( if ( j = 0 , ( P - 1 ) , P ) - ( ( C ` l ) ` j ) ) <_ if ( j = 0 , ( P - 1 ) , P ) )
62 61 adantr 
 |-  ( ( ( ( ph /\ l e. dom C ) /\ j e. ( 0 ... M ) ) /\ -. if ( j = 0 , ( P - 1 ) , P ) < ( ( C ` l ) ` j ) ) -> ( if ( j = 0 , ( P - 1 ) , P ) - ( ( C ` l ) ` j ) ) <_ if ( j = 0 , ( P - 1 ) , P ) )
63 37 43 46 52 62 elfzd 
 |-  ( ( ( ( ph /\ l e. dom C ) /\ j e. ( 0 ... M ) ) /\ -. if ( j = 0 , ( P - 1 ) , P ) < ( ( C ` l ) ` j ) ) -> ( if ( j = 0 , ( P - 1 ) , P ) - ( ( C ` l ) ` j ) ) e. ( 0 ... if ( j = 0 , ( P - 1 ) , P ) ) )
64 permnn 
 |-  ( ( if ( j = 0 , ( P - 1 ) , P ) - ( ( C ` l ) ` j ) ) e. ( 0 ... if ( j = 0 , ( P - 1 ) , P ) ) -> ( ( ! ` if ( j = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( j = 0 , ( P - 1 ) , P ) - ( ( C ` l ) ` j ) ) ) ) e. NN )
65 63 64 syl 
 |-  ( ( ( ( ph /\ l e. dom C ) /\ j e. ( 0 ... M ) ) /\ -. if ( j = 0 , ( P - 1 ) , P ) < ( ( C ` l ) ` j ) ) -> ( ( ! ` if ( j = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( j = 0 , ( P - 1 ) , P ) - ( ( C ` l ) ` j ) ) ) ) e. NN )
66 65 nnzd 
 |-  ( ( ( ( ph /\ l e. dom C ) /\ j e. ( 0 ... M ) ) /\ -. if ( j = 0 , ( P - 1 ) , P ) < ( ( C ` l ) ` j ) ) -> ( ( ! ` if ( j = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( j = 0 , ( P - 1 ) , P ) - ( ( C ` l ) ` j ) ) ) ) e. ZZ )
67 9 ad3antrrr 
 |-  ( ( ( ( ph /\ l e. dom C ) /\ j e. ( 0 ... M ) ) /\ -. if ( j = 0 , ( P - 1 ) , P ) < ( ( C ` l ) ` j ) ) -> J e. ZZ )
68 elfzelz 
 |-  ( j e. ( 0 ... M ) -> j e. ZZ )
69 68 ad2antlr 
 |-  ( ( ( ( ph /\ l e. dom C ) /\ j e. ( 0 ... M ) ) /\ -. if ( j = 0 , ( P - 1 ) , P ) < ( ( C ` l ) ` j ) ) -> j e. ZZ )
70 67 69 zsubcld 
 |-  ( ( ( ( ph /\ l e. dom C ) /\ j e. ( 0 ... M ) ) /\ -. if ( j = 0 , ( P - 1 ) , P ) < ( ( C ` l ) ` j ) ) -> ( J - j ) e. ZZ )
71 elnn0z 
 |-  ( ( if ( j = 0 , ( P - 1 ) , P ) - ( ( C ` l ) ` j ) ) e. NN0 <-> ( ( if ( j = 0 , ( P - 1 ) , P ) - ( ( C ` l ) ` j ) ) e. ZZ /\ 0 <_ ( if ( j = 0 , ( P - 1 ) , P ) - ( ( C ` l ) ` j ) ) ) )
72 46 52 71 sylanbrc 
 |-  ( ( ( ( ph /\ l e. dom C ) /\ j e. ( 0 ... M ) ) /\ -. if ( j = 0 , ( P - 1 ) , P ) < ( ( C ` l ) ` j ) ) -> ( if ( j = 0 , ( P - 1 ) , P ) - ( ( C ` l ) ` j ) ) e. NN0 )
73 zexpcl 
 |-  ( ( ( J - j ) e. ZZ /\ ( if ( j = 0 , ( P - 1 ) , P ) - ( ( C ` l ) ` j ) ) e. NN0 ) -> ( ( J - j ) ^ ( if ( j = 0 , ( P - 1 ) , P ) - ( ( C ` l ) ` j ) ) ) e. ZZ )
74 70 72 73 syl2anc 
 |-  ( ( ( ( ph /\ l e. dom C ) /\ j e. ( 0 ... M ) ) /\ -. if ( j = 0 , ( P - 1 ) , P ) < ( ( C ` l ) ` j ) ) -> ( ( J - j ) ^ ( if ( j = 0 , ( P - 1 ) , P ) - ( ( C ` l ) ` j ) ) ) e. ZZ )
75 66 74 zmulcld 
 |-  ( ( ( ( ph /\ l e. dom C ) /\ j e. ( 0 ... M ) ) /\ -. if ( j = 0 , ( P - 1 ) , P ) < ( ( C ` l ) ` j ) ) -> ( ( ( ! ` if ( j = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( j = 0 , ( P - 1 ) , P ) - ( ( C ` l ) ` j ) ) ) ) x. ( ( J - j ) ^ ( if ( j = 0 , ( P - 1 ) , P ) - ( ( C ` l ) ` j ) ) ) ) e. ZZ )
76 37 75 ifcld 
 |-  ( ( ( ( ph /\ l e. dom C ) /\ j e. ( 0 ... M ) ) /\ -. if ( j = 0 , ( P - 1 ) , P ) < ( ( C ` l ) ` j ) ) -> if ( if ( j = 0 , ( P - 1 ) , P ) < ( ( C ` l ) ` j ) , 0 , ( ( ( ! ` if ( j = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( j = 0 , ( P - 1 ) , P ) - ( ( C ` l ) ` j ) ) ) ) x. ( ( J - j ) ^ ( if ( j = 0 , ( P - 1 ) , P ) - ( ( C ` l ) ` j ) ) ) ) ) e. ZZ )
77 36 76 pm2.61dan 
 |-  ( ( ( ph /\ l e. dom C ) /\ j e. ( 0 ... M ) ) -> if ( if ( j = 0 , ( P - 1 ) , P ) < ( ( C ` l ) ` j ) , 0 , ( ( ( ! ` if ( j = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( j = 0 , ( P - 1 ) , P ) - ( ( C ` l ) ` j ) ) ) ) x. ( ( J - j ) ^ ( if ( j = 0 , ( P - 1 ) , P ) - ( ( C ` l ) ` j ) ) ) ) ) e. ZZ )
78 32 77 eqeltrd 
 |-  ( ( ( ph /\ l e. dom C ) /\ j e. ( 0 ... M ) ) -> ( ( ( S Dn ( H ` j ) ) ` ( ( C ` l ) ` j ) ) ` J ) e. ZZ )
79 15 78 fprodzcl 
 |-  ( ( ph /\ l e. dom C ) -> prod_ j e. ( 0 ... M ) ( ( ( S Dn ( H ` j ) ) ` ( ( C ` l ) ` j ) ) ` J ) e. ZZ )
80 14 79 fsumzcl 
 |-  ( ph -> sum_ l e. dom C prod_ j e. ( 0 ... M ) ( ( ( S Dn ( H ` j ) ) ` ( ( C ` l ) ` j ) ) ` J ) e. ZZ )
81 31 80 eqeltrd 
 |-  ( ph -> ( G ` J ) e. ZZ )