Theorem taylthlem2 24576

Description: Lemma for taylth 24577. (Contributed by Mario Carneiro, 1-Jan-2017.)

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
taylthlem2	⊢ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑀 + 1)))) limℂ 𝐵))

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

Proof of Theorem taylthlem2

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 12759	. . . . . . . . . . 11 ⊢ (1...𝑁) ⊆ (0...𝑁)
4		taylthlem2.m	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ (1..^𝑁))
5		fzofzp1 12889	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ (1..^𝑁) → (𝑀 + 1) ∈ (1...𝑁))
6	4, 5	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀 + 1) ∈ (1...𝑁))
7	3, 6	sseldi 3819	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀 + 1) ∈ (0...𝑁))
8		fznn0sub2 12770	. . . . . . . . . 10 ⊢ ((𝑀 + 1) ∈ (0...𝑁) → (𝑁 − (𝑀 + 1)) ∈ (0...𝑁))
9	7, 8	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 − (𝑀 + 1)) ∈ (0...𝑁))
10		elfznn0 12756	. . . . . . . . 9 ⊢ ((𝑁 − (𝑀 + 1)) ∈ (0...𝑁) → (𝑁 − (𝑀 + 1)) ∈ ℕ0)
11	9, 10	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑁 − (𝑀 + 1)) ∈ ℕ0)
12		dvnfre 24163	. . . . . . . 8 ⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ ∧ (𝑁 − (𝑀 + 1)) ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))⟶ℝ)
13	2, 1, 11, 12	syl3anc 1439	. . . . . . 7 ⊢ (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))⟶ℝ)
14		reelprrecn 10366	. . . . . . . . . . . 12 ⊢ ℝ ∈ {ℝ, ℂ}
15	14	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})
16		cnex 10355	. . . . . . . . . . . . 13 ⊢ ℂ ∈ V
17	16	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ℂ ∈ V)
18		reex 10365	. . . . . . . . . . . . 13 ⊢ ℝ ∈ V
19	18	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ℝ ∈ V)
20		ax-resscn 10331	. . . . . . . . . . . . 13 ⊢ ℝ ⊆ ℂ
21		fss 6306	. . . . . . . . . . . . 13 ⊢ ((𝐹:𝐴⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐹:𝐴⟶ℂ)
22	2, 20, 21	sylancl 580	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)
23		elpm2r 8160	. . . . . . . . . . . 12 ⊢ (((ℂ ∈ V ∧ ℝ ∈ V) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ)) → 𝐹 ∈ (ℂ ↑pm ℝ))
24	17, 19, 22, 1, 23	syl22anc 829	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ (ℂ ↑pm ℝ))
25		dvnbss 24139	. . . . . . . . . . 11 ⊢ ((ℝ ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm ℝ) ∧ (𝑁 − (𝑀 + 1)) ∈ ℕ0) → dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) ⊆ dom 𝐹)
26	15, 24, 11, 25	syl3anc 1439	. . . . . . . . . 10 ⊢ (𝜑 → dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) ⊆ dom 𝐹)
27	2, 26	fssdmd 6308	. . . . . . . . 9 ⊢ (𝜑 → dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) ⊆ 𝐴)
28		taylth.d	. . . . . . . . . 10 ⊢ (𝜑 → dom ((ℝ D𝑛 𝐹)‘𝑁) = 𝐴)
29		dvn2bss 24141	. . . . . . . . . . 11 ⊢ ((ℝ ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm ℝ) ∧ (𝑁 − (𝑀 + 1)) ∈ (0...𝑁)) → dom ((ℝ D𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))))
30	15, 24, 9, 29	syl3anc 1439	. . . . . . . . . 10 ⊢ (𝜑 → dom ((ℝ D𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))))
31	28, 30	eqsstr3d 3859	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ⊆ dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))))
32	27, 31	eqssd 3838	. . . . . . . 8 ⊢ (𝜑 → dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) = 𝐴)
33	32	feq2d 6279	. . . . . . 7 ⊢ (𝜑 → (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):dom ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))⟶ℝ ↔ ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℝ))
34	13, 33	mpbid 224	. . . . . 6 ⊢ (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℝ)
35	34	ffvelrnda 6625	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℝ)
36	1	sselda 3821	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ)
37		fvres 6467	. . . . . . . 8 ⊢ (𝑦 ∈ ℝ → ((((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ↾ ℝ)‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))
38	37	adantl 475	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ↾ ℝ)‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))
39		resubdrg 20362	. . . . . . . . . . . 12 ⊢ (ℝ ∈ (SubRing‘ℂfld) ∧ ℝfld ∈ DivRing)
40	39	simpli 478	. . . . . . . . . . 11 ⊢ ℝ ∈ (SubRing‘ℂfld)
41	40	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ℝ ∈ (SubRing‘ℂfld))
42		taylth.n	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℕ)
43	42	nnnn0d 11707	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℕ0)
44		taylth.b	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ 𝐴)
45	44, 28	eleqtrrd 2862	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ dom ((ℝ D𝑛 𝐹)‘𝑁))
46		taylth.t	. . . . . . . . . . . 12 ⊢ 𝑇 = (𝑁(ℝ Tayl 𝐹)𝐵)
47	1, 44	sseldd 3822	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ ℝ)
48	2	adantr 474	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐹:𝐴⟶ℝ)
49	1	adantr 474	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐴 ⊆ ℝ)
50		elfznn0 12756	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0)
51	50	adantl 475	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
52		dvnfre 24163	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ ∧ 𝑘 ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘𝑘):dom ((ℝ D𝑛 𝐹)‘𝑘)⟶ℝ)
53	48, 49, 51, 52	syl3anc 1439	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((ℝ D𝑛 𝐹)‘𝑘):dom ((ℝ D𝑛 𝐹)‘𝑘)⟶ℝ)
54	14	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ℝ ∈ {ℝ, ℂ})
55	24	adantr 474	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐹 ∈ (ℂ ↑pm ℝ))
56		simpr 479	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ (0...𝑁))
57		dvn2bss 24141	. . . . . . . . . . . . . . . 16 ⊢ ((ℝ ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm ℝ) ∧ 𝑘 ∈ (0...𝑁)) → dom ((ℝ D𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ D𝑛 𝐹)‘𝑘))
58	54, 55, 56, 57	syl3anc 1439	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → dom ((ℝ D𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ D𝑛 𝐹)‘𝑘))
59	45	adantr 474	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐵 ∈ dom ((ℝ D𝑛 𝐹)‘𝑁))
60	58, 59	sseldd 3822	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐵 ∈ dom ((ℝ D𝑛 𝐹)‘𝑘))
61	53, 60	ffvelrnd 6626	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (((ℝ D𝑛 𝐹)‘𝑘)‘𝐵) ∈ ℝ)
62		faccl 13394	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ0 → (!‘𝑘) ∈ ℕ)
63	51, 62	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ)
64	61, 63	nndivred 11434	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((((ℝ D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) ∈ ℝ)
65	15, 22, 1, 43, 45, 46, 41, 47, 64	taylply2 24570	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑇 ∈ (Poly‘ℝ) ∧ (deg‘𝑇) ≤ 𝑁))
66	65	simpld 490	. . . . . . . . . 10 ⊢ (𝜑 → 𝑇 ∈ (Poly‘ℝ))
67		dvnply2 24490	. . . . . . . . . 10 ⊢ ((ℝ ∈ (SubRing‘ℂfld) ∧ 𝑇 ∈ (Poly‘ℝ) ∧ (𝑁 − (𝑀 + 1)) ∈ ℕ0) → ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (Poly‘ℝ))
68	41, 66, 11, 67	syl3anc 1439	. . . . . . . . 9 ⊢ (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (Poly‘ℝ))
69		plyreres 24486	. . . . . . . . 9 ⊢ (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (Poly‘ℝ) → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ↾ ℝ):ℝ⟶ℝ)
70	68, 69	syl 17	. . . . . . . 8 ⊢ (𝜑 → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ↾ ℝ):ℝ⟶ℝ)
71	70	ffvelrnda 6625	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ↾ ℝ)‘𝑦) ∈ ℝ)
72	38, 71	eqeltrrd 2860	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℝ)
73	36, 72	syldan 585	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℝ)
74	35, 73	resubcld 10806	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)) ∈ ℝ)
75	74	fmpttd 6651	. . 3 ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))):𝐴⟶ℝ)
76	47	adantr 474	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝐵 ∈ ℝ)
77	36, 76	resubcld 10806	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑦 − 𝐵) ∈ ℝ)
78		elfzouz 12798	. . . . . . . . . 10 ⊢ (𝑀 ∈ (1..^𝑁) → 𝑀 ∈ (ℤ≥‘1))
79	4, 78	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘1))
80		nnuz 12034	. . . . . . . . 9 ⊢ ℕ = (ℤ≥‘1)
81	79, 80	syl6eleqr 2870	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℕ)
82	81	nnnn0d 11707	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℕ0)
83	82	adantr 474	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑀 ∈ ℕ0)
84		1nn0 11665	. . . . . . 7 ⊢ 1 ∈ ℕ0
85	84	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 1 ∈ ℕ0)
86	83, 85	nn0addcld 11711	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑀 + 1) ∈ ℕ0)
87	77, 86	reexpcld 13349	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ((𝑦 − 𝐵)↑(𝑀 + 1)) ∈ ℝ)
88	87	fmpttd 6651	. . 3 ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))):𝐴⟶ℝ)
89		retop 22984	. . . . . 6 ⊢ (topGen‘ran (,)) ∈ Top
90		uniretop 22985	. . . . . . 7 ⊢ ℝ = ∪ (topGen‘ran (,))
91	90	ntrss2 21280	. . . . . 6 ⊢ (((topGen‘ran (,)) ∈ Top ∧ 𝐴 ⊆ ℝ) → ((int‘(topGen‘ran (,)))‘𝐴) ⊆ 𝐴)
92	89, 1, 91	sylancr 581	. . . . 5 ⊢ (𝜑 → ((int‘(topGen‘ran (,)))‘𝐴) ⊆ 𝐴)
93	42	nncnd 11397	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℂ)
94	81	nncnd 11397	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℂ)
95		1cnd 10373	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ ℂ)
96	93, 94, 95	nppcan2d 10762	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑁 − (𝑀 + 1)) + 1) = (𝑁 − 𝑀))
97	96	fveq2d 6452	. . . . . . . . 9 ⊢ (𝜑 → ((ℝ D𝑛 𝐹)‘((𝑁 − (𝑀 + 1)) + 1)) = ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)))
98	20	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ℝ ⊆ ℂ)
99		dvnp1 24136	. . . . . . . . . 10 ⊢ ((ℝ ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm ℝ) ∧ (𝑁 − (𝑀 + 1)) ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘((𝑁 − (𝑀 + 1)) + 1)) = (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))))
100	98, 24, 11, 99	syl3anc 1439	. . . . . . . . 9 ⊢ (𝜑 → ((ℝ D𝑛 𝐹)‘((𝑁 − (𝑀 + 1)) + 1)) = (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))))
101	97, 100	eqtr3d 2816	. . . . . . . 8 ⊢ (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)) = (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))))
102	101	dmeqd 5573	. . . . . . 7 ⊢ (𝜑 → dom ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)) = dom (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))))
103		fzonnsub 12817	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ (1..^𝑁) → (𝑁 − 𝑀) ∈ ℕ)
104	4, 103	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 − 𝑀) ∈ ℕ)
105	104	nnnn0d 11707	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 − 𝑀) ∈ ℕ0)
106		dvnbss 24139	. . . . . . . . . 10 ⊢ ((ℝ ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm ℝ) ∧ (𝑁 − 𝑀) ∈ ℕ0) → dom ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)) ⊆ dom 𝐹)
107	15, 24, 105, 106	syl3anc 1439	. . . . . . . . 9 ⊢ (𝜑 → dom ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)) ⊆ dom 𝐹)
108	2, 107	fssdmd 6308	. . . . . . . 8 ⊢ (𝜑 → dom ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)) ⊆ 𝐴)
109		elfzofz 12809	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ (1..^𝑁) → 𝑀 ∈ (1...𝑁))
110	4, 109	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ (1...𝑁))
111	3, 110	sseldi 3819	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ (0...𝑁))
112		fznn0sub2 12770	. . . . . . . . . . 11 ⊢ (𝑀 ∈ (0...𝑁) → (𝑁 − 𝑀) ∈ (0...𝑁))
113	111, 112	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 − 𝑀) ∈ (0...𝑁))
114		dvn2bss 24141	. . . . . . . . . 10 ⊢ ((ℝ ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm ℝ) ∧ (𝑁 − 𝑀) ∈ (0...𝑁)) → dom ((ℝ D𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)))
115	15, 24, 113, 114	syl3anc 1439	. . . . . . . . 9 ⊢ (𝜑 → dom ((ℝ D𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)))
116	28, 115	eqsstr3d 3859	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ⊆ dom ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)))
117	108, 116	eqssd 3838	. . . . . . 7 ⊢ (𝜑 → dom ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)) = 𝐴)
118	102, 117	eqtr3d 2816	. . . . . 6 ⊢ (𝜑 → dom (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))) = 𝐴)
119		fss 6306	. . . . . . . 8 ⊢ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℝ ∧ ℝ ⊆ ℂ) → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℂ)
120	34, 20, 119	sylancl 580	. . . . . . 7 ⊢ (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℂ)
121		eqid 2778	. . . . . . . 8 ⊢ (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
122	121	tgioo2 23025	. . . . . . 7 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
123	98, 120, 1, 122, 121	dvbssntr 24112	. . . . . 6 ⊢ (𝜑 → dom (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))) ⊆ ((int‘(topGen‘ran (,)))‘𝐴))
124	118, 123	eqsstr3d 3859	. . . . 5 ⊢ (𝜑 → 𝐴 ⊆ ((int‘(topGen‘ran (,)))‘𝐴))
125	92, 124	eqssd 3838	. . . 4 ⊢ (𝜑 → ((int‘(topGen‘ran (,)))‘𝐴) = 𝐴)
126	90	isopn3 21289	. . . . 5 ⊢ (((topGen‘ran (,)) ∈ Top ∧ 𝐴 ⊆ ℝ) → (𝐴 ∈ (topGen‘ran (,)) ↔ ((int‘(topGen‘ran (,)))‘𝐴) = 𝐴))
127	89, 1, 126	sylancr 581	. . . 4 ⊢ (𝜑 → (𝐴 ∈ (topGen‘ran (,)) ↔ ((int‘(topGen‘ran (,)))‘𝐴) = 𝐴))
128	125, 127	mpbird 249	. . 3 ⊢ (𝜑 → 𝐴 ∈ (topGen‘ran (,)))
129		eqid 2778	. . 3 ⊢ (𝐴 ∖ {𝐵}) = (𝐴 ∖ {𝐵})
130		difss 3960	. . . 4 ⊢ (𝐴 ∖ {𝐵}) ⊆ 𝐴
131	35	recnd 10407	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℂ)
132		dvnf 24138	. . . . . . . . . 10 ⊢ ((ℝ ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm ℝ) ∧ (𝑁 − 𝑀) ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)):dom ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))⟶ℂ)
133	15, 24, 105, 132	syl3anc 1439	. . . . . . . . 9 ⊢ (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)):dom ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))⟶ℂ)
134	117	feq2d 6279	. . . . . . . . 9 ⊢ (𝜑 → (((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)):dom ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))⟶ℂ ↔ ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)):𝐴⟶ℂ))
135	133, 134	mpbid 224	. . . . . . . 8 ⊢ (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)):𝐴⟶ℂ)
136	135	ffvelrnda 6625	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑦) ∈ ℂ)
137		dvnfre 24163	. . . . . . . . . . 11 ⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ ∧ (𝑁 − 𝑀) ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)):dom ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))⟶ℝ)
138	2, 1, 105, 137	syl3anc 1439	. . . . . . . . . 10 ⊢ (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)):dom ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))⟶ℝ)
139	117	feq2d 6279	. . . . . . . . . 10 ⊢ (𝜑 → (((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)):dom ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))⟶ℝ ↔ ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)):𝐴⟶ℝ))
140	138, 139	mpbid 224	. . . . . . . . 9 ⊢ (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)):𝐴⟶ℝ)
141	140	feqmptd 6511	. . . . . . . 8 ⊢ (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀)) = (𝑦 ∈ 𝐴 ↦ (((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑦)))
142	34	feqmptd 6511	. . . . . . . . 9 ⊢ (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) = (𝑦 ∈ 𝐴 ↦ (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦)))
143	142	oveq2d 6940	. . . . . . . 8 ⊢ (𝜑 → (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))) = (ℝ D (𝑦 ∈ 𝐴 ↦ (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦))))
144	101, 141, 143	3eqtr3rd 2823	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝑦 ∈ 𝐴 ↦ (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦))) = (𝑦 ∈ 𝐴 ↦ (((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑦)))
145	73	recnd 10407	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℂ)
146		fvexd 6463	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦) ∈ V)
147	72	recnd 10407	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℂ)
148		recn 10364	. . . . . . . . 9 ⊢ (𝑦 ∈ ℝ → 𝑦 ∈ ℂ)
149		dvnply2 24490	. . . . . . . . . . . 12 ⊢ ((ℝ ∈ (SubRing‘ℂfld) ∧ 𝑇 ∈ (Poly‘ℝ) ∧ (𝑁 − 𝑀) ∈ ℕ0) → ((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀)) ∈ (Poly‘ℝ))
150	41, 66, 105, 149	syl3anc 1439	. . . . . . . . . . 11 ⊢ (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀)) ∈ (Poly‘ℝ))
151		plyf 24402	. . . . . . . . . . 11 ⊢ (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀)) ∈ (Poly‘ℝ) → ((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀)):ℂ⟶ℂ)
152	150, 151	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀)):ℂ⟶ℂ)
153	152	ffvelrnda 6625	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦) ∈ ℂ)
154	148, 153	sylan2 586	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦) ∈ ℂ)
155	121	cnfldtopon 23005	. . . . . . . . . 10 ⊢ (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
156		toponmax 21149	. . . . . . . . . 10 ⊢ ((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) → ℂ ∈ (TopOpen‘ℂfld))
157	155, 156	mp1i 13	. . . . . . . . 9 ⊢ (𝜑 → ℂ ∈ (TopOpen‘ℂfld))
158		df-ss 3806	. . . . . . . . . 10 ⊢ (ℝ ⊆ ℂ ↔ (ℝ ∩ ℂ) = ℝ)
159	98, 158	sylib 210	. . . . . . . . 9 ⊢ (𝜑 → (ℝ ∩ ℂ) = ℝ)
160		plyf 24402	. . . . . . . . . . 11 ⊢ (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (Poly‘ℝ) → ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))):ℂ⟶ℂ)
161	68, 160	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))):ℂ⟶ℂ)
162	161	ffvelrnda 6625	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℂ)
163	96	fveq2d 6452	. . . . . . . . . . 11 ⊢ (𝜑 → ((ℂ D𝑛 𝑇)‘((𝑁 − (𝑀 + 1)) + 1)) = ((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀)))
164		ssid 3842	. . . . . . . . . . . . 13 ⊢ ℂ ⊆ ℂ
165	164	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ℂ ⊆ ℂ)
166		mapsspm 8176	. . . . . . . . . . . . 13 ⊢ (ℂ ↑𝑚 ℂ) ⊆ (ℂ ↑pm ℂ)
167		plyf 24402	. . . . . . . . . . . . . . 15 ⊢ (𝑇 ∈ (Poly‘ℝ) → 𝑇:ℂ⟶ℂ)
168	66, 167	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑇:ℂ⟶ℂ)
169	16, 16	elmap 8171	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ (ℂ ↑𝑚 ℂ) ↔ 𝑇:ℂ⟶ℂ)
170	168, 169	sylibr 226	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑇 ∈ (ℂ ↑𝑚 ℂ))
171	166, 170	sseldi 3819	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑇 ∈ (ℂ ↑pm ℂ))
172		dvnp1 24136	. . . . . . . . . . . 12 ⊢ ((ℂ ⊆ ℂ ∧ 𝑇 ∈ (ℂ ↑pm ℂ) ∧ (𝑁 − (𝑀 + 1)) ∈ ℕ0) → ((ℂ D𝑛 𝑇)‘((𝑁 − (𝑀 + 1)) + 1)) = (ℂ D ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))))
173	165, 171, 11, 172	syl3anc 1439	. . . . . . . . . . 11 ⊢ (𝜑 → ((ℂ D𝑛 𝑇)‘((𝑁 − (𝑀 + 1)) + 1)) = (ℂ D ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))))
174	163, 173	eqtr3d 2816	. . . . . . . . . 10 ⊢ (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀)) = (ℂ D ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))))
175	152	feqmptd 6511	. . . . . . . . . 10 ⊢ (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀)) = (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦)))
176	161	feqmptd 6511	. . . . . . . . . . 11 ⊢ (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) = (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))
177	176	oveq2d 6940	. . . . . . . . . 10 ⊢ (𝜑 → (ℂ D ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))) = (ℂ D (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))
178	174, 175, 177	3eqtr3rd 2823	. . . . . . . . 9 ⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) = (𝑦 ∈ ℂ ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦)))
179	121, 15, 157, 159, 162, 153, 178	dvmptres3 24167	. . . . . . . 8 ⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) = (𝑦 ∈ ℝ ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦)))
180	15, 147, 154, 179, 1, 122, 121, 128	dvmptres 24174	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝑦 ∈ 𝐴 ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) = (𝑦 ∈ 𝐴 ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦)))
181	15, 131, 136, 144, 145, 146, 180	dvmptsub 24178	. . . . . 6 ⊢ (𝜑 → (ℝ D (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))) = (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦))))
182	181	dmeqd 5573	. . . . 5 ⊢ (𝜑 → dom (ℝ D (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))) = dom (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦))))
183		ovex 6956	. . . . . 6 ⊢ ((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦)) ∈ V
184		eqid 2778	. . . . . 6 ⊢ (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦))) = (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦)))
185	183, 184	dmmpti 6271	. . . . 5 ⊢ dom (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦))) = 𝐴
186	182, 185	syl6eq 2830	. . . 4 ⊢ (𝜑 → dom (ℝ D (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))) = 𝐴)
187	130, 186	syl5sseqr 3873	. . 3 ⊢ (𝜑 → (𝐴 ∖ {𝐵}) ⊆ dom (ℝ D (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))))
188		simpr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝑦 ∈ ℂ)
189	47	adantr 474	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝐵 ∈ ℝ)
190	189	recnd 10407	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝐵 ∈ ℂ)
191	188, 190	subcld 10736	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝑦 − 𝐵) ∈ ℂ)
192	82	adantr 474	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝑀 ∈ ℕ0)
193	84	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 1 ∈ ℕ0)
194	192, 193	nn0addcld 11711	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝑀 + 1) ∈ ℕ0)
195	191, 194	expcld 13332	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((𝑦 − 𝐵)↑(𝑀 + 1)) ∈ ℂ)
196	148, 195	sylan2 586	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑦 − 𝐵)↑(𝑀 + 1)) ∈ ℂ)
197	94	adantr 474	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝑀 ∈ ℂ)
198		1cnd 10373	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 1 ∈ ℂ)
199	197, 198	addcld 10398	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝑀 + 1) ∈ ℂ)
200	191, 192	expcld 13332	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((𝑦 − 𝐵)↑𝑀) ∈ ℂ)
201	199, 200	mulcld 10399	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)) ∈ ℂ)
202	148, 201	sylan2 586	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)) ∈ ℂ)
203	16	prid2 4530	. . . . . . . . . . 11 ⊢ ℂ ∈ {ℝ, ℂ}
204	203	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ℂ ∈ {ℝ, ℂ})
205		simpr 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝑥 ∈ ℂ)
206		elfznn 12692	. . . . . . . . . . . . . 14 ⊢ ((𝑀 + 1) ∈ (1...𝑁) → (𝑀 + 1) ∈ ℕ)
207	6, 206	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑀 + 1) ∈ ℕ)
208	207	nnnn0d 11707	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀 + 1) ∈ ℕ0)
209	208	adantr 474	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝑀 + 1) ∈ ℕ0)
210	205, 209	expcld 13332	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝑥↑(𝑀 + 1)) ∈ ℂ)
211		ovexd 6958	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((𝑀 + 1) · (𝑥↑𝑀)) ∈ V)
212	204	dvmptid 24168	. . . . . . . . . . . 12 ⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ 𝑦)) = (𝑦 ∈ ℂ ↦ 1))
213		0cnd 10371	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 0 ∈ ℂ)
214	47	recnd 10407	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ ℂ)
215	204, 214	dvmptc 24169	. . . . . . . . . . . 12 ⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ 𝐵)) = (𝑦 ∈ ℂ ↦ 0))
216	204, 188, 198, 212, 190, 213, 215	dvmptsub 24178	. . . . . . . . . . 11 ⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦 − 𝐵))) = (𝑦 ∈ ℂ ↦ (1 − 0)))
217		1m0e1 11508	. . . . . . . . . . . 12 ⊢ (1 − 0) = 1
218	217	mpteq2i 4978	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℂ ↦ (1 − 0)) = (𝑦 ∈ ℂ ↦ 1)
219	216, 218	syl6eq 2830	. . . . . . . . . 10 ⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦 − 𝐵))) = (𝑦 ∈ ℂ ↦ 1))
220		dvexp 24164	. . . . . . . . . . . 12 ⊢ ((𝑀 + 1) ∈ ℕ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑(𝑀 + 1)))) = (𝑥 ∈ ℂ ↦ ((𝑀 + 1) · (𝑥↑((𝑀 + 1) − 1)))))
221	207, 220	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑(𝑀 + 1)))) = (𝑥 ∈ ℂ ↦ ((𝑀 + 1) · (𝑥↑((𝑀 + 1) − 1)))))
222	94, 95	pncand 10737	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀 + 1) − 1) = 𝑀)
223	222	oveq2d 6940	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥↑((𝑀 + 1) − 1)) = (𝑥↑𝑀))
224	223	oveq2d 6940	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑀 + 1) · (𝑥↑((𝑀 + 1) − 1))) = ((𝑀 + 1) · (𝑥↑𝑀)))
225	224	mpteq2dv 4982	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((𝑀 + 1) · (𝑥↑((𝑀 + 1) − 1)))) = (𝑥 ∈ ℂ ↦ ((𝑀 + 1) · (𝑥↑𝑀))))
226	221, 225	eqtrd 2814	. . . . . . . . . 10 ⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑(𝑀 + 1)))) = (𝑥 ∈ ℂ ↦ ((𝑀 + 1) · (𝑥↑𝑀))))
227		oveq1 6931	. . . . . . . . . 10 ⊢ (𝑥 = (𝑦 − 𝐵) → (𝑥↑(𝑀 + 1)) = ((𝑦 − 𝐵)↑(𝑀 + 1)))
228		oveq1 6931	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑦 − 𝐵) → (𝑥↑𝑀) = ((𝑦 − 𝐵)↑𝑀))
229	228	oveq2d 6940	. . . . . . . . . 10 ⊢ (𝑥 = (𝑦 − 𝐵) → ((𝑀 + 1) · (𝑥↑𝑀)) = ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)))
230	204, 204, 191, 198, 210, 211, 219, 226, 227, 229	dvmptco 24183	. . . . . . . . 9 ⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) = (𝑦 ∈ ℂ ↦ (((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)) · 1)))
231	201	mulid1d 10396	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)) · 1) = ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)))
232	231	mpteq2dva 4981	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ ℂ ↦ (((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)) · 1)) = (𝑦 ∈ ℂ ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))))
233	230, 232	eqtrd 2814	. . . . . . . 8 ⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) = (𝑦 ∈ ℂ ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))))
234	121, 15, 157, 159, 195, 201, 233	dvmptres3 24167	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) = (𝑦 ∈ ℝ ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))))
235	15, 196, 202, 234, 1, 122, 121, 128	dvmptres 24174	. . . . . 6 ⊢ (𝜑 → (ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) = (𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))))
236	235	dmeqd 5573	. . . . 5 ⊢ (𝜑 → dom (ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) = dom (𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))))
237		ovex 6956	. . . . . 6 ⊢ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)) ∈ V
238		eqid 2778	. . . . . 6 ⊢ (𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) = (𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)))
239	237, 238	dmmpti 6271	. . . . 5 ⊢ dom (𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) = 𝐴
240	236, 239	syl6eq 2830	. . . 4 ⊢ (𝜑 → dom (ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) = 𝐴)
241	130, 240	syl5sseqr 3873	. . 3 ⊢ (𝜑 → (𝐴 ∖ {𝐵}) ⊆ dom (ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))))
242	15, 22, 1, 9, 45, 46	dvntaylp0 24574	. . . . . 6 ⊢ (𝜑 → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵) = (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵))
243	242	oveq2d 6940	. . . . 5 ⊢ (𝜑 → ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵)) = ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵)))
244	120, 44	ffvelrnd 6626	. . . . . 6 ⊢ (𝜑 → (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) ∈ ℂ)
245	244	subidd 10724	. . . . 5 ⊢ (𝜑 → ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵)) = 0)
246	243, 245	eqtrd 2814	. . . 4 ⊢ (𝜑 → ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵)) = 0)
247	121	subcn 23088	. . . . . . 7 ⊢ − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
248	247	a1i 11	. . . . . 6 ⊢ (𝜑 → − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)))
249		dvcn 24132	. . . . . . . 8 ⊢ (((ℝ ⊆ ℂ ∧ ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) ∧ dom (ℝ D ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))) = 𝐴) → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) ∈ (𝐴–cn→ℂ))
250	98, 120, 1, 118, 249	syl31anc 1441	. . . . . . 7 ⊢ (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) ∈ (𝐴–cn→ℂ))
251	142, 250	eqeltrrd 2860	. . . . . 6 ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦)) ∈ (𝐴–cn→ℂ))
252		plycn 24465	. . . . . . . 8 ⊢ (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (Poly‘ℝ) → ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (ℂ–cn→ℂ))
253	68, 252	syl 17	. . . . . . 7 ⊢ (𝜑 → ((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (ℂ–cn→ℂ))
254	1, 20	syl6ss 3833	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ⊆ ℂ)
255		cncfmptid 23134	. . . . . . . 8 ⊢ ((𝐴 ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑦 ∈ 𝐴 ↦ 𝑦) ∈ (𝐴–cn→ℂ))
256	254, 164, 255	sylancl 580	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ 𝑦) ∈ (𝐴–cn→ℂ))
257	253, 256	cncfmpt1f 23135	. . . . . 6 ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)) ∈ (𝐴–cn→ℂ))
258	121, 248, 251, 257	cncfmpt2f 23136	. . . . 5 ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) ∈ (𝐴–cn→ℂ))
259		fveq2 6448	. . . . . 6 ⊢ (𝑦 = 𝐵 → (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) = (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵))
260		fveq2 6448	. . . . . 6 ⊢ (𝑦 = 𝐵 → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵))
261	259, 260	oveq12d 6942	. . . . 5 ⊢ (𝑦 = 𝐵 → ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)) = ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵)))
262	258, 44, 261	cnmptlimc 24102	. . . 4 ⊢ (𝜑 → ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵)) ∈ ((𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) limℂ 𝐵))
263	246, 262	eqeltrrd 2860	. . 3 ⊢ (𝜑 → 0 ∈ ((𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) limℂ 𝐵))
264	214	subidd 10724	. . . . . 6 ⊢ (𝜑 → (𝐵 − 𝐵) = 0)
265	264	oveq1d 6939	. . . . 5 ⊢ (𝜑 → ((𝐵 − 𝐵)↑(𝑀 + 1)) = (0↑(𝑀 + 1)))
266	207	0expd 13348	. . . . 5 ⊢ (𝜑 → (0↑(𝑀 + 1)) = 0)
267	265, 266	eqtrd 2814	. . . 4 ⊢ (𝜑 → ((𝐵 − 𝐵)↑(𝑀 + 1)) = 0)
268	254	sselda 3821	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℂ)
269	268, 195	syldan 585	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ((𝑦 − 𝐵)↑(𝑀 + 1)) ∈ ℂ)
270	269	fmpttd 6651	. . . . . 6 ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))):𝐴⟶ℂ)
271		dvcn 24132	. . . . . 6 ⊢ (((ℝ ⊆ ℂ ∧ (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))):𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) ∧ dom (ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) = 𝐴) → (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) ∈ (𝐴–cn→ℂ))
272	98, 270, 1, 240, 271	syl31anc 1441	. . . . 5 ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) ∈ (𝐴–cn→ℂ))
273		oveq1 6931	. . . . . 6 ⊢ (𝑦 = 𝐵 → (𝑦 − 𝐵) = (𝐵 − 𝐵))
274	273	oveq1d 6939	. . . . 5 ⊢ (𝑦 = 𝐵 → ((𝑦 − 𝐵)↑(𝑀 + 1)) = ((𝐵 − 𝐵)↑(𝑀 + 1)))
275	272, 44, 274	cnmptlimc 24102	. . . 4 ⊢ (𝜑 → ((𝐵 − 𝐵)↑(𝑀 + 1)) ∈ ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) limℂ 𝐵))
276	267, 275	eqeltrrd 2860	. . 3 ⊢ (𝜑 → 0 ∈ ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) limℂ 𝐵))
277	254	ssdifssd 3971	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 ∖ {𝐵}) ⊆ ℂ)
278	277	sselda 3821	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑦 ∈ ℂ)
279	214	adantr 474	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝐵 ∈ ℂ)
280	278, 279	subcld 10736	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑦 − 𝐵) ∈ ℂ)
281		eldifsni 4553	. . . . . . . . . 10 ⊢ (𝑦 ∈ (𝐴 ∖ {𝐵}) → 𝑦 ≠ 𝐵)
282	281	adantl 475	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑦 ≠ 𝐵)
283	278, 279, 282	subne0d 10745	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑦 − 𝐵) ≠ 0)
284	207	adantr 474	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ∈ ℕ)
285	284	nnzd 11838	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ∈ ℤ)
286	280, 283, 285	expne0d 13338	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → ((𝑦 − 𝐵)↑(𝑀 + 1)) ≠ 0)
287	286	necomd 3024	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → 0 ≠ ((𝑦 − 𝐵)↑(𝑀 + 1)))
288	287	neneqd 2974	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → ¬ 0 = ((𝑦 − 𝐵)↑(𝑀 + 1)))
289	288	nrexdv 3182	. . . 4 ⊢ (𝜑 → ¬ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑦 − 𝐵)↑(𝑀 + 1)))
290		df-ima 5370	. . . . . 6 ⊢ ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) “ (𝐴 ∖ {𝐵})) = ran ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) ↾ (𝐴 ∖ {𝐵}))
291	290	eleq2i 2851	. . . . 5 ⊢ (0 ∈ ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) “ (𝐴 ∖ {𝐵})) ↔ 0 ∈ ran ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})))
292		resmpt 5701	. . . . . . 7 ⊢ ((𝐴 ∖ {𝐵}) ⊆ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))))
293	130, 292	ax-mp 5	. . . . . 6 ⊢ ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))
294		ovex 6956	. . . . . 6 ⊢ ((𝑦 − 𝐵)↑(𝑀 + 1)) ∈ V
295	293, 294	elrnmpti 5624	. . . . 5 ⊢ (0 ∈ ran ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) ↔ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑦 − 𝐵)↑(𝑀 + 1)))
296	291, 295	bitri 267	. . . 4 ⊢ (0 ∈ ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) “ (𝐴 ∖ {𝐵})) ↔ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑦 − 𝐵)↑(𝑀 + 1)))
297	289, 296	sylnibr 321	. . 3 ⊢ (𝜑 → ¬ 0 ∈ ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) “ (𝐴 ∖ {𝐵})))
298	94	adantr 474	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑀 ∈ ℂ)
299		1cnd 10373	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → 1 ∈ ℂ)
300	298, 299	addcld 10398	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ∈ ℂ)
301	278, 200	syldan 585	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → ((𝑦 − 𝐵)↑𝑀) ∈ ℂ)
302	284	nnne0d 11430	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ≠ 0)
303	81	adantr 474	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑀 ∈ ℕ)
304	303	nnzd 11838	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑀 ∈ ℤ)
305	280, 283, 304	expne0d 13338	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → ((𝑦 − 𝐵)↑𝑀) ≠ 0)
306	300, 301, 302, 305	mulne0d 11030	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)) ≠ 0)
307	306	necomd 3024	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → 0 ≠ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)))
308	307	neneqd 2974	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → ¬ 0 = ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)))
309	308	nrexdv 3182	. . . 4 ⊢ (𝜑 → ¬ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)))
310	235	imaeq1d 5721	. . . . . . 7 ⊢ (𝜑 → ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) “ (𝐴 ∖ {𝐵})) = ((𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) “ (𝐴 ∖ {𝐵})))
311		df-ima 5370	. . . . . . 7 ⊢ ((𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) “ (𝐴 ∖ {𝐵})) = ran ((𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵}))
312	310, 311	syl6eq 2830	. . . . . 6 ⊢ (𝜑 → ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) “ (𝐴 ∖ {𝐵})) = ran ((𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵})))
313	312	eleq2d 2845	. . . . 5 ⊢ (𝜑 → (0 ∈ ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) “ (𝐴 ∖ {𝐵})) ↔ 0 ∈ ran ((𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵}))))
314		resmpt 5701	. . . . . . 7 ⊢ ((𝐴 ∖ {𝐵}) ⊆ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵})) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))))
315	130, 314	ax-mp 5	. . . . . 6 ⊢ ((𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵})) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)))
316	315, 237	elrnmpti 5624	. . . . 5 ⊢ (0 ∈ ran ((𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵})) ↔ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)))
317	313, 316	syl6bb 279	. . . 4 ⊢ (𝜑 → (0 ∈ ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) “ (𝐴 ∖ {𝐵})) ↔ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))))
318	309, 317	mtbird 317	. . 3 ⊢ (𝜑 → ¬ 0 ∈ ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) “ (𝐴 ∖ {𝐵})))
319		eldifi 3955	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴 ∖ {𝐵}) → 𝑥 ∈ 𝐴)
320	135	ffvelrnda 6625	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) ∈ ℂ)
321	319, 320	sylan2 586	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) ∈ ℂ)
322	1	ssdifssd 3971	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 ∖ {𝐵}) ⊆ ℝ)
323	322	sselda 3821	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ ℝ)
324	323	recnd 10407	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ ℂ)
325	152	ffvelrnda 6625	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥) ∈ ℂ)
326	324, 325	syldan 585	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥) ∈ ℂ)
327	321, 326	subcld 10736	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) ∈ ℂ)
328	47	adantr 474	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝐵 ∈ ℝ)
329	323, 328	resubcld 10806	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑥 − 𝐵) ∈ ℝ)
330	82	adantr 474	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑀 ∈ ℕ0)
331	329, 330	reexpcld 13349	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑥 − 𝐵)↑𝑀) ∈ ℝ)
332	331	recnd 10407	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑥 − 𝐵)↑𝑀) ∈ ℂ)
333	328	recnd 10407	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝐵 ∈ ℂ)
334	324, 333	subcld 10736	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑥 − 𝐵) ∈ ℂ)
335		eldifsni 4553	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴 ∖ {𝐵}) → 𝑥 ≠ 𝐵)
336	335	adantl 475	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ≠ 𝐵)
337	324, 333, 336	subne0d 10745	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑥 − 𝐵) ≠ 0)
338	330	nn0zd 11837	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑀 ∈ ℤ)
339	334, 337, 338	expne0d 13338	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑥 − 𝐵)↑𝑀) ≠ 0)
340	327, 332, 339	divcld 11154	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) ∈ ℂ)
341	207	nnrecred 11431	. . . . . . 7 ⊢ (𝜑 → (1 / (𝑀 + 1)) ∈ ℝ)
342	341	recnd 10407	. . . . . 6 ⊢ (𝜑 → (1 / (𝑀 + 1)) ∈ ℂ)
343	342	adantr 474	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (1 / (𝑀 + 1)) ∈ ℂ)
344		txtopon 21814	. . . . . . 7 ⊢ (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) → ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ∈ (TopOn‘(ℂ × ℂ)))
345	155, 155, 344	mp2an 682	. . . . . 6 ⊢ ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ∈ (TopOn‘(ℂ × ℂ))
346	345	toponrestid 21144	. . . . 5 ⊢ ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) = (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) ↾t (ℂ × ℂ))
347		taylthlem2.i	. . . . 5 ⊢ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀))) limℂ 𝐵))
348		limcresi 24097	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 ↦ (1 / (𝑀 + 1))) limℂ 𝐵) ⊆ (((𝑥 ∈ 𝐴 ↦ (1 / (𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) limℂ 𝐵)
349		resmpt 5701	. . . . . . . . 9 ⊢ ((𝐴 ∖ {𝐵}) ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ (1 / (𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (1 / (𝑀 + 1))))
350	130, 349	ax-mp 5	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 ↦ (1 / (𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (1 / (𝑀 + 1)))
351	350	oveq1i 6934	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐴 ↦ (1 / (𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) limℂ 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (1 / (𝑀 + 1))) limℂ 𝐵)
352	348, 351	sseqtri 3856	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ↦ (1 / (𝑀 + 1))) limℂ 𝐵) ⊆ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (1 / (𝑀 + 1))) limℂ 𝐵)
353		cncfmptc 23133	. . . . . . . 8 ⊢ (((1 / (𝑀 + 1)) ∈ ℝ ∧ 𝐴 ⊆ ℂ ∧ ℝ ⊆ ℂ) → (𝑥 ∈ 𝐴 ↦ (1 / (𝑀 + 1))) ∈ (𝐴–cn→ℝ))
354	341, 254, 98, 353	syl3anc 1439	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (1 / (𝑀 + 1))) ∈ (𝐴–cn→ℝ))
355		eqidd 2779	. . . . . . 7 ⊢ (𝑥 = 𝐵 → (1 / (𝑀 + 1)) = (1 / (𝑀 + 1)))
356	354, 44, 355	cnmptlimc 24102	. . . . . 6 ⊢ (𝜑 → (1 / (𝑀 + 1)) ∈ ((𝑥 ∈ 𝐴 ↦ (1 / (𝑀 + 1))) limℂ 𝐵))
357	352, 356	sseldi 3819	. . . . 5 ⊢ (𝜑 → (1 / (𝑀 + 1)) ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (1 / (𝑀 + 1))) limℂ 𝐵))
358	121	mulcn 23089	. . . . . 6 ⊢ · ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
359		0cn 10370	. . . . . . 7 ⊢ 0 ∈ ℂ
360		opelxpi 5394	. . . . . . 7 ⊢ ((0 ∈ ℂ ∧ (1 / (𝑀 + 1)) ∈ ℂ) → ⟨0, (1 / (𝑀 + 1))⟩ ∈ (ℂ × ℂ))
361	359, 342, 360	sylancr 581	. . . . . 6 ⊢ (𝜑 → ⟨0, (1 / (𝑀 + 1))⟩ ∈ (ℂ × ℂ))
362	345	toponunii 21139	. . . . . . 7 ⊢ (ℂ × ℂ) = ∪ ((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld))
363	362	cncnpi 21501	. . . . . 6 ⊢ (( · ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)) ∧ ⟨0, (1 / (𝑀 + 1))⟩ ∈ (ℂ × ℂ)) → · ∈ ((((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) CnP (TopOpen‘ℂfld))‘⟨0, (1 / (𝑀 + 1))⟩))
364	358, 361, 363	sylancr 581	. . . . 5 ⊢ (𝜑 → · ∈ ((((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) CnP (TopOpen‘ℂfld))‘⟨0, (1 / (𝑀 + 1))⟩))
365	340, 343, 165, 165, 121, 346, 347, 357, 364	limccnp2 24104	. . . 4 ⊢ (𝜑 → (0 · (1 / (𝑀 + 1))) ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1)))) limℂ 𝐵))
366	342	mul02d 10576	. . . 4 ⊢ (𝜑 → (0 · (1 / (𝑀 + 1))) = 0)
367	181	fveq1d 6450	. . . . . . . . 9 ⊢ (𝜑 → ((ℝ D (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) = ((𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦)))‘𝑥))
368		fveq2 6448	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → (((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑦) = (((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥))
369		fveq2 6448	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥))
370	368, 369	oveq12d 6942	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 → ((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦)) = ((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)))
371		ovex 6956	. . . . . . . . . . 11 ⊢ ((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) ∈ V
372	370, 184, 371	fvmpt 6544	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦)))‘𝑥) = ((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)))
373	319, 372	syl 17	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴 ∖ {𝐵}) → ((𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦)))‘𝑥) = ((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)))
374	367, 373	sylan9eq 2834	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((ℝ D (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) = ((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)))
375	235	fveq1d 6450	. . . . . . . . . 10 ⊢ (𝜑 → ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))))‘𝑥) = ((𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)))‘𝑥))
376		oveq1 6931	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑥 → (𝑦 − 𝐵) = (𝑥 − 𝐵))
377	376	oveq1d 6939	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑥 → ((𝑦 − 𝐵)↑𝑀) = ((𝑥 − 𝐵)↑𝑀))
378	377	oveq2d 6940	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)) = ((𝑀 + 1) · ((𝑥 − 𝐵)↑𝑀)))
379		ovex 6956	. . . . . . . . . . . 12 ⊢ ((𝑀 + 1) · ((𝑥 − 𝐵)↑𝑀)) ∈ V
380	378, 238, 379	fvmpt 6544	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)))‘𝑥) = ((𝑀 + 1) · ((𝑥 − 𝐵)↑𝑀)))
381	319, 380	syl 17	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐴 ∖ {𝐵}) → ((𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)))‘𝑥) = ((𝑀 + 1) · ((𝑥 − 𝐵)↑𝑀)))
382	375, 381	sylan9eq 2834	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))))‘𝑥) = ((𝑀 + 1) · ((𝑥 − 𝐵)↑𝑀)))
383	207	adantr 474	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ∈ ℕ)
384	383	nncnd 11397	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ∈ ℂ)
385	384, 332	mulcomd 10400	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑀 + 1) · ((𝑥 − 𝐵)↑𝑀)) = (((𝑥 − 𝐵)↑𝑀) · (𝑀 + 1)))
386	382, 385	eqtrd 2814	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))))‘𝑥) = (((𝑥 − 𝐵)↑𝑀) · (𝑀 + 1)))
387	374, 386	oveq12d 6942	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (((ℝ D (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) / ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))))‘𝑥)) = (((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / (((𝑥 − 𝐵)↑𝑀) · (𝑀 + 1))))
388	383	nnne0d 11430	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ≠ 0)
389	327, 332, 384, 339, 388	divdiv1d 11185	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) / (𝑀 + 1)) = (((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / (((𝑥 − 𝐵)↑𝑀) · (𝑀 + 1))))
390	340, 384, 388	divrecd 11157	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) / (𝑀 + 1)) = ((((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1))))
391	387, 389, 390	3eqtr2rd 2821	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1))) = (((ℝ D (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) / ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))))‘𝑥)))
392	391	mpteq2dva 4981	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1)))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((ℝ D (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) / ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))))‘𝑥))))
393	392	oveq1d 6939	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ D𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1)))) limℂ 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((ℝ D (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) / ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))))‘𝑥))) limℂ 𝐵))
394	365, 366, 393	3eltr3d 2873	. . 3 ⊢ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((ℝ D (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) / ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))))‘𝑥))) limℂ 𝐵))
395	1, 75, 88, 128, 44, 129, 187, 241, 263, 276, 297, 318, 394	lhop 24227	. 2 ⊢ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) / ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))‘𝑥))) limℂ 𝐵))
396	319	adantl 475	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ 𝐴)
397		fveq2 6448	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) = (((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥))
398		fveq2 6448	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) = (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥))
399	397, 398	oveq12d 6942	. . . . . . 7 ⊢ (𝑦 = 𝑥 → ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)) = ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)))
400		eqid 2778	. . . . . . 7 ⊢ (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) = (𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))
401		ovex 6956	. . . . . . 7 ⊢ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) ∈ V
402	399, 400, 401	fvmpt 6544	. . . . . 6 ⊢ (𝑥 ∈ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) = ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)))
403	396, 402	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) = ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)))
404	376	oveq1d 6939	. . . . . . 7 ⊢ (𝑦 = 𝑥 → ((𝑦 − 𝐵)↑(𝑀 + 1)) = ((𝑥 − 𝐵)↑(𝑀 + 1)))
405		eqid 2778	. . . . . . 7 ⊢ (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) = (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))
406		ovex 6956	. . . . . . 7 ⊢ ((𝑥 − 𝐵)↑(𝑀 + 1)) ∈ V
407	404, 405, 406	fvmpt 6544	. . . . . 6 ⊢ (𝑥 ∈ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))‘𝑥) = ((𝑥 − 𝐵)↑(𝑀 + 1)))
408	396, 407	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))‘𝑥) = ((𝑥 − 𝐵)↑(𝑀 + 1)))
409	403, 408	oveq12d 6942	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (((𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) / ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))‘𝑥)) = (((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑀 + 1))))
410	409	mpteq2dva 4981	. . 3 ⊢ (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) / ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))‘𝑥))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑀 + 1)))))
411	410	oveq1d 6939	. 2 ⊢ (𝜑 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝑦 ∈ 𝐴 ↦ ((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) / ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))‘𝑥))) limℂ 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑀 + 1)))) limℂ 𝐵))
412	395, 411	eleqtrd 2861	1 ⊢ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((ℝ D𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑀 + 1)))) limℂ 𝐵))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   = wceq 1601   ∈ wcel 2107   ≠ wne 2969  ∃wrex 3091  Vcvv 3398   ∖ cdif 3789   ∩ cin 3791   ⊆ wss 3792  {csn 4398  {cpr 4400  ⟨cop 4404   class class class wbr 4888   ↦ cmpt 4967   × cxp 5355  dom cdm 5357  ran crn 5358   ↾ cres 5359   “ cima 5360  ⟶wf 6133  ‘cfv 6137  (class class class)co 6924   ↑_𝑚 cmap 8142   ↑_pm cpm 8143  ℂcc 10272  ℝcr 10273  0cc0 10274  1c1 10275   + caddc 10277   · cmul 10279   ≤ cle 10414   − cmin 10608   / cdiv 11035  ℕcn 11379  ℕ₀cn0 11647  ℤ_≥cuz 11997  (,)cioo 12492  ...cfz 12648  ..^cfzo 12789  ↑cexp 13183  !cfa 13384  TopOpenctopn 16479  topGenctg 16495  DivRingcdr 19150  SubRingcsubrg 19179  ℂ_fldccnfld 20153  ℝ_fldcrefld 20358  Topctop 21116  TopOnctopon 21133  intcnt 21240   Cn ccn 21447   CnP ccnp 21448   ×_t ctx 21783  –cn→ccncf 23098   lim_ℂ climc 24074   D cdv 24075   D^𝑛 cdvn 24076  Polycply 24388  degcdgr 24391   Tayl ctayl 24555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5008  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228  ax-inf2 8837  ax-cnex 10330  ax-resscn 10331  ax-1cn 10332  ax-icn 10333  ax-addcl 10334  ax-addrcl 10335  ax-mulcl 10336  ax-mulrcl 10337  ax-mulcom 10338  ax-addass 10339  ax-mulass 10340  ax-distr 10341  ax-i2m1 10342  ax-1ne0 10343  ax-1rid 10344  ax-rnegex 10345  ax-rrecex 10346  ax-cnre 10347  ax-pre-lttri 10348  ax-pre-lttrn 10349  ax-pre-ltadd 10350  ax-pre-mulgt0 10351  ax-pre-sup 10352  ax-addf 10353  ax-mulf 10354

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-fal 1615  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4674  df-int 4713  df-iun 4757  df-iin 4758  df-br 4889  df-opab 4951  df-mpt 4968  df-tr 4990  df-id 5263  df-eprel 5268  df-po 5276  df-so 5277  df-fr 5316  df-se 5317  df-we 5318  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-pred 5935  df-ord 5981  df-on 5982  df-lim 5983  df-suc 5984  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-f1 6142  df-fo 6143  df-f1o 6144  df-fv 6145  df-isom 6146  df-riota 6885  df-ov 6927  df-oprab 6928  df-mpt2 6929  df-of 7176  df-om 7346  df-1st 7447  df-2nd 7448  df-supp 7579  df-tpos 7636  df-wrecs 7691  df-recs 7753  df-rdg 7791  df-1o 7845  df-2o 7846  df-oadd 7849  df-er 8028  df-map 8144  df-pm 8145  df-ixp 8197  df-en 8244  df-dom 8245  df-sdom 8246  df-fin 8247  df-fsupp 8566  df-fi 8607  df-sup 8638  df-inf 8639  df-oi 8706  df-card 9100  df-cda 9327  df-pnf 10415  df-mnf 10416  df-xr 10417  df-ltxr 10418  df-le 10419  df-sub 10610  df-neg 10611  df-div 11036  df-nn 11380  df-2 11443  df-3 11444  df-4 11445  df-5 11446  df-6 11447  df-7 11448  df-8 11449  df-9 11450  df-n0 11648  df-xnn0 11720  df-z 11734  df-dec 11851  df-uz 11998  df-q 12101  df-rp 12143  df-xneg 12262  df-xadd 12263  df-xmul 12264  df-ioo 12496  df-ioc 12497  df-ico 12498  df-icc 12499  df-fz 12649  df-fzo 12790  df-fl 12917  df-seq 13125  df-exp 13184  df-fac 13385  df-hash 13442  df-cj 14252  df-re 14253  df-im 14254  df-sqrt 14388  df-abs 14389  df-clim 14636  df-rlim 14637  df-sum 14834  df-struct 16268  df-ndx 16269  df-slot 16270  df-base 16272  df-sets 16273  df-ress 16274  df-plusg 16362  df-mulr 16363  df-starv 16364  df-sca 16365  df-vsca 16366  df-ip 16367  df-tset 16368  df-ple 16369  df-ds 16371  df-unif 16372  df-hom 16373  df-cco 16374  df-rest 16480  df-topn 16481  df-0g 16499  df-gsum 16500  df-topgen 16501  df-pt 16502  df-prds 16505  df-xrs 16559  df-qtop 16564  df-imas 16565  df-xps 16567  df-mre 16643  df-mrc 16644  df-acs 16646  df-mgm 17639  df-sgrp 17681  df-mnd 17692  df-submnd 17733  df-grp 17823  df-minusg 17824  df-mulg 17939  df-subg 17986  df-cntz 18144  df-cmn 18592  df-abl 18593  df-mgp 18888  df-ur 18900  df-ring 18947  df-cring 18948  df-oppr 19021  df-dvdsr 19039  df-unit 19040  df-invr 19070  df-dvr 19081  df-drng 19152  df-subrg 19181  df-psmet 20145  df-xmet 20146  df-met 20147  df-bl 20148  df-mopn 20149  df-fbas 20150  df-fg 20151  df-cnfld 20154  df-refld 20359  df-top 21117  df-topon 21134  df-topsp 21156  df-bases 21169  df-cld 21242  df-ntr 21243  df-cls 21244  df-nei 21321  df-lp 21359  df-perf 21360  df-cn 21450  df-cnp 21451  df-haus 21538  df-cmp 21610  df-tx 21785  df-hmeo 21978  df-fil 22069  df-fm 22161  df-flim 22162  df-flf 22163  df-tsms 22349  df-xms 22544  df-ms 22545  df-tms 22546  df-cncf 23100  df-0p 23885  df-limc 24078  df-dv 24079  df-dvn 24080  df-ply 24392  df-idp 24393  df-coe 24394  df-dgr 24395  df-tayl 24557

This theorem is referenced by:  taylth  24577