Metamath Proof Explorer

Theorem etransclem21

Description: The N -th derivative of H applied to Y . (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem21.s 
|- ( ph -> S e. { RR , CC } )
etransclem21.x 
|- ( ph -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
etransclem21.p 
|- ( ph -> P e. NN )
etransclem21.h 
|- H = ( j e. ( 0 ... M ) |-> ( x e. X |-> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) )
etransclem21.j 
|- ( ph -> J e. ( 0 ... M ) )
etransclem21.n 
|- ( ph -> N e. NN0 )
etransclem21.y 
|- ( ph -> Y e. X )
Assertion etransclem21 
|- ( ph -> ( ( ( S Dn ( H ` J ) ) ` N ) ` Y ) = if ( if ( J = 0 , ( P - 1 ) , P ) < N , 0 , ( ( ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) x. ( ( Y - J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) ) )

Proof

Step Hyp Ref Expression
1 etransclem21.s 
 |-  ( ph -> S e. { RR , CC } )
2 etransclem21.x 
 |-  ( ph -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
3 etransclem21.p 
 |-  ( ph -> P e. NN )
4 etransclem21.h 
 |-  H = ( j e. ( 0 ... M ) |-> ( x e. X |-> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) )
5 etransclem21.j 
 |-  ( ph -> J e. ( 0 ... M ) )
6 etransclem21.n 
 |-  ( ph -> N e. NN0 )
7 etransclem21.y 
 |-  ( ph -> Y e. X )
8 1 2 3 4 5 6 etransclem17 
 |-  ( ph -> ( ( S Dn ( H ` J ) ) ` N ) = ( x e. X |-> if ( if ( J = 0 , ( P - 1 ) , P ) < N , 0 , ( ( ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) x. ( ( x - J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) ) ) )
9 oveq1 
 |-  ( x = Y -> ( x - J ) = ( Y - J ) )
10 9 oveq1d 
 |-  ( x = Y -> ( ( x - J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) = ( ( Y - J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) )
11 10 oveq2d 
 |-  ( x = Y -> ( ( ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) x. ( ( x - J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) = ( ( ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) x. ( ( Y - J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) )
12 11 ifeq2d 
 |-  ( x = Y -> if ( if ( J = 0 , ( P - 1 ) , P ) < N , 0 , ( ( ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) x. ( ( x - J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) ) = if ( if ( J = 0 , ( P - 1 ) , P ) < N , 0 , ( ( ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) x. ( ( Y - J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) ) )
13 12 adantl 
 |-  ( ( ph /\ x = Y ) -> if ( if ( J = 0 , ( P - 1 ) , P ) < N , 0 , ( ( ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) x. ( ( x - J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) ) = if ( if ( J = 0 , ( P - 1 ) , P ) < N , 0 , ( ( ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) x. ( ( Y - J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) ) )
14 0cnd 
 |-  ( ( ph /\ if ( J = 0 , ( P - 1 ) , P ) < N ) -> 0 e. CC )
15 nnm1nn0 
 |-  ( P e. NN -> ( P - 1 ) e. NN0 )
16 3 15 syl 
 |-  ( ph -> ( P - 1 ) e. NN0 )
17 3 nnnn0d 
 |-  ( ph -> P e. NN0 )
18 16 17 ifcld 
 |-  ( ph -> if ( J = 0 , ( P - 1 ) , P ) e. NN0 )
19 18 faccld 
 |-  ( ph -> ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) e. NN )
20 19 nncnd 
 |-  ( ph -> ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) e. CC )
21 20 adantr 
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) e. CC )
22 18 nn0zd 
 |-  ( ph -> if ( J = 0 , ( P - 1 ) , P ) e. ZZ )
23 6 nn0zd 
 |-  ( ph -> N e. ZZ )
24 22 23 zsubcld 
 |-  ( ph -> ( if ( J = 0 , ( P - 1 ) , P ) - N ) e. ZZ )
25 24 adantr 
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( if ( J = 0 , ( P - 1 ) , P ) - N ) e. ZZ )
26 6 nn0red 
 |-  ( ph -> N e. RR )
27 26 adantr 
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> N e. RR )
28 18 nn0red 
 |-  ( ph -> if ( J = 0 , ( P - 1 ) , P ) e. RR )
29 28 adantr 
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> if ( J = 0 , ( P - 1 ) , P ) e. RR )
30 simpr 
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> -. if ( J = 0 , ( P - 1 ) , P ) < N )
31 27 29 30 nltled 
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> N <_ if ( J = 0 , ( P - 1 ) , P ) )
32 29 27 subge0d 
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( 0 <_ ( if ( J = 0 , ( P - 1 ) , P ) - N ) <-> N <_ if ( J = 0 , ( P - 1 ) , P ) ) )
33 31 32 mpbird 
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> 0 <_ ( if ( J = 0 , ( P - 1 ) , P ) - N ) )
34 elnn0z 
 |-  ( ( if ( J = 0 , ( P - 1 ) , P ) - N ) e. NN0 <-> ( ( if ( J = 0 , ( P - 1 ) , P ) - N ) e. ZZ /\ 0 <_ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) )
35 25 33 34 sylanbrc 
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( if ( J = 0 , ( P - 1 ) , P ) - N ) e. NN0 )
36 35 faccld 
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) e. NN )
37 36 nncnd 
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) e. CC )
38 36 nnne0d 
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) =/= 0 )
39 21 37 38 divcld 
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) e. CC )
40 1 2 dvdmsscn 
 |-  ( ph -> X C_ CC )
41 40 7 sseldd 
 |-  ( ph -> Y e. CC )
42 5 elfzelzd 
 |-  ( ph -> J e. ZZ )
43 42 zcnd 
 |-  ( ph -> J e. CC )
44 41 43 subcld 
 |-  ( ph -> ( Y - J ) e. CC )
45 44 adantr 
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( Y - J ) e. CC )
46 45 35 expcld 
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( ( Y - J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) e. CC )
47 39 46 mulcld 
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( ( ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) x. ( ( Y - J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) e. CC )
48 14 47 ifclda 
 |-  ( ph -> if ( if ( J = 0 , ( P - 1 ) , P ) < N , 0 , ( ( ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) x. ( ( Y - J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) ) e. CC )
49 8 13 7 48 fvmptd 
 |-  ( ph -> ( ( ( S Dn ( H ` J ) ) ` N ) ` Y ) = if ( if ( J = 0 , ( P - 1 ) , P ) < N , 0 , ( ( ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) x. ( ( Y - J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) ) )