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 ‘ 𝑇 ) ≤ 𝑁 ) )