Theorem taylthlem2OLD 26417

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

Hypotheses

Ref	Expression
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

Ref	Expression
taylthlem2OLD	⊢ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑀 + 1)))) limℂ 𝐵))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐹   𝑥,𝑀   𝑥,𝑇   𝑥,𝑁   𝜑,𝑥

Proof of Theorem taylthlem2OLD

Dummy variables 𝑦 𝑘 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		taylth.a	. . 3 ⊢ (𝜑 → 𝐴 ⊆ ℝ)
2		taylth.f	. . . . . . . 8 ⊢ (𝜑 → 𝐹:𝐴⟶ℝ)
3		fz1ssfz0 13663	. . . . . . . . . . 11 ⊢ (1...𝑁) ⊆ (0...𝑁)
4		taylthlem2.m	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ (1..^𝑁))
5		fzofzp1 13803	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ (1..^𝑁) → (𝑀 + 1) ∈ (1...𝑁))
6	4, 5	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀 + 1) ∈ (1...𝑁))
7	3, 6	sselid 3981	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀 + 1) ∈ (0...𝑁))
8		fznn0sub2 13675	. . . . . . . . . 10 ⊢ ((𝑀 + 1) ∈ (0...𝑁) → (𝑁 − (𝑀 + 1)) ∈ (0...𝑁))
9	7, 8	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 − (𝑀 + 1)) ∈ (0...𝑁))
10		elfznn0 13660	. . . . . . . . 9 ⊢ ((𝑁 − (𝑀 + 1)) ∈ (0...𝑁) → (𝑁 − (𝑀 + 1)) ∈ ℕ0)
11	9, 10	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑁 − (𝑀 + 1)) ∈ ℕ0)
12		dvnfre 25990	. . . . . . . 8 ⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ ∧ (𝑁 − (𝑀 + 1)) ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))⟶ℝ)
13	2, 1, 11, 12	syl3anc 1373	. . . . . . 7 ⊢ (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))⟶ℝ)
14		reelprrecn 11247	. . . . . . . . . . . 12 ⊢ ℝ ∈ {ℝ, ℂ}
15	14	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})
16		cnex 11236	. . . . . . . . . . . . 13 ⊢ ℂ ∈ V
17	16	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ℂ ∈ V)
18		reex 11246	. . . . . . . . . . . . 13 ⊢ ℝ ∈ V
19	18	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ℝ ∈ V)
20		ax-resscn 11212	. . . . . . . . . . . . 13 ⊢ ℝ ⊆ ℂ
21		fss 6752	. . . . . . . . . . . . 13 ⊢ ((𝐹:𝐴⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐹:𝐴⟶ℂ)
22	2, 20, 21	sylancl 586	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)
23		elpm2r 8885	. . . . . . . . . . . 12 ⊢ (((ℂ ∈ V ∧ ℝ ∈ V) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ)) → 𝐹 ∈ (ℂ ↑pm ℝ))
24	17, 19, 22, 1, 23	syl22anc 839	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ (ℂ ↑pm ℝ))
25		dvnbss 25964	. . . . . . . . . . 11 ⊢ ((ℝ ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm ℝ) ∧ (𝑁 − (𝑀 + 1)) ∈ ℕ0) → dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) ⊆ dom 𝐹)
26	15, 24, 11, 25	syl3anc 1373	. . . . . . . . . 10 ⊢ (𝜑 → dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) ⊆ dom 𝐹)
27	2, 26	fssdmd 6754	. . . . . . . . 9 ⊢ (𝜑 → dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) ⊆ 𝐴)
28		taylth.d	. . . . . . . . . 10 ⊢ (𝜑 → dom ((ℝ D𝑛 𝐹)‘𝑁) = 𝐴)
29		dvn2bss 25966	. . . . . . . . . . 11 ⊢ ((ℝ ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm ℝ) ∧ (𝑁 − (𝑀 + 1)) ∈ (0...𝑁)) → dom ((ℝ D𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))))
30	15, 24, 9, 29	syl3anc 1373	. . . . . . . . . 10 ⊢ (𝜑 → dom ((ℝ D𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))))
31	28, 30	eqsstrrd 4019	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ⊆ dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))))
32	27, 31	eqssd 4001	. . . . . . . 8 ⊢ (𝜑 → dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) = 𝐴)
33	32	feq2d 6722	. . . . . . 7 ⊢ (𝜑 → (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))⟶ℝ ↔ ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℝ))
34	13, 33	mpbid 232	. . . . . 6 ⊢ (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℝ)
35	34	ffvelcdmda 7104	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℝ)
36	1	sselda 3983	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ)
37		fvres 6925	. . . . . . . 8 ⊢ (𝑦 ∈ ℝ → ((((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ↾ ℝ)‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))
38	37	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ↾ ℝ)‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))
39		resubdrg 21626	. . . . . . . . . . . 12 ⊢ (ℝ ∈ (SubRing‘ℂfld) ∧ ℝfld ∈ DivRing)
40	39	simpli 483	. . . . . . . . . . 11 ⊢ ℝ ∈ (SubRing‘ℂfld)
41	40	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ℝ ∈ (SubRing‘ℂfld))
42		taylth.n	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℕ)
43	42	nnnn0d 12587	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℕ0)
44		taylth.b	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ 𝐴)
45	44, 28	eleqtrrd 2844	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ dom ((ℝ D𝑛 𝐹)‘𝑁))
46		taylth.t	. . . . . . . . . . . 12 ⊢ 𝑇 = (𝑁(ℝ Tayl 𝐹)𝐵)
47	1, 44	sseldd 3984	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ ℝ)
48		elfznn0 13660	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0)
49		dvnfre 25990	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ ∧ 𝑘 ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘𝑘):dom ((ℝ D𝑛 𝐹)‘𝑘)⟶ℝ)
50	2, 1, 48, 49	syl2an3an 1424	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((ℝ D𝑛 𝐹)‘𝑘):dom ((ℝ D𝑛 𝐹)‘𝑘)⟶ℝ)
51		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ (0...𝑁))
52		dvn2bss 25966	. . . . . . . . . . . . . . . 16 ⊢ ((ℝ ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm ℝ) ∧ 𝑘 ∈ (0...𝑁)) → dom ((ℝ D𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ D𝑛 𝐹)‘𝑘))
53	14, 24, 51, 52	mp3an2ani 1470	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → dom ((ℝ D𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ D𝑛 𝐹)‘𝑘))
54	45	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐵 ∈ dom ((ℝ D𝑛 𝐹)‘𝑁))
55	53, 54	sseldd 3984	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐵 ∈ dom ((ℝ D𝑛 𝐹)‘𝑘))
56	50, 55	ffvelcdmd 7105	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (((ℝ D𝑛 𝐹)‘𝑘)‘𝐵) ∈ ℝ)
57	48	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
58	57	faccld 14323	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ)
59	56, 58	nndivred 12320	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((((ℝ D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) ∈ ℝ)
60	15, 22, 1, 43, 45, 46, 41, 47, 59	taylply2 26409	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑇 ∈ (Poly‘ℝ) ∧ (deg‘𝑇) ≤ 𝑁))
61	60	simpld 494	. . . . . . . . . 10 ⊢ (𝜑 → 𝑇 ∈ (Poly‘ℝ))
62		dvnply2 26329	. . . . . . . . . 10 ⊢ ((ℝ ∈ (SubRing‘ℂfld) ∧ 𝑇 ∈ (Poly‘ℝ) ∧ (𝑁 − (𝑀 + 1)) ∈ ℕ0) → ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (Poly‘ℝ))
63	41, 61, 11, 62	syl3anc 1373	. . . . . . . . 9 ⊢ (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (Poly‘ℝ))
64		plyreres 26324	. . . . . . . . 9 ⊢ (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (Poly‘ℝ) → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ↾ ℝ):ℝ⟶ℝ)
65	63, 64	syl 17	. . . . . . . 8 ⊢ (𝜑 → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ↾ ℝ):ℝ⟶ℝ)
66	65	ffvelcdmda 7104	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ↾ ℝ)‘𝑦) ∈ ℝ)
67	38, 66	eqeltrrd 2842	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℝ)
68	36, 67	syldan 591	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℝ)
69	35, 68	resubcld 11691	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)) ∈ ℝ)
70	69	fmpttd 7135	. . 3 ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))):𝐴⟶ℝ)
71	47	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝐵 ∈ ℝ)
72	36, 71	resubcld 11691	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑦 − 𝐵) ∈ ℝ)
73		elfzouz 13703	. . . . . . . . . 10 ⊢ (𝑀 ∈ (1..^𝑁) → 𝑀 ∈ (ℤ≥‘1))
74	4, 73	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘1))
75		nnuz 12921	. . . . . . . . 9 ⊢ ℕ = (ℤ≥‘1)
76	74, 75	eleqtrrdi 2852	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℕ)
77	76	nnnn0d 12587	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℕ0)
78	77	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑀 ∈ ℕ0)
79		1nn0 12542	. . . . . . 7 ⊢ 1 ∈ ℕ0
80	79	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 1 ∈ ℕ0)
81	78, 80	nn0addcld 12591	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑀 + 1) ∈ ℕ0)
82	72, 81	reexpcld 14203	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ((𝑦 − 𝐵)↑(𝑀 + 1)) ∈ ℝ)
83	82	fmpttd 7135	. . 3 ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))):𝐴⟶ℝ)
84		retop 24782	. . . . . 6 ⊢ (topGen‘ran (,)) ∈ Top
85		uniretop 24783	. . . . . . 7 ⊢ ℝ = ∪ (topGen‘ran (,))
86	85	ntrss2 23065	. . . . . 6 ⊢ (((topGen‘ran (,)) ∈ Top ∧ 𝐴 ⊆ ℝ) → ((int‘(topGen‘ran (,)))‘𝐴) ⊆ 𝐴)
87	84, 1, 86	sylancr 587	. . . . 5 ⊢ (𝜑 → ((int‘(topGen‘ran (,)))‘𝐴) ⊆ 𝐴)
88	42	nncnd 12282	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℂ)
89	76	nncnd 12282	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℂ)
90		1cnd 11256	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ ℂ)
91	88, 89, 90	nppcan2d 11646	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑁 − (𝑀 + 1)) + 1) = (𝑁 − 𝑀))
92	91	fveq2d 6910	. . . . . . . . 9 ⊢ (𝜑 → ((ℝ D𝑛 𝐹)‘((𝑁 − (𝑀 + 1)) + 1)) = ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)))
93	20	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ℝ ⊆ ℂ)
94		dvnp1 25961	. . . . . . . . . 10 ⊢ ((ℝ ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm ℝ) ∧ (𝑁 − (𝑀 + 1)) ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘((𝑁 − (𝑀 + 1)) + 1)) = (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))))
95	93, 24, 11, 94	syl3anc 1373	. . . . . . . . 9 ⊢ (𝜑 → ((ℝ D𝑛 𝐹)‘((𝑁 − (𝑀 + 1)) + 1)) = (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))))
96	92, 95	eqtr3d 2779	. . . . . . . 8 ⊢ (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)) = (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))))
97	96	dmeqd 5916	. . . . . . 7 ⊢ (𝜑 → dom ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)) = dom (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))))
98		fzonnsub 13724	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ (1..^𝑁) → (𝑁 − 𝑀) ∈ ℕ)
99	4, 98	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 − 𝑀) ∈ ℕ)
100	99	nnnn0d 12587	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 − 𝑀) ∈ ℕ0)
101		dvnbss 25964	. . . . . . . . . 10 ⊢ ((ℝ ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm ℝ) ∧ (𝑁 − 𝑀) ∈ ℕ0) → dom ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)) ⊆ dom 𝐹)
102	15, 24, 100, 101	syl3anc 1373	. . . . . . . . 9 ⊢ (𝜑 → dom ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)) ⊆ dom 𝐹)
103	2, 102	fssdmd 6754	. . . . . . . 8 ⊢ (𝜑 → dom ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)) ⊆ 𝐴)
104		elfzofz 13715	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ (1..^𝑁) → 𝑀 ∈ (1...𝑁))
105	4, 104	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ (1...𝑁))
106	3, 105	sselid 3981	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ (0...𝑁))
107		fznn0sub2 13675	. . . . . . . . . . 11 ⊢ (𝑀 ∈ (0...𝑁) → (𝑁 − 𝑀) ∈ (0...𝑁))
108	106, 107	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 − 𝑀) ∈ (0...𝑁))
109		dvn2bss 25966	. . . . . . . . . 10 ⊢ ((ℝ ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm ℝ) ∧ (𝑁 − 𝑀) ∈ (0...𝑁)) → dom ((ℝ D𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)))
110	15, 24, 108, 109	syl3anc 1373	. . . . . . . . 9 ⊢ (𝜑 → dom ((ℝ D𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)))
111	28, 110	eqsstrrd 4019	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ⊆ dom ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)))
112	103, 111	eqssd 4001	. . . . . . 7 ⊢ (𝜑 → dom ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)) = 𝐴)
113	97, 112	eqtr3d 2779	. . . . . 6 ⊢ (𝜑 → dom (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))) = 𝐴)
114		fss 6752	. . . . . . . 8 ⊢ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℝ ∧ ℝ ⊆ ℂ) → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℂ)
115	34, 20, 114	sylancl 586	. . . . . . 7 ⊢ (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℂ)
116		eqid 2737	. . . . . . . 8 ⊢ (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
117	116	tgioo2 24824	. . . . . . 7 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
118	93, 115, 1, 117, 116	dvbssntr 25935	. . . . . 6 ⊢ (𝜑 → dom (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))) ⊆ ((int‘(topGen‘ran (,)))‘𝐴))
119	113, 118	eqsstrrd 4019	. . . . 5 ⊢ (𝜑 → 𝐴 ⊆ ((int‘(topGen‘ran (,)))‘𝐴))
120	87, 119	eqssd 4001	. . . 4 ⊢ (𝜑 → ((int‘(topGen‘ran (,)))‘𝐴) = 𝐴)
121	85	isopn3 23074	. . . . 5 ⊢ (((topGen‘ran (,)) ∈ Top ∧ 𝐴 ⊆ ℝ) → (𝐴 ∈ (topGen‘ran (,)) ↔ ((int‘(topGen‘ran (,)))‘𝐴) = 𝐴))
122	84, 1, 121	sylancr 587	. . . 4 ⊢ (𝜑 → (𝐴 ∈ (topGen‘ran (,)) ↔ ((int‘(topGen‘ran (,)))‘𝐴) = 𝐴))
123	120, 122	mpbird 257	. . 3 ⊢ (𝜑 → 𝐴 ∈ (topGen‘ran (,)))
124		eqid 2737	. . 3 ⊢ (𝐴 ∖ {𝐵}) = (𝐴 ∖ {𝐵})
125		difss 4136	. . . 4 ⊢ (𝐴 ∖ {𝐵}) ⊆ 𝐴
126	35	recnd 11289	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℂ)
127		dvnf 25963	. . . . . . . . . 10 ⊢ ((ℝ ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm ℝ) ∧ (𝑁 − 𝑀) ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)):dom ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))⟶ℂ)
128	15, 24, 100, 127	syl3anc 1373	. . . . . . . . 9 ⊢ (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)):dom ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))⟶ℂ)
129	112	feq2d 6722	. . . . . . . . 9 ⊢ (𝜑 → (((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)):dom ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))⟶ℂ ↔ ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)):𝐴⟶ℂ))
130	128, 129	mpbid 232	. . . . . . . 8 ⊢ (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)):𝐴⟶ℂ)
131	130	ffvelcdmda 7104	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑦) ∈ ℂ)
132		dvnfre 25990	. . . . . . . . . . 11 ⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ ∧ (𝑁 − 𝑀) ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)):dom ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))⟶ℝ)
133	2, 1, 100, 132	syl3anc 1373	. . . . . . . . . 10 ⊢ (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)):dom ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))⟶ℝ)
134	112	feq2d 6722	. . . . . . . . . 10 ⊢ (𝜑 → (((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)):dom ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))⟶ℝ ↔ ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)):𝐴⟶ℝ))
135	133, 134	mpbid 232	. . . . . . . . 9 ⊢ (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)):𝐴⟶ℝ)
136	135	feqmptd 6977	. . . . . . . 8 ⊢ (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)) = (𝑦 ∈ 𝐴 ↦ (((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑦)))
137	34	feqmptd 6977	. . . . . . . . 9 ⊢ (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) = (𝑦 ∈ 𝐴 ↦ (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦)))
138	137	oveq2d 7447	. . . . . . . 8 ⊢ (𝜑 → (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))) = (ℝ D (𝑦 ∈ 𝐴 ↦ (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦))))
139	96, 136, 138	3eqtr3rd 2786	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝑦 ∈ 𝐴 ↦ (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦))) = (𝑦 ∈ 𝐴 ↦ (((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑦)))
140	68	recnd 11289	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℂ)
141		fvexd 6921	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦) ∈ V)
142	67	recnd 11289	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℂ)
143		recn 11245	. . . . . . . . 9 ⊢ (𝑦 ∈ ℝ → 𝑦 ∈ ℂ)
144		dvnply2 26329	. . . . . . . . . . . 12 ⊢ ((ℝ ∈ (SubRing‘ℂfld) ∧ 𝑇 ∈ (Poly‘ℝ) ∧ (𝑁 − 𝑀) ∈ ℕ0) → ((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀)) ∈ (Poly‘ℝ))
145	41, 61, 100, 144	syl3anc 1373	. . . . . . . . . . 11 ⊢ (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀)) ∈ (Poly‘ℝ))
146		plyf 26237	. . . . . . . . . . 11 ⊢ (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀)) ∈ (Poly‘ℝ) → ((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀)):ℂ⟶ℂ)
147	145, 146	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀)):ℂ⟶ℂ)
148	147	ffvelcdmda 7104	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦) ∈ ℂ)
149	143, 148	sylan2 593	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦) ∈ ℂ)
150	116	cnfldtopon 24803	. . . . . . . . . 10 ⊢ (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
151		toponmax 22932	. . . . . . . . . 10 ⊢ ((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) → ℂ ∈ (TopOpen‘ℂfld))
152	150, 151	mp1i 13	. . . . . . . . 9 ⊢ (𝜑 → ℂ ∈ (TopOpen‘ℂfld))
153		dfss2 3969	. . . . . . . . . 10 ⊢ (ℝ ⊆ ℂ ↔ (ℝ ∩ ℂ) = ℝ)
154	93, 153	sylib 218	. . . . . . . . 9 ⊢ (𝜑 → (ℝ ∩ ℂ) = ℝ)
155		plyf 26237	. . . . . . . . . . 11 ⊢ (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (Poly‘ℝ) → ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))):ℂ⟶ℂ)
156	63, 155	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))):ℂ⟶ℂ)
157	156	ffvelcdmda 7104	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℂ)
158	91	fveq2d 6910	. . . . . . . . . . 11 ⊢ (𝜑 → ((ℂ D𝑛 𝑇)‘((𝑁 − (𝑀 + 1)) + 1)) = ((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀)))
159		ssid 4006	. . . . . . . . . . . . 13 ⊢ ℂ ⊆ ℂ
160	159	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ℂ ⊆ ℂ)
161		mapsspm 8916	. . . . . . . . . . . . 13 ⊢ (ℂ ↑m ℂ) ⊆ (ℂ ↑pm ℂ)
162		plyf 26237	. . . . . . . . . . . . . . 15 ⊢ (𝑇 ∈ (Poly‘ℝ) → 𝑇:ℂ⟶ℂ)
163	61, 162	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑇:ℂ⟶ℂ)
164	16, 16	elmap 8911	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ (ℂ ↑m ℂ) ↔ 𝑇:ℂ⟶ℂ)
165	163, 164	sylibr 234	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑇 ∈ (ℂ ↑m ℂ))
166	161, 165	sselid 3981	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑇 ∈ (ℂ ↑pm ℂ))
167		dvnp1 25961	. . . . . . . . . . . 12 ⊢ ((ℂ ⊆ ℂ ∧ 𝑇 ∈ (ℂ ↑pm ℂ) ∧ (𝑁 − (𝑀 + 1)) ∈ ℕ0) → ((ℂ D𝑛 𝑇)‘((𝑁 − (𝑀 + 1)) + 1)) = (ℂ D ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))))
168	160, 166, 11, 167	syl3anc 1373	. . . . . . . . . . 11 ⊢ (𝜑 → ((ℂ D𝑛 𝑇)‘((𝑁 − (𝑀 + 1)) + 1)) = (ℂ D ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))))
169	158, 168	eqtr3d 2779	. . . . . . . . . 10 ⊢ (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀)) = (ℂ D ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))))
170	147	feqmptd 6977	. . . . . . . . . 10 ⊢ (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀)) = (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦)))
171	156	feqmptd 6977	. . . . . . . . . . 11 ⊢ (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) = (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))
172	171	oveq2d 7447	. . . . . . . . . 10 ⊢ (𝜑 → (ℂ D ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))) = (ℂ D (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))
173	169, 170, 172	3eqtr3rd 2786	. . . . . . . . 9 ⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) = (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦)))
174	116, 15, 152, 154, 157, 148, 173	dvmptres3 25994	. . . . . . . 8 ⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) = (𝑦 ∈ ℝ ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦)))
175	15, 142, 149, 174, 1, 117, 116, 123	dvmptres 26001	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝑦 ∈ 𝐴 ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) = (𝑦 ∈ 𝐴 ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦)))
176	15, 126, 131, 139, 140, 141, 175	dvmptsub 26005	. . . . . 6 ⊢ (𝜑 → (ℝ D (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))) = (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦))))
177	176	dmeqd 5916	. . . . 5 ⊢ (𝜑 → dom (ℝ D (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))) = dom (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦))))
178		ovex 7464	. . . . . 6 ⊢ ((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦)) ∈ V
179		eqid 2737	. . . . . 6 ⊢ (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦))) = (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦)))
180	178, 179	dmmpti 6712	. . . . 5 ⊢ dom (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦))) = 𝐴
181	177, 180	eqtrdi 2793	. . . 4 ⊢ (𝜑 → dom (ℝ D (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))) = 𝐴)
182	125, 181	sseqtrrid 4027	. . 3 ⊢ (𝜑 → (𝐴 ∖ {𝐵}) ⊆ dom (ℝ D (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))))
183		simpr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝑦 ∈ ℂ)
184	47	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝐵 ∈ ℝ)
185	184	recnd 11289	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝐵 ∈ ℂ)
186	183, 185	subcld 11620	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝑦 − 𝐵) ∈ ℂ)
187	77	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝑀 ∈ ℕ0)
188	79	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 1 ∈ ℕ0)
189	187, 188	nn0addcld 12591	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝑀 + 1) ∈ ℕ0)
190	186, 189	expcld 14186	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((𝑦 − 𝐵)↑(𝑀 + 1)) ∈ ℂ)
191	143, 190	sylan2 593	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑦 − 𝐵)↑(𝑀 + 1)) ∈ ℂ)
192	89	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝑀 ∈ ℂ)
193		1cnd 11256	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 1 ∈ ℂ)
194	192, 193	addcld 11280	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝑀 + 1) ∈ ℂ)
195	186, 187	expcld 14186	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((𝑦 − 𝐵)↑𝑀) ∈ ℂ)
196	194, 195	mulcld 11281	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)) ∈ ℂ)
197	143, 196	sylan2 593	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)) ∈ ℂ)
198	16	prid2 4763	. . . . . . . . . . 11 ⊢ ℂ ∈ {ℝ, ℂ}
199	198	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ℂ ∈ {ℝ, ℂ})
200		simpr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝑥 ∈ ℂ)
201		elfznn 13593	. . . . . . . . . . . . . 14 ⊢ ((𝑀 + 1) ∈ (1...𝑁) → (𝑀 + 1) ∈ ℕ)
202	6, 201	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑀 + 1) ∈ ℕ)
203	202	nnnn0d 12587	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀 + 1) ∈ ℕ0)
204	203	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝑀 + 1) ∈ ℕ0)
205	200, 204	expcld 14186	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝑥↑(𝑀 + 1)) ∈ ℂ)
206		ovexd 7466	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((𝑀 + 1) · (𝑥↑𝑀)) ∈ V)
207	199	dvmptid 25995	. . . . . . . . . . . 12 ⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ 𝑦)) = (𝑦 ∈ ℂ ↦ 1))
208		0cnd 11254	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 0 ∈ ℂ)
209	47	recnd 11289	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ ℂ)
210	199, 209	dvmptc 25996	. . . . . . . . . . . 12 ⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ 𝐵)) = (𝑦 ∈ ℂ ↦ 0))
211	199, 183, 193, 207, 185, 208, 210	dvmptsub 26005	. . . . . . . . . . 11 ⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦 − 𝐵))) = (𝑦 ∈ ℂ ↦ (1 − 0)))
212		1m0e1 12387	. . . . . . . . . . . 12 ⊢ (1 − 0) = 1
213	212	mpteq2i 5247	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℂ ↦ (1 − 0)) = (𝑦 ∈ ℂ ↦ 1)
214	211, 213	eqtrdi 2793	. . . . . . . . . 10 ⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦 − 𝐵))) = (𝑦 ∈ ℂ ↦ 1))
215		dvexp 25991	. . . . . . . . . . . 12 ⊢ ((𝑀 + 1) ∈ ℕ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑(𝑀 + 1)))) = (𝑥 ∈ ℂ ↦ ((𝑀 + 1) · (𝑥↑((𝑀 + 1) − 1)))))
216	202, 215	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑(𝑀 + 1)))) = (𝑥 ∈ ℂ ↦ ((𝑀 + 1) · (𝑥↑((𝑀 + 1) − 1)))))
217	89, 90	pncand 11621	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀 + 1) − 1) = 𝑀)
218	217	oveq2d 7447	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥↑((𝑀 + 1) − 1)) = (𝑥↑𝑀))
219	218	oveq2d 7447	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑀 + 1) · (𝑥↑((𝑀 + 1) − 1))) = ((𝑀 + 1) · (𝑥↑𝑀)))
220	219	mpteq2dv 5244	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((𝑀 + 1) · (𝑥↑((𝑀 + 1) − 1)))) = (𝑥 ∈ ℂ ↦ ((𝑀 + 1) · (𝑥↑𝑀))))
221	216, 220	eqtrd 2777	. . . . . . . . . 10 ⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑(𝑀 + 1)))) = (𝑥 ∈ ℂ ↦ ((𝑀 + 1) · (𝑥↑𝑀))))
222		oveq1 7438	. . . . . . . . . 10 ⊢ (𝑥 = (𝑦 − 𝐵) → (𝑥↑(𝑀 + 1)) = ((𝑦 − 𝐵)↑(𝑀 + 1)))
223		oveq1 7438	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑦 − 𝐵) → (𝑥↑𝑀) = ((𝑦 − 𝐵)↑𝑀))
224	223	oveq2d 7447	. . . . . . . . . 10 ⊢ (𝑥 = (𝑦 − 𝐵) → ((𝑀 + 1) · (𝑥↑𝑀)) = ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)))
225	199, 199, 186, 193, 205, 206, 214, 221, 222, 224	dvmptco 26010	. . . . . . . . 9 ⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) = (𝑦 ∈ ℂ ↦ (((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)) · 1)))
226	196	mulridd 11278	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)) · 1) = ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)))
227	226	mpteq2dva 5242	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ ℂ ↦ (((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)) · 1)) = (𝑦 ∈ ℂ ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))))
228	225, 227	eqtrd 2777	. . . . . . . 8 ⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) = (𝑦 ∈ ℂ ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))))
229	116, 15, 152, 154, 190, 196, 228	dvmptres3 25994	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) = (𝑦 ∈ ℝ ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))))
230	15, 191, 197, 229, 1, 117, 116, 123	dvmptres 26001	. . . . . 6 ⊢ (𝜑 → (ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) = (𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))))
231	230	dmeqd 5916	. . . . 5 ⊢ (𝜑 → dom (ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) = dom (𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))))
232		ovex 7464	. . . . . 6 ⊢ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)) ∈ V
233		eqid 2737	. . . . . 6 ⊢ (𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) = (𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)))
234	232, 233	dmmpti 6712	. . . . 5 ⊢ dom (𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) = 𝐴
235	231, 234	eqtrdi 2793	. . . 4 ⊢ (𝜑 → dom (ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) = 𝐴)
236	125, 235	sseqtrrid 4027	. . 3 ⊢ (𝜑 → (𝐴 ∖ {𝐵}) ⊆ dom (ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))))
237	15, 22, 1, 9, 45, 46	dvntaylp0 26414	. . . . . 6 ⊢ (𝜑 → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵) = (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵))
238	237	oveq2d 7447	. . . . 5 ⊢ (𝜑 → ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵)) = ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵)))
239	115, 44	ffvelcdmd 7105	. . . . . 6 ⊢ (𝜑 → (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) ∈ ℂ)
240	239	subidd 11608	. . . . 5 ⊢ (𝜑 → ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵)) = 0)
241	238, 240	eqtrd 2777	. . . 4 ⊢ (𝜑 → ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵)) = 0)
242	116	subcn 24888	. . . . . . 7 ⊢ − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
243	242	a1i 11	. . . . . 6 ⊢ (𝜑 → − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)))
244		dvcn 25957	. . . . . . . 8 ⊢ (((ℝ ⊆ ℂ ∧ ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) ∧ dom (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))) = 𝐴) → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) ∈ (𝐴–cn→ℂ))
245	93, 115, 1, 113, 244	syl31anc 1375	. . . . . . 7 ⊢ (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) ∈ (𝐴–cn→ℂ))
246	137, 245	eqeltrrd 2842	. . . . . 6 ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦)) ∈ (𝐴–cn→ℂ))
247		plycn 26300	. . . . . . . 8 ⊢ (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (Poly‘ℝ) → ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (ℂ–cn→ℂ))
248	63, 247	syl 17	. . . . . . 7 ⊢ (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (ℂ–cn→ℂ))
249	1, 20	sstrdi 3996	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ⊆ ℂ)
250		cncfmptid 24939	. . . . . . . 8 ⊢ ((𝐴 ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑦 ∈ 𝐴 ↦ 𝑦) ∈ (𝐴–cn→ℂ))
251	249, 159, 250	sylancl 586	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ 𝑦) ∈ (𝐴–cn→ℂ))
252	248, 251	cncfmpt1f 24940	. . . . . 6 ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)) ∈ (𝐴–cn→ℂ))
253	116, 243, 246, 252	cncfmpt2f 24941	. . . . 5 ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) ∈ (𝐴–cn→ℂ))
254		fveq2 6906	. . . . . 6 ⊢ (𝑦 = 𝐵 → (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) = (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵))
255		fveq2 6906	. . . . . 6 ⊢ (𝑦 = 𝐵 → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵))
256	254, 255	oveq12d 7449	. . . . 5 ⊢ (𝑦 = 𝐵 → ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)) = ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵)))
257	253, 44, 256	cnmptlimc 25925	. . . 4 ⊢ (𝜑 → ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵)) ∈ ((𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) limℂ 𝐵))
258	241, 257	eqeltrrd 2842	. . 3 ⊢ (𝜑 → 0 ∈ ((𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) limℂ 𝐵))
259	209	subidd 11608	. . . . . 6 ⊢ (𝜑 → (𝐵 − 𝐵) = 0)
260	259	oveq1d 7446	. . . . 5 ⊢ (𝜑 → ((𝐵 − 𝐵)↑(𝑀 + 1)) = (0↑(𝑀 + 1)))
261	202	0expd 14179	. . . . 5 ⊢ (𝜑 → (0↑(𝑀 + 1)) = 0)
262	260, 261	eqtrd 2777	. . . 4 ⊢ (𝜑 → ((𝐵 − 𝐵)↑(𝑀 + 1)) = 0)
263	249	sselda 3983	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℂ)
264	263, 190	syldan 591	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ((𝑦 − 𝐵)↑(𝑀 + 1)) ∈ ℂ)
265	264	fmpttd 7135	. . . . . 6 ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))):𝐴⟶ℂ)
266		dvcn 25957	. . . . . 6 ⊢ (((ℝ ⊆ ℂ ∧ (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))):𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) ∧ dom (ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) = 𝐴) → (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) ∈ (𝐴–cn→ℂ))
267	93, 265, 1, 235, 266	syl31anc 1375	. . . . 5 ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) ∈ (𝐴–cn→ℂ))
268		oveq1 7438	. . . . . 6 ⊢ (𝑦 = 𝐵 → (𝑦 − 𝐵) = (𝐵 − 𝐵))
269	268	oveq1d 7446	. . . . 5 ⊢ (𝑦 = 𝐵 → ((𝑦 − 𝐵)↑(𝑀 + 1)) = ((𝐵 − 𝐵)↑(𝑀 + 1)))
270	267, 44, 269	cnmptlimc 25925	. . . 4 ⊢ (𝜑 → ((𝐵 − 𝐵)↑(𝑀 + 1)) ∈ ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) limℂ 𝐵))
271	262, 270	eqeltrrd 2842	. . 3 ⊢ (𝜑 → 0 ∈ ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) limℂ 𝐵))
272	249	ssdifssd 4147	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 ∖ {𝐵}) ⊆ ℂ)
273	272	sselda 3983	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑦 ∈ ℂ)
274	209	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝐵 ∈ ℂ)
275	273, 274	subcld 11620	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑦 − 𝐵) ∈ ℂ)
276		eldifsni 4790	. . . . . . . . . 10 ⊢ (𝑦 ∈ (𝐴 ∖ {𝐵}) → 𝑦 ≠ 𝐵)
277	276	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑦 ≠ 𝐵)
278	273, 274, 277	subne0d 11629	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑦 − 𝐵) ≠ 0)
279	202	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ∈ ℕ)
280	279	nnzd 12640	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ∈ ℤ)
281	275, 278, 280	expne0d 14192	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → ((𝑦 − 𝐵)↑(𝑀 + 1)) ≠ 0)
282	281	necomd 2996	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → 0 ≠ ((𝑦 − 𝐵)↑(𝑀 + 1)))
283	282	neneqd 2945	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → ¬ 0 = ((𝑦 − 𝐵)↑(𝑀 + 1)))
284	283	nrexdv 3149	. . . 4 ⊢ (𝜑 → ¬ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑦 − 𝐵)↑(𝑀 + 1)))
285		df-ima 5698	. . . . . 6 ⊢ ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) “ (𝐴 ∖ {𝐵})) = ran ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) ↾ (𝐴 ∖ {𝐵}))
286	285	eleq2i 2833	. . . . 5 ⊢ (0 ∈ ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) “ (𝐴 ∖ {𝐵})) ↔ 0 ∈ ran ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})))
287		resmpt 6055	. . . . . . 7 ⊢ ((𝐴 ∖ {𝐵}) ⊆ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))))
288	125, 287	ax-mp 5	. . . . . 6 ⊢ ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))
289		ovex 7464	. . . . . 6 ⊢ ((𝑦 − 𝐵)↑(𝑀 + 1)) ∈ V
290	288, 289	elrnmpti 5973	. . . . 5 ⊢ (0 ∈ ran ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) ↔ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑦 − 𝐵)↑(𝑀 + 1)))
291	286, 290	bitri 275	. . . 4 ⊢ (0 ∈ ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) “ (𝐴 ∖ {𝐵})) ↔ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑦 − 𝐵)↑(𝑀 + 1)))
292	284, 291	sylnibr 329	. . 3 ⊢ (𝜑 → ¬ 0 ∈ ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) “ (𝐴 ∖ {𝐵})))
293	89	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑀 ∈ ℂ)
294		1cnd 11256	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → 1 ∈ ℂ)
295	293, 294	addcld 11280	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ∈ ℂ)
296	273, 195	syldan 591	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → ((𝑦 − 𝐵)↑𝑀) ∈ ℂ)
297	279	nnne0d 12316	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ≠ 0)
298	76	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑀 ∈ ℕ)
299	298	nnzd 12640	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑀 ∈ ℤ)
300	275, 278, 299	expne0d 14192	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → ((𝑦 − 𝐵)↑𝑀) ≠ 0)
301	295, 296, 297, 300	mulne0d 11915	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)) ≠ 0)
302	301	necomd 2996	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → 0 ≠ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)))
303	302	neneqd 2945	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → ¬ 0 = ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)))
304	303	nrexdv 3149	. . . 4 ⊢ (𝜑 → ¬ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)))
305	230	imaeq1d 6077	. . . . . . 7 ⊢ (𝜑 → ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) “ (𝐴 ∖ {𝐵})) = ((𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) “ (𝐴 ∖ {𝐵})))
306		df-ima 5698	. . . . . . 7 ⊢ ((𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) “ (𝐴 ∖ {𝐵})) = ran ((𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵}))
307	305, 306	eqtrdi 2793	. . . . . 6 ⊢ (𝜑 → ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) “ (𝐴 ∖ {𝐵})) = ran ((𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵})))
308	307	eleq2d 2827	. . . . 5 ⊢ (𝜑 → (0 ∈ ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) “ (𝐴 ∖ {𝐵})) ↔ 0 ∈ ran ((𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵}))))
309		resmpt 6055	. . . . . . 7 ⊢ ((𝐴 ∖ {𝐵}) ⊆ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵})) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))))
310	125, 309	ax-mp 5	. . . . . 6 ⊢ ((𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵})) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)))
311	310, 232	elrnmpti 5973	. . . . 5 ⊢ (0 ∈ ran ((𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵})) ↔ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)))
312	308, 311	bitrdi 287	. . . 4 ⊢ (𝜑 → (0 ∈ ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) “ (𝐴 ∖ {𝐵})) ↔ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))))
313	304, 312	mtbird 325	. . 3 ⊢ (𝜑 → ¬ 0 ∈ ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) “ (𝐴 ∖ {𝐵})))
314		eldifi 4131	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴 ∖ {𝐵}) → 𝑥 ∈ 𝐴)
315	130	ffvelcdmda 7104	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) ∈ ℂ)
316	314, 315	sylan2 593	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) ∈ ℂ)
317	1	ssdifssd 4147	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 ∖ {𝐵}) ⊆ ℝ)
318	317	sselda 3983	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ ℝ)
319	318	recnd 11289	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ ℂ)
320	147	ffvelcdmda 7104	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥) ∈ ℂ)
321	319, 320	syldan 591	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥) ∈ ℂ)
322	316, 321	subcld 11620	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) ∈ ℂ)
323	47	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝐵 ∈ ℝ)
324	318, 323	resubcld 11691	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑥 − 𝐵) ∈ ℝ)
325	77	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑀 ∈ ℕ0)
326	324, 325	reexpcld 14203	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑥 − 𝐵)↑𝑀) ∈ ℝ)
327	326	recnd 11289	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑥 − 𝐵)↑𝑀) ∈ ℂ)
328	323	recnd 11289	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝐵 ∈ ℂ)
329	319, 328	subcld 11620	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑥 − 𝐵) ∈ ℂ)
330		eldifsni 4790	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴 ∖ {𝐵}) → 𝑥 ≠ 𝐵)
331	330	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ≠ 𝐵)
332	319, 328, 331	subne0d 11629	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑥 − 𝐵) ≠ 0)
333	325	nn0zd 12639	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑀 ∈ ℤ)
334	329, 332, 333	expne0d 14192	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑥 − 𝐵)↑𝑀) ≠ 0)
335	322, 327, 334	divcld 12043	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) ∈ ℂ)
336	202	nnrecred 12317	. . . . . . 7 ⊢ (𝜑 → (1 / (𝑀 + 1)) ∈ ℝ)
337	336	recnd 11289	. . . . . 6 ⊢ (𝜑 → (1 / (𝑀 + 1)) ∈ ℂ)
338	337	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (1 / (𝑀 + 1)) ∈ ℂ)
339		txtopon 23599	. . . . . . 7 ⊢ (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) → ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ∈ (TopOn‘(ℂ × ℂ)))
340	150, 150, 339	mp2an 692	. . . . . 6 ⊢ ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ∈ (TopOn‘(ℂ × ℂ))
341	340	toponrestid 22927	. . . . 5 ⊢ ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) = (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ↾t (ℂ × ℂ))
342		taylthlem2.i	. . . . 5 ⊢ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀))) limℂ 𝐵))
343		limcresi 25920	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 ↦ (1 / (𝑀 + 1))) limℂ 𝐵) ⊆ (((𝑥 ∈ 𝐴 ↦ (1 / (𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) limℂ 𝐵)
344		resmpt 6055	. . . . . . . . 9 ⊢ ((𝐴 ∖ {𝐵}) ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ (1 / (𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (1 / (𝑀 + 1))))
345	125, 344	ax-mp 5	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 ↦ (1 / (𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (1 / (𝑀 + 1)))
346	345	oveq1i 7441	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐴 ↦ (1 / (𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) limℂ 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (1 / (𝑀 + 1))) limℂ 𝐵)
347	343, 346	sseqtri 4032	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ↦ (1 / (𝑀 + 1))) limℂ 𝐵) ⊆ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (1 / (𝑀 + 1))) limℂ 𝐵)
348		cncfmptc 24938	. . . . . . . 8 ⊢ (((1 / (𝑀 + 1)) ∈ ℝ ∧ 𝐴 ⊆ ℂ ∧ ℝ ⊆ ℂ) → (𝑥 ∈ 𝐴 ↦ (1 / (𝑀 + 1))) ∈ (𝐴–cn→ℝ))
349	336, 249, 93, 348	syl3anc 1373	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (1 / (𝑀 + 1))) ∈ (𝐴–cn→ℝ))
350		eqidd 2738	. . . . . . 7 ⊢ (𝑥 = 𝐵 → (1 / (𝑀 + 1)) = (1 / (𝑀 + 1)))
351	349, 44, 350	cnmptlimc 25925	. . . . . 6 ⊢ (𝜑 → (1 / (𝑀 + 1)) ∈ ((𝑥 ∈ 𝐴 ↦ (1 / (𝑀 + 1))) limℂ 𝐵))
352	347, 351	sselid 3981	. . . . 5 ⊢ (𝜑 → (1 / (𝑀 + 1)) ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (1 / (𝑀 + 1))) limℂ 𝐵))
353	116	mulcn 24889	. . . . . 6 ⊢ · ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
354		0cn 11253	. . . . . . 7 ⊢ 0 ∈ ℂ
355		opelxpi 5722	. . . . . . 7 ⊢ ((0 ∈ ℂ ∧ (1 / (𝑀 + 1)) ∈ ℂ) → ⟨0, (1 / (𝑀 + 1))⟩ ∈ (ℂ × ℂ))
356	354, 337, 355	sylancr 587	. . . . . 6 ⊢ (𝜑 → ⟨0, (1 / (𝑀 + 1))⟩ ∈ (ℂ × ℂ))
357	340	toponunii 22922	. . . . . . 7 ⊢ (ℂ × ℂ) = ∪ ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld))
358	357	cncnpi 23286	. . . . . 6 ⊢ (( · ∈ (((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 587	. . . . 5 ⊢ (𝜑 → · ∈ ((((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) CnP (TopOpen‘ℂfld))‘⟨0, (1 / (𝑀 + 1))⟩))
360	335, 338, 160, 160, 116, 341, 342, 352, 359	limccnp2 25927	. . . 4 ⊢ (𝜑 → (0 · (1 / (𝑀 + 1))) ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1)))) limℂ 𝐵))
361	337	mul02d 11459	. . . 4 ⊢ (𝜑 → (0 · (1 / (𝑀 + 1))) = 0)
362	176	fveq1d 6908	. . . . . . . . 9 ⊢ (𝜑 → ((ℝ D (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) = ((𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦)))‘𝑥))
363		fveq2 6906	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → (((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑦) = (((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥))
364		fveq2 6906	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥))
365	363, 364	oveq12d 7449	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 → ((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦)) = ((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)))
366		ovex 7464	. . . . . . . . . . 11 ⊢ ((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) ∈ V
367	365, 179, 366	fvmpt 7016	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦)))‘𝑥) = ((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)))
368	314, 367	syl 17	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴 ∖ {𝐵}) → ((𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦)))‘𝑥) = ((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)))
369	362, 368	sylan9eq 2797	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((ℝ D (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) = ((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)))
370	230	fveq1d 6908	. . . . . . . . . 10 ⊢ (𝜑 → ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))))‘𝑥) = ((𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)))‘𝑥))
371		oveq1 7438	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑥 → (𝑦 − 𝐵) = (𝑥 − 𝐵))
372	371	oveq1d 7446	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑥 → ((𝑦 − 𝐵)↑𝑀) = ((𝑥 − 𝐵)↑𝑀))
373	372	oveq2d 7447	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)) = ((𝑀 + 1) · ((𝑥 − 𝐵)↑𝑀)))
374		ovex 7464	. . . . . . . . . . . 12 ⊢ ((𝑀 + 1) · ((𝑥 − 𝐵)↑𝑀)) ∈ V
375	373, 233, 374	fvmpt 7016	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)))‘𝑥) = ((𝑀 + 1) · ((𝑥 − 𝐵)↑𝑀)))
376	314, 375	syl 17	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐴 ∖ {𝐵}) → ((𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)))‘𝑥) = ((𝑀 + 1) · ((𝑥 − 𝐵)↑𝑀)))
377	370, 376	sylan9eq 2797	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))))‘𝑥) = ((𝑀 + 1) · ((𝑥 − 𝐵)↑𝑀)))
378	202	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ∈ ℕ)
379	378	nncnd 12282	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ∈ ℂ)
380	379, 327	mulcomd 11282	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑀 + 1) · ((𝑥 − 𝐵)↑𝑀)) = (((𝑥 − 𝐵)↑𝑀) · (𝑀 + 1)))
381	377, 380	eqtrd 2777	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))))‘𝑥) = (((𝑥 − 𝐵)↑𝑀) · (𝑀 + 1)))
382	369, 381	oveq12d 7449	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (((ℝ D (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) / ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))))‘𝑥)) = (((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / (((𝑥 − 𝐵)↑𝑀) · (𝑀 + 1))))
383	378	nnne0d 12316	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ≠ 0)
384	322, 327, 379, 334, 383	divdiv1d 12074	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) / (𝑀 + 1)) = (((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / (((𝑥 − 𝐵)↑𝑀) · (𝑀 + 1))))
385	335, 379, 383	divrecd 12046	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) / (𝑀 + 1)) = ((((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1))))
386	382, 384, 385	3eqtr2rd 2784	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1))) = (((ℝ D (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) / ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))))‘𝑥)))
387	386	mpteq2dva 5242	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1)))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((ℝ D (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) / ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))))‘𝑥))))
388	387	oveq1d 7446	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1)))) limℂ 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((ℝ D (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) / ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))))‘𝑥))) limℂ 𝐵))
389	360, 361, 388	3eltr3d 2855	. . 3 ⊢ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((ℝ D (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) / ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))))‘𝑥))) limℂ 𝐵))
390	1, 70, 83, 123, 44, 124, 182, 236, 258, 271, 292, 313, 389	lhop 26055	. 2 ⊢ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) / ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))‘𝑥))) limℂ 𝐵))
391	314	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ 𝐴)
392		fveq2 6906	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) = (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥))
393		fveq2 6906	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥))
394	392, 393	oveq12d 7449	. . . . . . 7 ⊢ (𝑦 = 𝑥 → ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)) = ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)))
395		eqid 2737	. . . . . . 7 ⊢ (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) = (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))
396		ovex 7464	. . . . . . 7 ⊢ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) ∈ V
397	394, 395, 396	fvmpt 7016	. . . . . 6 ⊢ (𝑥 ∈ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) = ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)))
398	391, 397	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) = ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)))
399	371	oveq1d 7446	. . . . . . 7 ⊢ (𝑦 = 𝑥 → ((𝑦 − 𝐵)↑(𝑀 + 1)) = ((𝑥 − 𝐵)↑(𝑀 + 1)))
400		eqid 2737	. . . . . . 7 ⊢ (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) = (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))
401		ovex 7464	. . . . . . 7 ⊢ ((𝑥 − 𝐵)↑(𝑀 + 1)) ∈ V
402	399, 400, 401	fvmpt 7016	. . . . . 6 ⊢ (𝑥 ∈ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))‘𝑥) = ((𝑥 − 𝐵)↑(𝑀 + 1)))
403	391, 402	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))‘𝑥) = ((𝑥 − 𝐵)↑(𝑀 + 1)))
404	398, 403	oveq12d 7449	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (((𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) / ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))‘𝑥)) = (((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑀 + 1))))
405	404	mpteq2dva 5242	. . 3 ⊢ (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) / ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))‘𝑥))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑀 + 1)))))
406	405	oveq1d 7446	. 2 ⊢ (𝜑 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) / ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))‘𝑥))) limℂ 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑀 + 1)))) limℂ 𝐵))
407	390, 406	eleqtrd 2843	1 ⊢ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑀 + 1)))) limℂ 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2108   ≠ wne 2940  ∃wrex 3070  Vcvv 3480   ∖ cdif 3948   ∩ cin 3950   ⊆ wss 3951  {csn 4626  {cpr 4628  ⟨cop 4632   class class class wbr 5143   ↦ cmpt 5225   × cxp 5683  dom cdm 5685  ran crn 5686   ↾ cres 5687   “ cima 5688  ⟶wf 6557  ‘cfv 6561  (class class class)co 7431   ↑_m cmap 8866   ↑_pm cpm 8867  ℂcc 11153  ℝcr 11154  0cc0 11155  1c1 11156   + caddc 11158   · cmul 11160   ≤ cle 11296   − cmin 11492   / cdiv 11920  ℕcn 12266  ℕ₀cn0 12526  ℤ_≥cuz 12878  (,)cioo 13387  ...cfz 13547  ..^cfzo 13694  ↑cexp 14102  !cfa 14312  TopOpenctopn 17466  topGenctg 17482  SubRingcsubrg 20569  DivRingcdr 20729  ℂ_fldccnfld 21364  ℝ_fldcrefld 21622  Topctop 22899  TopOnctopon 22916  intcnt 23025   Cn ccn 23232   CnP ccnp 23233   ×_t ctx 23568  –cn→ccncf 24902   lim_ℂ climc 25897   D cdv 25898   D^𝑛 cdvn 25899  Polycply 26223  degcdgr 26226   Tayl ctayl 26394

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233  ax-addf 11234  ax-mulf 11235

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-tp 4631  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-iin 4994  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-om 7888  df-1st 8014  df-2nd 8015  df-supp 8186  df-tpos 8251  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-er 8745  df-map 8868  df-pm 8869  df-ixp 8938  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-fsupp 9402  df-fi 9451  df-sup 9482  df-inf 9483  df-oi 9550  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-4 12331  df-5 12332  df-6 12333  df-7 12334  df-8 12335  df-9 12336  df-n0 12527  df-xnn0 12600  df-z 12614  df-dec 12734  df-uz 12879  df-q 12991  df-rp 13035  df-xneg 13154  df-xadd 13155  df-xmul 13156  df-ioo 13391  df-ioc 13392  df-ico 13393  df-icc 13394  df-fz 13548  df-fzo 13695  df-fl 13832  df-seq 14043  df-exp 14103  df-fac 14313  df-hash 14370  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-clim 15524  df-rlim 15525  df-sum 15723  df-struct 17184  df-sets 17201  df-slot 17219  df-ndx 17231  df-base 17248  df-ress 17275  df-plusg 17310  df-mulr 17311  df-starv 17312  df-sca 17313  df-vsca 17314  df-ip 17315  df-tset 17316  df-ple 17317  df-ds 17319  df-unif 17320  df-hom 17321  df-cco 17322  df-rest 17467  df-topn 17468  df-0g 17486  df-gsum 17487  df-topgen 17488  df-pt 17489  df-prds 17492  df-xrs 17547  df-qtop 17552  df-imas 17553  df-xps 17555  df-mre 17629  df-mrc 17630  df-acs 17632  df-mgm 18653  df-sgrp 18732  df-mnd 18748  df-submnd 18797  df-grp 18954  df-minusg 18955  df-mulg 19086  df-subg 19141  df-cntz 19335  df-cmn 19800  df-abl 19801  df-mgp 20138  df-rng 20150  df-ur 20179  df-ring 20232  df-cring 20233  df-oppr 20334  df-dvdsr 20357  df-unit 20358  df-invr 20388  df-dvr 20401  df-subrng 20546  df-subrg 20570  df-drng 20731  df-psmet 21356  df-xmet 21357  df-met 21358  df-bl 21359  df-mopn 21360  df-fbas 21361  df-fg 21362  df-cnfld 21365  df-refld 21623  df-top 22900  df-topon 22917  df-topsp 22939  df-bases 22953  df-cld 23027  df-ntr 23028  df-cls 23029  df-nei 23106  df-lp 23144  df-perf 23145  df-cn 23235  df-cnp 23236  df-haus 23323  df-cmp 23395  df-tx 23570  df-hmeo 23763  df-fil 23854  df-fm 23946  df-flim 23947  df-flf 23948  df-tsms 24135  df-xms 24330  df-ms 24331  df-tms 24332  df-cncf 24904  df-0p 25705  df-limc 25901  df-dv 25902  df-dvn 25903  df-ply 26227  df-idp 26228  df-coe 26229  df-dgr 26230  df-tayl 26396

This theorem is referenced by: (None)