Metamath Proof Explorer

Theorem etransclem8

Description: F is a function. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem8.x 
|- ( ph -> X C_ CC )
etransclem8.p 
|- ( ph -> P e. NN )
etransclem8.f 
|- F = ( x e. X |-> ( ( x ^ ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( ( x - j ) ^ P ) ) )
Assertion etransclem8 
|- ( ph -> F : X --> CC )

Proof

Step Hyp Ref Expression
1 etransclem8.x 
 |-  ( ph -> X C_ CC )
2 etransclem8.p 
 |-  ( ph -> P e. NN )
3 etransclem8.f 
 |-  F = ( x e. X |-> ( ( x ^ ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( ( x - j ) ^ P ) ) )
4 1 sselda 
 |-  ( ( ph /\ x e. X ) -> x e. CC )
5 2 adantr 
 |-  ( ( ph /\ x e. X ) -> P e. NN )
6 nnm1nn0 
 |-  ( P e. NN -> ( P - 1 ) e. NN0 )
7 5 6 syl 
 |-  ( ( ph /\ x e. X ) -> ( P - 1 ) e. NN0 )
8 4 7 expcld 
 |-  ( ( ph /\ x e. X ) -> ( x ^ ( P - 1 ) ) e. CC )
9 fzfid 
 |-  ( ( ph /\ x e. X ) -> ( 1 ... M ) e. Fin )
10 4 adantr 
 |-  ( ( ( ph /\ x e. X ) /\ j e. ( 1 ... M ) ) -> x e. CC )
11 elfzelz 
 |-  ( j e. ( 1 ... M ) -> j e. ZZ )
12 11 zcnd 
 |-  ( j e. ( 1 ... M ) -> j e. CC )
13 12 adantl 
 |-  ( ( ( ph /\ x e. X ) /\ j e. ( 1 ... M ) ) -> j e. CC )
14 10 13 subcld 
 |-  ( ( ( ph /\ x e. X ) /\ j e. ( 1 ... M ) ) -> ( x - j ) e. CC )
15 2 nnnn0d 
 |-  ( ph -> P e. NN0 )
16 15 ad2antrr 
 |-  ( ( ( ph /\ x e. X ) /\ j e. ( 1 ... M ) ) -> P e. NN0 )
17 14 16 expcld 
 |-  ( ( ( ph /\ x e. X ) /\ j e. ( 1 ... M ) ) -> ( ( x - j ) ^ P ) e. CC )
18 9 17 fprodcl 
 |-  ( ( ph /\ x e. X ) -> prod_ j e. ( 1 ... M ) ( ( x - j ) ^ P ) e. CC )
19 8 18 mulcld 
 |-  ( ( ph /\ x e. X ) -> ( ( x ^ ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( ( x - j ) ^ P ) ) e. CC )
20 19 3 fmptd 
 |-  ( ph -> F : X --> CC )