Metamath Proof Explorer

Theorem taylfvallem

Description: Lemma for taylfval . (Contributed by Mario Carneiro, 30-Dec-2016)

Ref Expression
Hypotheses taylfval.s 
|- ( ph -> S e. { RR , CC } )
taylfval.f 
|- ( ph -> F : A --> CC )
taylfval.a 
|- ( ph -> A C_ S )
taylfval.n 
|- ( ph -> ( N e. NN0 \/ N = +oo ) )
taylfval.b 
|- ( ( ph /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> B e. dom ( ( S Dn F ) ` k ) )
Assertion taylfvallem 
|- ( ( ph /\ X e. CC ) -> ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( X - B ) ^ k ) ) ) ) C_ CC )

Proof

Step Hyp Ref Expression
1 taylfval.s 
 |-  ( ph -> S e. { RR , CC } )
2 taylfval.f 
 |-  ( ph -> F : A --> CC )
3 taylfval.a 
 |-  ( ph -> A C_ S )
4 taylfval.n 
 |-  ( ph -> ( N e. NN0 \/ N = +oo ) )
5 taylfval.b 
 |-  ( ( ph /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> B e. dom ( ( S Dn F ) ` k ) )
6 cnfldbas 
 |-  CC = ( Base ` CCfld )
7 cnring 
 |-  CCfld e. Ring
8 ringcmn 
 |-  ( CCfld e. Ring -> CCfld e. CMnd )
9 7 8 mp1i 
 |-  ( ( ph /\ X e. CC ) -> CCfld e. CMnd )
10 cnfldtps 
 |-  CCfld e. TopSp
11 10 a1i 
 |-  ( ( ph /\ X e. CC ) -> CCfld e. TopSp )
12 ovex 
 |-  ( 0 [,] N ) e. _V
13 12 inex1 
 |-  ( ( 0 [,] N ) i^i ZZ ) e. _V
14 13 a1i 
 |-  ( ( ph /\ X e. CC ) -> ( ( 0 [,] N ) i^i ZZ ) e. _V )
15 1 2 3 4 5 taylfvallem1 
 |-  ( ( ( ph /\ X e. CC ) /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( X - B ) ^ k ) ) e. CC )
16 15 fmpttd 
 |-  ( ( ph /\ X e. CC ) -> ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( X - B ) ^ k ) ) ) : ( ( 0 [,] N ) i^i ZZ ) --> CC )
17 6 9 11 14 16 tsmscl 
 |-  ( ( ph /\ X e. CC ) -> ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( X - B ) ^ k ) ) ) ) C_ CC )