Metamath Proof Explorer

Theorem etransclem17

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

Ref Expression
Hypotheses etransclem17.s 
|- ( ph -> S e. { RR , CC } )
etransclem17.x 
|- ( ph -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
etransclem17.p 
|- ( ph -> P e. NN )
etransclem17.1 
|- H = ( j e. ( 0 ... M ) |-> ( x e. X |-> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) )
etransclem17.J 
|- ( ph -> J e. ( 0 ... M ) )
etransclem17.n 
|- ( ph -> N e. NN0 )
Assertion 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 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 etransclem17.s 
 |-  ( ph -> S e. { RR , CC } )
2 etransclem17.x 
 |-  ( ph -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
3 etransclem17.p 
 |-  ( ph -> P e. NN )
4 etransclem17.1 
 |-  H = ( j e. ( 0 ... M ) |-> ( x e. X |-> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) )
5 etransclem17.J 
 |-  ( ph -> J e. ( 0 ... M ) )
6 etransclem17.n 
 |-  ( ph -> N e. NN0 )
7 1 2 dvdmsscn 
 |-  ( ph -> X C_ CC )
8 7 sselda 
 |-  ( ( ph /\ x e. X ) -> x e. CC )
9 8 adantlr 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. X ) -> x e. CC )
10 elfzelz 
 |-  ( j e. ( 0 ... M ) -> j e. ZZ )
11 10 zcnd 
 |-  ( j e. ( 0 ... M ) -> j e. CC )
12 11 ad2antlr 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. X ) -> j e. CC )
13 9 12 negsubd 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. X ) -> ( x + -u j ) = ( x - j ) )
14 13 eqcomd 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. X ) -> ( x - j ) = ( x + -u j ) )
15 14 oveq1d 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. X ) -> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) = ( ( x + -u j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) )
16 15 mpteq2dva 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( x e. X |-> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) = ( x e. X |-> ( ( x + -u j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) )
17 16 mpteq2dva 
 |-  ( ph -> ( j e. ( 0 ... M ) |-> ( x e. X |-> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) ) = ( j e. ( 0 ... M ) |-> ( x e. X |-> ( ( x + -u j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) ) )
18 4 17 syl5eq 
 |-  ( ph -> H = ( j e. ( 0 ... M ) |-> ( x e. X |-> ( ( x + -u j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) ) )
19 negeq 
 |-  ( j = J -> -u j = -u J )
20 19 oveq2d 
 |-  ( j = J -> ( x + -u j ) = ( x + -u J ) )
21 eqeq1 
 |-  ( j = J -> ( j = 0 <-> J = 0 ) )
22 21 ifbid 
 |-  ( j = J -> if ( j = 0 , ( P - 1 ) , P ) = if ( J = 0 , ( P - 1 ) , P ) )
23 20 22 oveq12d 
 |-  ( j = J -> ( ( x + -u j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) = ( ( x + -u J ) ^ if ( J = 0 , ( P - 1 ) , P ) ) )
24 23 mpteq2dv 
 |-  ( j = J -> ( x e. X |-> ( ( x + -u j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) = ( x e. X |-> ( ( x + -u J ) ^ if ( J = 0 , ( P - 1 ) , P ) ) ) )
25 24 adantl 
 |-  ( ( ph /\ j = J ) -> ( x e. X |-> ( ( x + -u j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) = ( x e. X |-> ( ( x + -u J ) ^ if ( J = 0 , ( P - 1 ) , P ) ) ) )
26 mptexg 
 |-  ( X e. ( ( TopOpen ` CCfld ) |`t S ) -> ( x e. X |-> ( ( x + -u J ) ^ if ( J = 0 , ( P - 1 ) , P ) ) ) e. _V )
27 2 26 syl 
 |-  ( ph -> ( x e. X |-> ( ( x + -u J ) ^ if ( J = 0 , ( P - 1 ) , P ) ) ) e. _V )
28 18 25 5 27 fvmptd 
 |-  ( ph -> ( H ` J ) = ( x e. X |-> ( ( x + -u J ) ^ if ( J = 0 , ( P - 1 ) , P ) ) ) )
29 28 oveq2d 
 |-  ( ph -> ( S Dn ( H ` J ) ) = ( S Dn ( x e. X |-> ( ( x + -u J ) ^ if ( J = 0 , ( P - 1 ) , P ) ) ) ) )
30 29 fveq1d 
 |-  ( ph -> ( ( S Dn ( H ` J ) ) ` N ) = ( ( S Dn ( x e. X |-> ( ( x + -u J ) ^ if ( J = 0 , ( P - 1 ) , P ) ) ) ) ` N ) )
31 elfzelz 
 |-  ( J e. ( 0 ... M ) -> J e. ZZ )
32 31 zcnd 
 |-  ( J e. ( 0 ... M ) -> J e. CC )
33 5 32 syl 
 |-  ( ph -> J e. CC )
34 33 negcld 
 |-  ( ph -> -u J e. CC )
35 nnm1nn0 
 |-  ( P e. NN -> ( P - 1 ) e. NN0 )
36 3 35 syl 
 |-  ( ph -> ( P - 1 ) e. NN0 )
37 3 nnnn0d 
 |-  ( ph -> P e. NN0 )
38 36 37 ifcld 
 |-  ( ph -> if ( J = 0 , ( P - 1 ) , P ) e. NN0 )
39 eqid 
 |-  ( x e. X |-> ( ( x + -u J ) ^ if ( J = 0 , ( P - 1 ) , P ) ) ) = ( x e. X |-> ( ( x + -u J ) ^ if ( J = 0 , ( P - 1 ) , P ) ) )
40 1 2 34 38 39 dvnxpaek 
 |-  ( ( ph /\ N e. NN0 ) -> ( ( S Dn ( x e. X |-> ( ( x + -u J ) ^ if ( J = 0 , ( P - 1 ) , P ) ) ) ) ` 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 + -u J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) ) ) )
41 6 40 mpdan 
 |-  ( ph -> ( ( S Dn ( x e. X |-> ( ( x + -u J ) ^ if ( J = 0 , ( P - 1 ) , P ) ) ) ) ` 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 + -u J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) ) ) )
42 33 adantr 
 |-  ( ( ph /\ x e. X ) -> J e. CC )
43 8 42 negsubd 
 |-  ( ( ph /\ x e. X ) -> ( x + -u J ) = ( x - J ) )
44 43 oveq1d 
 |-  ( ( ph /\ x e. X ) -> ( ( x + -u J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) = ( ( x - J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) )
45 44 oveq2d 
 |-  ( ( ph /\ x e. X ) -> ( ( ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) x. ( ( x + -u J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) = ( ( ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) x. ( ( x - J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) )
46 45 ifeq2d 
 |-  ( ( ph /\ 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 + -u 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. ( ( x - J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) ) )
47 46 mpteq2dva 
 |-  ( ph -> ( 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 + -u J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - 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 ) ) ) ) ) )
48 30 41 47 3eqtrd 
 |-  ( 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 ) ) ) ) ) )