taylthlem2OLD

Description: Obsolete version of taylthlem2 as of 30-Apr-2025. (Contributed by Mario Carneiro, 1-Jan-2017) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	taylth.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
	taylth.a	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
	taylth.d	⊢ ( 𝜑 → dom ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑁 ) = 𝐴 )
	taylth.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	taylth.b	⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
	taylth.t	⊢ 𝑇 = ( 𝑁 ( ℝ Tayl 𝐹 ) 𝐵 )
	taylthlem2.m	⊢ ( 𝜑 → 𝑀 ∈ ( 1 ..^ 𝑁 ) )
	taylthlem2.i	⊢ ( 𝜑 → 0 ∈ ( ( 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑥 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑥 ) ) / ( ( 𝑥 − 𝐵 ) ↑ 𝑀 ) ) ) lim_ℂ 𝐵 ) )
Assertion	taylthlem2OLD	⊢ ( 𝜑 → 0 ∈ ( ( 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑥 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑥 ) ) / ( ( 𝑥 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) ) lim_ℂ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		taylth.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
2		taylth.a	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
3		taylth.d	⊢ ( 𝜑 → dom ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑁 ) = 𝐴 )
4		taylth.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
5		taylth.b	⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
6		taylth.t	⊢ 𝑇 = ( 𝑁 ( ℝ Tayl 𝐹 ) 𝐵 )
7		taylthlem2.m	⊢ ( 𝜑 → 𝑀 ∈ ( 1 ..^ 𝑁 ) )
8		taylthlem2.i	⊢ ( 𝜑 → 0 ∈ ( ( 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑥 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑥 ) ) / ( ( 𝑥 − 𝐵 ) ↑ 𝑀 ) ) ) lim_ℂ 𝐵 ) )
9		fz1ssfz0	⊢ ( 1 ... 𝑁 ) ⊆ ( 0 ... 𝑁 )
10		fzofzp1	⊢ ( 𝑀 ∈ ( 1 ..^ 𝑁 ) → ( 𝑀 + 1 ) ∈ ( 1 ... 𝑁 ) )
11	7 10	syl	⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ( 1 ... 𝑁 ) )
12	9 11	sselid	⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ( 0 ... 𝑁 ) )
13		fznn0sub2	⊢ ( ( 𝑀 + 1 ) ∈ ( 0 ... 𝑁 ) → ( 𝑁 − ( 𝑀 + 1 ) ) ∈ ( 0 ... 𝑁 ) )
14	12 13	syl	⊢ ( 𝜑 → ( 𝑁 − ( 𝑀 + 1 ) ) ∈ ( 0 ... 𝑁 ) )
15		elfznn0	⊢ ( ( 𝑁 − ( 𝑀 + 1 ) ) ∈ ( 0 ... 𝑁 ) → ( 𝑁 − ( 𝑀 + 1 ) ) ∈ ℕ₀ )
16	14 15	syl	⊢ ( 𝜑 → ( 𝑁 − ( 𝑀 + 1 ) ) ∈ ℕ₀ )
17		dvnfre	⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ∧ ( 𝑁 − ( 𝑀 + 1 ) ) ∈ ℕ₀ ) → ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) : dom ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ⟶ ℝ )
18	1 2 16 17	syl3anc	⊢ ( 𝜑 → ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) : dom ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ⟶ ℝ )
19		reelprrecn	⊢ ℝ ∈ { ℝ , ℂ }
20	19	a1i	⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
21		cnex	⊢ ℂ ∈ V
22	21	a1i	⊢ ( 𝜑 → ℂ ∈ V )
23		reex	⊢ ℝ ∈ V
24	23	a1i	⊢ ( 𝜑 → ℝ ∈ V )
25		ax-resscn	⊢ ℝ ⊆ ℂ
26		fss	⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ ℝ ⊆ ℂ ) → 𝐹 : 𝐴 ⟶ ℂ )
27	1 25 26	sylancl	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
28		elpm2r	⊢ ( ( ( ℂ ∈ V ∧ ℝ ∈ V ) ∧ ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ) → 𝐹 ∈ ( ℂ ↑_pm ℝ ) )
29	22 24 27 2 28	syl22anc	⊢ ( 𝜑 → 𝐹 ∈ ( ℂ ↑_pm ℝ ) )
30		dvnbss	⊢ ( ( ℝ ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm ℝ ) ∧ ( 𝑁 − ( 𝑀 + 1 ) ) ∈ ℕ₀ ) → dom ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ⊆ dom 𝐹 )
31	20 29 16 30	syl3anc	⊢ ( 𝜑 → dom ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ⊆ dom 𝐹 )
32	1 31	fssdmd	⊢ ( 𝜑 → dom ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ⊆ 𝐴 )
33		dvn2bss	⊢ ( ( ℝ ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm ℝ ) ∧ ( 𝑁 − ( 𝑀 + 1 ) ) ∈ ( 0 ... 𝑁 ) ) → dom ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑁 ) ⊆ dom ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) )
34	20 29 14 33	syl3anc	⊢ ( 𝜑 → dom ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑁 ) ⊆ dom ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) )
35	3 34	eqsstrrd	⊢ ( 𝜑 → 𝐴 ⊆ dom ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) )
36	32 35	eqssd	⊢ ( 𝜑 → dom ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) = 𝐴 )
37	36	feq2d	⊢ ( 𝜑 → ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) : dom ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ⟶ ℝ ↔ ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) : 𝐴 ⟶ ℝ ) )
38	18 37	mpbid	⊢ ( 𝜑 → ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) : 𝐴 ⟶ ℝ )
39	38	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) ∈ ℝ )
40	2	sselda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℝ )
41		fvres	⊢ ( 𝑦 ∈ ℝ → ( ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ↾ ℝ ) ‘ 𝑦 ) = ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) )
42	41	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ↾ ℝ ) ‘ 𝑦 ) = ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) )
43		resubdrg	⊢ ( ℝ ∈ ( SubRing ‘ ℂ_fld ) ∧ ℝ_fld ∈ DivRing )
44	43	simpli	⊢ ℝ ∈ ( SubRing ‘ ℂ_fld )
45	44	a1i	⊢ ( 𝜑 → ℝ ∈ ( SubRing ‘ ℂ_fld ) )
46	4	nnnn0d	⊢ ( 𝜑 → 𝑁 ∈ ℕ₀ )
47	5 3	eleqtrrd	⊢ ( 𝜑 → 𝐵 ∈ dom ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑁 ) )
48	2 5	sseldd	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
49		elfznn0	⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℕ₀ )
50		dvnfre	⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ∧ 𝑘 ∈ ℕ₀ ) → ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑘 ) : dom ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑘 ) ⟶ ℝ )
51	1 2 49 50	syl2an3an	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑘 ) : dom ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑘 ) ⟶ ℝ )
52		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ( 0 ... 𝑁 ) )
53		dvn2bss	⊢ ( ( ℝ ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm ℝ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → dom ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑁 ) ⊆ dom ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑘 ) )
54	19 29 52 53	mp3an2ani	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → dom ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑁 ) ⊆ dom ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑘 ) )
55	47	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐵 ∈ dom ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑁 ) )
56	54 55	sseldd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐵 ∈ dom ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑘 ) )
57	51 56	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) ∈ ℝ )
58	49	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℕ₀ )
59	58	faccld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ! ‘ 𝑘 ) ∈ ℕ )
60	57 59	nndivred	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) ∈ ℝ )
61	20 27 2 46 47 6 45 48 60	taylply2	⊢ ( 𝜑 → ( 𝑇 ∈ ( Poly ‘ ℝ ) ∧ ( deg ‘ 𝑇 ) ≤ 𝑁 ) )
62	61	simpld	⊢ ( 𝜑 → 𝑇 ∈ ( Poly ‘ ℝ ) )
63		dvnply2	⊢ ( ( ℝ ∈ ( SubRing ‘ ℂ_fld ) ∧ 𝑇 ∈ ( Poly ‘ ℝ ) ∧ ( 𝑁 − ( 𝑀 + 1 ) ) ∈ ℕ₀ ) → ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ∈ ( Poly ‘ ℝ ) )
64	45 62 16 63	syl3anc	⊢ ( 𝜑 → ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ∈ ( Poly ‘ ℝ ) )
65		plyreres	⊢ ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ∈ ( Poly ‘ ℝ ) → ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ↾ ℝ ) : ℝ ⟶ ℝ )
66	64 65	syl	⊢ ( 𝜑 → ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ↾ ℝ ) : ℝ ⟶ ℝ )
67	66	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ↾ ℝ ) ‘ 𝑦 ) ∈ ℝ )
68	42 67	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) ∈ ℝ )
69	40 68	syldan	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) ∈ ℝ )
70	39 69	resubcld	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) ) ∈ ℝ )
71	70	fmpttd	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 ↦ ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) ) ) : 𝐴 ⟶ ℝ )
72	48	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
73	40 72	resubcld	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 − 𝐵 ) ∈ ℝ )
74		elfzouz	⊢ ( 𝑀 ∈ ( 1 ..^ 𝑁 ) → 𝑀 ∈ ( ℤ_≥ ‘ 1 ) )
75	7 74	syl	⊢ ( 𝜑 → 𝑀 ∈ ( ℤ_≥ ‘ 1 ) )
76		nnuz	⊢ ℕ = ( ℤ_≥ ‘ 1 )
77	75 76	eleqtrrdi	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
78	77	nnnn0d	⊢ ( 𝜑 → 𝑀 ∈ ℕ₀ )
79	78	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝑀 ∈ ℕ₀ )
80		1nn0	⊢ 1 ∈ ℕ₀
81	80	a1i	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 1 ∈ ℕ₀ )
82	79 81	nn0addcld	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑀 + 1 ) ∈ ℕ₀ )
83	73 82	reexpcld	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ∈ ℝ )
84	83	fmpttd	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) : 𝐴 ⟶ ℝ )
85		retop	⊢ ( topGen ‘ ran (,) ) ∈ Top
86		uniretop	⊢ ℝ = ∪ ( topGen ‘ ran (,) )
87	86	ntrss2	⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ 𝐴 ⊆ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐴 ) ⊆ 𝐴 )
88	85 2 87	sylancr	⊢ ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐴 ) ⊆ 𝐴 )
89	4	nncnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
90	77	nncnd	⊢ ( 𝜑 → 𝑀 ∈ ℂ )
91		1cnd	⊢ ( 𝜑 → 1 ∈ ℂ )
92	89 90 91	nppcan2d	⊢ ( 𝜑 → ( ( 𝑁 − ( 𝑀 + 1 ) ) + 1 ) = ( 𝑁 − 𝑀 ) )
93	92	fveq2d	⊢ ( 𝜑 → ( ( ℝ D^𝑛 𝐹 ) ‘ ( ( 𝑁 − ( 𝑀 + 1 ) ) + 1 ) ) = ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) )
94	25	a1i	⊢ ( 𝜑 → ℝ ⊆ ℂ )
95		dvnp1	⊢ ( ( ℝ ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑_pm ℝ ) ∧ ( 𝑁 − ( 𝑀 + 1 ) ) ∈ ℕ₀ ) → ( ( ℝ D^𝑛 𝐹 ) ‘ ( ( 𝑁 − ( 𝑀 + 1 ) ) + 1 ) ) = ( ℝ D ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ) )
96	94 29 16 95	syl3anc	⊢ ( 𝜑 → ( ( ℝ D^𝑛 𝐹 ) ‘ ( ( 𝑁 − ( 𝑀 + 1 ) ) + 1 ) ) = ( ℝ D ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ) )
97	93 96	eqtr3d	⊢ ( 𝜑 → ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) = ( ℝ D ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ) )
98	97	dmeqd	⊢ ( 𝜑 → dom ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) = dom ( ℝ D ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ) )
99		fzonnsub	⊢ ( 𝑀 ∈ ( 1 ..^ 𝑁 ) → ( 𝑁 − 𝑀 ) ∈ ℕ )
100	7 99	syl	⊢ ( 𝜑 → ( 𝑁 − 𝑀 ) ∈ ℕ )
101	100	nnnn0d	⊢ ( 𝜑 → ( 𝑁 − 𝑀 ) ∈ ℕ₀ )
102		dvnbss	⊢ ( ( ℝ ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm ℝ ) ∧ ( 𝑁 − 𝑀 ) ∈ ℕ₀ ) → dom ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) ⊆ dom 𝐹 )
103	20 29 101 102	syl3anc	⊢ ( 𝜑 → dom ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) ⊆ dom 𝐹 )
104	1 103	fssdmd	⊢ ( 𝜑 → dom ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) ⊆ 𝐴 )
105		elfzofz	⊢ ( 𝑀 ∈ ( 1 ..^ 𝑁 ) → 𝑀 ∈ ( 1 ... 𝑁 ) )
106	7 105	syl	⊢ ( 𝜑 → 𝑀 ∈ ( 1 ... 𝑁 ) )
107	9 106	sselid	⊢ ( 𝜑 → 𝑀 ∈ ( 0 ... 𝑁 ) )
108		fznn0sub2	⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → ( 𝑁 − 𝑀 ) ∈ ( 0 ... 𝑁 ) )
109	107 108	syl	⊢ ( 𝜑 → ( 𝑁 − 𝑀 ) ∈ ( 0 ... 𝑁 ) )
110		dvn2bss	⊢ ( ( ℝ ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm ℝ ) ∧ ( 𝑁 − 𝑀 ) ∈ ( 0 ... 𝑁 ) ) → dom ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑁 ) ⊆ dom ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) )
111	20 29 109 110	syl3anc	⊢ ( 𝜑 → dom ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑁 ) ⊆ dom ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) )
112	3 111	eqsstrrd	⊢ ( 𝜑 → 𝐴 ⊆ dom ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) )
113	104 112	eqssd	⊢ ( 𝜑 → dom ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) = 𝐴 )
114	98 113	eqtr3d	⊢ ( 𝜑 → dom ( ℝ D ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ) = 𝐴 )
115		fss	⊢ ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) : 𝐴 ⟶ ℝ ∧ ℝ ⊆ ℂ ) → ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) : 𝐴 ⟶ ℂ )
116	38 25 115	sylancl	⊢ ( 𝜑 → ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) : 𝐴 ⟶ ℂ )
117		eqid	⊢ ( TopOpen ‘ ℂ_fld ) = ( TopOpen ‘ ℂ_fld )
118	117	tgioo2	⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂ_fld ) ↾_t ℝ )
119	94 116 2 118 117	dvbssntr	⊢ ( 𝜑 → dom ( ℝ D ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ) ⊆ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐴 ) )
120	114 119	eqsstrrd	⊢ ( 𝜑 → 𝐴 ⊆ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐴 ) )
121	88 120	eqssd	⊢ ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐴 ) = 𝐴 )
122	86	isopn3	⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ 𝐴 ⊆ ℝ ) → ( 𝐴 ∈ ( topGen ‘ ran (,) ) ↔ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐴 ) = 𝐴 ) )
123	85 2 122	sylancr	⊢ ( 𝜑 → ( 𝐴 ∈ ( topGen ‘ ran (,) ) ↔ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐴 ) = 𝐴 ) )
124	121 123	mpbird	⊢ ( 𝜑 → 𝐴 ∈ ( topGen ‘ ran (,) ) )
125		eqid	⊢ ( 𝐴 ∖ { 𝐵 } ) = ( 𝐴 ∖ { 𝐵 } )
126		difss	⊢ ( 𝐴 ∖ { 𝐵 } ) ⊆ 𝐴
127	39	recnd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) ∈ ℂ )
128		dvnf	⊢ ( ( ℝ ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm ℝ ) ∧ ( 𝑁 − 𝑀 ) ∈ ℕ₀ ) → ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) : dom ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) ⟶ ℂ )
129	20 29 101 128	syl3anc	⊢ ( 𝜑 → ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) : dom ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) ⟶ ℂ )
130	113	feq2d	⊢ ( 𝜑 → ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) : dom ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) ⟶ ℂ ↔ ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) : 𝐴 ⟶ ℂ ) )
131	129 130	mpbid	⊢ ( 𝜑 → ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) : 𝐴 ⟶ ℂ )
132	131	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑦 ) ∈ ℂ )
133		dvnfre	⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ∧ ( 𝑁 − 𝑀 ) ∈ ℕ₀ ) → ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) : dom ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) ⟶ ℝ )
134	1 2 101 133	syl3anc	⊢ ( 𝜑 → ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) : dom ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) ⟶ ℝ )
135	113	feq2d	⊢ ( 𝜑 → ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) : dom ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) ⟶ ℝ ↔ ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) : 𝐴 ⟶ ℝ ) )
136	134 135	mpbid	⊢ ( 𝜑 → ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) : 𝐴 ⟶ ℝ )
137	136	feqmptd	⊢ ( 𝜑 → ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) = ( 𝑦 ∈ 𝐴 ↦ ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑦 ) ) )
138	38	feqmptd	⊢ ( 𝜑 → ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) = ( 𝑦 ∈ 𝐴 ↦ ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) ) )
139	138	oveq2d	⊢ ( 𝜑 → ( ℝ D ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ) = ( ℝ D ( 𝑦 ∈ 𝐴 ↦ ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) ) ) )
140	97 137 139	3eqtr3rd	⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ 𝐴 ↦ ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) ) ) = ( 𝑦 ∈ 𝐴 ↦ ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑦 ) ) )
141	69	recnd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) ∈ ℂ )
142		fvexd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑦 ) ∈ V )
143	68	recnd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) ∈ ℂ )
144		recn	⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℂ )
145		dvnply2	⊢ ( ( ℝ ∈ ( SubRing ‘ ℂ_fld ) ∧ 𝑇 ∈ ( Poly ‘ ℝ ) ∧ ( 𝑁 − 𝑀 ) ∈ ℕ₀ ) → ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) ∈ ( Poly ‘ ℝ ) )
146	45 62 101 145	syl3anc	⊢ ( 𝜑 → ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) ∈ ( Poly ‘ ℝ ) )
147		plyf	⊢ ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) ∈ ( Poly ‘ ℝ ) → ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) : ℂ ⟶ ℂ )
148	146 147	syl	⊢ ( 𝜑 → ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) : ℂ ⟶ ℂ )
149	148	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑦 ) ∈ ℂ )
150	144 149	sylan2	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑦 ) ∈ ℂ )
151	117	cnfldtopon	⊢ ( TopOpen ‘ ℂ_fld ) ∈ ( TopOn ‘ ℂ )
152		toponmax	⊢ ( ( TopOpen ‘ ℂ_fld ) ∈ ( TopOn ‘ ℂ ) → ℂ ∈ ( TopOpen ‘ ℂ_fld ) )
153	151 152	mp1i	⊢ ( 𝜑 → ℂ ∈ ( TopOpen ‘ ℂ_fld ) )
154		dfss2	⊢ ( ℝ ⊆ ℂ ↔ ( ℝ ∩ ℂ ) = ℝ )
155	94 154	sylib	⊢ ( 𝜑 → ( ℝ ∩ ℂ ) = ℝ )
156		plyf	⊢ ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ∈ ( Poly ‘ ℝ ) → ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) : ℂ ⟶ ℂ )
157	64 156	syl	⊢ ( 𝜑 → ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) : ℂ ⟶ ℂ )
158	157	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) ∈ ℂ )
159	92	fveq2d	⊢ ( 𝜑 → ( ( ℂ D^𝑛 𝑇 ) ‘ ( ( 𝑁 − ( 𝑀 + 1 ) ) + 1 ) ) = ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) )
160		ssid	⊢ ℂ ⊆ ℂ
161	160	a1i	⊢ ( 𝜑 → ℂ ⊆ ℂ )
162		mapsspm	⊢ ( ℂ ↑_m ℂ ) ⊆ ( ℂ ↑_pm ℂ )
163		plyf	⊢ ( 𝑇 ∈ ( Poly ‘ ℝ ) → 𝑇 : ℂ ⟶ ℂ )
164	62 163	syl	⊢ ( 𝜑 → 𝑇 : ℂ ⟶ ℂ )
165	21 21	elmap	⊢ ( 𝑇 ∈ ( ℂ ↑_m ℂ ) ↔ 𝑇 : ℂ ⟶ ℂ )
166	164 165	sylibr	⊢ ( 𝜑 → 𝑇 ∈ ( ℂ ↑_m ℂ ) )
167	162 166	sselid	⊢ ( 𝜑 → 𝑇 ∈ ( ℂ ↑_pm ℂ ) )
168		dvnp1	⊢ ( ( ℂ ⊆ ℂ ∧ 𝑇 ∈ ( ℂ ↑_pm ℂ ) ∧ ( 𝑁 − ( 𝑀 + 1 ) ) ∈ ℕ₀ ) → ( ( ℂ D^𝑛 𝑇 ) ‘ ( ( 𝑁 − ( 𝑀 + 1 ) ) + 1 ) ) = ( ℂ D ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ) )
169	161 167 16 168	syl3anc	⊢ ( 𝜑 → ( ( ℂ D^𝑛 𝑇 ) ‘ ( ( 𝑁 − ( 𝑀 + 1 ) ) + 1 ) ) = ( ℂ D ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ) )
170	159 169	eqtr3d	⊢ ( 𝜑 → ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) = ( ℂ D ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ) )
171	148	feqmptd	⊢ ( 𝜑 → ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) = ( 𝑦 ∈ ℂ ↦ ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑦 ) ) )
172	157	feqmptd	⊢ ( 𝜑 → ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) = ( 𝑦 ∈ ℂ ↦ ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) ) )
173	172	oveq2d	⊢ ( 𝜑 → ( ℂ D ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ) = ( ℂ D ( 𝑦 ∈ ℂ ↦ ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) ) ) )
174	170 171 173	3eqtr3rd	⊢ ( 𝜑 → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ℂ ↦ ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑦 ) ) )
175	117 20 153 155 158 149 174	dvmptres3	⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ℝ ↦ ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ℝ ↦ ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑦 ) ) )
176	20 143 150 175 2 118 117 124	dvmptres	⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ 𝐴 ↦ ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) ) ) = ( 𝑦 ∈ 𝐴 ↦ ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑦 ) ) )
177	20 127 132 140 141 142 176	dvmptsub	⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ 𝐴 ↦ ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) ) ) ) = ( 𝑦 ∈ 𝐴 ↦ ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑦 ) ) ) )
178	177	dmeqd	⊢ ( 𝜑 → dom ( ℝ D ( 𝑦 ∈ 𝐴 ↦ ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) ) ) ) = dom ( 𝑦 ∈ 𝐴 ↦ ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑦 ) ) ) )
179		ovex	⊢ ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑦 ) ) ∈ V
180		eqid	⊢ ( 𝑦 ∈ 𝐴 ↦ ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑦 ) ) ) = ( 𝑦 ∈ 𝐴 ↦ ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑦 ) ) )
181	179 180	dmmpti	⊢ dom ( 𝑦 ∈ 𝐴 ↦ ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑦 ) ) ) = 𝐴
182	178 181	eqtrdi	⊢ ( 𝜑 → dom ( ℝ D ( 𝑦 ∈ 𝐴 ↦ ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) ) ) ) = 𝐴 )
183	126 182	sseqtrrid	⊢ ( 𝜑 → ( 𝐴 ∖ { 𝐵 } ) ⊆ dom ( ℝ D ( 𝑦 ∈ 𝐴 ↦ ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) ) ) ) )
184		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → 𝑦 ∈ ℂ )
185	48	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → 𝐵 ∈ ℝ )
186	185	recnd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → 𝐵 ∈ ℂ )
187	184 186	subcld	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 𝑦 − 𝐵 ) ∈ ℂ )
188	78	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → 𝑀 ∈ ℕ₀ )
189	80	a1i	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → 1 ∈ ℕ₀ )
190	188 189	nn0addcld	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 𝑀 + 1 ) ∈ ℕ₀ )
191	187 190	expcld	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ∈ ℂ )
192	144 191	sylan2	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ∈ ℂ )
193	90	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → 𝑀 ∈ ℂ )
194		1cnd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → 1 ∈ ℂ )
195	193 194	addcld	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 𝑀 + 1 ) ∈ ℂ )
196	187 188	expcld	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( ( 𝑦 − 𝐵 ) ↑ 𝑀 ) ∈ ℂ )
197	195 196	mulcld	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( ( 𝑀 + 1 ) · ( ( 𝑦 − 𝐵 ) ↑ 𝑀 ) ) ∈ ℂ )
198	144 197	sylan2	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( 𝑀 + 1 ) · ( ( 𝑦 − 𝐵 ) ↑ 𝑀 ) ) ∈ ℂ )
199	21	prid2	⊢ ℂ ∈ { ℝ , ℂ }
200	199	a1i	⊢ ( 𝜑 → ℂ ∈ { ℝ , ℂ } )
201		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝑥 ∈ ℂ )
202		elfznn	⊢ ( ( 𝑀 + 1 ) ∈ ( 1 ... 𝑁 ) → ( 𝑀 + 1 ) ∈ ℕ )
203	11 202	syl	⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ℕ )
204	203	nnnn0d	⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ℕ₀ )
205	204	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝑀 + 1 ) ∈ ℕ₀ )
206	201 205	expcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝑥 ↑ ( 𝑀 + 1 ) ) ∈ ℂ )
207		ovexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( 𝑀 + 1 ) · ( 𝑥 ↑ 𝑀 ) ) ∈ V )
208	200	dvmptid	⊢ ( 𝜑 → ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) = ( 𝑦 ∈ ℂ ↦ 1 ) )
209		0cnd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → 0 ∈ ℂ )
210	48	recnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
211	200 210	dvmptc	⊢ ( 𝜑 → ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝐵 ) ) = ( 𝑦 ∈ ℂ ↦ 0 ) )
212	200 184 194 208 186 209 211	dvmptsub	⊢ ( 𝜑 → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝑦 − 𝐵 ) ) ) = ( 𝑦 ∈ ℂ ↦ ( 1 − 0 ) ) )
213		1m0e1	⊢ ( 1 − 0 ) = 1
214	213	mpteq2i	⊢ ( 𝑦 ∈ ℂ ↦ ( 1 − 0 ) ) = ( 𝑦 ∈ ℂ ↦ 1 )
215	212 214	eqtrdi	⊢ ( 𝜑 → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝑦 − 𝐵 ) ) ) = ( 𝑦 ∈ ℂ ↦ 1 ) )
216		dvexp	⊢ ( ( 𝑀 + 1 ) ∈ ℕ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ ( 𝑀 + 1 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( 𝑀 + 1 ) · ( 𝑥 ↑ ( ( 𝑀 + 1 ) − 1 ) ) ) ) )
217	203 216	syl	⊢ ( 𝜑 → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ ( 𝑀 + 1 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( 𝑀 + 1 ) · ( 𝑥 ↑ ( ( 𝑀 + 1 ) − 1 ) ) ) ) )
218	90 91	pncand	⊢ ( 𝜑 → ( ( 𝑀 + 1 ) − 1 ) = 𝑀 )
219	218	oveq2d	⊢ ( 𝜑 → ( 𝑥 ↑ ( ( 𝑀 + 1 ) − 1 ) ) = ( 𝑥 ↑ 𝑀 ) )
220	219	oveq2d	⊢ ( 𝜑 → ( ( 𝑀 + 1 ) · ( 𝑥 ↑ ( ( 𝑀 + 1 ) − 1 ) ) ) = ( ( 𝑀 + 1 ) · ( 𝑥 ↑ 𝑀 ) ) )
221	220	mpteq2dv	⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( ( 𝑀 + 1 ) · ( 𝑥 ↑ ( ( 𝑀 + 1 ) − 1 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( 𝑀 + 1 ) · ( 𝑥 ↑ 𝑀 ) ) ) )
222	217 221	eqtrd	⊢ ( 𝜑 → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ ( 𝑀 + 1 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( 𝑀 + 1 ) · ( 𝑥 ↑ 𝑀 ) ) ) )
223		oveq1	⊢ ( 𝑥 = ( 𝑦 − 𝐵 ) → ( 𝑥 ↑ ( 𝑀 + 1 ) ) = ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) )
224		oveq1	⊢ ( 𝑥 = ( 𝑦 − 𝐵 ) → ( 𝑥 ↑ 𝑀 ) = ( ( 𝑦 − 𝐵 ) ↑ 𝑀 ) )
225	224	oveq2d	⊢ ( 𝑥 = ( 𝑦 − 𝐵 ) → ( ( 𝑀 + 1 ) · ( 𝑥 ↑ 𝑀 ) ) = ( ( 𝑀 + 1 ) · ( ( 𝑦 − 𝐵 ) ↑ 𝑀 ) ) )
226	200 200 187 194 206 207 215 222 223 225	dvmptco	⊢ ( 𝜑 → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) ) = ( 𝑦 ∈ ℂ ↦ ( ( ( 𝑀 + 1 ) · ( ( 𝑦 − 𝐵 ) ↑ 𝑀 ) ) · 1 ) ) )
227	197	mulridd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( ( ( 𝑀 + 1 ) · ( ( 𝑦 − 𝐵 ) ↑ 𝑀 ) ) · 1 ) = ( ( 𝑀 + 1 ) · ( ( 𝑦 − 𝐵 ) ↑ 𝑀 ) ) )
228	227	mpteq2dva	⊢ ( 𝜑 → ( 𝑦 ∈ ℂ ↦ ( ( ( 𝑀 + 1 ) · ( ( 𝑦 − 𝐵 ) ↑ 𝑀 ) ) · 1 ) ) = ( 𝑦 ∈ ℂ ↦ ( ( 𝑀 + 1 ) · ( ( 𝑦 − 𝐵 ) ↑ 𝑀 ) ) ) )
229	226 228	eqtrd	⊢ ( 𝜑 → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) ) = ( 𝑦 ∈ ℂ ↦ ( ( 𝑀 + 1 ) · ( ( 𝑦 − 𝐵 ) ↑ 𝑀 ) ) ) )
230	117 20 153 155 191 197 229	dvmptres3	⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ℝ ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) ) = ( 𝑦 ∈ ℝ ↦ ( ( 𝑀 + 1 ) · ( ( 𝑦 − 𝐵 ) ↑ 𝑀 ) ) ) )
231	20 192 198 230 2 118 117 124	dvmptres	⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) ) = ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑀 + 1 ) · ( ( 𝑦 − 𝐵 ) ↑ 𝑀 ) ) ) )
232	231	dmeqd	⊢ ( 𝜑 → dom ( ℝ D ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) ) = dom ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑀 + 1 ) · ( ( 𝑦 − 𝐵 ) ↑ 𝑀 ) ) ) )
233		ovex	⊢ ( ( 𝑀 + 1 ) · ( ( 𝑦 − 𝐵 ) ↑ 𝑀 ) ) ∈ V
234		eqid	⊢ ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑀 + 1 ) · ( ( 𝑦 − 𝐵 ) ↑ 𝑀 ) ) ) = ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑀 + 1 ) · ( ( 𝑦 − 𝐵 ) ↑ 𝑀 ) ) )
235	233 234	dmmpti	⊢ dom ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑀 + 1 ) · ( ( 𝑦 − 𝐵 ) ↑ 𝑀 ) ) ) = 𝐴
236	232 235	eqtrdi	⊢ ( 𝜑 → dom ( ℝ D ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) ) = 𝐴 )
237	126 236	sseqtrrid	⊢ ( 𝜑 → ( 𝐴 ∖ { 𝐵 } ) ⊆ dom ( ℝ D ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) ) )
238	20 27 2 14 47 6	dvntaylp0	⊢ ( 𝜑 → ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝐵 ) = ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝐵 ) )
239	238	oveq2d	⊢ ( 𝜑 → ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝐵 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝐵 ) ) = ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝐵 ) − ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝐵 ) ) )
240	116 5	ffvelcdmd	⊢ ( 𝜑 → ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝐵 ) ∈ ℂ )
241	240	subidd	⊢ ( 𝜑 → ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝐵 ) − ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝐵 ) ) = 0 )
242	239 241	eqtrd	⊢ ( 𝜑 → ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝐵 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝐵 ) ) = 0 )
243	117	subcn	⊢ − ∈ ( ( ( TopOpen ‘ ℂ_fld ) ×_t ( TopOpen ‘ ℂ_fld ) ) Cn ( TopOpen ‘ ℂ_fld ) )
244	243	a1i	⊢ ( 𝜑 → − ∈ ( ( ( TopOpen ‘ ℂ_fld ) ×_t ( TopOpen ‘ ℂ_fld ) ) Cn ( TopOpen ‘ ℂ_fld ) ) )
245		dvcn	⊢ ( ( ( ℝ ⊆ ℂ ∧ ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ∧ dom ( ℝ D ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ) = 𝐴 ) → ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ∈ ( 𝐴 –cn→ ℂ ) )
246	94 116 2 114 245	syl31anc	⊢ ( 𝜑 → ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ∈ ( 𝐴 –cn→ ℂ ) )
247	138 246	eqeltrrd	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 ↦ ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) ) ∈ ( 𝐴 –cn→ ℂ ) )
248		plycn	⊢ ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ∈ ( Poly ‘ ℝ ) → ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ∈ ( ℂ –cn→ ℂ ) )
249	64 248	syl	⊢ ( 𝜑 → ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ∈ ( ℂ –cn→ ℂ ) )
250	2 25	sstrdi	⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
251		cncfmptid	⊢ ( ( 𝐴 ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑦 ∈ 𝐴 ↦ 𝑦 ) ∈ ( 𝐴 –cn→ ℂ ) )
252	250 160 251	sylancl	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 ↦ 𝑦 ) ∈ ( 𝐴 –cn→ ℂ ) )
253	249 252	cncfmpt1f	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 ↦ ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) ) ∈ ( 𝐴 –cn→ ℂ ) )
254	117 244 247 253	cncfmpt2f	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 ↦ ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) ) ) ∈ ( 𝐴 –cn→ ℂ ) )
255		fveq2	⊢ ( 𝑦 = 𝐵 → ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) = ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝐵 ) )
256		fveq2	⊢ ( 𝑦 = 𝐵 → ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) = ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝐵 ) )
257	255 256	oveq12d	⊢ ( 𝑦 = 𝐵 → ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) ) = ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝐵 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝐵 ) ) )
258	254 5 257	cnmptlimc	⊢ ( 𝜑 → ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝐵 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝐵 ) ) ∈ ( ( 𝑦 ∈ 𝐴 ↦ ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) ) ) lim_ℂ 𝐵 ) )
259	242 258	eqeltrrd	⊢ ( 𝜑 → 0 ∈ ( ( 𝑦 ∈ 𝐴 ↦ ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) ) ) lim_ℂ 𝐵 ) )
260	210	subidd	⊢ ( 𝜑 → ( 𝐵 − 𝐵 ) = 0 )
261	260	oveq1d	⊢ ( 𝜑 → ( ( 𝐵 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) = ( 0 ↑ ( 𝑀 + 1 ) ) )
262	203	0expd	⊢ ( 𝜑 → ( 0 ↑ ( 𝑀 + 1 ) ) = 0 )
263	261 262	eqtrd	⊢ ( 𝜑 → ( ( 𝐵 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) = 0 )
264	250	sselda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℂ )
265	264 191	syldan	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ∈ ℂ )
266	265	fmpttd	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) : 𝐴 ⟶ ℂ )
267		dvcn	⊢ ( ( ( ℝ ⊆ ℂ ∧ ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ∧ dom ( ℝ D ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) ) = 𝐴 ) → ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) ∈ ( 𝐴 –cn→ ℂ ) )
268	94 266 2 236 267	syl31anc	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) ∈ ( 𝐴 –cn→ ℂ ) )
269		oveq1	⊢ ( 𝑦 = 𝐵 → ( 𝑦 − 𝐵 ) = ( 𝐵 − 𝐵 ) )
270	269	oveq1d	⊢ ( 𝑦 = 𝐵 → ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) = ( ( 𝐵 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) )
271	268 5 270	cnmptlimc	⊢ ( 𝜑 → ( ( 𝐵 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ∈ ( ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) lim_ℂ 𝐵 ) )
272	263 271	eqeltrrd	⊢ ( 𝜑 → 0 ∈ ( ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) lim_ℂ 𝐵 ) )
273	250	ssdifssd	⊢ ( 𝜑 → ( 𝐴 ∖ { 𝐵 } ) ⊆ ℂ )
274	273	sselda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 𝑦 ∈ ℂ )
275	210	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 𝐵 ∈ ℂ )
276	274 275	subcld	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( 𝑦 − 𝐵 ) ∈ ℂ )
277		eldifsni	⊢ ( 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) → 𝑦 ≠ 𝐵 )
278	277	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 𝑦 ≠ 𝐵 )
279	274 275 278	subne0d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( 𝑦 − 𝐵 ) ≠ 0 )
280	203	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( 𝑀 + 1 ) ∈ ℕ )
281	280	nnzd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( 𝑀 + 1 ) ∈ ℤ )
282	276 279 281	expne0d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ≠ 0 )
283	282	necomd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 0 ≠ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) )
284	283	neneqd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ¬ 0 = ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) )
285	284	nrexdv	⊢ ( 𝜑 → ¬ ∃ 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) 0 = ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) )
286		df-ima	⊢ ( ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) “ ( 𝐴 ∖ { 𝐵 } ) ) = ran ( ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) ↾ ( 𝐴 ∖ { 𝐵 } ) )
287	286	eleq2i	⊢ ( 0 ∈ ( ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) “ ( 𝐴 ∖ { 𝐵 } ) ) ↔ 0 ∈ ran ( ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) ↾ ( 𝐴 ∖ { 𝐵 } ) ) )
288		resmpt	⊢ ( ( 𝐴 ∖ { 𝐵 } ) ⊆ 𝐴 → ( ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) ↾ ( 𝐴 ∖ { 𝐵 } ) ) = ( 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) )
289	126 288	ax-mp	⊢ ( ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) ↾ ( 𝐴 ∖ { 𝐵 } ) ) = ( 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) )
290		ovex	⊢ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ∈ V
291	289 290	elrnmpti	⊢ ( 0 ∈ ran ( ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) ↾ ( 𝐴 ∖ { 𝐵 } ) ) ↔ ∃ 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) 0 = ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) )
292	287 291	bitri	⊢ ( 0 ∈ ( ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) “ ( 𝐴 ∖ { 𝐵 } ) ) ↔ ∃ 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) 0 = ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) )
293	285 292	sylnibr	⊢ ( 𝜑 → ¬ 0 ∈ ( ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) “ ( 𝐴 ∖ { 𝐵 } ) ) )
294	90	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 𝑀 ∈ ℂ )
295		1cnd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 1 ∈ ℂ )
296	294 295	addcld	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( 𝑀 + 1 ) ∈ ℂ )
297	274 196	syldan	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( ( 𝑦 − 𝐵 ) ↑ 𝑀 ) ∈ ℂ )
298	280	nnne0d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( 𝑀 + 1 ) ≠ 0 )
299	77	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 𝑀 ∈ ℕ )
300	299	nnzd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 𝑀 ∈ ℤ )
301	276 279 300	expne0d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( ( 𝑦 − 𝐵 ) ↑ 𝑀 ) ≠ 0 )
302	296 297 298 301	mulne0d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( ( 𝑀 + 1 ) · ( ( 𝑦 − 𝐵 ) ↑ 𝑀 ) ) ≠ 0 )
303	302	necomd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 0 ≠ ( ( 𝑀 + 1 ) · ( ( 𝑦 − 𝐵 ) ↑ 𝑀 ) ) )
304	303	neneqd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ¬ 0 = ( ( 𝑀 + 1 ) · ( ( 𝑦 − 𝐵 ) ↑ 𝑀 ) ) )
305	304	nrexdv	⊢ ( 𝜑 → ¬ ∃ 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) 0 = ( ( 𝑀 + 1 ) · ( ( 𝑦 − 𝐵 ) ↑ 𝑀 ) ) )
306	231	imaeq1d	⊢ ( 𝜑 → ( ( ℝ D ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) ) “ ( 𝐴 ∖ { 𝐵 } ) ) = ( ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑀 + 1 ) · ( ( 𝑦 − 𝐵 ) ↑ 𝑀 ) ) ) “ ( 𝐴 ∖ { 𝐵 } ) ) )
307		df-ima	⊢ ( ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑀 + 1 ) · ( ( 𝑦 − 𝐵 ) ↑ 𝑀 ) ) ) “ ( 𝐴 ∖ { 𝐵 } ) ) = ran ( ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑀 + 1 ) · ( ( 𝑦 − 𝐵 ) ↑ 𝑀 ) ) ) ↾ ( 𝐴 ∖ { 𝐵 } ) )
308	306 307	eqtrdi	⊢ ( 𝜑 → ( ( ℝ D ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) ) “ ( 𝐴 ∖ { 𝐵 } ) ) = ran ( ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑀 + 1 ) · ( ( 𝑦 − 𝐵 ) ↑ 𝑀 ) ) ) ↾ ( 𝐴 ∖ { 𝐵 } ) ) )
309	308	eleq2d	⊢ ( 𝜑 → ( 0 ∈ ( ( ℝ D ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) ) “ ( 𝐴 ∖ { 𝐵 } ) ) ↔ 0 ∈ ran ( ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑀 + 1 ) · ( ( 𝑦 − 𝐵 ) ↑ 𝑀 ) ) ) ↾ ( 𝐴 ∖ { 𝐵 } ) ) ) )
310		resmpt	⊢ ( ( 𝐴 ∖ { 𝐵 } ) ⊆ 𝐴 → ( ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑀 + 1 ) · ( ( 𝑦 − 𝐵 ) ↑ 𝑀 ) ) ) ↾ ( 𝐴 ∖ { 𝐵 } ) ) = ( 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( 𝑀 + 1 ) · ( ( 𝑦 − 𝐵 ) ↑ 𝑀 ) ) ) )
311	126 310	ax-mp	⊢ ( ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑀 + 1 ) · ( ( 𝑦 − 𝐵 ) ↑ 𝑀 ) ) ) ↾ ( 𝐴 ∖ { 𝐵 } ) ) = ( 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( 𝑀 + 1 ) · ( ( 𝑦 − 𝐵 ) ↑ 𝑀 ) ) )
312	311 233	elrnmpti	⊢ ( 0 ∈ ran ( ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑀 + 1 ) · ( ( 𝑦 − 𝐵 ) ↑ 𝑀 ) ) ) ↾ ( 𝐴 ∖ { 𝐵 } ) ) ↔ ∃ 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) 0 = ( ( 𝑀 + 1 ) · ( ( 𝑦 − 𝐵 ) ↑ 𝑀 ) ) )
313	309 312	bitrdi	⊢ ( 𝜑 → ( 0 ∈ ( ( ℝ D ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) ) “ ( 𝐴 ∖ { 𝐵 } ) ) ↔ ∃ 𝑦 ∈ ( 𝐴 ∖ { 𝐵 } ) 0 = ( ( 𝑀 + 1 ) · ( ( 𝑦 − 𝐵 ) ↑ 𝑀 ) ) ) )
314	305 313	mtbird	⊢ ( 𝜑 → ¬ 0 ∈ ( ( ℝ D ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) ) “ ( 𝐴 ∖ { 𝐵 } ) ) )
315		eldifi	⊢ ( 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) → 𝑥 ∈ 𝐴 )
316	131	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑥 ) ∈ ℂ )
317	315 316	sylan2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑥 ) ∈ ℂ )
318	2	ssdifssd	⊢ ( 𝜑 → ( 𝐴 ∖ { 𝐵 } ) ⊆ ℝ )
319	318	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 𝑥 ∈ ℝ )
320	319	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 𝑥 ∈ ℂ )
321	148	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑥 ) ∈ ℂ )
322	320 321	syldan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑥 ) ∈ ℂ )
323	317 322	subcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑥 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑥 ) ) ∈ ℂ )
324	48	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 𝐵 ∈ ℝ )
325	319 324	resubcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( 𝑥 − 𝐵 ) ∈ ℝ )
326	78	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 𝑀 ∈ ℕ₀ )
327	325 326	reexpcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( ( 𝑥 − 𝐵 ) ↑ 𝑀 ) ∈ ℝ )
328	327	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( ( 𝑥 − 𝐵 ) ↑ 𝑀 ) ∈ ℂ )
329	324	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 𝐵 ∈ ℂ )
330	320 329	subcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( 𝑥 − 𝐵 ) ∈ ℂ )
331		eldifsni	⊢ ( 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) → 𝑥 ≠ 𝐵 )
332	331	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 𝑥 ≠ 𝐵 )
333	320 329 332	subne0d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( 𝑥 − 𝐵 ) ≠ 0 )
334	326	nn0zd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 𝑀 ∈ ℤ )
335	330 333 334	expne0d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( ( 𝑥 − 𝐵 ) ↑ 𝑀 ) ≠ 0 )
336	323 328 335	divcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑥 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑥 ) ) / ( ( 𝑥 − 𝐵 ) ↑ 𝑀 ) ) ∈ ℂ )
337	203	nnrecred	⊢ ( 𝜑 → ( 1 / ( 𝑀 + 1 ) ) ∈ ℝ )
338	337	recnd	⊢ ( 𝜑 → ( 1 / ( 𝑀 + 1 ) ) ∈ ℂ )
339	338	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( 1 / ( 𝑀 + 1 ) ) ∈ ℂ )
340		txtopon	⊢ ( ( ( TopOpen ‘ ℂ_fld ) ∈ ( TopOn ‘ ℂ ) ∧ ( TopOpen ‘ ℂ_fld ) ∈ ( TopOn ‘ ℂ ) ) → ( ( TopOpen ‘ ℂ_fld ) ×_t ( TopOpen ‘ ℂ_fld ) ) ∈ ( TopOn ‘ ( ℂ × ℂ ) ) )
341	151 151 340	mp2an	⊢ ( ( TopOpen ‘ ℂ_fld ) ×_t ( TopOpen ‘ ℂ_fld ) ) ∈ ( TopOn ‘ ( ℂ × ℂ ) )
342	341	toponrestid	⊢ ( ( TopOpen ‘ ℂ_fld ) ×_t ( TopOpen ‘ ℂ_fld ) ) = ( ( ( TopOpen ‘ ℂ_fld ) ×_t ( TopOpen ‘ ℂ_fld ) ) ↾_t ( ℂ × ℂ ) )
343		limcresi	⊢ ( ( 𝑥 ∈ 𝐴 ↦ ( 1 / ( 𝑀 + 1 ) ) ) lim_ℂ 𝐵 ) ⊆ ( ( ( 𝑥 ∈ 𝐴 ↦ ( 1 / ( 𝑀 + 1 ) ) ) ↾ ( 𝐴 ∖ { 𝐵 } ) ) lim_ℂ 𝐵 )
344		resmpt	⊢ ( ( 𝐴 ∖ { 𝐵 } ) ⊆ 𝐴 → ( ( 𝑥 ∈ 𝐴 ↦ ( 1 / ( 𝑀 + 1 ) ) ) ↾ ( 𝐴 ∖ { 𝐵 } ) ) = ( 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( 1 / ( 𝑀 + 1 ) ) ) )
345	126 344	ax-mp	⊢ ( ( 𝑥 ∈ 𝐴 ↦ ( 1 / ( 𝑀 + 1 ) ) ) ↾ ( 𝐴 ∖ { 𝐵 } ) ) = ( 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( 1 / ( 𝑀 + 1 ) ) )
346	345	oveq1i	⊢ ( ( ( 𝑥 ∈ 𝐴 ↦ ( 1 / ( 𝑀 + 1 ) ) ) ↾ ( 𝐴 ∖ { 𝐵 } ) ) lim_ℂ 𝐵 ) = ( ( 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( 1 / ( 𝑀 + 1 ) ) ) lim_ℂ 𝐵 )
347	343 346	sseqtri	⊢ ( ( 𝑥 ∈ 𝐴 ↦ ( 1 / ( 𝑀 + 1 ) ) ) lim_ℂ 𝐵 ) ⊆ ( ( 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( 1 / ( 𝑀 + 1 ) ) ) lim_ℂ 𝐵 )
348		cncfmptc	⊢ ( ( ( 1 / ( 𝑀 + 1 ) ) ∈ ℝ ∧ 𝐴 ⊆ ℂ ∧ ℝ ⊆ ℂ ) → ( 𝑥 ∈ 𝐴 ↦ ( 1 / ( 𝑀 + 1 ) ) ) ∈ ( 𝐴 –cn→ ℝ ) )
349	337 250 94 348	syl3anc	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 1 / ( 𝑀 + 1 ) ) ) ∈ ( 𝐴 –cn→ ℝ ) )
350		eqidd	⊢ ( 𝑥 = 𝐵 → ( 1 / ( 𝑀 + 1 ) ) = ( 1 / ( 𝑀 + 1 ) ) )
351	349 5 350	cnmptlimc	⊢ ( 𝜑 → ( 1 / ( 𝑀 + 1 ) ) ∈ ( ( 𝑥 ∈ 𝐴 ↦ ( 1 / ( 𝑀 + 1 ) ) ) lim_ℂ 𝐵 ) )
352	347 351	sselid	⊢ ( 𝜑 → ( 1 / ( 𝑀 + 1 ) ) ∈ ( ( 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( 1 / ( 𝑀 + 1 ) ) ) lim_ℂ 𝐵 ) )
353	117	mulcn	⊢ · ∈ ( ( ( TopOpen ‘ ℂ_fld ) ×_t ( TopOpen ‘ ℂ_fld ) ) Cn ( TopOpen ‘ ℂ_fld ) )
354		0cn	⊢ 0 ∈ ℂ
355		opelxpi	⊢ ( ( 0 ∈ ℂ ∧ ( 1 / ( 𝑀 + 1 ) ) ∈ ℂ ) → ⟨ 0 , ( 1 / ( 𝑀 + 1 ) ) ⟩ ∈ ( ℂ × ℂ ) )
356	354 338 355	sylancr	⊢ ( 𝜑 → ⟨ 0 , ( 1 / ( 𝑀 + 1 ) ) ⟩ ∈ ( ℂ × ℂ ) )
357	341	toponunii	⊢ ( ℂ × ℂ ) = ∪ ( ( TopOpen ‘ ℂ_fld ) ×_t ( TopOpen ‘ ℂ_fld ) )
358	357	cncnpi	⊢ ( ( · ∈ ( ( ( TopOpen ‘ ℂ_fld ) ×_t ( TopOpen ‘ ℂ_fld ) ) Cn ( TopOpen ‘ ℂ_fld ) ) ∧ ⟨ 0 , ( 1 / ( 𝑀 + 1 ) ) ⟩ ∈ ( ℂ × ℂ ) ) → · ∈ ( ( ( ( TopOpen ‘ ℂ_fld ) ×_t ( TopOpen ‘ ℂ_fld ) ) CnP ( TopOpen ‘ ℂ_fld ) ) ‘ ⟨ 0 , ( 1 / ( 𝑀 + 1 ) ) ⟩ ) )
359	353 356 358	sylancr	⊢ ( 𝜑 → · ∈ ( ( ( ( TopOpen ‘ ℂ_fld ) ×_t ( TopOpen ‘ ℂ_fld ) ) CnP ( TopOpen ‘ ℂ_fld ) ) ‘ ⟨ 0 , ( 1 / ( 𝑀 + 1 ) ) ⟩ ) )
360	336 339 161 161 117 342 8 352 359	limccnp2	⊢ ( 𝜑 → ( 0 · ( 1 / ( 𝑀 + 1 ) ) ) ∈ ( ( 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑥 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑥 ) ) / ( ( 𝑥 − 𝐵 ) ↑ 𝑀 ) ) · ( 1 / ( 𝑀 + 1 ) ) ) ) lim_ℂ 𝐵 ) )
361	338	mul02d	⊢ ( 𝜑 → ( 0 · ( 1 / ( 𝑀 + 1 ) ) ) = 0 )
362	177	fveq1d	⊢ ( 𝜑 → ( ( ℝ D ( 𝑦 ∈ 𝐴 ↦ ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) ) ) ) ‘ 𝑥 ) = ( ( 𝑦 ∈ 𝐴 ↦ ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑦 ) ) ) ‘ 𝑥 ) )
363		fveq2	⊢ ( 𝑦 = 𝑥 → ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑦 ) = ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑥 ) )
364		fveq2	⊢ ( 𝑦 = 𝑥 → ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑦 ) = ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑥 ) )
365	363 364	oveq12d	⊢ ( 𝑦 = 𝑥 → ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑦 ) ) = ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑥 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑥 ) ) )
366		ovex	⊢ ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑥 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑥 ) ) ∈ V
367	365 180 366	fvmpt	⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝑦 ∈ 𝐴 ↦ ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑦 ) ) ) ‘ 𝑥 ) = ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑥 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑥 ) ) )
368	315 367	syl	⊢ ( 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) → ( ( 𝑦 ∈ 𝐴 ↦ ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑦 ) ) ) ‘ 𝑥 ) = ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑥 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑥 ) ) )
369	362 368	sylan9eq	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( ( ℝ D ( 𝑦 ∈ 𝐴 ↦ ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) ) ) ) ‘ 𝑥 ) = ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑥 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑥 ) ) )
370	231	fveq1d	⊢ ( 𝜑 → ( ( ℝ D ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) ) ‘ 𝑥 ) = ( ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑀 + 1 ) · ( ( 𝑦 − 𝐵 ) ↑ 𝑀 ) ) ) ‘ 𝑥 ) )
371		oveq1	⊢ ( 𝑦 = 𝑥 → ( 𝑦 − 𝐵 ) = ( 𝑥 − 𝐵 ) )
372	371	oveq1d	⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 − 𝐵 ) ↑ 𝑀 ) = ( ( 𝑥 − 𝐵 ) ↑ 𝑀 ) )
373	372	oveq2d	⊢ ( 𝑦 = 𝑥 → ( ( 𝑀 + 1 ) · ( ( 𝑦 − 𝐵 ) ↑ 𝑀 ) ) = ( ( 𝑀 + 1 ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑀 ) ) )
374		ovex	⊢ ( ( 𝑀 + 1 ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑀 ) ) ∈ V
375	373 234 374	fvmpt	⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑀 + 1 ) · ( ( 𝑦 − 𝐵 ) ↑ 𝑀 ) ) ) ‘ 𝑥 ) = ( ( 𝑀 + 1 ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑀 ) ) )
376	315 375	syl	⊢ ( 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) → ( ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑀 + 1 ) · ( ( 𝑦 − 𝐵 ) ↑ 𝑀 ) ) ) ‘ 𝑥 ) = ( ( 𝑀 + 1 ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑀 ) ) )
377	370 376	sylan9eq	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( ( ℝ D ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) ) ‘ 𝑥 ) = ( ( 𝑀 + 1 ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑀 ) ) )
378	203	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( 𝑀 + 1 ) ∈ ℕ )
379	378	nncnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( 𝑀 + 1 ) ∈ ℂ )
380	379 328	mulcomd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( ( 𝑀 + 1 ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑀 ) ) = ( ( ( 𝑥 − 𝐵 ) ↑ 𝑀 ) · ( 𝑀 + 1 ) ) )
381	377 380	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( ( ℝ D ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) ) ‘ 𝑥 ) = ( ( ( 𝑥 − 𝐵 ) ↑ 𝑀 ) · ( 𝑀 + 1 ) ) )
382	369 381	oveq12d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( ( ( ℝ D ( 𝑦 ∈ 𝐴 ↦ ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) ) ) ) ‘ 𝑥 ) / ( ( ℝ D ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) ) ‘ 𝑥 ) ) = ( ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑥 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑥 ) ) / ( ( ( 𝑥 − 𝐵 ) ↑ 𝑀 ) · ( 𝑀 + 1 ) ) ) )
383	378	nnne0d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( 𝑀 + 1 ) ≠ 0 )
384	323 328 379 335 383	divdiv1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( ( ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑥 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑥 ) ) / ( ( 𝑥 − 𝐵 ) ↑ 𝑀 ) ) / ( 𝑀 + 1 ) ) = ( ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑥 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑥 ) ) / ( ( ( 𝑥 − 𝐵 ) ↑ 𝑀 ) · ( 𝑀 + 1 ) ) ) )
385	336 379 383	divrecd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( ( ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑥 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑥 ) ) / ( ( 𝑥 − 𝐵 ) ↑ 𝑀 ) ) / ( 𝑀 + 1 ) ) = ( ( ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑥 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑥 ) ) / ( ( 𝑥 − 𝐵 ) ↑ 𝑀 ) ) · ( 1 / ( 𝑀 + 1 ) ) ) )
386	382 384 385	3eqtr2rd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( ( ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑥 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑥 ) ) / ( ( 𝑥 − 𝐵 ) ↑ 𝑀 ) ) · ( 1 / ( 𝑀 + 1 ) ) ) = ( ( ( ℝ D ( 𝑦 ∈ 𝐴 ↦ ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) ) ) ) ‘ 𝑥 ) / ( ( ℝ D ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) ) ‘ 𝑥 ) ) )
387	386	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑥 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑥 ) ) / ( ( 𝑥 − 𝐵 ) ↑ 𝑀 ) ) · ( 1 / ( 𝑀 + 1 ) ) ) ) = ( 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ℝ D ( 𝑦 ∈ 𝐴 ↦ ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) ) ) ) ‘ 𝑥 ) / ( ( ℝ D ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) ) ‘ 𝑥 ) ) ) )
388	387	oveq1d	⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑥 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − 𝑀 ) ) ‘ 𝑥 ) ) / ( ( 𝑥 − 𝐵 ) ↑ 𝑀 ) ) · ( 1 / ( 𝑀 + 1 ) ) ) ) lim_ℂ 𝐵 ) = ( ( 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ℝ D ( 𝑦 ∈ 𝐴 ↦ ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) ) ) ) ‘ 𝑥 ) / ( ( ℝ D ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) ) ‘ 𝑥 ) ) ) lim_ℂ 𝐵 ) )
389	360 361 388	3eltr3d	⊢ ( 𝜑 → 0 ∈ ( ( 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ℝ D ( 𝑦 ∈ 𝐴 ↦ ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) ) ) ) ‘ 𝑥 ) / ( ( ℝ D ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) ) ‘ 𝑥 ) ) ) lim_ℂ 𝐵 ) )
390	2 71 84 124 5 125 183 237 259 272 293 314 389	lhop	⊢ ( 𝜑 → 0 ∈ ( ( 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( 𝑦 ∈ 𝐴 ↦ ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) ) ) ‘ 𝑥 ) / ( ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) ‘ 𝑥 ) ) ) lim_ℂ 𝐵 ) )
391	315	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 𝑥 ∈ 𝐴 )
392		fveq2	⊢ ( 𝑦 = 𝑥 → ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) = ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑥 ) )
393		fveq2	⊢ ( 𝑦 = 𝑥 → ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) = ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑥 ) )
394	392 393	oveq12d	⊢ ( 𝑦 = 𝑥 → ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) ) = ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑥 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑥 ) ) )
395		eqid	⊢ ( 𝑦 ∈ 𝐴 ↦ ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) ) ) = ( 𝑦 ∈ 𝐴 ↦ ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) ) )
396		ovex	⊢ ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑥 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑥 ) ) ∈ V
397	394 395 396	fvmpt	⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝑦 ∈ 𝐴 ↦ ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) ) ) ‘ 𝑥 ) = ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑥 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑥 ) ) )
398	391 397	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( ( 𝑦 ∈ 𝐴 ↦ ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) ) ) ‘ 𝑥 ) = ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑥 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑥 ) ) )
399	371	oveq1d	⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) = ( ( 𝑥 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) )
400		eqid	⊢ ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) = ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) )
401		ovex	⊢ ( ( 𝑥 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ∈ V
402	399 400 401	fvmpt	⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) ‘ 𝑥 ) = ( ( 𝑥 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) )
403	391 402	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) ‘ 𝑥 ) = ( ( 𝑥 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) )
404	398 403	oveq12d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( ( ( 𝑦 ∈ 𝐴 ↦ ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) ) ) ‘ 𝑥 ) / ( ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) ‘ 𝑥 ) ) = ( ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑥 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑥 ) ) / ( ( 𝑥 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) )
405	404	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( 𝑦 ∈ 𝐴 ↦ ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) ) ) ‘ 𝑥 ) / ( ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑥 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑥 ) ) / ( ( 𝑥 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) ) )
406	405	oveq1d	⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( 𝑦 ∈ 𝐴 ↦ ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑦 ) ) ) ‘ 𝑥 ) / ( ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑦 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) ‘ 𝑥 ) ) ) lim_ℂ 𝐵 ) = ( ( 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑥 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑥 ) ) / ( ( 𝑥 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) ) lim_ℂ 𝐵 ) )
407	390 406	eleqtrd	⊢ ( 𝜑 → 0 ∈ ( ( 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑥 ) − ( ( ( ℂ D^𝑛 𝑇 ) ‘ ( 𝑁 − ( 𝑀 + 1 ) ) ) ‘ 𝑥 ) ) / ( ( 𝑥 − 𝐵 ) ↑ ( 𝑀 + 1 ) ) ) ) lim_ℂ 𝐵 ) )

Metamath Proof Explorer

Theorem taylthlem2OLD

Proof