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) Avoid ax-mulf . (Revised by GG, 30-Apr-2025)

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 40 sseld 
 |-  ( D e. ( SubRing ` CCfld ) -> ( u e. D -> u e. CC ) )
57 56 a1dd 
 |-  ( D e. ( SubRing ` CCfld ) -> ( u e. D -> ( v e. D -> u e. CC ) ) )
58 57 3imp 
 |-  ( ( D e. ( SubRing ` CCfld ) /\ u e. D /\ v e. D ) -> u e. CC )
59 40 sseld 
 |-  ( D e. ( SubRing ` CCfld ) -> ( v e. D -> v e. CC ) )
60 59 a1d 
 |-  ( D e. ( SubRing ` CCfld ) -> ( u e. D -> ( v e. D -> v e. CC ) ) )
61 60 3imp 
 |-  ( ( D e. ( SubRing ` CCfld ) /\ u e. D /\ v e. D ) -> v e. CC )
62 ovmpot 
 |-  ( ( u e. CC /\ v e. CC ) -> ( u ( x e. CC , y e. CC |-> ( x x. y ) ) v ) = ( u x. v ) )
63 58 61 62 syl2anc 
 |-  ( ( D e. ( SubRing ` CCfld ) /\ u e. D /\ v e. D ) -> ( u ( x e. CC , y e. CC |-> ( x x. y ) ) v ) = ( u x. v ) )
64 mpocnfldmul 
 |-  ( x e. CC , y e. CC |-> ( x x. y ) ) = ( .r ` CCfld )
65 64 subrgmcl 
 |-  ( ( D e. ( SubRing ` CCfld ) /\ u e. D /\ v e. D ) -> ( u ( x e. CC , y e. CC |-> ( x x. y ) ) v ) e. D )
66 63 65 eqeltrrd 
 |-  ( ( D e. ( SubRing ` CCfld ) /\ u e. D /\ v e. D ) -> ( u x. v ) e. D )
67 66 3expb 
 |-  ( ( D e. ( SubRing ` CCfld ) /\ ( u e. D /\ v e. D ) ) -> ( u x. v ) e. D )
68 7 67 sylan 
 |-  ( ( ph /\ ( u e. D /\ v e. D ) ) -> ( u x. v ) e. D )
69 ax-1cn 
 |-  1 e. CC
70 cnfldneg 
 |-  ( 1 e. CC -> ( ( invg ` CCfld ) ` 1 ) = -u 1 )
71 69 70 ax-mp 
 |-  ( ( invg ` CCfld ) ` 1 ) = -u 1
72 eqid 
 |-  ( invg ` CCfld ) = ( invg ` CCfld )
73 72 subginvcl 
 |-  ( ( D e. ( SubGrp ` CCfld ) /\ 1 e. D ) -> ( ( invg ` CCfld ) ` 1 ) e. D )
74 51 45 73 syl2anc 
 |-  ( ph -> ( ( invg ` CCfld ) ` 1 ) e. D )
75 71 74 eqeltrrid 
 |-  ( ph -> -u 1 e. D )
76 47 49 55 68 75 plysub 
 |-  ( ph -> ( Xp oF - ( CC X. { B } ) ) e. ( Poly ` D ) )
77 42 76 55 68 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 ) )
78 38 77 eqeltrd 
 |-  ( ph -> T e. ( Poly ` D ) )
79 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 } ) ) ) ) )
80 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 ) ) ) )
81 eqid 
 |-  ( deg ` ( Xp oF - ( CC X. { B } ) ) ) = ( deg ` ( Xp oF - ( CC X. { B } ) ) )
82 80 81 42 76 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 } ) ) ) ) )
83 eqid 
 |-  ( Xp oF - ( CC X. { B } ) ) = ( Xp oF - ( CC X. { B } ) )
84 83 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 } ) )
85 23 84 syl 
 |-  ( ph -> ( ( Xp oF - ( CC X. { B } ) ) e. ( Poly ` CC ) /\ ( deg ` ( Xp oF - ( CC X. { B } ) ) ) = 1 /\ ( `' ( Xp oF - ( CC X. { B } ) ) " { 0 } ) = { B } ) )
86 85 simp2d 
 |-  ( ph -> ( deg ` ( Xp oF - ( CC X. { B } ) ) ) = 1 )
87 86 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 ) )
88 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 )
89 42 88 syl 
 |-  ( ph -> ( deg ` ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( y ^ k ) ) ) ) e. NN0 )
90 89 nn0cnd 
 |-  ( ph -> ( deg ` ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( y ^ k ) ) ) ) e. CC )
91 90 mulridd 
 |-  ( 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 ) ) ) ) )
92 87 91 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 ) ) ) ) )
93 79 82 92 3eqtrd 
 |-  ( ph -> ( deg ` T ) = ( deg ` ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( y ^ k ) ) ) ) )
94 elfznn0 
 |-  ( k e. ( 0 ... N ) -> k e. NN0 )
95 dvnf 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ k e. NN0 ) -> ( ( S Dn F ) ` k ) : dom ( ( S Dn F ) ` k ) --> CC )
96 1 15 94 95 syl2an3an 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( S Dn F ) ` k ) : dom ( ( S Dn F ) ` k ) --> CC )
97 id 
 |-  ( k e. ( 0 ... N ) -> k e. ( 0 ... N ) )
98 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 ) )
99 1 15 97 98 syl2an3an 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> dom ( ( S Dn F ) ` N ) C_ dom ( ( S Dn F ) ` k ) )
100 5 adantr 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> B e. dom ( ( S Dn F ) ` N ) )
101 99 100 sseldd 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> B e. dom ( ( S Dn F ) ` k ) )
102 96 101 ffvelcdmd 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( ( S Dn F ) ` k ) ` B ) e. CC )
103 94 adantl 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> k e. NN0 )
104 103 faccld 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ! ` k ) e. NN )
105 104 nncnd 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ! ` k ) e. CC )
106 104 nnne0d 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ! ` k ) =/= 0 )
107 102 105 106 divcld 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) e. CC )
108 42 4 107 33 dgrle 
 |-  ( ph -> ( deg ` ( y e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( y ^ k ) ) ) ) <_ N )
109 93 108 eqbrtrd 
 |-  ( ph -> ( deg ` T ) <_ N )
110 78 109 jca 
 |-  ( ph -> ( T e. ( Poly ` D ) /\ ( deg ` T ) <_ N ) )