Metamath Proof Explorer

Theorem etransclem22

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

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

Proof

Step Hyp Ref Expression
1 etransclem22.s 
 |-  ( ph -> S e. { RR , CC } )
2 etransclem22.x 
 |-  ( ph -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
3 etransclem22.p 
 |-  ( ph -> P e. NN )
4 etransclem22.h 
 |-  H = ( j e. ( 0 ... M ) |-> ( x e. X |-> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) )
5 etransclem22.J 
 |-  ( ph -> J e. ( 0 ... M ) )
6 etransclem22.n 
 |-  ( ph -> N e. NN0 )
7 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 ) ) ) ) ) )
8 simpr 
 |-  ( ( ph /\ if ( J = 0 , ( P - 1 ) , P ) < N ) -> if ( J = 0 , ( P - 1 ) , P ) < N )
9 8 iftrued 
 |-  ( ( ph /\ 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 ) ) ) ) = 0 )
10 9 mpteq2dv 
 |-  ( ( ph /\ 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 ) ) ) ) ) = ( x e. X |-> 0 ) )
11 1 2 dvdmsscn 
 |-  ( ph -> X C_ CC )
12 0cnd 
 |-  ( ph -> 0 e. CC )
13 ssid 
 |-  CC C_ CC
14 13 a1i 
 |-  ( ph -> CC C_ CC )
15 11 12 14 constcncfg 
 |-  ( ph -> ( x e. X |-> 0 ) e. ( X -cn-> CC ) )
16 15 adantr 
 |-  ( ( ph /\ if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( x e. X |-> 0 ) e. ( X -cn-> CC ) )
17 10 16 eqeltrd 
 |-  ( ( ph /\ 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 ) ) ) ) ) e. ( X -cn-> CC ) )
18 simpr 
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> -. if ( J = 0 , ( P - 1 ) , P ) < N )
19 18 iffalsed 
 |-  ( ( ph /\ -. 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 ) ) ) ) = ( ( ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) x. ( ( x - J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) )
20 19 mpteq2dv 
 |-  ( ( ph /\ -. 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 ) ) ) ) ) = ( x e. X |-> ( ( ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) x. ( ( x - J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) ) )
21 nfv 
 |-  F/ x ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N )
22 11 14 idcncfg 
 |-  ( ph -> ( x e. X |-> x ) e. ( X -cn-> CC ) )
23 5 elfzelzd 
 |-  ( ph -> J e. ZZ )
24 23 zcnd 
 |-  ( ph -> J e. CC )
25 11 24 14 constcncfg 
 |-  ( ph -> ( x e. X |-> J ) e. ( X -cn-> CC ) )
26 22 25 subcncf 
 |-  ( ph -> ( x e. X |-> ( x - J ) ) e. ( X -cn-> CC ) )
27 26 adantr 
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( x e. X |-> ( x - J ) ) e. ( X -cn-> CC ) )
28 13 a1i 
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> CC C_ CC )
29 nnm1nn0 
 |-  ( P e. NN -> ( P - 1 ) e. NN0 )
30 3 29 syl 
 |-  ( ph -> ( P - 1 ) e. NN0 )
31 3 nnnn0d 
 |-  ( ph -> P e. NN0 )
32 30 31 ifcld 
 |-  ( ph -> if ( J = 0 , ( P - 1 ) , P ) e. NN0 )
33 32 faccld 
 |-  ( ph -> ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) e. NN )
34 33 nncnd 
 |-  ( ph -> ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) e. CC )
35 34 adantr 
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) e. CC )
36 32 nn0zd 
 |-  ( ph -> if ( J = 0 , ( P - 1 ) , P ) e. ZZ )
37 6 nn0zd 
 |-  ( ph -> N e. ZZ )
38 36 37 zsubcld 
 |-  ( ph -> ( if ( J = 0 , ( P - 1 ) , P ) - N ) e. ZZ )
39 38 adantr 
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( if ( J = 0 , ( P - 1 ) , P ) - N ) e. ZZ )
40 6 nn0red 
 |-  ( ph -> N e. RR )
41 40 adantr 
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> N e. RR )
42 32 nn0red 
 |-  ( ph -> if ( J = 0 , ( P - 1 ) , P ) e. RR )
43 42 adantr 
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> if ( J = 0 , ( P - 1 ) , P ) e. RR )
44 41 43 18 nltled 
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> N <_ if ( J = 0 , ( P - 1 ) , P ) )
45 43 41 subge0d 
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( 0 <_ ( if ( J = 0 , ( P - 1 ) , P ) - N ) <-> N <_ if ( J = 0 , ( P - 1 ) , P ) ) )
46 44 45 mpbird 
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> 0 <_ ( if ( J = 0 , ( P - 1 ) , P ) - N ) )
47 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 ) ) )
48 39 46 47 sylanbrc 
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( if ( J = 0 , ( P - 1 ) , P ) - N ) e. NN0 )
49 48 faccld 
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) e. NN )
50 49 nncnd 
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) e. CC )
51 49 nnne0d 
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) =/= 0 )
52 35 50 51 divcld 
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) e. CC )
53 28 52 28 constcncfg 
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( y e. CC |-> ( ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) ) e. ( CC -cn-> CC ) )
54 expcncf 
 |-  ( ( if ( J = 0 , ( P - 1 ) , P ) - N ) e. NN0 -> ( y e. CC |-> ( y ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) e. ( CC -cn-> CC ) )
55 48 54 syl 
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( y e. CC |-> ( y ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) e. ( CC -cn-> CC ) )
56 53 55 mulcncf 
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( y e. CC |-> ( ( ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) x. ( y ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) ) e. ( CC -cn-> CC ) )
57 oveq1 
 |-  ( y = ( x - J ) -> ( y ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) = ( ( x - J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) )
58 57 oveq2d 
 |-  ( y = ( x - J ) -> ( ( ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) x. ( y ^ ( 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 ) ) ) )
59 21 27 56 28 58 cncfcompt2 
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( x e. X |-> ( ( ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) x. ( ( x - J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) ) e. ( X -cn-> CC ) )
60 20 59 eqeltrd 
 |-  ( ( ph /\ -. 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 ) ) ) ) ) e. ( X -cn-> CC ) )
61 17 60 pm2.61dan 
 |-  ( 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 - J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) ) ) e. ( X -cn-> CC ) )
62 7 61 eqeltrd 
 |-  ( ph -> ( ( S Dn ( H ` J ) ) ` N ) e. ( X -cn-> CC ) )