Metamath Proof Explorer

Theorem etransclem39

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

Ref Expression
Hypotheses etransclem39.p 
|- ( ph -> P e. NN )
etransclem39.m 
|- ( ph -> M e. NN0 )
etransclem39.f 
|- F = ( x e. RR |-> ( ( x ^ ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( ( x - j ) ^ P ) ) )
etransclem39.g 
|- G = ( x e. RR |-> sum_ i e. ( 0 ... R ) ( ( ( RR Dn F ) ` i ) ` x ) )
Assertion etransclem39 
|- ( ph -> G : RR --> CC )

Proof

Step Hyp Ref Expression
1 etransclem39.p 
 |-  ( ph -> P e. NN )
2 etransclem39.m 
 |-  ( ph -> M e. NN0 )
3 etransclem39.f 
 |-  F = ( x e. RR |-> ( ( x ^ ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( ( x - j ) ^ P ) ) )
4 etransclem39.g 
 |-  G = ( x e. RR |-> sum_ i e. ( 0 ... R ) ( ( ( RR Dn F ) ` i ) ` x ) )
5 fzfid 
 |-  ( ( ph /\ x e. RR ) -> ( 0 ... R ) e. Fin )
6 reelprrecn 
 |-  RR e. { RR , CC }
7 6 a1i 
 |-  ( ( ph /\ i e. ( 0 ... R ) ) -> RR e. { RR , CC } )
8 reopn 
 |-  RR e. ( topGen ` ran (,) )
9 tgioo4 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
10 8 9 eleqtri 
 |-  RR e. ( ( TopOpen ` CCfld ) |`t RR )
11 10 a1i 
 |-  ( ( ph /\ i e. ( 0 ... R ) ) -> RR e. ( ( TopOpen ` CCfld ) |`t RR ) )
12 1 adantr 
 |-  ( ( ph /\ i e. ( 0 ... R ) ) -> P e. NN )
13 2 adantr 
 |-  ( ( ph /\ i e. ( 0 ... R ) ) -> M e. NN0 )
14 elfznn0 
 |-  ( i e. ( 0 ... R ) -> i e. NN0 )
15 14 adantl 
 |-  ( ( ph /\ i e. ( 0 ... R ) ) -> i e. NN0 )
16 7 11 12 13 3 15 etransclem33 
 |-  ( ( ph /\ i e. ( 0 ... R ) ) -> ( ( RR Dn F ) ` i ) : RR --> CC )
17 16 adantlr 
 |-  ( ( ( ph /\ x e. RR ) /\ i e. ( 0 ... R ) ) -> ( ( RR Dn F ) ` i ) : RR --> CC )
18 simplr 
 |-  ( ( ( ph /\ x e. RR ) /\ i e. ( 0 ... R ) ) -> x e. RR )
19 17 18 ffvelcdmd 
 |-  ( ( ( ph /\ x e. RR ) /\ i e. ( 0 ... R ) ) -> ( ( ( RR Dn F ) ` i ) ` x ) e. CC )
20 5 19 fsumcl 
 |-  ( ( ph /\ x e. RR ) -> sum_ i e. ( 0 ... R ) ( ( ( RR Dn F ) ` i ) ` x ) e. CC )
21 20 4 fmptd 
 |-  ( ph -> G : RR --> CC )