taylthlem1 - Metamath Proof Explorer

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

Theorem taylthlem1 26338

Description: Lemma for taylth 26341. This is the main part of Taylor's theorem, except for the induction step, which is supposed to be proven using L'Hôpital's rule. However, since our proof of L'Hôpital assumes that 𝑆 = ℝ, we can only do this part generically, and for taylth 26341 itself we must restrict to ℝ. (Contributed by Mario Carneiro, 1-Jan-2017.)

**Hypotheses**
Ref	Expression
taylthlem1.s	⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})
taylthlem1.f	⊢ (𝜑 → 𝐹:𝐴⟶ℂ)
taylthlem1.a	⊢ (𝜑 → 𝐴 ⊆ 𝑆)
taylthlem1.d	⊢ (𝜑 → dom ((𝑆 D^𝑛 𝐹)‘𝑁) = 𝐴)
taylthlem1.n	⊢ (𝜑 → 𝑁 ∈ ℕ)
taylthlem1.b	⊢ (𝜑 → 𝐵 ∈ 𝐴)
taylthlem1.t	⊢ 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵)
taylthlem1.r	⊢ 𝑅 = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝐹‘𝑥) − (𝑇‘𝑥)) / ((𝑥 − 𝐵)↑𝑁)))
taylthlem1.i	⊢ ((𝜑 ∧ (𝑛 ∈ (1..^𝑁) ∧ 0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) lim_ℂ 𝐵))) → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))) lim_ℂ 𝐵))

**Assertion**
Ref	Expression
taylthlem1	⊢ (𝜑 → 0 ∈ (𝑅 lim_ℂ 𝐵))

Distinct variable groups: 𝑥,𝑛,𝑦,𝐴 𝐵,𝑛,𝑥,𝑦 𝑛,𝐹,𝑥,𝑦 𝜑,𝑛,𝑥,𝑦 𝑛,𝑁,𝑥,𝑦 𝑆,𝑛,𝑥,𝑦 𝑇,𝑛,𝑥,𝑦 Allowed substitution hints: 𝑅(𝑥,𝑦,𝑛)

Proof of Theorem taylthlem1 Dummy variable 𝑚 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		taylthlem1.n	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℕ)
2		elfz1end 13576	. . . 4 ⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈ (1...𝑁))
3	1, 2	sylib 218	. . 3 ⊢ (𝜑 → 𝑁 ∈ (1...𝑁))
4		oveq2 7418	. . . . . . . . . . . 12 ⊢ (𝑚 = 1 → (𝑁 − 𝑚) = (𝑁 − 1))
5	4	fveq2d 6885	. . . . . . . . . . 11 ⊢ (𝑚 = 1 → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚)) = ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))
6	5	fveq1d 6883	. . . . . . . . . 10 ⊢ (𝑚 = 1 → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) = (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥))
7	4	fveq2d 6885	. . . . . . . . . . 11 ⊢ (𝑚 = 1 → ((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚)) = ((ℂ D^𝑛 𝑇)‘(𝑁 − 1)))
8	7	fveq1d 6883	. . . . . . . . . 10 ⊢ (𝑚 = 1 → (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥) = (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥))
9	6, 8	oveq12d 7428	. . . . . . . . 9 ⊢ (𝑚 = 1 → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) = ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)))
10		oveq2 7418	. . . . . . . . 9 ⊢ (𝑚 = 1 → ((𝑥 − 𝐵)↑𝑚) = ((𝑥 − 𝐵)↑1))
11	9, 10	oveq12d 7428	. . . . . . . 8 ⊢ (𝑚 = 1 → (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚)) = (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1)))
12	11	mpteq2dv 5220	. . . . . . 7 ⊢ (𝑚 = 1 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))))
13	12	oveq1d 7425	. . . . . 6 ⊢ (𝑚 = 1 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) lim_ℂ 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))) lim_ℂ 𝐵))
14	13	eleq2d 2821	. . . . 5 ⊢ (𝑚 = 1 → (0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) lim_ℂ 𝐵) ↔ 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))) lim_ℂ 𝐵)))
15	14	imbi2d 340	. . . 4 ⊢ (𝑚 = 1 → ((𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) lim_ℂ 𝐵)) ↔ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))) lim_ℂ 𝐵))))
16		oveq2 7418	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑛 → (𝑁 − 𝑚) = (𝑁 − 𝑛))
17	16	fveq2d 6885	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚)) = ((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛)))
18	17	fveq1d 6883	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) = (((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥))
19	16	fveq2d 6885	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → ((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚)) = ((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛)))
20	19	fveq1d 6883	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥) = (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑥))
21	18, 20	oveq12d 7428	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) = ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑥)))
22		oveq2 7418	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → ((𝑥 − 𝐵)↑𝑚) = ((𝑥 − 𝐵)↑𝑛))
23	21, 22	oveq12d 7428	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚)) = (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑥)) / ((𝑥 − 𝐵)↑𝑛)))
24	23	mpteq2dv 5220	. . . . . . . 8 ⊢ (𝑚 = 𝑛 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑥)) / ((𝑥 − 𝐵)↑𝑛))))
25		fveq2 6881	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) = (((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦))
26		fveq2 6881	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑥) = (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑦))
27	25, 26	oveq12d 7428	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑥)) = ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑦)))
28		oveq1 7417	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑥 − 𝐵) = (𝑦 − 𝐵))
29	28	oveq1d 7425	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((𝑥 − 𝐵)↑𝑛) = ((𝑦 − 𝐵)↑𝑛))
30	27, 29	oveq12d 7428	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑥)) / ((𝑥 − 𝐵)↑𝑛)) = (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛)))
31	30	cbvmptv 5230	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑥)) / ((𝑥 − 𝐵)↑𝑛))) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛)))
32	24, 31	eqtrdi 2787	. . . . . . 7 ⊢ (𝑚 = 𝑛 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))))
33	32	oveq1d 7425	. . . . . 6 ⊢ (𝑚 = 𝑛 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) lim_ℂ 𝐵) = ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) lim_ℂ 𝐵))
34	33	eleq2d 2821	. . . . 5 ⊢ (𝑚 = 𝑛 → (0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) lim_ℂ 𝐵) ↔ 0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) lim_ℂ 𝐵)))
35	34	imbi2d 340	. . . 4 ⊢ (𝑚 = 𝑛 → ((𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) lim_ℂ 𝐵)) ↔ (𝜑 → 0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) lim_ℂ 𝐵))))
36		oveq2 7418	. . . . . . . . . . . 12 ⊢ (𝑚 = (𝑛 + 1) → (𝑁 − 𝑚) = (𝑁 − (𝑛 + 1)))
37	36	fveq2d 6885	. . . . . . . . . . 11 ⊢ (𝑚 = (𝑛 + 1) → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚)) = ((𝑆 D^𝑛 𝐹)‘(𝑁 − (𝑛 + 1))))
38	37	fveq1d 6883	. . . . . . . . . 10 ⊢ (𝑚 = (𝑛 + 1) → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) = (((𝑆 D^𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥))
39	36	fveq2d 6885	. . . . . . . . . . 11 ⊢ (𝑚 = (𝑛 + 1) → ((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚)) = ((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑛 + 1))))
40	39	fveq1d 6883	. . . . . . . . . 10 ⊢ (𝑚 = (𝑛 + 1) → (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥) = (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥))
41	38, 40	oveq12d 7428	. . . . . . . . 9 ⊢ (𝑚 = (𝑛 + 1) → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) = ((((𝑆 D^𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)))
42		oveq2 7418	. . . . . . . . 9 ⊢ (𝑚 = (𝑛 + 1) → ((𝑥 − 𝐵)↑𝑚) = ((𝑥 − 𝐵)↑(𝑛 + 1)))
43	41, 42	oveq12d 7428	. . . . . . . 8 ⊢ (𝑚 = (𝑛 + 1) → (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚)) = (((((𝑆 D^𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1))))
44	43	mpteq2dv 5220	. . . . . . 7 ⊢ (𝑚 = (𝑛 + 1) → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))))
45	44	oveq1d 7425	. . . . . 6 ⊢ (𝑚 = (𝑛 + 1) → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) lim_ℂ 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))) lim_ℂ 𝐵))
46	45	eleq2d 2821	. . . . 5 ⊢ (𝑚 = (𝑛 + 1) → (0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) lim_ℂ 𝐵) ↔ 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))) lim_ℂ 𝐵)))
47	46	imbi2d 340	. . . 4 ⊢ (𝑚 = (𝑛 + 1) → ((𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) lim_ℂ 𝐵)) ↔ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))) lim_ℂ 𝐵))))
48		oveq2 7418	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑁 → (𝑁 − 𝑚) = (𝑁 − 𝑁))
49	48	fveq2d 6885	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑁 → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚)) = ((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁)))
50	49	fveq1d 6883	. . . . . . . . . 10 ⊢ (𝑚 = 𝑁 → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) = (((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥))
51	48	fveq2d 6885	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑁 → ((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚)) = ((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁)))
52	51	fveq1d 6883	. . . . . . . . . 10 ⊢ (𝑚 = 𝑁 → (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥) = (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥))
53	50, 52	oveq12d 7428	. . . . . . . . 9 ⊢ (𝑚 = 𝑁 → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) = ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)))
54		oveq2 7418	. . . . . . . . 9 ⊢ (𝑚 = 𝑁 → ((𝑥 − 𝐵)↑𝑚) = ((𝑥 − 𝐵)↑𝑁))
55	53, 54	oveq12d 7428	. . . . . . . 8 ⊢ (𝑚 = 𝑁 → (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚)) = (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁)))
56	55	mpteq2dv 5220	. . . . . . 7 ⊢ (𝑚 = 𝑁 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))))
57	56	oveq1d 7425	. . . . . 6 ⊢ (𝑚 = 𝑁 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) lim_ℂ 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) lim_ℂ 𝐵))
58	57	eleq2d 2821	. . . . 5 ⊢ (𝑚 = 𝑁 → (0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) lim_ℂ 𝐵) ↔ 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) lim_ℂ 𝐵)))
59	58	imbi2d 340	. . . 4 ⊢ (𝑚 = 𝑁 → ((𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) lim_ℂ 𝐵)) ↔ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) lim_ℂ 𝐵))))
60		taylthlem1.b	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ 𝐴)
61		fveq2 6881	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝐵 → (((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) = (((𝑆 D^𝑛 𝐹)‘𝑁)‘𝐵))
62		fveq2 6881	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝐵 → (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦) = (((ℂ D^𝑛 𝑇)‘𝑁)‘𝐵))
63	61, 62	oveq12d 7428	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝐵 → ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)) = ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝐵) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝐵)))
64		eqid 2736	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦))) = (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))
65		ovex 7443	. . . . . . . . . . . . 13 ⊢ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝐵) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝐵)) ∈ V
66	63, 64, 65	fvmpt 6991	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))‘𝐵) = ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝐵) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝐵)))
67	60, 66	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))‘𝐵) = ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝐵) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝐵)))
68		taylthlem1.s	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})
69		taylthlem1.f	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)
70		taylthlem1.a	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ⊆ 𝑆)
71	1	nnnn0d 12567	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
72		nn0uz 12899	. . . . . . . . . . . . . . 15 ⊢ ℕ₀ = (ℤ_≥‘0)
73	71, 72	eleqtrdi 2845	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘0))
74		eluzfz2b 13555	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ (ℤ_≥‘0) ↔ 𝑁 ∈ (0...𝑁))
75	73, 74	sylib 218	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ (0...𝑁))
76		taylthlem1.d	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom ((𝑆 D^𝑛 𝐹)‘𝑁) = 𝐴)
77	60, 76	eleqtrrd 2838	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D^𝑛 𝐹)‘𝑁))
78		taylthlem1.t	. . . . . . . . . . . . 13 ⊢ 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵)
79	68, 69, 70, 75, 77, 78	dvntaylp0 26337	. . . . . . . . . . . 12 ⊢ (𝜑 → (((ℂ D^𝑛 𝑇)‘𝑁)‘𝐵) = (((𝑆 D^𝑛 𝐹)‘𝑁)‘𝐵))
80	79	oveq2d 7426	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝐵) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝐵)) = ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝐵) − (((𝑆 D^𝑛 𝐹)‘𝑁)‘𝐵)))
81		cnex 11215	. . . . . . . . . . . . . . . 16 ⊢ ℂ ∈ V
82	81	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ℂ ∈ V)
83		elpm2r 8864	. . . . . . . . . . . . . . 15 ⊢ (((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆)) → 𝐹 ∈ (ℂ ↑_pm 𝑆))
84	82, 68, 69, 70, 83	syl22anc 838	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹 ∈ (ℂ ↑_pm 𝑆))
85		dvnf 25886	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ 𝑁 ∈ ℕ₀) → ((𝑆 D^𝑛 𝐹)‘𝑁):dom ((𝑆 D^𝑛 𝐹)‘𝑁)⟶ℂ)
86	68, 84, 71, 85	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘𝑁):dom ((𝑆 D^𝑛 𝐹)‘𝑁)⟶ℂ)
87	86, 77	ffvelcdmd 7080	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑆 D^𝑛 𝐹)‘𝑁)‘𝐵) ∈ ℂ)
88	87	subidd 11587	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝐵) − (((𝑆 D^𝑛 𝐹)‘𝑁)‘𝐵)) = 0)
89	67, 80, 88	3eqtrd 2775	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))‘𝐵) = 0)
90		funmpt 6579	. . . . . . . . . . 11 ⊢ Fun (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))
91		ovex 7443	. . . . . . . . . . . . 13 ⊢ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)) ∈ V
92	91, 64	dmmpti 6687	. . . . . . . . . . . 12 ⊢ dom (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦))) = 𝐴
93	60, 92	eleqtrrdi 2846	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ dom (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦))))
94		funbrfvb 6937	. . . . . . . . . . 11 ⊢ ((Fun (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦))) ∧ 𝐵 ∈ dom (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))) → (((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))‘𝐵) = 0 ↔ 𝐵(𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))0))
95	90, 93, 94	sylancr 587	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))‘𝐵) = 0 ↔ 𝐵(𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))0))
96	89, 95	mpbid 232	. . . . . . . . 9 ⊢ (𝜑 → 𝐵(𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))0)
97		nnm1nn0 12547	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ₀)
98	1, 97	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑁 − 1) ∈ ℕ₀)
99		dvnf 25886	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ (𝑁 − 1) ∈ ℕ₀) → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)):dom ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))⟶ℂ)
100	68, 84, 98, 99	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)):dom ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))⟶ℂ)
101		dvnbss 25887	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ (𝑁 − 1) ∈ ℕ₀) → dom ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)) ⊆ dom 𝐹)
102	68, 84, 98, 101	syl3anc 1373	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)) ⊆ dom 𝐹)
103	69, 102	fssdmd 6729	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)) ⊆ 𝐴)
104		fzo0end 13779	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ (0..^𝑁))
105		elfzofz 13697	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 − 1) ∈ (0..^𝑁) → (𝑁 − 1) ∈ (0...𝑁))
106	1, 104, 105	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑁 − 1) ∈ (0...𝑁))
107		dvn2bss 25889	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ (𝑁 − 1) ∈ (0...𝑁)) → dom ((𝑆 D^𝑛 𝐹)‘𝑁) ⊆ dom ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))
108	68, 84, 106, 107	syl3anc 1373	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom ((𝑆 D^𝑛 𝐹)‘𝑁) ⊆ dom ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))
109	76, 108	eqsstrrd 3999	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ⊆ dom ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))
110	103, 109	eqssd 3981	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)) = 𝐴)
111	110	feq2d 6697	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)):dom ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))⟶ℂ ↔ ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)):𝐴⟶ℂ))
112	100, 111	mpbid 232	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)):𝐴⟶ℂ)
113	112	ffvelcdmda 7079	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) ∈ ℂ)
114	76	feq2d 6697	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑆 D^𝑛 𝐹)‘𝑁):dom ((𝑆 D^𝑛 𝐹)‘𝑁)⟶ℂ ↔ ((𝑆 D^𝑛 𝐹)‘𝑁):𝐴⟶ℂ))
115	86, 114	mpbid 232	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘𝑁):𝐴⟶ℂ)
116	115	ffvelcdmda 7079	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) ∈ ℂ)
117	1	nncnd 12261	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ ℂ)
118		1cnd 11235	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 ∈ ℂ)
119	117, 118	npcand 11603	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
120	119	fveq2d 6885	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘((𝑁 − 1) + 1)) = ((𝑆 D^𝑛 𝐹)‘𝑁))
121		recnprss 25862	. . . . . . . . . . . . . . 15 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
122	68, 121	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
123		dvnp1 25884	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ (𝑁 − 1) ∈ ℕ₀) → ((𝑆 D^𝑛 𝐹)‘((𝑁 − 1) + 1)) = (𝑆 D ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))))
124	122, 84, 98, 123	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘((𝑁 − 1) + 1)) = (𝑆 D ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))))
125	120, 124	eqtr3d 2773	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘𝑁) = (𝑆 D ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))))
126	115	feqmptd 6952	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘𝑁) = (𝑦 ∈ 𝐴 ↦ (((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦)))
127	112	feqmptd 6952	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)) = (𝑦 ∈ 𝐴 ↦ (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦)))
128	127	oveq2d 7426	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆 D ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))) = (𝑆 D (𝑦 ∈ 𝐴 ↦ (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦))))
129	125, 126, 128	3eqtr3rd 2780	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝐴 ↦ (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦))) = (𝑦 ∈ 𝐴 ↦ (((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦)))
130	70, 122	sstrd 3974	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ⊆ ℂ)
131	130	sselda 3963	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℂ)
132		1nn0 12522	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℕ₀
133	132	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 ∈ ℕ₀)
134		elpm2r 8864	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)):𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆)) → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)) ∈ (ℂ ↑_pm 𝑆))
135	82, 68, 112, 70, 134	syl22anc 838	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)) ∈ (ℂ ↑_pm 𝑆))
136		dvn1 25885	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ⊆ ℂ ∧ ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)) ∈ (ℂ ↑_pm 𝑆)) → ((𝑆 D^𝑛 ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))‘1) = (𝑆 D ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))))
137	122, 135, 136	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑆 D^𝑛 ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))‘1) = (𝑆 D ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))))
138	124, 120	eqtr3d 2773	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑆 D ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))) = ((𝑆 D^𝑛 𝐹)‘𝑁))
139	137, 138	eqtrd 2771	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑆 D^𝑛 ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))‘1) = ((𝑆 D^𝑛 𝐹)‘𝑁))
140	139	dmeqd 5890	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom ((𝑆 D^𝑛 ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))‘1) = dom ((𝑆 D^𝑛 𝐹)‘𝑁))
141	77, 140	eleqtrrd 2838	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D^𝑛 ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))‘1))
142		eqid 2736	. . . . . . . . . . . . . . 15 ⊢ (1(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))𝐵) = (1(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))𝐵)
143	68, 112, 70, 133, 141, 142	taylpf 26330	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))𝐵):ℂ⟶ℂ)
144	118, 117	pncan3d 11602	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (1 + (𝑁 − 1)) = 𝑁)
145	144	oveq1d 7425	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵) = (𝑁(𝑆 Tayl 𝐹)𝐵))
146	78, 145	eqtr4id 2790	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑇 = ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵))
147	146	oveq2d 7426	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (ℂ D^𝑛 𝑇) = (ℂ D^𝑛 ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵)))
148	147	fveq1d 6883	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘(𝑁 − 1)) = ((ℂ D^𝑛 ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵))‘(𝑁 − 1)))
149	144	fveq2d 6885	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘(1 + (𝑁 − 1))) = ((𝑆 D^𝑛 𝐹)‘𝑁))
150	149	dmeqd 5890	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → dom ((𝑆 D^𝑛 𝐹)‘(1 + (𝑁 − 1))) = dom ((𝑆 D^𝑛 𝐹)‘𝑁))
151	77, 150	eleqtrrd 2838	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D^𝑛 𝐹)‘(1 + (𝑁 − 1))))
152	68, 69, 70, 98, 133, 151	dvntaylp 26336	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((ℂ D^𝑛 ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵))‘(𝑁 − 1)) = (1(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))𝐵))
153	148, 152	eqtrd 2771	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘(𝑁 − 1)) = (1(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))𝐵))
154	153	feq1d 6695	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((ℂ D^𝑛 𝑇)‘(𝑁 − 1)):ℂ⟶ℂ ↔ (1(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))𝐵):ℂ⟶ℂ))
155	143, 154	mpbird 257	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘(𝑁 − 1)):ℂ⟶ℂ)
156	155	ffvelcdmda 7079	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦) ∈ ℂ)
157	131, 156	syldan 591	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦) ∈ ℂ)
158		0nn0 12521	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℕ₀
159	158	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 0 ∈ ℕ₀)
160		elpm2r 8864	. . . . . . . . . . . . . . . . . . 19 ⊢ (((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (((𝑆 D^𝑛 𝐹)‘𝑁):𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆)) → ((𝑆 D^𝑛 𝐹)‘𝑁) ∈ (ℂ ↑_pm 𝑆))
161	82, 68, 115, 70, 160	syl22anc 838	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘𝑁) ∈ (ℂ ↑_pm 𝑆))
162		dvn0 25883	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑆 ⊆ ℂ ∧ ((𝑆 D^𝑛 𝐹)‘𝑁) ∈ (ℂ ↑_pm 𝑆)) → ((𝑆 D^𝑛 ((𝑆 D^𝑛 𝐹)‘𝑁))‘0) = ((𝑆 D^𝑛 𝐹)‘𝑁))
163	122, 161, 162	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑆 D^𝑛 ((𝑆 D^𝑛 𝐹)‘𝑁))‘0) = ((𝑆 D^𝑛 𝐹)‘𝑁))
164	163	dmeqd 5890	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom ((𝑆 D^𝑛 ((𝑆 D^𝑛 𝐹)‘𝑁))‘0) = dom ((𝑆 D^𝑛 𝐹)‘𝑁))
165	77, 164	eleqtrrd 2838	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D^𝑛 ((𝑆 D^𝑛 𝐹)‘𝑁))‘0))
166		eqid 2736	. . . . . . . . . . . . . . 15 ⊢ (0(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘𝑁))𝐵) = (0(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘𝑁))𝐵)
167	68, 115, 70, 159, 165, 166	taylpf 26330	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘𝑁))𝐵):ℂ⟶ℂ)
168	117	addlidd 11441	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (0 + 𝑁) = 𝑁)
169	168	oveq1d 7425	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵) = (𝑁(𝑆 Tayl 𝐹)𝐵))
170	169, 78	eqtr4di 2789	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵) = 𝑇)
171	170	oveq2d 7426	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (ℂ D^𝑛 ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵)) = (ℂ D^𝑛 𝑇))
172	171	fveq1d 6883	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((ℂ D^𝑛 ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵))‘𝑁) = ((ℂ D^𝑛 𝑇)‘𝑁))
173	168	fveq2d 6885	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘(0 + 𝑁)) = ((𝑆 D^𝑛 𝐹)‘𝑁))
174	173	dmeqd 5890	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → dom ((𝑆 D^𝑛 𝐹)‘(0 + 𝑁)) = dom ((𝑆 D^𝑛 𝐹)‘𝑁))
175	77, 174	eleqtrrd 2838	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D^𝑛 𝐹)‘(0 + 𝑁)))
176	68, 69, 70, 71, 159, 175	dvntaylp 26336	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((ℂ D^𝑛 ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵))‘𝑁) = (0(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘𝑁))𝐵))
177	172, 176	eqtr3d 2773	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘𝑁) = (0(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘𝑁))𝐵))
178	177	feq1d 6695	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((ℂ D^𝑛 𝑇)‘𝑁):ℂ⟶ℂ ↔ (0(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘𝑁))𝐵):ℂ⟶ℂ))
179	167, 178	mpbird 257	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘𝑁):ℂ⟶ℂ)
180	179	ffvelcdmda 7079	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦) ∈ ℂ)
181	131, 180	syldan 591	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦) ∈ ℂ)
182	122	sselda 3963	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ ℂ)
183	182, 156	syldan 591	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦) ∈ ℂ)
184	182, 180	syldan 591	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦) ∈ ℂ)
185		eqid 2736	. . . . . . . . . . . . 13 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
186	185	cnfldtopon 24726	. . . . . . . . . . . . . 14 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
187		toponmax 22869	. . . . . . . . . . . . . 14 ⊢ ((TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ) → ℂ ∈ (TopOpen‘ℂ_fld))
188	186, 187	mp1i 13	. . . . . . . . . . . . 13 ⊢ (𝜑 → ℂ ∈ (TopOpen‘ℂ_fld))
189		dfss2 3949	. . . . . . . . . . . . . 14 ⊢ (𝑆 ⊆ ℂ ↔ (𝑆 ∩ ℂ) = 𝑆)
190	122, 189	sylib 218	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆 ∩ ℂ) = 𝑆)
191		ssid 3986	. . . . . . . . . . . . . . . . 17 ⊢ ℂ ⊆ ℂ
192	191	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ℂ ⊆ ℂ)
193		mapsspm 8895	. . . . . . . . . . . . . . . . 17 ⊢ (ℂ ↑_m ℂ) ⊆ (ℂ ↑_pm ℂ)
194	68, 69, 70, 71, 77, 78	taylpf 26330	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑇:ℂ⟶ℂ)
195	81, 81	elmap 8890	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑇 ∈ (ℂ ↑_m ℂ) ↔ 𝑇:ℂ⟶ℂ)
196	194, 195	sylibr 234	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑇 ∈ (ℂ ↑_m ℂ))
197	193, 196	sselid 3961	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑇 ∈ (ℂ ↑_pm ℂ))
198		dvnp1 25884	. . . . . . . . . . . . . . . 16 ⊢ ((ℂ ⊆ ℂ ∧ 𝑇 ∈ (ℂ ↑_pm ℂ) ∧ (𝑁 − 1) ∈ ℕ₀) → ((ℂ D^𝑛 𝑇)‘((𝑁 − 1) + 1)) = (ℂ D ((ℂ D^𝑛 𝑇)‘(𝑁 − 1))))
199	192, 197, 98, 198	syl3anc 1373	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘((𝑁 − 1) + 1)) = (ℂ D ((ℂ D^𝑛 𝑇)‘(𝑁 − 1))))
200	119	fveq2d 6885	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘((𝑁 − 1) + 1)) = ((ℂ D^𝑛 𝑇)‘𝑁))
201	199, 200	eqtr3d 2773	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℂ D ((ℂ D^𝑛 𝑇)‘(𝑁 − 1))) = ((ℂ D^𝑛 𝑇)‘𝑁))
202	155	feqmptd 6952	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘(𝑁 − 1)) = (𝑦 ∈ ℂ ↦ (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))
203	202	oveq2d 7426	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℂ D ((ℂ D^𝑛 𝑇)‘(𝑁 − 1))) = (ℂ D (𝑦 ∈ ℂ ↦ (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦))))
204	179	feqmptd 6952	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘𝑁) = (𝑦 ∈ ℂ ↦ (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))
205	201, 203, 204	3eqtr3d 2779	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦))) = (𝑦 ∈ ℂ ↦ (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))
206	185, 68, 188, 190, 156, 180, 205	dvmptres3 25917	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝑆 ↦ (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦))) = (𝑦 ∈ 𝑆 ↦ (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))
207		eqid 2736	. . . . . . . . . . . 12 ⊢ ((TopOpen‘ℂ_fld) ↾_t 𝑆) = ((TopOpen‘ℂ_fld) ↾_t 𝑆)
208		resttopon 23104	. . . . . . . . . . . . . . . 16 ⊢ (((TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ) ∧ 𝑆 ⊆ ℂ) → ((TopOpen‘ℂ_fld) ↾_t 𝑆) ∈ (TopOn‘𝑆))
209	186, 122, 208	sylancr 587	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((TopOpen‘ℂ_fld) ↾_t 𝑆) ∈ (TopOn‘𝑆))
210		topontop 22856	. . . . . . . . . . . . . . 15 ⊢ (((TopOpen‘ℂ_fld) ↾_t 𝑆) ∈ (TopOn‘𝑆) → ((TopOpen‘ℂ_fld) ↾_t 𝑆) ∈ Top)
211	209, 210	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((TopOpen‘ℂ_fld) ↾_t 𝑆) ∈ Top)
212		toponuni 22857	. . . . . . . . . . . . . . . 16 ⊢ (((TopOpen‘ℂ_fld) ↾_t 𝑆) ∈ (TopOn‘𝑆) → 𝑆 = ∪ ((TopOpen‘ℂ_fld) ↾_t 𝑆))
213	209, 212	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑆 = ∪ ((TopOpen‘ℂ_fld) ↾_t 𝑆))
214	70, 213	sseqtrd 4000	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ⊆ ∪ ((TopOpen‘ℂ_fld) ↾_t 𝑆))
215		eqid 2736	. . . . . . . . . . . . . . 15 ⊢ ∪ ((TopOpen‘ℂ_fld) ↾_t 𝑆) = ∪ ((TopOpen‘ℂ_fld) ↾_t 𝑆)
216	215	ntrss2 23000	. . . . . . . . . . . . . 14 ⊢ ((((TopOpen‘ℂ_fld) ↾_t 𝑆) ∈ Top ∧ 𝐴 ⊆ ∪ ((TopOpen‘ℂ_fld) ↾_t 𝑆)) → ((int‘((TopOpen‘ℂ_fld) ↾_t 𝑆))‘𝐴) ⊆ 𝐴)
217	211, 214, 216	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((int‘((TopOpen‘ℂ_fld) ↾_t 𝑆))‘𝐴) ⊆ 𝐴)
218	138	dmeqd 5890	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom (𝑆 D ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))) = dom ((𝑆 D^𝑛 𝐹)‘𝑁))
219	218, 76	eqtrd 2771	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom (𝑆 D ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))) = 𝐴)
220	122, 112, 70, 207, 185	dvbssntr 25858	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom (𝑆 D ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))) ⊆ ((int‘((TopOpen‘ℂ_fld) ↾_t 𝑆))‘𝐴))
221	219, 220	eqsstrrd 3999	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ⊆ ((int‘((TopOpen‘ℂ_fld) ↾_t 𝑆))‘𝐴))
222	217, 221	eqssd 3981	. . . . . . . . . . . 12 ⊢ (𝜑 → ((int‘((TopOpen‘ℂ_fld) ↾_t 𝑆))‘𝐴) = 𝐴)
223	68, 183, 184, 206, 70, 207, 185, 222	dvmptres2 25923	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝐴 ↦ (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦))) = (𝑦 ∈ 𝐴 ↦ (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))
224	68, 113, 116, 129, 157, 181, 223	dvmptsub 25928	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))) = (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦))))
225	224	breqd 5135	. . . . . . . . 9 ⊢ (𝜑 → (𝐵(𝑆 D (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦))))0 ↔ 𝐵(𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))0))
226	96, 225	mpbird 257	. . . . . . . 8 ⊢ (𝜑 → 𝐵(𝑆 D (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦))))0)
227		eqid 2736	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵)))
228	113, 157	subcld 11599	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)) ∈ ℂ)
229	228	fmpttd 7110	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦))):𝐴⟶ℂ)
230	207, 185, 227, 122, 229, 70	eldv 25856	. . . . . . . 8 ⊢ (𝜑 → (𝐵(𝑆 D (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦))))0 ↔ (𝐵 ∈ ((int‘((TopOpen‘ℂ_fld) ↾_t 𝑆))‘𝐴) ∧ 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵))) lim_ℂ 𝐵))))
231	226, 230	mpbid 232	. . . . . . 7 ⊢ (𝜑 → (𝐵 ∈ ((int‘((TopOpen‘ℂ_fld) ↾_t 𝑆))‘𝐴) ∧ 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵))) lim_ℂ 𝐵)))
232	231	simprd 495	. . . . . 6 ⊢ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵))) lim_ℂ 𝐵))
233		eldifi 4111	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐴 ∖ {𝐵}) → 𝑥 ∈ 𝐴)
234		fveq2 6881	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑥 → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) = (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥))
235		fveq2 6881	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑥 → (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦) = (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥))
236	234, 235	oveq12d 7428	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑥 → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)) = ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)))
237		eqid 2736	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦))) = (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))
238		ovex 7443	. . . . . . . . . . . . 13 ⊢ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) ∈ V
239	236, 237, 238	fvmpt 6991	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) = ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)))
240		fveq2 6881	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝐵 → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) = (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝐵))
241		fveq2 6881	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝐵 → (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦) = (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝐵))
242	240, 241	oveq12d 7428	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝐵 → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)) = ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝐵)))
243		ovex 7443	. . . . . . . . . . . . . . 15 ⊢ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝐵)) ∈ V
244	242, 237, 243	fvmpt 6991	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵) = ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝐵)))
245	60, 244	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵) = ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝐵)))
246	68, 69, 70, 106, 77, 78	dvntaylp0 26337	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝐵) = (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝐵))
247	246	oveq2d 7426	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝐵)) = ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝐵)))
248	112, 60	ffvelcdmd 7080	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝐵) ∈ ℂ)
249	248	subidd 11587	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝐵)) = 0)
250	245, 247, 249	3eqtrd 2775	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵) = 0)
251	239, 250	oveqan12rd 7430	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) = (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) − 0))
252	112	ffvelcdmda 7079	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) ∈ ℂ)
253	130	sselda 3963	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℂ)
254	155	ffvelcdmda 7079	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥) ∈ ℂ)
255	253, 254	syldan 591	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥) ∈ ℂ)
256	252, 255	subcld 11599	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) ∈ ℂ)
257	256	subid1d 11588	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) − 0) = ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)))
258	251, 257	eqtr2d 2772	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) = (((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)))
259	233, 258	sylan2 593	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) = (((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)))
260	130	ssdifssd 4127	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 ∖ {𝐵}) ⊆ ℂ)
261	260	sselda 3963	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ ℂ)
262	130, 60	sseldd 3964	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ ℂ)
263	262	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝐵 ∈ ℂ)
264	261, 263	subcld 11599	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑥 − 𝐵) ∈ ℂ)
265	264	exp1d 14164	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑥 − 𝐵)↑1) = (𝑥 − 𝐵))
266	259, 265	oveq12d 7428	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1)) = ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵)))
267	266	mpteq2dva 5219	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵))))
268	267	oveq1d 7425	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))) lim_ℂ 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵))) lim_ℂ 𝐵))
269	232, 268	eleqtrrd 2838	. . . . 5 ⊢ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))) lim_ℂ 𝐵))
270	269	a1i 11	. . . 4 ⊢ (𝑁 ∈ (ℤ_≥‘1) → (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))) lim_ℂ 𝐵)))
271		taylthlem1.i	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑛 ∈ (1..^𝑁) ∧ 0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) lim_ℂ 𝐵))) → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))) lim_ℂ 𝐵))
272	271	expr 456	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1..^𝑁)) → (0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) lim_ℂ 𝐵) → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))) lim_ℂ 𝐵)))
273	272	expcom 413	. . . . 5 ⊢ (𝑛 ∈ (1..^𝑁) → (𝜑 → (0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) lim_ℂ 𝐵) → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))) lim_ℂ 𝐵))))
274	273	a2d 29	. . . 4 ⊢ (𝑛 ∈ (1..^𝑁) → ((𝜑 → 0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) lim_ℂ 𝐵)) → (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))) lim_ℂ 𝐵))))
275	15, 35, 47, 59, 270, 274	fzind2 13806	. . 3 ⊢ (𝑁 ∈ (1...𝑁) → (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) lim_ℂ 𝐵)))
276	3, 275	mpcom 38	. 2 ⊢ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) lim_ℂ 𝐵))
277	117	subidd 11587	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 − 𝑁) = 0)
278	277	fveq2d 6885	. . . . . . . . 9 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁)) = ((𝑆 D^𝑛 𝐹)‘0))
279		dvn0 25883	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆)) → ((𝑆 D^𝑛 𝐹)‘0) = 𝐹)
280	122, 84, 279	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘0) = 𝐹)
281	278, 280	eqtrd 2771	. . . . . . . 8 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁)) = 𝐹)
282	281	fveq1d 6883	. . . . . . 7 ⊢ (𝜑 → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) = (𝐹‘𝑥))
283	277	fveq2d 6885	. . . . . . . . 9 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁)) = ((ℂ D^𝑛 𝑇)‘0))
284		dvn0 25883	. . . . . . . . . 10 ⊢ ((ℂ ⊆ ℂ ∧ 𝑇 ∈ (ℂ ↑_pm ℂ)) → ((ℂ D^𝑛 𝑇)‘0) = 𝑇)
285	191, 197, 284	sylancr 587	. . . . . . . . 9 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘0) = 𝑇)
286	283, 285	eqtrd 2771	. . . . . . . 8 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁)) = 𝑇)
287	286	fveq1d 6883	. . . . . . 7 ⊢ (𝜑 → (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥) = (𝑇‘𝑥))
288	282, 287	oveq12d 7428	. . . . . 6 ⊢ (𝜑 → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) = ((𝐹‘𝑥) − (𝑇‘𝑥)))
289	288	oveq1d 7425	. . . . 5 ⊢ (𝜑 → (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁)) = (((𝐹‘𝑥) − (𝑇‘𝑥)) / ((𝑥 − 𝐵)↑𝑁)))
290	289	mpteq2dv 5220	. . . 4 ⊢ (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝐹‘𝑥) − (𝑇‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))))
291		taylthlem1.r	. . . 4 ⊢ 𝑅 = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝐹‘𝑥) − (𝑇‘𝑥)) / ((𝑥 − 𝐵)↑𝑁)))
292	290, 291	eqtr4di 2789	. . 3 ⊢ (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) = 𝑅)
293	292	oveq1d 7425	. 2 ⊢ (𝜑 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) lim_ℂ 𝐵) = (𝑅 lim_ℂ 𝐵))
294	276, 293	eleqtrd 2837	1 ⊢ (𝜑 → 0 ∈ (𝑅 lim_ℂ 𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2109 Vcvv 3464 ∖ cdif 3928 ∩ cin 3930 ⊆ wss 3931 {csn 4606 {cpr 4608 ∪ cuni 4888 class class class wbr 5124 ↦ cmpt 5206 dom cdm 5659 Fun wfun 6530 ⟶wf 6532 ‘cfv 6536 (class class class)co 7410 ↑_m cmap 8845 ↑_pm cpm 8846 ℂcc 11132 ℝcr 11133 0cc0 11134 1c1 11135 + caddc 11137 − cmin 11471 / cdiv 11899 ℕcn 12245 ℕ₀cn0 12506 ℤ_≥cuz 12857 ...cfz 13529 ..^cfzo 13676 ↑cexp 14084 ↾_t crest 17439 TopOpenctopn 17440 ℂ_fldccnfld 21320 Topctop 22836 TopOnctopon 22853 intcnt 22960 lim_ℂ climc 25820 D cdv 25821 D^𝑛 cdvn 25822 Tayl ctayl 26317

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2708 ax-rep 5254 ax-sep 5271 ax-nul 5281 ax-pow 5340 ax-pr 5407 ax-un 7734 ax-inf2 9660 ax-cnex 11190 ax-resscn 11191 ax-1cn 11192 ax-icn 11193 ax-addcl 11194 ax-addrcl 11195 ax-mulcl 11196 ax-mulrcl 11197 ax-mulcom 11198 ax-addass 11199 ax-mulass 11200 ax-distr 11201 ax-i2m1 11202 ax-1ne0 11203 ax-1rid 11204 ax-rnegex 11205 ax-rrecex 11206 ax-cnre 11207 ax-pre-lttri 11208 ax-pre-lttrn 11209 ax-pre-ltadd 11210 ax-pre-mulgt0 11211 ax-pre-sup 11212 ax-addf 11213

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2810 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3062 df-rmo 3364 df-reu 3365 df-rab 3421 df-v 3466 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-pss 3951 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-tp 4611 df-op 4613 df-uni 4889 df-int 4928 df-iun 4974 df-iin 4975 df-br 5125 df-opab 5187 df-mpt 5207 df-tr 5235 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-se 5612 df-we 5613 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 6295 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-isom 6545 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-of 7676 df-om 7867 df-1st 7993 df-2nd 7994 df-supp 8165 df-frecs 8285 df-wrecs 8316 df-recs 8390 df-rdg 8429 df-1o 8485 df-2o 8486 df-er 8724 df-map 8847 df-pm 8848 df-ixp 8917 df-en 8965 df-dom 8966 df-sdom 8967 df-fin 8968 df-fsupp 9379 df-fi 9428 df-sup 9459 df-inf 9460 df-oi 9529 df-card 9958 df-pnf 11276 df-mnf 11277 df-xr 11278 df-ltxr 11279 df-le 11280 df-sub 11473 df-neg 11474 df-div 11900 df-nn 12246 df-2 12308 df-3 12309 df-4 12310 df-5 12311 df-6 12312 df-7 12313 df-8 12314 df-9 12315 df-n0 12507 df-xnn0 12580 df-z 12594 df-dec 12714 df-uz 12858 df-q 12970 df-rp 13014 df-xneg 13133 df-xadd 13134 df-xmul 13135 df-icc 13374 df-fz 13530 df-fzo 13677 df-seq 14025 df-exp 14085 df-fac 14297 df-hash 14354 df-cj 15123 df-re 15124 df-im 15125 df-sqrt 15259 df-abs 15260 df-clim 15509 df-sum 15708 df-struct 17171 df-sets 17188 df-slot 17206 df-ndx 17218 df-base 17234 df-ress 17257 df-plusg 17289 df-mulr 17290 df-starv 17291 df-sca 17292 df-vsca 17293 df-ip 17294 df-tset 17295 df-ple 17296 df-ds 17298 df-unif 17299 df-hom 17300 df-cco 17301 df-rest 17441 df-topn 17442 df-0g 17460 df-gsum 17461 df-topgen 17462 df-pt 17463 df-prds 17466 df-xrs 17521 df-qtop 17526 df-imas 17527 df-xps 17529 df-mre 17603 df-mrc 17604 df-acs 17606 df-mgm 18623 df-sgrp 18702 df-mnd 18718 df-submnd 18767 df-grp 18924 df-minusg 18925 df-mulg 19056 df-cntz 19305 df-cmn 19768 df-abl 19769 df-mgp 20106 df-ur 20147 df-ring 20200 df-cring 20201 df-psmet 21312 df-xmet 21313 df-met 21314 df-bl 21315 df-mopn 21316 df-fbas 21317 df-fg 21318 df-cnfld 21321 df-top 22837 df-topon 22854 df-topsp 22876 df-bases 22889 df-cld 22962 df-ntr 22963 df-cls 22964 df-nei 23041 df-lp 23079 df-perf 23080 df-cn 23170 df-cnp 23171 df-haus 23258 df-tx 23505 df-hmeo 23698 df-fil 23789 df-fm 23881 df-flim 23882 df-flf 23883 df-tsms 24070 df-xms 24264 df-ms 24265 df-tms 24266 df-cncf 24827 df-limc 25824 df-dv 25825 df-dvn 25826 df-tayl 26319

This theorem is referenced by: taylth 26341

W3C validator