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 )