Metamath Proof Explorer


Theorem etransclem20

Description: H is smooth. (Contributed by Glauco Siliprandi, 5-Apr-2020)

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

Proof

Step Hyp Ref Expression
1 etransclem20.s
 |-  ( ph -> S e. { RR , CC } )
2 etransclem20.x
 |-  ( ph -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
3 etransclem20.p
 |-  ( ph -> P e. NN )
4 etransclem20.h
 |-  H = ( j e. ( 0 ... M ) |-> ( x e. X |-> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) )
5 etransclem20.J
 |-  ( ph -> J e. ( 0 ... M ) )
6 etransclem20.n
 |-  ( ph -> N e. NN0 )
7 iftrue
 |-  ( 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 )
8 0cnd
 |-  ( if ( J = 0 , ( P - 1 ) , P ) < N -> 0 e. CC )
9 7 8 eqeltrd
 |-  ( 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 ) ) ) ) e. CC )
10 9 adantl
 |-  ( ( ( ph /\ x e. X ) /\ 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 ) ) ) ) e. CC )
11 simpr
 |-  ( ( ( ph /\ x e. X ) /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> -. if ( J = 0 , ( P - 1 ) , P ) < N )
12 11 iffalsed
 |-  ( ( ( ph /\ x e. X ) /\ -. 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 ) ) ) )
13 nnm1nn0
 |-  ( P e. NN -> ( P - 1 ) e. NN0 )
14 3 13 syl
 |-  ( ph -> ( P - 1 ) e. NN0 )
15 3 nnnn0d
 |-  ( ph -> P e. NN0 )
16 14 15 ifcld
 |-  ( ph -> if ( J = 0 , ( P - 1 ) , P ) e. NN0 )
17 16 faccld
 |-  ( ph -> ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) e. NN )
18 17 nncnd
 |-  ( ph -> ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) e. CC )
19 18 adantr
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) e. CC )
20 16 nn0zd
 |-  ( ph -> if ( J = 0 , ( P - 1 ) , P ) e. ZZ )
21 6 nn0zd
 |-  ( ph -> N e. ZZ )
22 20 21 zsubcld
 |-  ( ph -> ( if ( J = 0 , ( P - 1 ) , P ) - N ) e. ZZ )
23 22 adantr
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( if ( J = 0 , ( P - 1 ) , P ) - N ) e. ZZ )
24 6 nn0red
 |-  ( ph -> N e. RR )
25 24 adantr
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> N e. RR )
26 16 nn0red
 |-  ( ph -> if ( J = 0 , ( P - 1 ) , P ) e. RR )
27 26 adantr
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> if ( J = 0 , ( P - 1 ) , P ) e. RR )
28 simpr
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> -. if ( J = 0 , ( P - 1 ) , P ) < N )
29 25 27 28 nltled
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> N <_ if ( J = 0 , ( P - 1 ) , P ) )
30 27 25 subge0d
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( 0 <_ ( if ( J = 0 , ( P - 1 ) , P ) - N ) <-> N <_ if ( J = 0 , ( P - 1 ) , P ) ) )
31 29 30 mpbird
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> 0 <_ ( if ( J = 0 , ( P - 1 ) , P ) - N ) )
32 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 ) ) )
33 23 31 32 sylanbrc
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( if ( J = 0 , ( P - 1 ) , P ) - N ) e. NN0 )
34 33 faccld
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) e. NN )
35 34 nncnd
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) e. CC )
36 34 nnne0d
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) =/= 0 )
37 19 35 36 divcld
 |-  ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) e. CC )
38 37 adantlr
 |-  ( ( ( ph /\ x e. X ) /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) e. CC )
39 1 2 dvdmsscn
 |-  ( ph -> X C_ CC )
40 39 sselda
 |-  ( ( ph /\ x e. X ) -> x e. CC )
41 elfzelz
 |-  ( J e. ( 0 ... M ) -> J e. ZZ )
42 41 zcnd
 |-  ( J e. ( 0 ... M ) -> J e. CC )
43 5 42 syl
 |-  ( ph -> J e. CC )
44 43 adantr
 |-  ( ( ph /\ x e. X ) -> J e. CC )
45 40 44 subcld
 |-  ( ( ph /\ x e. X ) -> ( x - J ) e. CC )
46 45 adantr
 |-  ( ( ( ph /\ x e. X ) /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( x - J ) e. CC )
47 33 adantlr
 |-  ( ( ( ph /\ x e. X ) /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( if ( J = 0 , ( P - 1 ) , P ) - N ) e. NN0 )
48 46 47 expcld
 |-  ( ( ( ph /\ x e. X ) /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( ( x - J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) e. CC )
49 38 48 mulcld
 |-  ( ( ( ph /\ x e. X ) /\ -. 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 ) ) ) e. CC )
50 12 49 eqeltrd
 |-  ( ( ( ph /\ x e. X ) /\ -. 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 ) ) ) ) e. CC )
51 10 50 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. CC )
52 eqid
 |-  ( 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 ( 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 ) ) ) ) )
53 51 52 fmptd
 |-  ( 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 ) ) ) ) ) : X --> CC )
54 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 ) ) ) ) ) )
55 54 feq1d
 |-  ( ph -> ( ( ( S Dn ( H ` J ) ) ` N ) : X --> CC <-> ( 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 --> CC ) )
56 53 55 mpbird
 |-  ( ph -> ( ( S Dn ( H ` J ) ) ` N ) : X --> CC )