Metamath Proof Explorer


Theorem etransclem43

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

Ref Expression
Hypotheses etransclem43.s
|- ( ph -> S e. { RR , CC } )
etransclem43.x
|- ( ph -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
etransclem43.p
|- ( ph -> P e. NN )
etransclem43.m
|- ( ph -> M e. NN0 )
etransclem43.f
|- F = ( x e. X |-> ( ( x ^ ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( ( x - j ) ^ P ) ) )
etransclem43.g
|- G = ( x e. X |-> sum_ i e. ( 0 ... R ) ( ( ( S Dn F ) ` i ) ` x ) )
Assertion etransclem43
|- ( ph -> G e. ( X -cn-> CC ) )

Proof

Step Hyp Ref Expression
1 etransclem43.s
 |-  ( ph -> S e. { RR , CC } )
2 etransclem43.x
 |-  ( ph -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
3 etransclem43.p
 |-  ( ph -> P e. NN )
4 etransclem43.m
 |-  ( ph -> M e. NN0 )
5 etransclem43.f
 |-  F = ( x e. X |-> ( ( x ^ ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( ( x - j ) ^ P ) ) )
6 etransclem43.g
 |-  G = ( x e. X |-> sum_ i e. ( 0 ... R ) ( ( ( S Dn F ) ` i ) ` x ) )
7 1 2 dvdmsscn
 |-  ( ph -> X C_ CC )
8 fzfid
 |-  ( ph -> ( 0 ... R ) e. Fin )
9 1 adantr
 |-  ( ( ph /\ i e. ( 0 ... R ) ) -> S e. { RR , CC } )
10 2 adantr
 |-  ( ( ph /\ i e. ( 0 ... R ) ) -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
11 3 adantr
 |-  ( ( ph /\ i e. ( 0 ... R ) ) -> P e. NN )
12 4 adantr
 |-  ( ( ph /\ i e. ( 0 ... R ) ) -> M e. NN0 )
13 elfznn0
 |-  ( i e. ( 0 ... R ) -> i e. NN0 )
14 13 adantl
 |-  ( ( ph /\ i e. ( 0 ... R ) ) -> i e. NN0 )
15 9 10 11 12 5 14 etransclem33
 |-  ( ( ph /\ i e. ( 0 ... R ) ) -> ( ( S Dn F ) ` i ) : X --> CC )
16 15 feqmptd
 |-  ( ( ph /\ i e. ( 0 ... R ) ) -> ( ( S Dn F ) ` i ) = ( x e. X |-> ( ( ( S Dn F ) ` i ) ` x ) ) )
17 9 10 11 12 5 14 etransclem40
 |-  ( ( ph /\ i e. ( 0 ... R ) ) -> ( ( S Dn F ) ` i ) e. ( X -cn-> CC ) )
18 16 17 eqeltrrd
 |-  ( ( ph /\ i e. ( 0 ... R ) ) -> ( x e. X |-> ( ( ( S Dn F ) ` i ) ` x ) ) e. ( X -cn-> CC ) )
19 7 8 18 fsumcncf
 |-  ( ph -> ( x e. X |-> sum_ i e. ( 0 ... R ) ( ( ( S Dn F ) ` i ) ` x ) ) e. ( X -cn-> CC ) )
20 6 19 eqeltrid
 |-  ( ph -> G e. ( X -cn-> CC ) )