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 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
10 9 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
11 8 10 eleqtri 
 |-  RR e. ( ( TopOpen ` CCfld ) |`t RR )
12 11 a1i 
 |-  ( ( ph /\ i e. ( 0 ... R ) ) -> RR e. ( ( TopOpen ` CCfld ) |`t RR ) )
13 1 adantr 
 |-  ( ( ph /\ i e. ( 0 ... R ) ) -> P e. NN )
14 2 adantr 
 |-  ( ( ph /\ i e. ( 0 ... R ) ) -> M e. NN0 )
15 elfznn0 
 |-  ( i e. ( 0 ... R ) -> i e. NN0 )
16 15 adantl 
 |-  ( ( ph /\ i e. ( 0 ... R ) ) -> i e. NN0 )
17 7 12 13 14 3 16 etransclem33 
 |-  ( ( ph /\ i e. ( 0 ... R ) ) -> ( ( RR Dn F ) ` i ) : RR --> CC )
18 17 adantlr 
 |-  ( ( ( ph /\ x e. RR ) /\ i e. ( 0 ... R ) ) -> ( ( RR Dn F ) ` i ) : RR --> CC )
19 simplr 
 |-  ( ( ( ph /\ x e. RR ) /\ i e. ( 0 ... R ) ) -> x e. RR )
20 18 19 ffvelrnd 
 |-  ( ( ( ph /\ x e. RR ) /\ i e. ( 0 ... R ) ) -> ( ( ( RR Dn F ) ` i ) ` x ) e. CC )
21 5 20 fsumcl 
 |-  ( ( ph /\ x e. RR ) -> sum_ i e. ( 0 ... R ) ( ( ( RR Dn F ) ` i ) ` x ) e. CC )
22 21 4 fmptd 
 |-  ( ph -> G : RR --> CC )