Metamath Proof Explorer

Theorem taylf

Description: The Taylor series defines a function on a subset of the complex numbers. (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 ) )
taylfval.t 
|- T = ( N ( S Tayl F ) B )
Assertion taylf 
|- ( ph -> T : dom T --> 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 taylfval.t 
 |-  T = ( N ( S Tayl F ) B )
7 1 2 3 4 5 6 taylfval 
 |-  ( ph -> T = U_ x e. CC ( { x } X. ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) ) ) )
8 simpr 
 |-  ( ( ph /\ x e. CC ) -> x e. CC )
9 8 snssd 
 |-  ( ( ph /\ x e. CC ) -> { x } C_ CC )
10 1 2 3 4 5 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 )
11 xpss12 
 |-  ( ( { x } C_ CC /\ ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) ) C_ CC ) -> ( { x } X. ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) ) ) C_ ( CC X. CC ) )
12 9 10 11 syl2anc 
 |-  ( ( ph /\ x e. CC ) -> ( { x } X. ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) ) ) C_ ( CC X. CC ) )
13 12 ralrimiva 
 |-  ( ph -> A. x e. CC ( { x } X. ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) ) ) C_ ( CC X. CC ) )
14 iunss 
 |-  ( U_ x e. CC ( { x } X. ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) ) ) C_ ( CC X. CC ) <-> A. x e. CC ( { x } X. ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) ) ) C_ ( CC X. CC ) )
15 13 14 sylibr 
 |-  ( ph -> U_ x e. CC ( { x } X. ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) ) ) C_ ( CC X. CC ) )
16 7 15 eqsstrd 
 |-  ( ph -> T C_ ( CC X. CC ) )
17 relxp 
 |-  Rel ( CC X. CC )
18 relss 
 |-  ( T C_ ( CC X. CC ) -> ( Rel ( CC X. CC ) -> Rel T ) )
19 16 17 18 mpisyl 
 |-  ( ph -> Rel T )
20 1 2 3 4 5 6 eltayl 
 |-  ( ph -> ( x T y <-> ( x e. CC /\ y e. ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) ) ) ) )
21 20 biimpd 
 |-  ( ph -> ( x T y -> ( x e. CC /\ y e. ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) ) ) ) )
22 21 alrimiv 
 |-  ( ph -> A. y ( x T y -> ( x e. CC /\ y e. ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) ) ) ) )
23 cnfldbas 
 |-  CC = ( Base ` CCfld )
24 cnring 
 |-  CCfld e. Ring
25 ringcmn 
 |-  ( CCfld e. Ring -> CCfld e. CMnd )
26 24 25 mp1i 
 |-  ( ( ph /\ x e. CC ) -> CCfld e. CMnd )
27 cnfldtps 
 |-  CCfld e. TopSp
28 27 a1i 
 |-  ( ( ph /\ x e. CC ) -> CCfld e. TopSp )
29 ovex 
 |-  ( 0 [,] N ) e. _V
30 29 inex1 
 |-  ( ( 0 [,] N ) i^i ZZ ) e. _V
31 30 a1i 
 |-  ( ( ph /\ x e. CC ) -> ( ( 0 [,] N ) i^i ZZ ) e. _V )
32 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 )
33 32 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 )
34 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
35 34 cnfldhaus 
 |-  ( TopOpen ` CCfld ) e. Haus
36 35 a1i 
 |-  ( ( ph /\ x e. CC ) -> ( TopOpen ` CCfld ) e. Haus )
37 23 26 28 31 33 34 36 haustsms 
 |-  ( ( ph /\ x e. CC ) -> E* y y e. ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) ) )
38 37 ex 
 |-  ( ph -> ( x e. CC -> E* y y e. ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) ) ) )
39 moanimv 
 |-  ( E* y ( x e. CC /\ y e. ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) ) ) <-> ( x e. CC -> E* y y e. ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) ) ) )
40 38 39 sylibr 
 |-  ( ph -> E* y ( x e. CC /\ y e. ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) ) ) )
41 moim 
 |-  ( A. y ( x T y -> ( x e. CC /\ y e. ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) ) ) ) -> ( E* y ( x e. CC /\ y e. ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) ) ) -> E* y x T y ) )
42 22 40 41 sylc 
 |-  ( ph -> E* y x T y )
43 42 alrimiv 
 |-  ( ph -> A. x E* y x T y )
44 dffun6 
 |-  ( Fun T <-> ( Rel T /\ A. x E* y x T y ) )
45 19 43 44 sylanbrc 
 |-  ( ph -> Fun T )
46 45 funfnd 
 |-  ( ph -> T Fn dom T )
47 rnss 
 |-  ( T C_ ( CC X. CC ) -> ran T C_ ran ( CC X. CC ) )
48 16 47 syl 
 |-  ( ph -> ran T C_ ran ( CC X. CC ) )
49 rnxpss 
 |-  ran ( CC X. CC ) C_ CC
50 48 49 sstrdi 
 |-  ( ph -> ran T C_ CC )
51 df-f 
 |-  ( T : dom T --> CC <-> ( T Fn dom T /\ ran T C_ CC ) )
52 46 50 51 sylanbrc 
 |-  ( ph -> T : dom T --> CC )