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 ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
taylpfval.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
taylpfval.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝑆 )
taylpfval.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
taylpfval.b ⊢ ( 𝜑 → 𝐵 ∈ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) )
taylpfval.t ⊢ 𝑇 = ( 𝑁 ( 𝑆 Tayl 𝐹 ) 𝐵 )
taylply2.1 ⊢ ( 𝜑 → 𝐷 ∈ ( SubRing ‘ ℂfld ) )
taylply2.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
taylply2.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) ∈ 𝐷 )
Assertion taylply2 ( 𝜑 → ( 𝑇 ∈ ( Poly ‘ 𝐷 ) ∧ ( deg ‘ 𝑇 ) ≤ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 taylpfval.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2 taylpfval.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
3 taylpfval.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝑆 )
4 taylpfval.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
5 taylpfval.b ⊢ ( 𝜑 → 𝐵 ∈ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) )
6 taylpfval.t ⊢ 𝑇 = ( 𝑁 ( 𝑆 Tayl 𝐹 ) 𝐵 )
7 taylply2.1 ⊢ ( 𝜑 → 𝐷 ∈ ( SubRing ‘ ℂfld ) )
8 taylply2.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
9 taylply2.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) ∈ 𝐷 )
10 1 2 3 4 5 6 taylpfval ⊢ ( 𝜑 → 𝑇 = ( 𝑥 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) )
11 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝑥 ∈ ℂ )
12 cnex ⊢ ℂ ∈ V
13 12 a1i ⊢ ( 𝜑 → ℂ ∈ V )
14 elpm2r ⊢ ( ( ( ℂ ∈ V ∧ 𝑆 ∈ { ℝ , ℂ } ) ∧ ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ) → 𝐹 ∈ ( ℂ ↑pm 𝑆 ) )
15 13 1 2 3 14 syl22anc ⊢ ( 𝜑 → 𝐹 ∈ ( ℂ ↑pm 𝑆 ) )
16 dvnbss ⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ 𝑁 ∈ ℕ0 ) → dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ⊆ dom 𝐹 )
17 1 15 4 16 syl3anc ⊢ ( 𝜑 → dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ⊆ dom 𝐹 )
18 2 17 fssdmd ⊢ ( 𝜑 → dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ⊆ 𝐴 )
19 recnprss ⊢ ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ ℂ )
20 1 19 syl ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
21 3 20 sstrd ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
22 18 21 sstrd ⊢ ( 𝜑 → dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ⊆ ℂ )
23 22 5 sseldd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
24 23 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝐵 ∈ ℂ )
25 11 24 subcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝑥 − 𝐵 ) ∈ ℂ )
26 df-idp ⊢ Xp = ( I ↾ ℂ )
27 mptresid ⊢ ( I ↾ ℂ ) = ( 𝑥 ∈ ℂ ↦ 𝑥 )
28 26 27 eqtri ⊢ Xp = ( 𝑥 ∈ ℂ ↦ 𝑥 )
29 28 a1i ⊢ ( 𝜑 → Xp = ( 𝑥 ∈ ℂ ↦ 𝑥 ) )
30 fconstmpt ⊢ ( ℂ × { 𝐵 } ) = ( 𝑥 ∈ ℂ ↦ 𝐵 )
31 30 a1i ⊢ ( 𝜑 → ( ℂ × { 𝐵 } ) = ( 𝑥 ∈ ℂ ↦ 𝐵 ) )
32 13 11 24 29 31 offval2 ⊢ ( 𝜑 → ( Xp ∘f − ( ℂ × { 𝐵 } ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑥 − 𝐵 ) ) )
33 eqidd ⊢ ( 𝜑 → ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑦 ↑ 𝑘 ) ) ) = ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑦 ↑ 𝑘 ) ) ) )
34 oveq1 ⊢ ( 𝑦 = ( 𝑥 − 𝐵 ) → ( 𝑦 ↑ 𝑘 ) = ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) )
35 34 oveq2d ⊢ ( 𝑦 = ( 𝑥 − 𝐵 ) → ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑦 ↑ 𝑘 ) ) = ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) )
36 35 sumeq2sdv ⊢ ( 𝑦 = ( 𝑥 − 𝐵 ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑦 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) )
37 25 32 33 36 fmptco ⊢ ( 𝜑 → ( ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑦 ↑ 𝑘 ) ) ) ∘ ( Xp ∘f − ( ℂ × { 𝐵 } ) ) ) = ( 𝑥 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) )
38 10 37 eqtr4d ⊢ ( 𝜑 → 𝑇 = ( ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑦 ↑ 𝑘 ) ) ) ∘ ( Xp ∘f − ( ℂ × { 𝐵 } ) ) ) )
39 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
40 39 subrgss ⊢ ( 𝐷 ∈ ( SubRing ‘ ℂfld ) → 𝐷 ⊆ ℂ )
41 7 40 syl ⊢ ( 𝜑 → 𝐷 ⊆ ℂ )
42 41 4 9 elplyd ⊢ ( 𝜑 → ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑦 ↑ 𝑘 ) ) ) ∈ ( Poly ‘ 𝐷 ) )
43 cnfld1 ⊢ 1 = ( 1r ‘ ℂfld )
44 43 subrg1cl ⊢ ( 𝐷 ∈ ( SubRing ‘ ℂfld ) → 1 ∈ 𝐷 )
45 7 44 syl ⊢ ( 𝜑 → 1 ∈ 𝐷 )
46 plyid ⊢ ( ( 𝐷 ⊆ ℂ ∧ 1 ∈ 𝐷 ) → Xp ∈ ( Poly ‘ 𝐷 ) )
47 41 45 46 syl2anc ⊢ ( 𝜑 → Xp ∈ ( Poly ‘ 𝐷 ) )
48 plyconst ⊢ ( ( 𝐷 ⊆ ℂ ∧ 𝐵 ∈ 𝐷 ) → ( ℂ × { 𝐵 } ) ∈ ( Poly ‘ 𝐷 ) )
49 41 8 48 syl2anc ⊢ ( 𝜑 → ( ℂ × { 𝐵 } ) ∈ ( Poly ‘ 𝐷 ) )
50 subrgsubg ⊢ ( 𝐷 ∈ ( SubRing ‘ ℂfld ) → 𝐷 ∈ ( SubGrp ‘ ℂfld ) )
51 7 50 syl ⊢ ( 𝜑 → 𝐷 ∈ ( SubGrp ‘ ℂfld ) )
52 cnfldadd ⊢ + = ( +g ‘ ℂfld )
53 52 subgcl ⊢ ( ( 𝐷 ∈ ( SubGrp ‘ ℂfld ) ∧ 𝑢 ∈ 𝐷 ∧ 𝑣 ∈ 𝐷 ) → ( 𝑢 + 𝑣 ) ∈ 𝐷 )
54 53 3expb ⊢ ( ( 𝐷 ∈ ( SubGrp ‘ ℂfld ) ∧ ( 𝑢 ∈ 𝐷 ∧ 𝑣 ∈ 𝐷 ) ) → ( 𝑢 + 𝑣 ) ∈ 𝐷 )
55 51 54 sylan ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐷 ∧ 𝑣 ∈ 𝐷 ) ) → ( 𝑢 + 𝑣 ) ∈ 𝐷 )
56 40 sseld ⊢ ( 𝐷 ∈ ( SubRing ‘ ℂfld ) → ( 𝑢 ∈ 𝐷 → 𝑢 ∈ ℂ ) )
57 56 a1dd ⊢ ( 𝐷 ∈ ( SubRing ‘ ℂfld ) → ( 𝑢 ∈ 𝐷 → ( 𝑣 ∈ 𝐷 → 𝑢 ∈ ℂ ) ) )
58 57 3imp ⊢ ( ( 𝐷 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑢 ∈ 𝐷 ∧ 𝑣 ∈ 𝐷 ) → 𝑢 ∈ ℂ )
59 40 sseld ⊢ ( 𝐷 ∈ ( SubRing ‘ ℂfld ) → ( 𝑣 ∈ 𝐷 → 𝑣 ∈ ℂ ) )
60 59 a1d ⊢ ( 𝐷 ∈ ( SubRing ‘ ℂfld ) → ( 𝑢 ∈ 𝐷 → ( 𝑣 ∈ 𝐷 → 𝑣 ∈ ℂ ) ) )
61 60 3imp ⊢ ( ( 𝐷 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑢 ∈ 𝐷 ∧ 𝑣 ∈ 𝐷 ) → 𝑣 ∈ ℂ )
62 ovmpot ⊢ ( ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) → ( 𝑢 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑣 ) = ( 𝑢 · 𝑣 ) )
63 58 61 62 syl2anc ⊢ ( ( 𝐷 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑢 ∈ 𝐷 ∧ 𝑣 ∈ 𝐷 ) → ( 𝑢 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑣 ) = ( 𝑢 · 𝑣 ) )
64 mpocnfldmul ⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) = ( .r ‘ ℂfld )
65 64 subrgmcl ⊢ ( ( 𝐷 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑢 ∈ 𝐷 ∧ 𝑣 ∈ 𝐷 ) → ( 𝑢 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑣 ) ∈ 𝐷 )
66 63 65 eqeltrrd ⊢ ( ( 𝐷 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑢 ∈ 𝐷 ∧ 𝑣 ∈ 𝐷 ) → ( 𝑢 · 𝑣 ) ∈ 𝐷 )
67 66 3expb ⊢ ( ( 𝐷 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑢 ∈ 𝐷 ∧ 𝑣 ∈ 𝐷 ) ) → ( 𝑢 · 𝑣 ) ∈ 𝐷 )
68 7 67 sylan ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐷 ∧ 𝑣 ∈ 𝐷 ) ) → ( 𝑢 · 𝑣 ) ∈ 𝐷 )
69 ax-1cn ⊢ 1 ∈ ℂ
70 cnfldneg ⊢ ( 1 ∈ ℂ → ( ( invg ‘ ℂfld ) ‘ 1 ) = - 1 )
71 69 70 ax-mp ⊢ ( ( invg ‘ ℂfld ) ‘ 1 ) = - 1
72 eqid ⊢ ( invg ‘ ℂfld ) = ( invg ‘ ℂfld )
73 72 subginvcl ⊢ ( ( 𝐷 ∈ ( SubGrp ‘ ℂfld ) ∧ 1 ∈ 𝐷 ) → ( ( invg ‘ ℂfld ) ‘ 1 ) ∈ 𝐷 )
74 51 45 73 syl2anc ⊢ ( 𝜑 → ( ( invg ‘ ℂfld ) ‘ 1 ) ∈ 𝐷 )
75 71 74 eqeltrrid ⊢ ( 𝜑 → - 1 ∈ 𝐷 )
76 47 49 55 68 75 plysub ⊢ ( 𝜑 → ( Xp ∘f − ( ℂ × { 𝐵 } ) ) ∈ ( Poly ‘ 𝐷 ) )
77 42 76 55 68 plyco ⊢ ( 𝜑 → ( ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑦 ↑ 𝑘 ) ) ) ∘ ( Xp ∘f − ( ℂ × { 𝐵 } ) ) ) ∈ ( Poly ‘ 𝐷 ) )
78 38 77 eqeltrd ⊢ ( 𝜑 → 𝑇 ∈ ( Poly ‘ 𝐷 ) )
79 38 fveq2d ⊢ ( 𝜑 → ( deg ‘ 𝑇 ) = ( deg ‘ ( ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑦 ↑ 𝑘 ) ) ) ∘ ( Xp ∘f − ( ℂ × { 𝐵 } ) ) ) ) )
80 eqid ⊢ ( deg ‘ ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑦 ↑ 𝑘 ) ) ) ) = ( deg ‘ ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑦 ↑ 𝑘 ) ) ) )
81 eqid ⊢ ( deg ‘ ( Xp ∘f − ( ℂ × { 𝐵 } ) ) ) = ( deg ‘ ( Xp ∘f − ( ℂ × { 𝐵 } ) ) )
82 80 81 42 76 dgrco ⊢ ( 𝜑 → ( deg ‘ ( ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑦 ↑ 𝑘 ) ) ) ∘ ( Xp ∘f − ( ℂ × { 𝐵 } ) ) ) ) = ( ( deg ‘ ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑦 ↑ 𝑘 ) ) ) ) · ( deg ‘ ( Xp ∘f − ( ℂ × { 𝐵 } ) ) ) ) )
83 eqid ⊢ ( Xp ∘f − ( ℂ × { 𝐵 } ) ) = ( Xp ∘f − ( ℂ × { 𝐵 } ) )
84 83 plyremlem ⊢ ( 𝐵 ∈ ℂ → ( ( Xp ∘f − ( ℂ × { 𝐵 } ) ) ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ ( Xp ∘f − ( ℂ × { 𝐵 } ) ) ) = 1 ∧ ( ◡ ( Xp ∘f − ( ℂ × { 𝐵 } ) ) “ { 0 } ) = { 𝐵 } ) )
85 23 84 syl ⊢ ( 𝜑 → ( ( Xp ∘f − ( ℂ × { 𝐵 } ) ) ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ ( Xp ∘f − ( ℂ × { 𝐵 } ) ) ) = 1 ∧ ( ◡ ( Xp ∘f − ( ℂ × { 𝐵 } ) ) “ { 0 } ) = { 𝐵 } ) )
86 85 simp2d ⊢ ( 𝜑 → ( deg ‘ ( Xp ∘f − ( ℂ × { 𝐵 } ) ) ) = 1 )
87 86 oveq2d ⊢ ( 𝜑 → ( ( deg ‘ ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑦 ↑ 𝑘 ) ) ) ) · ( deg ‘ ( Xp ∘f − ( ℂ × { 𝐵 } ) ) ) ) = ( ( deg ‘ ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑦 ↑ 𝑘 ) ) ) ) · 1 ) )
88 dgrcl ⊢ ( ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑦 ↑ 𝑘 ) ) ) ∈ ( Poly ‘ 𝐷 ) → ( deg ‘ ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑦 ↑ 𝑘 ) ) ) ) ∈ ℕ0 )
89 42 88 syl ⊢ ( 𝜑 → ( deg ‘ ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑦 ↑ 𝑘 ) ) ) ) ∈ ℕ0 )
90 89 nn0cnd ⊢ ( 𝜑 → ( deg ‘ ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑦 ↑ 𝑘 ) ) ) ) ∈ ℂ )
91 90 mulridd ⊢ ( 𝜑 → ( ( deg ‘ ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑦 ↑ 𝑘 ) ) ) ) · 1 ) = ( deg ‘ ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑦 ↑ 𝑘 ) ) ) ) )
92 87 91 eqtrd ⊢ ( 𝜑 → ( ( deg ‘ ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑦 ↑ 𝑘 ) ) ) ) · ( deg ‘ ( Xp ∘f − ( ℂ × { 𝐵 } ) ) ) ) = ( deg ‘ ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑦 ↑ 𝑘 ) ) ) ) )
93 79 82 92 3eqtrd ⊢ ( 𝜑 → ( deg ‘ 𝑇 ) = ( deg ‘ ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑦 ↑ 𝑘 ) ) ) ) )
94 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℕ0 )
95 dvnf ⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) : dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ⟶ ℂ )
96 1 15 94 95 syl2an3an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) : dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ⟶ ℂ )
97 id ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ( 0 ... 𝑁 ) )
98 dvn2bss ⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ⊆ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) )
99 1 15 97 98 syl2an3an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ⊆ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) )
100 5 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐵 ∈ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) )
101 99 100 sseldd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐵 ∈ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) )
102 96 101 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) ∈ ℂ )
103 94 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℕ0 )
104 103 faccld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ! ‘ 𝑘 ) ∈ ℕ )
105 104 nncnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ! ‘ 𝑘 ) ∈ ℂ )
106 104 nnne0d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ! ‘ 𝑘 ) ≠ 0 )
107 102 105 106 divcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) ∈ ℂ )
108 42 4 107 33 dgrle ⊢ ( 𝜑 → ( deg ‘ ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑦 ↑ 𝑘 ) ) ) ) ≤ 𝑁 )
109 93 108 eqbrtrd ⊢ ( 𝜑 → ( deg ‘ 𝑇 ) ≤ 𝑁 )
110 78 109 jca ⊢ ( 𝜑 → ( 𝑇 ∈ ( Poly ‘ 𝐷 ) ∧ ( deg ‘ 𝑇 ) ≤ 𝑁 ) )