Metamath Proof Explorer

Theorem taylply2

Description: The Taylor polynomial is a polynomial of degree (at most) N . This version of taylply shows that the coefficients of T are in a subring of the complex numbers. (Contributed by Mario Carneiro, 1-Jan-2017)

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 )
taylply2.1 
|- ( ph -> D e. ( SubRing ` CCfld ) )
taylply2.2 
|- ( ph -> B e. D )
taylply2.3 
|- ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) e. D )
Assertion taylply2 
|- ( ph -> ( T e. ( Poly ` D ) /\ ( 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 taylply2.1 
 |-  ( ph -> D e. ( SubRing ` CCfld ) )
8 taylply2.2 
 |-  ( ph -> B e. D )
9 taylply2.3 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) e. D )
10 1 2 3 4 5 6 taylpfval 
 |-  ( ph -> T = ( x e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) )
11 simpr 
 |-  ( ( ph /\ x e. CC ) -> x e. CC )
12 cnex 
 |-  CC e. _V
13 12 a1i 
 |-  ( ph -> CC e. _V )
14 elpm2r 
 |-  ( ( ( CC e. _V /\ S e. { RR , CC } ) /\ ( F : A --> CC /\ A C_ S ) ) -> F e. ( CC ^pm S ) )
15 13 1 2 3 14 syl22anc 
 |-  ( ph -> F e. ( CC ^pm S ) )
16 dvnbss 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ N e. NN0 ) -> dom ( ( S Dn F ) ` N ) C_ dom F )
17 1 15 4 16 syl3anc 
 |-  ( ph -> dom ( ( S Dn F ) ` N ) C_ dom F )
18 2 17 fssdmd 
 |-  ( ph -> dom ( ( S Dn F ) ` N ) C_ A )
19 recnprss 
 |-  ( S e. { RR , CC } -> S C_ CC )
20 1 19 syl 
 |-  ( ph -> S C_ CC )
21 3 20 sstrd 
 |-  ( ph -> A C_ CC )
22 18 21 sstrd 
 |-  ( ph -> dom ( ( S Dn F ) ` N ) C_ CC )
23 22 5 sseldd 
 |-  ( ph -> B e. CC )
24 23 adantr 
 |-  ( ( ph /\ x e. CC ) -> B e. CC )
25 11 24 subcld 
 |-  ( ( ph /\ x e. CC ) -> ( x - B ) e. CC )
26 df-idp 
 |-  Xp = ( _I |` CC )
27 mptresid 
 |-  ( _I |` CC ) = ( x e. CC |-> x )
28 26 27 eqtri 
 |-  Xp = ( x e. CC |-> x )
29 28 a1i 
 |-  ( ph -> Xp = ( x e. CC |-> x ) )
30 fconstmpt 
 |-  ( CC X. { B } ) = ( x e. CC |-> B )
31 30 a1i 
 |-  ( ph -> ( CC X. { B } ) = ( x e. CC |-> B ) )
32 13 11 24 29 31 offval2 
 |-  ( ph -> ( Xp oF - ( CC X. { B } ) ) = ( x e. CC |-> ( x - B ) ) )
33 eqidd 
 |-  ( ph -> ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( y ^ k ) ) ) = ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( y ^ k ) ) ) )
34 oveq1 
 |-  ( y = ( x - B ) -> ( y ^ k ) = ( ( x - B ) ^ k ) )
35 34 oveq2d 
 |-  ( y = ( x - B ) -> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( y ^ k ) ) = ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) )
36 35 sumeq2sdv 
 |-  ( y = ( x - B ) -> sum_ k e. ( 0 ... N ) ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( y ^ k ) ) = sum_ k e. ( 0 ... N ) ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) )
37 25 32 33 36 fmptco 
 |-  ( ph -> ( ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( y ^ k ) ) ) o. ( Xp oF - ( CC X. { B } ) ) ) = ( x e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( x - B ) ^ k ) ) ) )
38 10 37 eqtr4d 
 |-  ( ph -> T = ( ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( y ^ k ) ) ) o. ( Xp oF - ( CC X. { B } ) ) ) )
39 cnfldbas 
 |-  CC = ( Base ` CCfld )
40 39 subrgss 
 |-  ( D e. ( SubRing ` CCfld ) -> D C_ CC )
41 7 40 syl 
 |-  ( ph -> D C_ CC )
42 41 4 9 elplyd 
 |-  ( ph -> ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( y ^ k ) ) ) e. ( Poly ` D ) )
43 cnfld1 
 |-  1 = ( 1r ` CCfld )
44 43 subrg1cl 
 |-  ( D e. ( SubRing ` CCfld ) -> 1 e. D )
45 7 44 syl 
 |-  ( ph -> 1 e. D )
46 plyid 
 |-  ( ( D C_ CC /\ 1 e. D ) -> Xp e. ( Poly ` D ) )
47 41 45 46 syl2anc 
 |-  ( ph -> Xp e. ( Poly ` D ) )
48 plyconst 
 |-  ( ( D C_ CC /\ B e. D ) -> ( CC X. { B } ) e. ( Poly ` D ) )
49 41 8 48 syl2anc 
 |-  ( ph -> ( CC X. { B } ) e. ( Poly ` D ) )
50 subrgsubg 
 |-  ( D e. ( SubRing ` CCfld ) -> D e. ( SubGrp ` CCfld ) )
51 7 50 syl 
 |-  ( ph -> D e. ( SubGrp ` CCfld ) )
52 cnfldadd 
 |-  + = ( +g ` CCfld )
53 52 subgcl 
 |-  ( ( D e. ( SubGrp ` CCfld ) /\ u e. D /\ v e. D ) -> ( u + v ) e. D )
54 53 3expb 
 |-  ( ( D e. ( SubGrp ` CCfld ) /\ ( u e. D /\ v e. D ) ) -> ( u + v ) e. D )
55 51 54 sylan 
 |-  ( ( ph /\ ( u e. D /\ v e. D ) ) -> ( u + v ) e. D )
56 cnfldmul 
 |-  x. = ( .r ` CCfld )
57 56 subrgmcl 
 |-  ( ( D e. ( SubRing ` CCfld ) /\ u e. D /\ v e. D ) -> ( u x. v ) e. D )
58 57 3expb 
 |-  ( ( D e. ( SubRing ` CCfld ) /\ ( u e. D /\ v e. D ) ) -> ( u x. v ) e. D )
59 7 58 sylan 
 |-  ( ( ph /\ ( u e. D /\ v e. D ) ) -> ( u x. v ) e. D )
60 ax-1cn 
 |-  1 e. CC
61 cnfldneg 
 |-  ( 1 e. CC -> ( ( invg ` CCfld ) ` 1 ) = -u 1 )
62 60 61 ax-mp 
 |-  ( ( invg ` CCfld ) ` 1 ) = -u 1
63 eqid 
 |-  ( invg ` CCfld ) = ( invg ` CCfld )
64 63 subginvcl 
 |-  ( ( D e. ( SubGrp ` CCfld ) /\ 1 e. D ) -> ( ( invg ` CCfld ) ` 1 ) e. D )
65 51 45 64 syl2anc 
 |-  ( ph -> ( ( invg ` CCfld ) ` 1 ) e. D )
66 62 65 eqeltrrid 
 |-  ( ph -> -u 1 e. D )
67 47 49 55 59 66 plysub 
 |-  ( ph -> ( Xp oF - ( CC X. { B } ) ) e. ( Poly ` D ) )
68 42 67 55 59 plyco 
 |-  ( ph -> ( ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( y ^ k ) ) ) o. ( Xp oF - ( CC X. { B } ) ) ) e. ( Poly ` D ) )
69 38 68 eqeltrd 
 |-  ( ph -> T e. ( Poly ` D ) )
70 38 fveq2d 
 |-  ( ph -> ( deg ` T ) = ( deg ` ( ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( y ^ k ) ) ) o. ( Xp oF - ( CC X. { B } ) ) ) ) )
71 eqid 
 |-  ( deg ` ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( y ^ k ) ) ) ) = ( deg ` ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( y ^ k ) ) ) )
72 eqid 
 |-  ( deg ` ( Xp oF - ( CC X. { B } ) ) ) = ( deg ` ( Xp oF - ( CC X. { B } ) ) )
73 71 72 42 67 dgrco 
 |-  ( ph -> ( deg ` ( ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( y ^ k ) ) ) o. ( Xp oF - ( CC X. { B } ) ) ) ) = ( ( deg ` ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( y ^ k ) ) ) ) x. ( deg ` ( Xp oF - ( CC X. { B } ) ) ) ) )
74 eqid 
 |-  ( Xp oF - ( CC X. { B } ) ) = ( Xp oF - ( CC X. { B } ) )
75 74 plyremlem 
 |-  ( B e. CC -> ( ( Xp oF - ( CC X. { B } ) ) e. ( Poly ` CC ) /\ ( deg ` ( Xp oF - ( CC X. { B } ) ) ) = 1 /\ ( `' ( Xp oF - ( CC X. { B } ) ) " { 0 } ) = { B } ) )
76 23 75 syl 
 |-  ( ph -> ( ( Xp oF - ( CC X. { B } ) ) e. ( Poly ` CC ) /\ ( deg ` ( Xp oF - ( CC X. { B } ) ) ) = 1 /\ ( `' ( Xp oF - ( CC X. { B } ) ) " { 0 } ) = { B } ) )
77 76 simp2d 
 |-  ( ph -> ( deg ` ( Xp oF - ( CC X. { B } ) ) ) = 1 )
78 77 oveq2d 
 |-  ( ph -> ( ( deg ` ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( y ^ k ) ) ) ) x. ( deg ` ( Xp oF - ( CC X. { B } ) ) ) ) = ( ( deg ` ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( y ^ k ) ) ) ) x. 1 ) )
79 dgrcl 
 |-  ( ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( y ^ k ) ) ) e. ( Poly ` D ) -> ( deg ` ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( y ^ k ) ) ) ) e. NN0 )
80 42 79 syl 
 |-  ( ph -> ( deg ` ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( y ^ k ) ) ) ) e. NN0 )
81 80 nn0cnd 
 |-  ( ph -> ( deg ` ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( y ^ k ) ) ) ) e. CC )
82 81 mulid1d 
 |-  ( ph -> ( ( deg ` ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( y ^ k ) ) ) ) x. 1 ) = ( deg ` ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( y ^ k ) ) ) ) )
83 78 82 eqtrd 
 |-  ( ph -> ( ( deg ` ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( y ^ k ) ) ) ) x. ( deg ` ( Xp oF - ( CC X. { B } ) ) ) ) = ( deg ` ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( y ^ k ) ) ) ) )
84 70 73 83 3eqtrd 
 |-  ( ph -> ( deg ` T ) = ( deg ` ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( y ^ k ) ) ) ) )
85 1 adantr 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> S e. { RR , CC } )
86 15 adantr 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> F e. ( CC ^pm S ) )
87 elfznn0 
 |-  ( k e. ( 0 ... N ) -> k e. NN0 )
88 87 adantl 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> k e. NN0 )
89 dvnf 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ k e. NN0 ) -> ( ( S Dn F ) ` k ) : dom ( ( S Dn F ) ` k ) --> CC )
90 85 86 88 89 syl3anc 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( S Dn F ) ` k ) : dom ( ( S Dn F ) ` k ) --> CC )
91 simpr 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> k e. ( 0 ... N ) )
92 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 ) )
93 85 86 91 92 syl3anc 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> dom ( ( S Dn F ) ` N ) C_ dom ( ( S Dn F ) ` k ) )
94 5 adantr 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> B e. dom ( ( S Dn F ) ` N ) )
95 93 94 sseldd 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> B e. dom ( ( S Dn F ) ` k ) )
96 90 95 ffvelrnd 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( ( S Dn F ) ` k ) ` B ) e. CC )
97 88 faccld 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ! ` k ) e. NN )
98 97 nncnd 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ! ` k ) e. CC )
99 97 nnne0d 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ! ` k ) =/= 0 )
100 96 98 99 divcld 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) e. CC )
101 42 4 100 33 dgrle 
 |-  ( ph -> ( deg ` ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( y ^ k ) ) ) ) <_ N )
102 84 101 eqbrtrd 
 |-  ( ph -> ( deg ` T ) <_ N )
103 69 102 jca 
 |-  ( ph -> ( T e. ( Poly ` D ) /\ ( deg ` T ) <_ N ) )