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 ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
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 cnfldmul ⊢ · = ( .r ‘ ℂfld )
57 56 subrgmcl ⊢ ( ( 𝐷 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑢 ∈ 𝐷 ∧ 𝑣 ∈ 𝐷 ) → ( 𝑢 · 𝑣 ) ∈ 𝐷 )
58 57 3expb ⊢ ( ( 𝐷 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑢 ∈ 𝐷 ∧ 𝑣 ∈ 𝐷 ) ) → ( 𝑢 · 𝑣 ) ∈ 𝐷 )
59 7 58 sylan ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐷 ∧ 𝑣 ∈ 𝐷 ) ) → ( 𝑢 · 𝑣 ) ∈ 𝐷 )
60 ax-1cn ⊢ 1 ∈ ℂ
61 cnfldneg ⊢ ( 1 ∈ ℂ → ( ( invg ‘ ℂfld ) ‘ 1 ) = - 1 )
62 60 61 ax-mp ⊢ ( ( invg ‘ ℂfld ) ‘ 1 ) = - 1
63 eqid ⊢ ( invg ‘ ℂfld ) = ( invg ‘ ℂfld )
64 63 subginvcl ⊢ ( ( 𝐷 ∈ ( SubGrp ‘ ℂfld ) ∧ 1 ∈ 𝐷 ) → ( ( invg ‘ ℂfld ) ‘ 1 ) ∈ 𝐷 )
65 51 45 64 syl2anc ⊢ ( 𝜑 → ( ( invg ‘ ℂfld ) ‘ 1 ) ∈ 𝐷 )
66 62 65 eqeltrrid ⊢ ( 𝜑 → - 1 ∈ 𝐷 )
67 47 49 55 59 66 plysub ⊢ ( 𝜑 → ( Xp ∘f − ( ℂ × { 𝐵 } ) ) ∈ ( Poly ‘ 𝐷 ) )
68 42 67 55 59 plyco ⊢ ( 𝜑 → ( ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑦 ↑ 𝑘 ) ) ) ∘ ( Xp ∘f − ( ℂ × { 𝐵 } ) ) ) ∈ ( Poly ‘ 𝐷 ) )
69 38 68 eqeltrd ⊢ ( 𝜑 → 𝑇 ∈ ( Poly ‘ 𝐷 ) )
70 38 fveq2d ⊢ ( 𝜑 → ( deg ‘ 𝑇 ) = ( deg ‘ ( ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑦 ↑ 𝑘 ) ) ) ∘ ( Xp ∘f − ( ℂ × { 𝐵 } ) ) ) ) )
71 eqid ⊢ ( deg ‘ ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑦 ↑ 𝑘 ) ) ) ) = ( deg ‘ ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑦 ↑ 𝑘 ) ) ) )
72 eqid ⊢ ( deg ‘ ( Xp ∘f − ( ℂ × { 𝐵 } ) ) ) = ( deg ‘ ( Xp ∘f − ( ℂ × { 𝐵 } ) ) )
73 71 72 42 67 dgrco ⊢ ( 𝜑 → ( deg ‘ ( ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑦 ↑ 𝑘 ) ) ) ∘ ( Xp ∘f − ( ℂ × { 𝐵 } ) ) ) ) = ( ( deg ‘ ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑦 ↑ 𝑘 ) ) ) ) · ( deg ‘ ( Xp ∘f − ( ℂ × { 𝐵 } ) ) ) ) )
74 eqid ⊢ ( Xp ∘f − ( ℂ × { 𝐵 } ) ) = ( Xp ∘f − ( ℂ × { 𝐵 } ) )
75 74 plyremlem ⊢ ( 𝐵 ∈ ℂ → ( ( Xp ∘f − ( ℂ × { 𝐵 } ) ) ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ ( Xp ∘f − ( ℂ × { 𝐵 } ) ) ) = 1 ∧ ( ◡ ( Xp ∘f − ( ℂ × { 𝐵 } ) ) “ { 0 } ) = { 𝐵 } ) )
76 23 75 syl ⊢ ( 𝜑 → ( ( Xp ∘f − ( ℂ × { 𝐵 } ) ) ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ ( Xp ∘f − ( ℂ × { 𝐵 } ) ) ) = 1 ∧ ( ◡ ( Xp ∘f − ( ℂ × { 𝐵 } ) ) “ { 0 } ) = { 𝐵 } ) )
77 76 simp2d ⊢ ( 𝜑 → ( deg ‘ ( Xp ∘f − ( ℂ × { 𝐵 } ) ) ) = 1 )
78 77 oveq2d ⊢ ( 𝜑 → ( ( deg ‘ ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑦 ↑ 𝑘 ) ) ) ) · ( deg ‘ ( Xp ∘f − ( ℂ × { 𝐵 } ) ) ) ) = ( ( deg ‘ ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑦 ↑ 𝑘 ) ) ) ) · 1 ) )
79 dgrcl ⊢ ( ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑦 ↑ 𝑘 ) ) ) ∈ ( Poly ‘ 𝐷 ) → ( deg ‘ ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑦 ↑ 𝑘 ) ) ) ) ∈ ℕ0 )
80 42 79 syl ⊢ ( 𝜑 → ( deg ‘ ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑦 ↑ 𝑘 ) ) ) ) ∈ ℕ0 )
81 80 nn0cnd ⊢ ( 𝜑 → ( deg ‘ ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑦 ↑ 𝑘 ) ) ) ) ∈ ℂ )
82 81 mulid1d ⊢ ( 𝜑 → ( ( deg ‘ ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑦 ↑ 𝑘 ) ) ) ) · 1 ) = ( deg ‘ ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑦 ↑ 𝑘 ) ) ) ) )
83 78 82 eqtrd ⊢ ( 𝜑 → ( ( deg ‘ ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑦 ↑ 𝑘 ) ) ) ) · ( deg ‘ ( Xp ∘f − ( ℂ × { 𝐵 } ) ) ) ) = ( deg ‘ ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑦 ↑ 𝑘 ) ) ) ) )
84 70 73 83 3eqtrd ⊢ ( 𝜑 → ( deg ‘ 𝑇 ) = ( deg ‘ ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑦 ↑ 𝑘 ) ) ) ) )
85 1 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑆 ∈ { ℝ , ℂ } )
86 15 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐹 ∈ ( ℂ ↑pm 𝑆 ) )
87 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℕ0 )
88 87 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℕ0 )
89 dvnf ⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) : dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ⟶ ℂ )
90 85 86 88 89 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) : dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ⟶ ℂ )
91 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ( 0 ... 𝑁 ) )
92 dvn2bss ⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ⊆ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) )
93 85 86 91 92 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ⊆ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) )
94 5 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐵 ∈ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) )
95 93 94 sseldd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐵 ∈ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) )
96 90 95 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) ∈ ℂ )
97 88 faccld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ! ‘ 𝑘 ) ∈ ℕ )
98 97 nncnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ! ‘ 𝑘 ) ∈ ℂ )
99 97 nnne0d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ! ‘ 𝑘 ) ≠ 0 )
100 96 98 99 divcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) ∈ ℂ )
101 42 4 100 33 dgrle ⊢ ( 𝜑 → ( deg ‘ ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( 𝑦 ↑ 𝑘 ) ) ) ) ≤ 𝑁 )
102 84 101 eqbrtrd ⊢ ( 𝜑 → ( deg ‘ 𝑇 ) ≤ 𝑁 )
103 69 102 jca ⊢ ( 𝜑 → ( 𝑇 ∈ ( Poly ‘ 𝐷 ) ∧ ( deg ‘ 𝑇 ) ≤ 𝑁 ) )