Metamath Proof Explorer

Theorem taylply

Description: The Taylor polynomial is a polynomial of degree (at most) N . (Contributed by Mario Carneiro, 31-Dec-2016)

Ref Expression
Hypotheses taylpfval.s 
|- ( ph -> S e. { RR , CC } )
taylpfval.f 
|- ( ph -> F : A --> CC )
taylpfval.a 
|- ( ph -> A C_ S )
taylpfval.n 
|- ( ph -> N e. NN0 )
taylpfval.b 
|- ( ph -> B e. dom ( ( S Dn F ) ` N ) )
taylpfval.t 
|- T = ( N ( S Tayl F ) B )
Assertion taylply 
|- ( ph -> ( T e. ( Poly ` CC ) /\ ( deg ` T ) <_ N ) )

Proof

Step Hyp Ref Expression
1 taylpfval.s 
 |-  ( ph -> S e. { RR , CC } )
2 taylpfval.f 
 |-  ( ph -> F : A --> CC )
3 taylpfval.a 
 |-  ( ph -> A C_ S )
4 taylpfval.n 
 |-  ( ph -> N e. NN0 )
5 taylpfval.b 
 |-  ( ph -> B e. dom ( ( S Dn F ) ` N ) )
6 taylpfval.t 
 |-  T = ( N ( S Tayl F ) B )
7 cnring 
 |-  CCfld e. Ring
8 cnfldbas 
 |-  CC = ( Base ` CCfld )
9 8 subrgid 
 |-  ( CCfld e. Ring -> CC e. ( SubRing ` CCfld ) )
10 7 9 mp1i 
 |-  ( ph -> CC e. ( SubRing ` CCfld ) )
11 cnex 
 |-  CC e. _V
12 11 a1i 
 |-  ( ph -> CC e. _V )
13 elpm2r 
 |-  ( ( ( CC e. _V /\ S e. { RR , CC } ) /\ ( F : A --> CC /\ A C_ S ) ) -> F e. ( CC ^pm S ) )
14 12 1 2 3 13 syl22anc 
 |-  ( ph -> F e. ( CC ^pm S ) )
15 dvnbss 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ N e. NN0 ) -> dom ( ( S Dn F ) ` N ) C_ dom F )
16 1 14 4 15 syl3anc 
 |-  ( ph -> dom ( ( S Dn F ) ` N ) C_ dom F )
17 2 16 fssdmd 
 |-  ( ph -> dom ( ( S Dn F ) ` N ) C_ A )
18 recnprss 
 |-  ( S e. { RR , CC } -> S C_ CC )
19 1 18 syl 
 |-  ( ph -> S C_ CC )
20 3 19 sstrd 
 |-  ( ph -> A C_ CC )
21 17 20 sstrd 
 |-  ( ph -> dom ( ( S Dn F ) ` N ) C_ CC )
22 21 5 sseldd 
 |-  ( ph -> B e. CC )
23 1 adantr 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> S e. { RR , CC } )
24 14 adantr 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> F e. ( CC ^pm S ) )
25 elfznn0 
 |-  ( k e. ( 0 ... N ) -> k e. NN0 )
26 25 adantl 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> k e. NN0 )
27 dvnf 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ k e. NN0 ) -> ( ( S Dn F ) ` k ) : dom ( ( S Dn F ) ` k ) --> CC )
28 23 24 26 27 syl3anc 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( S Dn F ) ` k ) : dom ( ( S Dn F ) ` k ) --> CC )
29 simpr 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> k e. ( 0 ... N ) )
30 dvn2bss 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ k e. ( 0 ... N ) ) -> dom ( ( S Dn F ) ` N ) C_ dom ( ( S Dn F ) ` k ) )
31 23 24 29 30 syl3anc 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> dom ( ( S Dn F ) ` N ) C_ dom ( ( S Dn F ) ` k ) )
32 5 adantr 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> B e. dom ( ( S Dn F ) ` N ) )
33 31 32 sseldd 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> B e. dom ( ( S Dn F ) ` k ) )
34 28 33 ffvelrnd 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( ( S Dn F ) ` k ) ` B ) e. CC )
35 26 faccld 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ! ` k ) e. NN )
36 35 nncnd 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ! ` k ) e. CC )
37 35 nnne0d 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ! ` k ) =/= 0 )
38 34 36 37 divcld 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) e. CC )
39 1 2 3 4 5 6 10 22 38 taylply2 
 |-  ( ph -> ( T e. ( Poly ` CC ) /\ ( deg ` T ) <_ N ) )