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 ) )