Metamath Proof Explorer

Theorem eltayl

Description: Value of the Taylor series as a relation (elementhood in the domain here expresses that the series is convergent). (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 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 ) ) ) ) ) ) )

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 7 eleq2d 
 |-  ( ph -> ( <. X , Y >. e. T <-> <. X , Y >. e. 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 ) ) ) ) ) ) )
9 df-br 
 |-  ( X T Y <-> <. X , Y >. e. T )
10 9 bicomi 
 |-  ( <. X , Y >. e. T <-> X T Y )
11 oveq1 
 |-  ( x = X -> ( x - B ) = ( X - B ) )
12 11 oveq1d 
 |-  ( x = X -> ( ( x - B ) ^ k ) = ( ( X - B ) ^ k ) )
13 12 oveq2d 
 |-  ( x = X -> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) = ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( X - B ) ^ k ) ) )
14 13 mpteq2dv 
 |-  ( x = X -> ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) = ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( X - B ) ^ k ) ) ) )
15 14 oveq2d 
 |-  ( x = X -> ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) ) = ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( X - B ) ^ k ) ) ) ) )
16 15 opeliunxp2 
 |-  ( <. X , Y >. e. 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 ) ) ) ) ) <-> ( X e. CC /\ Y e. ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( X - B ) ^ k ) ) ) ) ) )
17 8 10 16 3bitr3g 
 |-  ( 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 ) ) ) ) ) ) )