taylthlem2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > taylthlem2		Structured version Visualization version GIF version

Theorem taylthlem2 26617

Description: Lemma for taylth 26618. (Contributed by Mario Carneiro, 1-Jan-2017.) Avoid ax-mulf 11208. (Revised by GG, 19-Apr-2025.)

**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 13682	. . . . . . . . . . 11 ⊢ (1...𝑁) ⊆ (0...𝑁)
4		taylthlem2.m	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ (1..^𝑁))
5		fzofzp1 13824	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ (1..^𝑁) → (𝑀 + 1) ∈ (1...𝑁))
6	4, 5	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀 + 1) ∈ (1...𝑁))
7	3, 6	sselid 3932	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀 + 1) ∈ (0...𝑁))
8		fznn0sub2 13694	. . . . . . . . . 10 ⊢ ((𝑀 + 1) ∈ (0...𝑁) → (𝑁 − (𝑀 + 1)) ∈ (0...𝑁))
9	7, 8	syl 18	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 − (𝑀 + 1)) ∈ (0...𝑁))
10		elfznn0 13679	. . . . . . . . 9 ⊢ ((𝑁 − (𝑀 + 1)) ∈ (0...𝑁) → (𝑁 − (𝑀 + 1)) ∈ ℕ₀)
11	9, 10	syl 18	. . . . . . . 8 ⊢ (𝜑 → (𝑁 − (𝑀 + 1)) ∈ ℕ₀)
12		dvnfre 26186	. . . . . . . 8 ⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ ∧ (𝑁 − (𝑀 + 1)) ∈ ℕ₀) → ((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):dom ((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))⟶ℝ)
13	2, 1, 11, 12	syl3anc 1398	. . . . . . 7 ⊢ (𝜑 → ((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):dom ((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))⟶ℝ)
14		reelprrecn 11220	. . . . . . . . . . . 12 ⊢ ℝ ∈ {ℝ, ℂ}
15	14	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})
16		cnex 11209	. . . . . . . . . . . . 13 ⊢ ℂ ∈ V
17	16	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ℂ ∈ V)
18		reex 11219	. . . . . . . . . . . . 13 ⊢ ℝ ∈ V
19	18	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ℝ ∈ V)
20		ax-resscn 11185	. . . . . . . . . . . . 13 ⊢ ℝ ⊆ ℂ
21		fss 6723	. . . . . . . . . . . . 13 ⊢ ((𝐹:𝐴⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐹:𝐴⟶ℂ)
22	2, 20, 21	sylancl 598	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)
23		elpm2r 8848	. . . . . . . . . . . 12 ⊢ (((ℂ ∈ V ∧ ℝ ∈ V) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ)) → 𝐹 ∈ (ℂ ↑_pm ℝ))
24	17, 19, 22, 1, 23	syl22anc 852	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ (ℂ ↑_pm ℝ))
25		dvnbss 26162	. . . . . . . . . . 11 ⊢ ((ℝ ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑_pm ℝ) ∧ (𝑁 − (𝑀 + 1)) ∈ ℕ₀) → dom ((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) ⊆ dom 𝐹)
26	15, 24, 11, 25	syl3anc 1398	. . . . . . . . . 10 ⊢ (𝜑 → dom ((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) ⊆ dom 𝐹)
27	2, 26	fssdmd 6725	. . . . . . . . 9 ⊢ (𝜑 → dom ((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) ⊆ 𝐴)
28		taylth.d	. . . . . . . . . 10 ⊢ (𝜑 → dom ((ℝ D^𝑛 𝐹)‘𝑁) = 𝐴)
29		dvn2bss 26164	. . . . . . . . . . 11 ⊢ ((ℝ ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑_pm ℝ) ∧ (𝑁 − (𝑀 + 1)) ∈ (0...𝑁)) → dom ((ℝ D^𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1))))
30	15, 24, 9, 29	syl3anc 1398	. . . . . . . . . 10 ⊢ (𝜑 → dom ((ℝ D^𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1))))
31	28, 30	eqsstrrd 3969	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ⊆ dom ((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1))))
32	27, 31	eqssd 3951	. . . . . . . 8 ⊢ (𝜑 → dom ((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) = 𝐴)
33	32	feq2d 6690	. . . . . . 7 ⊢ (𝜑 → (((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):dom ((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))⟶ℝ ↔ ((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℝ))
34	13, 33	mpbid 235	. . . . . 6 ⊢ (𝜑 → ((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℝ)
35	34	ffvelcdmda 7081	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℝ)
36	1	sselda 3934	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ)
37		fvres 6901	. . . . . . . 8 ⊢ (𝑦 ∈ ℝ → ((((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ↾ ℝ)‘𝑦) = (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))
38	37	adantl 487	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ↾ ℝ)‘𝑦) = (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))
39		resubdrg 21827	. . . . . . . . . . . 12 ⊢ (ℝ ∈ (SubRing‘ℂ_fld) ∧ ℝ_fld ∈ DivRing)
40	39	simpli 489	. . . . . . . . . . 11 ⊢ ℝ ∈ (SubRing‘ℂ_fld)
41	40	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ℝ ∈ (SubRing‘ℂ_fld))
42		taylth.n	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℕ)
43	42	nnnn0d 12593	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
44		taylth.b	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ 𝐴)
45	44, 28	eleqtrrd 2865	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ dom ((ℝ D^𝑛 𝐹)‘𝑁))
46		taylth.t	. . . . . . . . . . . 12 ⊢ 𝑇 = (𝑁(ℝ Tayl 𝐹)𝐵)
47	1, 44	sseldd 3935	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ ℝ)
48		elfznn0 13679	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ₀)
49		dvnfre 26186	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ ∧ 𝑘 ∈ ℕ₀) → ((ℝ D^𝑛 𝐹)‘𝑘):dom ((ℝ D^𝑛 𝐹)‘𝑘)⟶ℝ)
50	2, 1, 48, 49	syl2an3an 1449	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((ℝ D^𝑛 𝐹)‘𝑘):dom ((ℝ D^𝑛 𝐹)‘𝑘)⟶ℝ)
51		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ (0...𝑁))
52		dvn2bss 26164	. . . . . . . . . . . . . . . 16 ⊢ ((ℝ ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑_pm ℝ) ∧ 𝑘 ∈ (0...𝑁)) → dom ((ℝ D^𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ D^𝑛 𝐹)‘𝑘))
53	14, 24, 51, 52	mp3an2ani 1497	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → dom ((ℝ D^𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ D^𝑛 𝐹)‘𝑘))
54	45	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐵 ∈ dom ((ℝ D^𝑛 𝐹)‘𝑁))
55	53, 54	sseldd 3935	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐵 ∈ dom ((ℝ D^𝑛 𝐹)‘𝑘))
56	50, 55	ffvelcdmd 7082	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (((ℝ D^𝑛 𝐹)‘𝑘)‘𝐵) ∈ ℝ)
57	48	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ₀)
58	57	faccld 14352	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ)
59	56, 58	nndivred 12318	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((((ℝ D^𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) ∈ ℝ)
60	15, 22, 1, 43, 45, 46, 41, 47, 59	taylply2 26611	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑇 ∈ (Poly‘ℝ) ∧ (deg‘𝑇) ≤ 𝑁))
61	60	simpld 500	. . . . . . . . . 10 ⊢ (𝜑 → 𝑇 ∈ (Poly‘ℝ))
62		dvnply2 26524	. . . . . . . . . 10 ⊢ ((ℝ ∈ (SubRing‘ℂ_fld) ∧ 𝑇 ∈ (Poly‘ℝ) ∧ (𝑁 − (𝑀 + 1)) ∈ ℕ₀) → ((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (Poly‘ℝ))
63	41, 61, 11, 62	syl3anc 1398	. . . . . . . . 9 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (Poly‘ℝ))
64		plyreres 26520	. . . . . . . . 9 ⊢ (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (Poly‘ℝ) → (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ↾ ℝ):ℝ⟶ℝ)
65	63, 64	syl 18	. . . . . . . 8 ⊢ (𝜑 → (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ↾ ℝ):ℝ⟶ℝ)
66	65	ffvelcdmda 7081	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ↾ ℝ)‘𝑦) ∈ ℝ)
67	38, 66	eqeltrrd 2863	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℝ)
68	36, 67	syldan 603	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℝ)
69	35, 68	resubcld 11670	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ((((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)) ∈ ℝ)
70	69	fmpttd 7112	. . 3 ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ ((((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))):𝐴⟶ℝ)
71	47	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝐵 ∈ ℝ)
72	36, 71	resubcld 11670	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑦 − 𝐵) ∈ ℝ)
73		elfzouz 13723	. . . . . . . . . 10 ⊢ (𝑀 ∈ (1..^𝑁) → 𝑀 ∈ (ℤ_≥‘1))
74	4, 73	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘1))
75		nnuz 12930	. . . . . . . . 9 ⊢ ℕ = (ℤ_≥‘1)
76	74, 75	eleqtrrdi 2873	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℕ)
77	76	nnnn0d 12593	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
78	77	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑀 ∈ ℕ₀)
79		1nn0 12548	. . . . . . 7 ⊢ 1 ∈ ℕ₀
80	79	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 1 ∈ ℕ₀)
81	78, 80	nn0addcld 12597	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑀 + 1) ∈ ℕ₀)
82	72, 81	reexpcld 14231	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ((𝑦 − 𝐵)↑(𝑀 + 1)) ∈ ℝ)
83	82	fmpttd 7112	. . 3 ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))):𝐴⟶ℝ)
84		retop 24993	. . . . . 6 ⊢ (topGen‘ran (,)) ∈ Top
85		uniretop 24994	. . . . . . 7 ⊢ ℝ = ∪ (topGen‘ran (,))
86	85	ntrss2 23288	. . . . . 6 ⊢ (((topGen‘ran (,)) ∈ Top ∧ 𝐴 ⊆ ℝ) → ((int‘(topGen‘ran (,)))‘𝐴) ⊆ 𝐴)
87	84, 1, 86	sylancr 599	. . . . 5 ⊢ (𝜑 → ((int‘(topGen‘ran (,)))‘𝐴) ⊆ 𝐴)
88	42	nncnd 12277	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℂ)
89	76	nncnd 12277	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℂ)
90		1cnd 11230	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ ℂ)
91	88, 89, 90	nppcan2d 11623	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑁 − (𝑀 + 1)) + 1) = (𝑁 − 𝑀))
92	91	fveq2d 6886	. . . . . . . . 9 ⊢ (𝜑 → ((ℝ D^𝑛 𝐹)‘((𝑁 − (𝑀 + 1)) + 1)) = ((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀)))
93	20	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ℝ ⊆ ℂ)
94		dvnp1 26159	. . . . . . . . . 10 ⊢ ((ℝ ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm ℝ) ∧ (𝑁 − (𝑀 + 1)) ∈ ℕ₀) → ((ℝ D^𝑛 𝐹)‘((𝑁 − (𝑀 + 1)) + 1)) = (ℝ D ((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))))
95	93, 24, 11, 94	syl3anc 1398	. . . . . . . . 9 ⊢ (𝜑 → ((ℝ D^𝑛 𝐹)‘((𝑁 − (𝑀 + 1)) + 1)) = (ℝ D ((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))))
96	92, 95	eqtr3d 2799	. . . . . . . 8 ⊢ (𝜑 → ((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀)) = (ℝ D ((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))))
97	96	dmeqd 5893	. . . . . . 7 ⊢ (𝜑 → dom ((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀)) = dom (ℝ D ((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))))
98		fzonnsub 13744	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ (1..^𝑁) → (𝑁 − 𝑀) ∈ ℕ)
99	4, 98	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 − 𝑀) ∈ ℕ)
100	99	nnnn0d 12593	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 − 𝑀) ∈ ℕ₀)
101		dvnbss 26162	. . . . . . . . . 10 ⊢ ((ℝ ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑_pm ℝ) ∧ (𝑁 − 𝑀) ∈ ℕ₀) → dom ((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀)) ⊆ dom 𝐹)
102	15, 24, 100, 101	syl3anc 1398	. . . . . . . . 9 ⊢ (𝜑 → dom ((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀)) ⊆ dom 𝐹)
103	2, 102	fssdmd 6725	. . . . . . . 8 ⊢ (𝜑 → dom ((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀)) ⊆ 𝐴)
104		elfzofz 13735	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ (1..^𝑁) → 𝑀 ∈ (1...𝑁))
105	4, 104	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ (1...𝑁))
106	3, 105	sselid 3932	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ (0...𝑁))
107		fznn0sub2 13694	. . . . . . . . . . 11 ⊢ (𝑀 ∈ (0...𝑁) → (𝑁 − 𝑀) ∈ (0...𝑁))
108	106, 107	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 − 𝑀) ∈ (0...𝑁))
109		dvn2bss 26164	. . . . . . . . . 10 ⊢ ((ℝ ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑_pm ℝ) ∧ (𝑁 − 𝑀) ∈ (0...𝑁)) → dom ((ℝ D^𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀)))
110	15, 24, 108, 109	syl3anc 1398	. . . . . . . . 9 ⊢ (𝜑 → dom ((ℝ D^𝑛 𝐹)‘𝑁) ⊆ dom ((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀)))
111	28, 110	eqsstrrd 3969	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ⊆ dom ((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀)))
112	103, 111	eqssd 3951	. . . . . . 7 ⊢ (𝜑 → dom ((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀)) = 𝐴)
113	97, 112	eqtr3d 2799	. . . . . 6 ⊢ (𝜑 → dom (ℝ D ((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))) = 𝐴)
114		fss 6723	. . . . . . . 8 ⊢ ((((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℝ ∧ ℝ ⊆ ℂ) → ((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℂ)
115	34, 20, 114	sylancl 598	. . . . . . 7 ⊢ (𝜑 → ((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℂ)
116		tgioo4 25037	. . . . . . 7 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
117		eqid 2762	. . . . . . 7 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
118	93, 115, 1, 116, 117	dvbssntr 26134	. . . . . 6 ⊢ (𝜑 → dom (ℝ D ((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))) ⊆ ((int‘(topGen‘ran (,)))‘𝐴))
119	113, 118	eqsstrrd 3969	. . . . 5 ⊢ (𝜑 → 𝐴 ⊆ ((int‘(topGen‘ran (,)))‘𝐴))
120	87, 119	eqssd 3951	. . . 4 ⊢ (𝜑 → ((int‘(topGen‘ran (,)))‘𝐴) = 𝐴)
121	85	isopn3 23297	. . . . 5 ⊢ (((topGen‘ran (,)) ∈ Top ∧ 𝐴 ⊆ ℝ) → (𝐴 ∈ (topGen‘ran (,)) ↔ ((int‘(topGen‘ran (,)))‘𝐴) = 𝐴))
122	84, 1, 121	sylancr 599	. . . 4 ⊢ (𝜑 → (𝐴 ∈ (topGen‘ran (,)) ↔ ((int‘(topGen‘ran (,)))‘𝐴) = 𝐴))
123	120, 122	mpbird 260	. . 3 ⊢ (𝜑 → 𝐴 ∈ (topGen‘ran (,)))
124		eqid 2762	. . 3 ⊢ (𝐴 ∖ {𝐵}) = (𝐴 ∖ {𝐵})
125		difss 4086	. . . 4 ⊢ (𝐴 ∖ {𝐵}) ⊆ 𝐴
126	35	recnd 11265	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℂ)
127		dvnf 26161	. . . . . . . . . 10 ⊢ ((ℝ ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑_pm ℝ) ∧ (𝑁 − 𝑀) ∈ ℕ₀) → ((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀)):dom ((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))⟶ℂ)
128	15, 24, 100, 127	syl3anc 1398	. . . . . . . . 9 ⊢ (𝜑 → ((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀)):dom ((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))⟶ℂ)
129	112	feq2d 6690	. . . . . . . . 9 ⊢ (𝜑 → (((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀)):dom ((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))⟶ℂ ↔ ((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀)):𝐴⟶ℂ))
130	128, 129	mpbid 235	. . . . . . . 8 ⊢ (𝜑 → ((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀)):𝐴⟶ℂ)
131	130	ffvelcdmda 7081	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑦) ∈ ℂ)
132		dvnfre 26186	. . . . . . . . . . 11 ⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ ∧ (𝑁 − 𝑀) ∈ ℕ₀) → ((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀)):dom ((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))⟶ℝ)
133	2, 1, 100, 132	syl3anc 1398	. . . . . . . . . 10 ⊢ (𝜑 → ((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀)):dom ((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))⟶ℝ)
134	112	feq2d 6690	. . . . . . . . . 10 ⊢ (𝜑 → (((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀)):dom ((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))⟶ℝ ↔ ((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀)):𝐴⟶ℝ))
135	133, 134	mpbid 235	. . . . . . . . 9 ⊢ (𝜑 → ((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀)):𝐴⟶ℝ)
136	135	feqmptd 6950	. . . . . . . 8 ⊢ (𝜑 → ((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀)) = (𝑦 ∈ 𝐴 ↦ (((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑦)))
137	34	feqmptd 6950	. . . . . . . . 9 ⊢ (𝜑 → ((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) = (𝑦 ∈ 𝐴 ↦ (((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦)))
138	137	oveq2d 7433	. . . . . . . 8 ⊢ (𝜑 → (ℝ D ((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))) = (ℝ D (𝑦 ∈ 𝐴 ↦ (((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦))))
139	96, 136, 138	3eqtr3rd 2806	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝑦 ∈ 𝐴 ↦ (((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦))) = (𝑦 ∈ 𝐴 ↦ (((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑦)))
140	68	recnd 11265	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℂ)
141		fvexd 6897	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦) ∈ V)
142	67	recnd 11265	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℂ)
143		recn 11218	. . . . . . . . 9 ⊢ (𝑦 ∈ ℝ → 𝑦 ∈ ℂ)
144		dvnply2 26524	. . . . . . . . . . . 12 ⊢ ((ℝ ∈ (SubRing‘ℂ_fld) ∧ 𝑇 ∈ (Poly‘ℝ) ∧ (𝑁 − 𝑀) ∈ ℕ₀) → ((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀)) ∈ (Poly‘ℝ))
145	41, 61, 100, 144	syl3anc 1398	. . . . . . . . . . 11 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀)) ∈ (Poly‘ℝ))
146		plyf 26430	. . . . . . . . . . 11 ⊢ (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀)) ∈ (Poly‘ℝ) → ((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀)):ℂ⟶ℂ)
147	145, 146	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀)):ℂ⟶ℂ)
148	147	ffvelcdmda 7081	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦) ∈ ℂ)
149	143, 148	sylan2 605	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦) ∈ ℂ)
150	117	cnfldtopon 25014	. . . . . . . . . 10 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
151		toponmax 23157	. . . . . . . . . 10 ⊢ ((TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ) → ℂ ∈ (TopOpen‘ℂ_fld))
152	150, 151	mp1i 14	. . . . . . . . 9 ⊢ (𝜑 → ℂ ∈ (TopOpen‘ℂ_fld))
153		dfss2 3920	. . . . . . . . . 10 ⊢ (ℝ ⊆ ℂ ↔ (ℝ ∩ ℂ) = ℝ)
154	93, 153	sylib 221	. . . . . . . . 9 ⊢ (𝜑 → (ℝ ∩ ℂ) = ℝ)
155		plyf 26430	. . . . . . . . . . 11 ⊢ (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (Poly‘ℝ) → ((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1))):ℂ⟶ℂ)
156	63, 155	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1))):ℂ⟶ℂ)
157	156	ffvelcdmda 7081	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) ∈ ℂ)
158	91	fveq2d 6886	. . . . . . . . . . 11 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘((𝑁 − (𝑀 + 1)) + 1)) = ((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀)))
159		ssid 3956	. . . . . . . . . . . . 13 ⊢ ℂ ⊆ ℂ
160	159	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ℂ ⊆ ℂ)
161		mapsspm 8887	. . . . . . . . . . . . 13 ⊢ (ℂ ↑_m ℂ) ⊆ (ℂ ↑_pm ℂ)
162		plyf 26430	. . . . . . . . . . . . . . 15 ⊢ (𝑇 ∈ (Poly‘ℝ) → 𝑇:ℂ⟶ℂ)
163	61, 162	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑇:ℂ⟶ℂ)
164	16, 16	elmap 8882	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ (ℂ ↑_m ℂ) ↔ 𝑇:ℂ⟶ℂ)
165	163, 164	sylibr 237	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑇 ∈ (ℂ ↑_m ℂ))
166	161, 165	sselid 3932	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑇 ∈ (ℂ ↑_pm ℂ))
167		dvnp1 26159	. . . . . . . . . . . 12 ⊢ ((ℂ ⊆ ℂ ∧ 𝑇 ∈ (ℂ ↑_pm ℂ) ∧ (𝑁 − (𝑀 + 1)) ∈ ℕ₀) → ((ℂ D^𝑛 𝑇)‘((𝑁 − (𝑀 + 1)) + 1)) = (ℂ D ((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))))
168	160, 166, 11, 167	syl3anc 1398	. . . . . . . . . . 11 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘((𝑁 − (𝑀 + 1)) + 1)) = (ℂ D ((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))))
169	158, 168	eqtr3d 2799	. . . . . . . . . 10 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀)) = (ℂ D ((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))))
170	147	feqmptd 6950	. . . . . . . . . 10 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀)) = (𝑦 ∈ ℂ ↦ (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦)))
171	156	feqmptd 6950	. . . . . . . . . . 11 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) = (𝑦 ∈ ℂ ↦ (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))
172	171	oveq2d 7433	. . . . . . . . . 10 ⊢ (𝜑 → (ℂ D ((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))) = (ℂ D (𝑦 ∈ ℂ ↦ (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))
173	169, 170, 172	3eqtr3rd 2806	. . . . . . . . 9 ⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) = (𝑦 ∈ ℂ ↦ (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦)))
174	117, 15, 152, 154, 157, 148, 173	dvmptres3 26190	. . . . . . . 8 ⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) = (𝑦 ∈ ℝ ↦ (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦)))
175	15, 142, 149, 174, 1, 116, 117, 123	dvmptres 26197	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝑦 ∈ 𝐴 ↦ (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) = (𝑦 ∈ 𝐴 ↦ (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦)))
176	15, 126, 131, 139, 140, 141, 175	dvmptsub 26201	. . . . . 6 ⊢ (𝜑 → (ℝ D (𝑦 ∈ 𝐴 ↦ ((((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))) = (𝑦 ∈ 𝐴 ↦ ((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦))))
177	176	dmeqd 5893	. . . . 5 ⊢ (𝜑 → dom (ℝ D (𝑦 ∈ 𝐴 ↦ ((((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))) = dom (𝑦 ∈ 𝐴 ↦ ((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦))))
178		ovex 7450	. . . . . 6 ⊢ ((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦)) ∈ V
179		eqid 2762	. . . . . 6 ⊢ (𝑦 ∈ 𝐴 ↦ ((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦))) = (𝑦 ∈ 𝐴 ↦ ((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦)))
180	178, 179	dmmpti 6680	. . . . 5 ⊢ dom (𝑦 ∈ 𝐴 ↦ ((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦))) = 𝐴
181	177, 180	eqtrdi 2813	. . . 4 ⊢ (𝜑 → dom (ℝ D (𝑦 ∈ 𝐴 ↦ ((((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))) = 𝐴)
182	125, 181	sseqtrrid 3977	. . 3 ⊢ (𝜑 → (𝐴 ∖ {𝐵}) ⊆ dom (ℝ D (𝑦 ∈ 𝐴 ↦ ((((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))))
183		simpr 490	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝑦 ∈ ℂ)
184	47	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝐵 ∈ ℝ)
185	184	recnd 11265	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝐵 ∈ ℂ)
186	183, 185	subcld 11597	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝑦 − 𝐵) ∈ ℂ)
187	77	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝑀 ∈ ℕ₀)
188	79	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 1 ∈ ℕ₀)
189	187, 188	nn0addcld 12597	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝑀 + 1) ∈ ℕ₀)
190	186, 189	expcld 14214	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((𝑦 − 𝐵)↑(𝑀 + 1)) ∈ ℂ)
191	143, 190	sylan2 605	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑦 − 𝐵)↑(𝑀 + 1)) ∈ ℂ)
192	89	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝑀 ∈ ℂ)
193		1cnd 11230	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 1 ∈ ℂ)
194	192, 193	addcld 11256	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝑀 + 1) ∈ ℂ)
195	186, 187	expcld 14214	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((𝑦 − 𝐵)↑𝑀) ∈ ℂ)
196	194, 195	mulcld 11257	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)) ∈ ℂ)
197	143, 196	sylan2 605	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)) ∈ ℂ)
198	16	prid2 4727	. . . . . . . . . . 11 ⊢ ℂ ∈ {ℝ, ℂ}
199	198	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ℂ ∈ {ℝ, ℂ})
200		simpr 490	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝑥 ∈ ℂ)
201		elfznn 13612	. . . . . . . . . . . . . 14 ⊢ ((𝑀 + 1) ∈ (1...𝑁) → (𝑀 + 1) ∈ ℕ)
202	6, 201	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑀 + 1) ∈ ℕ)
203	202	nnnn0d 12593	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀 + 1) ∈ ℕ₀)
204	203	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝑀 + 1) ∈ ℕ₀)
205	200, 204	expcld 14214	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝑥↑(𝑀 + 1)) ∈ ℂ)
206		ovexd 7452	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((𝑀 + 1) · (𝑥↑𝑀)) ∈ V)
207	199	dvmptid 26191	. . . . . . . . . . . 12 ⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ 𝑦)) = (𝑦 ∈ ℂ ↦ 1))
208		0cnd 11227	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 0 ∈ ℂ)
209	47	recnd 11265	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ ℂ)
210	199, 209	dvmptc 26192	. . . . . . . . . . . 12 ⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ 𝐵)) = (𝑦 ∈ ℂ ↦ 0))
211	199, 183, 193, 207, 185, 208, 210	dvmptsub 26201	. . . . . . . . . . 11 ⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦 − 𝐵))) = (𝑦 ∈ ℂ ↦ (1 − 0)))
212		1m0e1 12388	. . . . . . . . . . . 12 ⊢ (1 − 0) = 1
213	212	mpteq2i 5205	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℂ ↦ (1 − 0)) = (𝑦 ∈ ℂ ↦ 1)
214	211, 213	eqtrdi 2813	. . . . . . . . . 10 ⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦 − 𝐵))) = (𝑦 ∈ ℂ ↦ 1))
215		dvexp 26187	. . . . . . . . . . . 12 ⊢ ((𝑀 + 1) ∈ ℕ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑(𝑀 + 1)))) = (𝑥 ∈ ℂ ↦ ((𝑀 + 1) · (𝑥↑((𝑀 + 1) − 1)))))
216	202, 215	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑(𝑀 + 1)))) = (𝑥 ∈ ℂ ↦ ((𝑀 + 1) · (𝑥↑((𝑀 + 1) − 1)))))
217	89, 90	pncand 11598	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀 + 1) − 1) = 𝑀)
218	217	oveq2d 7433	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥↑((𝑀 + 1) − 1)) = (𝑥↑𝑀))
219	218	oveq2d 7433	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑀 + 1) · (𝑥↑((𝑀 + 1) − 1))) = ((𝑀 + 1) · (𝑥↑𝑀)))
220	219	mpteq2dv 5203	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ ((𝑀 + 1) · (𝑥↑((𝑀 + 1) − 1)))) = (𝑥 ∈ ℂ ↦ ((𝑀 + 1) · (𝑥↑𝑀))))
221	216, 220	eqtrd 2797	. . . . . . . . . 10 ⊢ (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑(𝑀 + 1)))) = (𝑥 ∈ ℂ ↦ ((𝑀 + 1) · (𝑥↑𝑀))))
222		oveq1 7424	. . . . . . . . . 10 ⊢ (𝑥 = (𝑦 − 𝐵) → (𝑥↑(𝑀 + 1)) = ((𝑦 − 𝐵)↑(𝑀 + 1)))
223		oveq1 7424	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑦 − 𝐵) → (𝑥↑𝑀) = ((𝑦 − 𝐵)↑𝑀))
224	223	oveq2d 7433	. . . . . . . . . 10 ⊢ (𝑥 = (𝑦 − 𝐵) → ((𝑀 + 1) · (𝑥↑𝑀)) = ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)))
225	199, 199, 186, 193, 205, 206, 214, 221, 222, 224	dvmptco 26206	. . . . . . . . 9 ⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) = (𝑦 ∈ ℂ ↦ (((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)) · 1)))
226	196	mulridd 11254	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)) · 1) = ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)))
227	226	mpteq2dva 5202	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ ℂ ↦ (((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)) · 1)) = (𝑦 ∈ ℂ ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))))
228	225, 227	eqtrd 2797	. . . . . . . 8 ⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) = (𝑦 ∈ ℂ ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))))
229	117, 15, 152, 154, 190, 196, 228	dvmptres3 26190	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) = (𝑦 ∈ ℝ ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))))
230	15, 191, 197, 229, 1, 116, 117, 123	dvmptres 26197	. . . . . 6 ⊢ (𝜑 → (ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) = (𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))))
231	230	dmeqd 5893	. . . . 5 ⊢ (𝜑 → dom (ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) = dom (𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))))
232		ovex 7450	. . . . . 6 ⊢ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)) ∈ V
233		eqid 2762	. . . . . 6 ⊢ (𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) = (𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)))
234	232, 233	dmmpti 6680	. . . . 5 ⊢ dom (𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) = 𝐴
235	231, 234	eqtrdi 2813	. . . 4 ⊢ (𝜑 → dom (ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) = 𝐴)
236	125, 235	sseqtrrid 3977	. . 3 ⊢ (𝜑 → (𝐴 ∖ {𝐵}) ⊆ dom (ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))))
237	15, 22, 1, 9, 45, 46	dvntaylp0 26615	. . . . . 6 ⊢ (𝜑 → (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵) = (((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵))
238	237	oveq2d 7433	. . . . 5 ⊢ (𝜑 → ((((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵)) = ((((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵)))
239	115, 44	ffvelcdmd 7082	. . . . . 6 ⊢ (𝜑 → (((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) ∈ ℂ)
240	239	subidd 11585	. . . . 5 ⊢ (𝜑 → ((((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵)) = 0)
241	238, 240	eqtrd 2797	. . . 4 ⊢ (𝜑 → ((((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵)) = 0)
242	117	subcn 25099	. . . . . . 7 ⊢ − ∈ (((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) Cn (TopOpen‘ℂ_fld))
243	242	a1i 11	. . . . . 6 ⊢ (𝜑 → − ∈ (((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) Cn (TopOpen‘ℂ_fld)))
244		dvcn 26155	. . . . . . . 8 ⊢ (((ℝ ⊆ ℂ ∧ ((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1))):𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) ∧ dom (ℝ D ((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))) = 𝐴) → ((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) ∈ (𝐴–cn→ℂ))
245	93, 115, 1, 113, 244	syl31anc 1400	. . . . . . 7 ⊢ (𝜑 → ((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1))) ∈ (𝐴–cn→ℂ))
246	137, 245	eqeltrrd 2863	. . . . . 6 ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ (((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦)) ∈ (𝐴–cn→ℂ))
247		plycn 26494	. . . . . . . 8 ⊢ (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (Poly‘ℝ) → ((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (ℂ–cn→ℂ))
248	63, 247	syl 18	. . . . . . 7 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1))) ∈ (ℂ–cn→ℂ))
249	1, 20	sstrdi 3946	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ⊆ ℂ)
250		cncfmptid 25147	. . . . . . . 8 ⊢ ((𝐴 ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑦 ∈ 𝐴 ↦ 𝑦) ∈ (𝐴–cn→ℂ))
251	249, 159, 250	sylancl 598	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ 𝑦) ∈ (𝐴–cn→ℂ))
252	248, 251	cncfmpt1f 25148	. . . . . 6 ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)) ∈ (𝐴–cn→ℂ))
253	117, 243, 246, 252	cncfmpt2f 25149	. . . . 5 ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ ((((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) ∈ (𝐴–cn→ℂ))
254		fveq2 6882	. . . . . 6 ⊢ (𝑦 = 𝐵 → (((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) = (((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵))
255		fveq2 6882	. . . . . 6 ⊢ (𝑦 = 𝐵 → (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) = (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵))
256	254, 255	oveq12d 7435	. . . . 5 ⊢ (𝑦 = 𝐵 → ((((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)) = ((((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵)))
257	253, 44, 256	cnmptlimc 26124	. . . 4 ⊢ (𝜑 → ((((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝐵) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝐵)) ∈ ((𝑦 ∈ 𝐴 ↦ ((((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) lim_ℂ 𝐵))
258	241, 257	eqeltrrd 2863	. . 3 ⊢ (𝜑 → 0 ∈ ((𝑦 ∈ 𝐴 ↦ ((((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) lim_ℂ 𝐵))
259	209	subidd 11585	. . . . . 6 ⊢ (𝜑 → (𝐵 − 𝐵) = 0)
260	259	oveq1d 7432	. . . . 5 ⊢ (𝜑 → ((𝐵 − 𝐵)↑(𝑀 + 1)) = (0↑(𝑀 + 1)))
261	202	0expd 14207	. . . . 5 ⊢ (𝜑 → (0↑(𝑀 + 1)) = 0)
262	260, 261	eqtrd 2797	. . . 4 ⊢ (𝜑 → ((𝐵 − 𝐵)↑(𝑀 + 1)) = 0)
263	249	sselda 3934	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℂ)
264	263, 190	syldan 603	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ((𝑦 − 𝐵)↑(𝑀 + 1)) ∈ ℂ)
265	264	fmpttd 7112	. . . . . 6 ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))):𝐴⟶ℂ)
266		dvcn 26155	. . . . . 6 ⊢ (((ℝ ⊆ ℂ ∧ (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))):𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) ∧ dom (ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) = 𝐴) → (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) ∈ (𝐴–cn→ℂ))
267	93, 265, 1, 235, 266	syl31anc 1400	. . . . 5 ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) ∈ (𝐴–cn→ℂ))
268		oveq1 7424	. . . . . 6 ⊢ (𝑦 = 𝐵 → (𝑦 − 𝐵) = (𝐵 − 𝐵))
269	268	oveq1d 7432	. . . . 5 ⊢ (𝑦 = 𝐵 → ((𝑦 − 𝐵)↑(𝑀 + 1)) = ((𝐵 − 𝐵)↑(𝑀 + 1)))
270	267, 44, 269	cnmptlimc 26124	. . . 4 ⊢ (𝜑 → ((𝐵 − 𝐵)↑(𝑀 + 1)) ∈ ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) lim_ℂ 𝐵))
271	262, 270	eqeltrrd 2863	. . 3 ⊢ (𝜑 → 0 ∈ ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) lim_ℂ 𝐵))
272	249	ssdifssd 4097	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 ∖ {𝐵}) ⊆ ℂ)
273	272	sselda 3934	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑦 ∈ ℂ)
274	209	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝐵 ∈ ℂ)
275	273, 274	subcld 11597	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑦 − 𝐵) ∈ ℂ)
276		eldifsni 4756	. . . . . . . . . 10 ⊢ (𝑦 ∈ (𝐴 ∖ {𝐵}) → 𝑦 ≠ 𝐵)
277	276	adantl 487	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑦 ≠ 𝐵)
278	273, 274, 277	subne0d 11607	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑦 − 𝐵) ≠ 0)
279	202	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ∈ ℕ)
280	279	nnzd 12645	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ∈ ℤ)
281	275, 278, 280	expne0d 14220	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → ((𝑦 − 𝐵)↑(𝑀 + 1)) ≠ 0)
282	281	necomd 3012	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → 0 ≠ ((𝑦 − 𝐵)↑(𝑀 + 1)))
283	282	neneqd 2962	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → ¬ 0 = ((𝑦 − 𝐵)↑(𝑀 + 1)))
284	283	nrexdv 3159	. . . 4 ⊢ (𝜑 → ¬ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑦 − 𝐵)↑(𝑀 + 1)))
285		df-ima 5672	. . . . . 6 ⊢ ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) “ (𝐴 ∖ {𝐵})) = ran ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) ↾ (𝐴 ∖ {𝐵}))
286	285	eleq2i 2854	. . . . 5 ⊢ (0 ∈ ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) “ (𝐴 ∖ {𝐵})) ↔ 0 ∈ ran ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})))
287		resmpt 6037	. . . . . . 7 ⊢ ((𝐴 ∖ {𝐵}) ⊆ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))))
288	125, 287	ax-mp 5	. . . . . 6 ⊢ ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))
289		ovex 7450	. . . . . 6 ⊢ ((𝑦 − 𝐵)↑(𝑀 + 1)) ∈ V
290	288, 289	elrnmpti 5950	. . . . 5 ⊢ (0 ∈ ran ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) ↔ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑦 − 𝐵)↑(𝑀 + 1)))
291	286, 290	bitri 278	. . . 4 ⊢ (0 ∈ ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) “ (𝐴 ∖ {𝐵})) ↔ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑦 − 𝐵)↑(𝑀 + 1)))
292	284, 291	sylnibr 332	. . 3 ⊢ (𝜑 → ¬ 0 ∈ ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) “ (𝐴 ∖ {𝐵})))
293	89	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑀 ∈ ℂ)
294		1cnd 11230	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → 1 ∈ ℂ)
295	293, 294	addcld 11256	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ∈ ℂ)
296	273, 195	syldan 603	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → ((𝑦 − 𝐵)↑𝑀) ∈ ℂ)
297	279	nnne0d 12314	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ≠ 0)
298	76	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑀 ∈ ℕ)
299	298	nnzd 12645	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → 𝑀 ∈ ℤ)
300	275, 278, 299	expne0d 14220	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → ((𝑦 − 𝐵)↑𝑀) ≠ 0)
301	295, 296, 297, 300	mulne0d 11894	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)) ≠ 0)
302	301	necomd 3012	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → 0 ≠ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)))
303	302	neneqd 2962	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∖ {𝐵})) → ¬ 0 = ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)))
304	303	nrexdv 3159	. . . 4 ⊢ (𝜑 → ¬ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)))
305	230	imaeq1d 6059	. . . . . . 7 ⊢ (𝜑 → ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) “ (𝐴 ∖ {𝐵})) = ((𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) “ (𝐴 ∖ {𝐵})))
306		df-ima 5672	. . . . . . 7 ⊢ ((𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) “ (𝐴 ∖ {𝐵})) = ran ((𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵}))
307	305, 306	eqtrdi 2813	. . . . . 6 ⊢ (𝜑 → ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) “ (𝐴 ∖ {𝐵})) = ran ((𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵})))
308	307	eleq2d 2848	. . . . 5 ⊢ (𝜑 → (0 ∈ ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) “ (𝐴 ∖ {𝐵})) ↔ 0 ∈ ran ((𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵}))))
309		resmpt 6037	. . . . . . 7 ⊢ ((𝐴 ∖ {𝐵}) ⊆ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵})) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))))
310	125, 309	ax-mp 5	. . . . . 6 ⊢ ((𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵})) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)))
311	310, 232	elrnmpti 5950	. . . . 5 ⊢ (0 ∈ ran ((𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))) ↾ (𝐴 ∖ {𝐵})) ↔ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)))
312	308, 311	bitrdi 290	. . . 4 ⊢ (𝜑 → (0 ∈ ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) “ (𝐴 ∖ {𝐵})) ↔ ∃𝑦 ∈ (𝐴 ∖ {𝐵})0 = ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀))))
313	304, 312	mtbird 328	. . 3 ⊢ (𝜑 → ¬ 0 ∈ ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))) “ (𝐴 ∖ {𝐵})))
314		eldifi 4081	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴 ∖ {𝐵}) → 𝑥 ∈ 𝐴)
315	130	ffvelcdmda 7081	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) ∈ ℂ)
316	314, 315	sylan2 605	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) ∈ ℂ)
317	1	ssdifssd 4097	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 ∖ {𝐵}) ⊆ ℝ)
318	317	sselda 3934	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ ℝ)
319	318	recnd 11265	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ ℂ)
320	147	ffvelcdmda 7081	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥) ∈ ℂ)
321	319, 320	syldan 603	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥) ∈ ℂ)
322	316, 321	subcld 11597	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) ∈ ℂ)
323	47	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝐵 ∈ ℝ)
324	318, 323	resubcld 11670	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑥 − 𝐵) ∈ ℝ)
325	77	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑀 ∈ ℕ₀)
326	324, 325	reexpcld 14231	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑥 − 𝐵)↑𝑀) ∈ ℝ)
327	326	recnd 11265	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑥 − 𝐵)↑𝑀) ∈ ℂ)
328	323	recnd 11265	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝐵 ∈ ℂ)
329	319, 328	subcld 11597	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑥 − 𝐵) ∈ ℂ)
330		eldifsni 4756	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐴 ∖ {𝐵}) → 𝑥 ≠ 𝐵)
331	330	adantl 487	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ≠ 𝐵)
332	319, 328, 331	subne0d 11607	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑥 − 𝐵) ≠ 0)
333	325	nn0zd 12644	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑀 ∈ ℤ)
334	329, 332, 333	expne0d 14220	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑥 − 𝐵)↑𝑀) ≠ 0)
335	322, 327, 334	divcld 12019	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) ∈ ℂ)
336	202	nnrecred 12315	. . . . . . . 8 ⊢ (𝜑 → (1 / (𝑀 + 1)) ∈ ℝ)
337	336	recnd 11265	. . . . . . 7 ⊢ (𝜑 → (1 / (𝑀 + 1)) ∈ ℂ)
338	337	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (1 / (𝑀 + 1)) ∈ ℂ)
339		txtopon 23823	. . . . . . . 8 ⊢ (((TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ) ∧ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)) → ((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) ∈ (TopOn‘(ℂ × ℂ)))
340	150, 150, 339	mp2an 705	. . . . . . 7 ⊢ ((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) ∈ (TopOn‘(ℂ × ℂ))
341	340	toponrestid 23152	. . . . . 6 ⊢ ((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) = (((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) ↾_t (ℂ × ℂ))
342		taylthlem2.i	. . . . . 6 ⊢ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀))) lim_ℂ 𝐵))
343		limcresi 26119	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 ↦ (1 / (𝑀 + 1))) lim_ℂ 𝐵) ⊆ (((𝑥 ∈ 𝐴 ↦ (1 / (𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) lim_ℂ 𝐵)
344		resmpt 6037	. . . . . . . . . 10 ⊢ ((𝐴 ∖ {𝐵}) ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ (1 / (𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (1 / (𝑀 + 1))))
345	125, 344	ax-mp 5	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 ↦ (1 / (𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (1 / (𝑀 + 1)))
346	345	oveq1i 7427	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ↦ (1 / (𝑀 + 1))) ↾ (𝐴 ∖ {𝐵})) lim_ℂ 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (1 / (𝑀 + 1))) lim_ℂ 𝐵)
347	343, 346	sseqtri 3982	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 ↦ (1 / (𝑀 + 1))) lim_ℂ 𝐵) ⊆ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (1 / (𝑀 + 1))) lim_ℂ 𝐵)
348		cncfmptc 25146	. . . . . . . . 9 ⊢ (((1 / (𝑀 + 1)) ∈ ℝ ∧ 𝐴 ⊆ ℂ ∧ ℝ ⊆ ℂ) → (𝑥 ∈ 𝐴 ↦ (1 / (𝑀 + 1))) ∈ (𝐴–cn→ℝ))
349	336, 249, 93, 348	syl3anc 1398	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (1 / (𝑀 + 1))) ∈ (𝐴–cn→ℝ))
350		eqidd 2763	. . . . . . . 8 ⊢ (𝑥 = 𝐵 → (1 / (𝑀 + 1)) = (1 / (𝑀 + 1)))
351	349, 44, 350	cnmptlimc 26124	. . . . . . 7 ⊢ (𝜑 → (1 / (𝑀 + 1)) ∈ ((𝑥 ∈ 𝐴 ↦ (1 / (𝑀 + 1))) lim_ℂ 𝐵))
352	347, 351	sselid 3932	. . . . . 6 ⊢ (𝜑 → (1 / (𝑀 + 1)) ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (1 / (𝑀 + 1))) lim_ℂ 𝐵))
353	117	mpomulcn 25101	. . . . . . 7 ⊢ (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ (((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) Cn (TopOpen‘ℂ_fld))
354		0cn 11226	. . . . . . . 8 ⊢ 0 ∈ ℂ
355		opelxpi 5696	. . . . . . . 8 ⊢ ((0 ∈ ℂ ∧ (1 / (𝑀 + 1)) ∈ ℂ) → ⟨0, (1 / (𝑀 + 1))⟩ ∈ (ℂ × ℂ))
356	354, 337, 355	sylancr 599	. . . . . . 7 ⊢ (𝜑 → ⟨0, (1 / (𝑀 + 1))⟩ ∈ (ℂ × ℂ))
357	340	toponunii 23147	. . . . . . . 8 ⊢ (ℂ × ℂ) = ∪ ((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld))
358	357	cncnpi 23509	. . . . . . 7 ⊢ (((𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ (((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 599	. . . . . 6 ⊢ (𝜑 → (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ ((((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) CnP (TopOpen‘ℂ_fld))‘⟨0, (1 / (𝑀 + 1))⟩))
360	335, 338, 160, 160, 117, 341, 342, 352, 359	limccnp2 26126	. . . . 5 ⊢ (𝜑 → (0(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(1 / (𝑀 + 1))) ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(1 / (𝑀 + 1)))) lim_ℂ 𝐵))
361		0cnd 11227	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ ℂ)
362	361, 337	jca 521	. . . . . . . . 9 ⊢ (𝜑 → (0 ∈ ℂ ∧ (1 / (𝑀 + 1)) ∈ ℂ))
363		ovmpot 7578	. . . . . . . . 9 ⊢ ((0 ∈ ℂ ∧ (1 / (𝑀 + 1)) ∈ ℂ) → (0(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(1 / (𝑀 + 1))) = (0 · (1 / (𝑀 + 1))))
364	362, 363	syl 18	. . . . . . . 8 ⊢ (𝜑 → (0(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(1 / (𝑀 + 1))) = (0 · (1 / (𝑀 + 1))))
365		df-mpt 5191	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(1 / (𝑀 + 1)))) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑧 = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(1 / (𝑀 + 1))))}
366	365	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(1 / (𝑀 + 1)))) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑧 = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(1 / (𝑀 + 1))))})
367		idd 25	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) → 𝑥 ∈ (𝐴 ∖ {𝐵})))
368	367	adantrd 497	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑧 = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(1 / (𝑀 + 1)))) → 𝑥 ∈ (𝐴 ∖ {𝐵})))
369	335, 338	jca 521	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) ∈ ℂ ∧ (1 / (𝑀 + 1)) ∈ ℂ))
370		ovmpot 7578	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) ∈ ℂ ∧ (1 / (𝑀 + 1)) ∈ ℂ) → ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(1 / (𝑀 + 1))) = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1))))
371	369, 370	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(1 / (𝑀 + 1))) = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1))))
372		eqeq2 2774	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(1 / (𝑀 + 1))) = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1))) → (𝑧 = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(1 / (𝑀 + 1))) ↔ 𝑧 = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1)))))
373	372	biimpd 232	. . . . . . . . . . . . . . . . 17 ⊢ (((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(1 / (𝑀 + 1))) = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1))) → (𝑧 = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(1 / (𝑀 + 1))) → 𝑧 = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1)))))
374	371, 373	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑧 = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(1 / (𝑀 + 1))) → 𝑧 = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1)))))
375	374	ex 418	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) → (𝑧 = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(1 / (𝑀 + 1))) → 𝑧 = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1))))))
376	375	impd 416	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑧 = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(1 / (𝑀 + 1)))) → 𝑧 = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1)))))
377	368, 376	jcad 522	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑧 = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(1 / (𝑀 + 1)))) → (𝑥 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑧 = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1))))))
378	367	adantrd 497	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑧 = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1)))) → 𝑥 ∈ (𝐴 ∖ {𝐵})))
379	370	eqcomd 2768	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) ∈ ℂ ∧ (1 / (𝑀 + 1)) ∈ ℂ) → ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1))) = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(1 / (𝑀 + 1))))
380	369, 379	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1))) = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(1 / (𝑀 + 1))))
381		eqeq2 2774	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1))) = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(1 / (𝑀 + 1))) → (𝑧 = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1))) ↔ 𝑧 = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(1 / (𝑀 + 1)))))
382	381	biimpd 232	. . . . . . . . . . . . . . . . 17 ⊢ (((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1))) = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(1 / (𝑀 + 1))) → (𝑧 = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1))) → 𝑧 = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(1 / (𝑀 + 1)))))
383	380, 382	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑧 = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1))) → 𝑧 = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(1 / (𝑀 + 1)))))
384	383	ex 418	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) → (𝑧 = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1))) → 𝑧 = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(1 / (𝑀 + 1))))))
385	384	impd 416	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑧 = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1)))) → 𝑧 = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(1 / (𝑀 + 1)))))
386	378, 385	jcad 522	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑧 = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1)))) → (𝑥 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑧 = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(1 / (𝑀 + 1))))))
387	377, 386	impbid 215	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑧 = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(1 / (𝑀 + 1)))) ↔ (𝑥 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑧 = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1))))))
388	387	opabbidv 5175	. . . . . . . . . . 11 ⊢ (𝜑 → {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑧 = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(1 / (𝑀 + 1))))} = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑧 = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1))))})
389	366, 388	eqtrd 2797	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(1 / (𝑀 + 1)))) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑧 = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1))))})
390		df-mpt 5191	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1)))) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑧 = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1))))}
391	390	eqcomi 2771	. . . . . . . . . . 11 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑧 = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1))))} = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1))))
392	391	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑧 = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1))))} = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1)))))
393	389, 392	eqtrd 2797	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(1 / (𝑀 + 1)))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1)))))
394	393	oveq1d 7432	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(1 / (𝑀 + 1)))) lim_ℂ 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1)))) lim_ℂ 𝐵))
395	364, 394	jca 521	. . . . . . 7 ⊢ (𝜑 → ((0(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(1 / (𝑀 + 1))) = (0 · (1 / (𝑀 + 1))) ∧ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(1 / (𝑀 + 1)))) lim_ℂ 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1)))) lim_ℂ 𝐵)))
396		eleq12 2852	. . . . . . 7 ⊢ (((0(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(1 / (𝑀 + 1))) = (0 · (1 / (𝑀 + 1))) ∧ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(1 / (𝑀 + 1)))) lim_ℂ 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1)))) lim_ℂ 𝐵)) → ((0(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(1 / (𝑀 + 1))) ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(1 / (𝑀 + 1)))) lim_ℂ 𝐵) ↔ (0 · (1 / (𝑀 + 1))) ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1)))) lim_ℂ 𝐵)))
397	395, 396	syl 18	. . . . . 6 ⊢ (𝜑 → ((0(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(1 / (𝑀 + 1))) ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(1 / (𝑀 + 1)))) lim_ℂ 𝐵) ↔ (0 · (1 / (𝑀 + 1))) ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1)))) lim_ℂ 𝐵)))
398	397	biimpd 232	. . . . 5 ⊢ (𝜑 → ((0(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(1 / (𝑀 + 1))) ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(1 / (𝑀 + 1)))) lim_ℂ 𝐵) → (0 · (1 / (𝑀 + 1))) ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1)))) lim_ℂ 𝐵)))
399	360, 398	mpd 16	. . . 4 ⊢ (𝜑 → (0 · (1 / (𝑀 + 1))) ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1)))) lim_ℂ 𝐵))
400	337	mul02d 11436	. . . 4 ⊢ (𝜑 → (0 · (1 / (𝑀 + 1))) = 0)
401	176	fveq1d 6884	. . . . . . . . 9 ⊢ (𝜑 → ((ℝ D (𝑦 ∈ 𝐴 ↦ ((((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) = ((𝑦 ∈ 𝐴 ↦ ((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦)))‘𝑥))
402		fveq2 6882	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → (((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑦) = (((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥))
403		fveq2 6882	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦) = (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥))
404	402, 403	oveq12d 7435	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 → ((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦)) = ((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)))
405		ovex 7450	. . . . . . . . . . 11 ⊢ ((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) ∈ V
406	404, 179, 405	fvmpt 6990	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦)))‘𝑥) = ((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)))
407	314, 406	syl 18	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴 ∖ {𝐵}) → ((𝑦 ∈ 𝐴 ↦ ((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑦)))‘𝑥) = ((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)))
408	401, 407	sylan9eq 2817	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((ℝ D (𝑦 ∈ 𝐴 ↦ ((((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) = ((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)))
409	230	fveq1d 6884	. . . . . . . . . 10 ⊢ (𝜑 → ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))))‘𝑥) = ((𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)))‘𝑥))
410		oveq1 7424	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑥 → (𝑦 − 𝐵) = (𝑥 − 𝐵))
411	410	oveq1d 7432	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑥 → ((𝑦 − 𝐵)↑𝑀) = ((𝑥 − 𝐵)↑𝑀))
412	411	oveq2d 7433	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)) = ((𝑀 + 1) · ((𝑥 − 𝐵)↑𝑀)))
413		ovex 7450	. . . . . . . . . . . 12 ⊢ ((𝑀 + 1) · ((𝑥 − 𝐵)↑𝑀)) ∈ V
414	412, 233, 413	fvmpt 6990	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)))‘𝑥) = ((𝑀 + 1) · ((𝑥 − 𝐵)↑𝑀)))
415	314, 414	syl 18	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐴 ∖ {𝐵}) → ((𝑦 ∈ 𝐴 ↦ ((𝑀 + 1) · ((𝑦 − 𝐵)↑𝑀)))‘𝑥) = ((𝑀 + 1) · ((𝑥 − 𝐵)↑𝑀)))
416	409, 415	sylan9eq 2817	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))))‘𝑥) = ((𝑀 + 1) · ((𝑥 − 𝐵)↑𝑀)))
417	202	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ∈ ℕ)
418	417	nncnd 12277	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ∈ ℂ)
419	418, 327	mulcomd 11258	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑀 + 1) · ((𝑥 − 𝐵)↑𝑀)) = (((𝑥 − 𝐵)↑𝑀) · (𝑀 + 1)))
420	416, 419	eqtrd 2797	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))))‘𝑥) = (((𝑥 − 𝐵)↑𝑀) · (𝑀 + 1)))
421	408, 420	oveq12d 7435	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (((ℝ D (𝑦 ∈ 𝐴 ↦ ((((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) / ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))))‘𝑥)) = (((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / (((𝑥 − 𝐵)↑𝑀) · (𝑀 + 1))))
422	417	nnne0d 12314	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑀 + 1) ≠ 0)
423	322, 327, 418, 334, 422	divdiv1d 12050	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) / (𝑀 + 1)) = (((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / (((𝑥 − 𝐵)↑𝑀) · (𝑀 + 1))))
424	335, 418, 422	divrecd 12022	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) / (𝑀 + 1)) = ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1))))
425	421, 423, 424	3eqtr2rd 2804	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1))) = (((ℝ D (𝑦 ∈ 𝐴 ↦ ((((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) / ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))))‘𝑥)))
426	425	mpteq2dva 5202	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1)))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((ℝ D (𝑦 ∈ 𝐴 ↦ ((((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) / ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))))‘𝑥))))
427	426	oveq1d 7432	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((((ℝ D^𝑛 𝐹)‘(𝑁 − 𝑀))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑀))‘𝑥)) / ((𝑥 − 𝐵)↑𝑀)) · (1 / (𝑀 + 1)))) lim_ℂ 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((ℝ D (𝑦 ∈ 𝐴 ↦ ((((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) / ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))))‘𝑥))) lim_ℂ 𝐵))
428	399, 400, 427	3eltr3d 2876	. . 3 ⊢ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((ℝ D (𝑦 ∈ 𝐴 ↦ ((((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))))‘𝑥) / ((ℝ D (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))))‘𝑥))) lim_ℂ 𝐵))
429	1, 70, 83, 123, 44, 124, 182, 236, 258, 271, 292, 313, 428	lhop 26250	. 2 ⊢ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝑦 ∈ 𝐴 ↦ ((((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) / ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))‘𝑥))) lim_ℂ 𝐵))
430	314	adantl 487	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ 𝐴)
431		fveq2 6882	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → (((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) = (((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥))
432		fveq2 6882	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦) = (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥))
433	431, 432	oveq12d 7435	. . . . . . 7 ⊢ (𝑦 = 𝑥 → ((((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)) = ((((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)))
434		eqid 2762	. . . . . . 7 ⊢ (𝑦 ∈ 𝐴 ↦ ((((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦))) = (𝑦 ∈ 𝐴 ↦ ((((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))
435		ovex 7450	. . . . . . 7 ⊢ ((((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) ∈ V
436	433, 434, 435	fvmpt 6990	. . . . . 6 ⊢ (𝑥 ∈ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ((((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) = ((((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)))
437	430, 436	syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑦 ∈ 𝐴 ↦ ((((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) = ((((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)))
438	410	oveq1d 7432	. . . . . . 7 ⊢ (𝑦 = 𝑥 → ((𝑦 − 𝐵)↑(𝑀 + 1)) = ((𝑥 − 𝐵)↑(𝑀 + 1)))
439		eqid 2762	. . . . . . 7 ⊢ (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1))) = (𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))
440		ovex 7450	. . . . . . 7 ⊢ ((𝑥 − 𝐵)↑(𝑀 + 1)) ∈ V
441	438, 439, 440	fvmpt 6990	. . . . . 6 ⊢ (𝑥 ∈ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))‘𝑥) = ((𝑥 − 𝐵)↑(𝑀 + 1)))
442	430, 441	syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))‘𝑥) = ((𝑥 − 𝐵)↑(𝑀 + 1)))
443	437, 442	oveq12d 7435	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (((𝑦 ∈ 𝐴 ↦ ((((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) / ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))‘𝑥)) = (((((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑀 + 1))))
444	443	mpteq2dva 5202	. . 3 ⊢ (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝑦 ∈ 𝐴 ↦ ((((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) / ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))‘𝑥))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑀 + 1)))))
445	444	oveq1d 7432	. 2 ⊢ (𝜑 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝑦 ∈ 𝐴 ↦ ((((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑦)))‘𝑥) / ((𝑦 ∈ 𝐴 ↦ ((𝑦 − 𝐵)↑(𝑀 + 1)))‘𝑥))) lim_ℂ 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑀 + 1)))) lim_ℂ 𝐵))
446	429, 445	eleqtrd 2864	1 ⊢ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((ℝ D^𝑛 𝐹)‘(𝑁 − (𝑀 + 1)))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑀 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑀 + 1)))) lim_ℂ 𝐵))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2145 ≠ wne 2957 ∃wrex 3088 Vcvv 3453 ∖ cdif 3899 ∩ cin 3901 ⊆ wss 3902 {csn 4587 {cpr 4589 ⟨cop 4593 class class class wbr 5107 {copab 5171 ↦ cmpt 5190 × cxp 5657 dom cdm 5659 ran crn 5660 ↾ cres 5661 “ cima 5662 ⟶wf 6533 ‘cfv 6537 (class class class)co 7417 ∈ cmpo 7419 ↑_m cmap 8830 ↑_pm cpm 8831 ℂcc 11126 ℝcr 11127 0cc0 11128 1c1 11129 + caddc 11131 · cmul 11133 ≤ cle 11272 − cmin 11469 / cdiv 11899 ℕcn 12261 ℕ₀cn0 12532 ℤ_≥cuz 12891 (,)cioo 13402 ...cfz 13565 ..^cfzo 13713 ↑cexp 14129 !cfa 14341 TopOpenctopn 17512 topGenctg 17528 SubRingcsubrg 20737 DivRingcdr 20896 ℂ_fldccnfld 21591 ℝ_fldcrefld 21823 Topctop 23124 TopOnctopon 23141 intcnt 23248 Cn ccn 23455 CnP ccnp 23456 ×_t ctx 23792 –cn→ccncf 25110 lim_ℂ climc 26096 D cdv 26097 D^𝑛 cdvn 26098 Polycply 26416 degcdgr 26419 Tayl ctayl 26596

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7740 ax-inf2 9624 ax-cnex 11184 ax-resscn 11185 ax-1cn 11186 ax-icn 11187 ax-addcl 11188 ax-addrcl 11189 ax-mulcl 11190 ax-mulrcl 11191 ax-mulcom 11192 ax-addass 11193 ax-mulass 11194 ax-distr 11195 ax-i2m1 11196 ax-1ne0 11197 ax-1rid 11198 ax-rnegex 11199 ax-rrecex 11200 ax-cnre 11201 ax-pre-lttri 11202 ax-pre-lttrn 11203 ax-pre-ltadd 11204 ax-pre-mulgt0 11205 ax-pre-sup 11206 ax-addf 11207

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-tp 4592 df-op 4594 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-se 5613 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7374 df-ov 7420 df-oprab 7421 df-mpo 7422 df-of 7682 df-om 7867 df-1st 7990 df-2nd 7991 df-supp 8163 df-tpos 8228 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-2o 8460 df-er 8700 df-map 8832 df-pm 8833 df-ixp 8909 df-en 8957 df-dom 8958 df-sdom 8959 df-fin 8960 df-fsupp 9336 df-fi 9385 df-sup 9416 df-inf 9417 df-oi 9486 df-card 9948 df-pnf 11273 df-mnf 11274 df-xr 11275 df-ltxr 11276 df-le 11277 df-sub 11471 df-neg 11472 df-div 11900 df-nn 12262 df-2 12331 df-3 12332 df-4 12333 df-5 12334 df-6 12335 df-7 12336 df-8 12337 df-9 12338 df-n0 12533 df-xnn0 12606 df-z 12620 df-dec 12741 df-uz 12892 df-q 13002 df-rp 13047 df-xneg 13167 df-xadd 13168 df-xmul 13169 df-ioo 13406 df-ioc 13407 df-ico 13408 df-icc 13409 df-fz 13566 df-fzo 13714 df-fl 13857 df-seq 14070 df-exp 14130 df-fac 14342 df-hash 14399 df-cj 15190 df-re 15191 df-im 15192 df-sqrt 15326 df-abs 15327 df-clim 15579 df-rlim 15580 df-sum 15778 df-struct 17245 df-sets 17262 df-slot 17280 df-ndx 17292 df-base 17308 df-ress 17329 df-plusg 17361 df-mulr 17362 df-starv 17363 df-sca 17364 df-vsca 17365 df-ip 17366 df-tset 17367 df-ple 17368 df-ds 17370 df-unif 17371 df-hom 17372 df-cco 17373 df-rest 17513 df-topn 17514 df-0g 17532 df-gsum 17533 df-topgen 17534 df-pt 17535 df-prds 17538 df-xrs 17594 df-qtop 17599 df-imas 17600 df-xps 17602 df-mre 17676 df-mrc 17677 df-acs 17679 df-mgm 18736 df-sgrp 18827 df-mnd 18843 df-submnd 18898 df-grp 19066 df-minusg 19067 df-mulg 19197 df-subg 19252 df-cntz 19450 df-cmn 19915 df-abl 19916 df-mgp 20280 df-rng 20294 df-ur 20327 df-ring 20380 df-cring 20381 df-oppr 20484 df-dvdsr 20504 df-unit 20505 df-invr 20535 df-dvr 20548 df-subrng 20714 df-subrg 20738 df-drng 20898 df-psmet 21583 df-xmet 21584 df-met 21585 df-bl 21586 df-mopn 21587 df-fbas 21588 df-fg 21589 df-cnfld 21592 df-refld 21824 df-top 23125 df-topon 23142 df-topsp 23164 df-bases 23177 df-cld 23250 df-ntr 23251 df-cls 23252 df-nei 23329 df-lp 23367 df-perf 23368 df-cn 23458 df-cnp 23459 df-haus 23546 df-cmp 23618 df-tx 23794 df-hmeo 23987 df-fil 24078 df-fm 24170 df-flim 24171 df-flf 24172 df-tsms 24359 df-xms 24552 df-ms 24553 df-tms 24554 df-cncf 25112 df-0p 25904 df-limc 26100 df-dv 26101 df-dvn 26102 df-ply 26420 df-idp 26421 df-coe 26422 df-dgr 26423 df-tayl 26598

This theorem is used by: taylth 26618

W3C validator