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 26350

Description: Lemma for taylth 26353. 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 26353 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 13499	. . . 4 ⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈ (1...𝑁))
3	1, 2	sylib 218	. . 3 ⊢ (𝜑 → 𝑁 ∈ (1...𝑁))
4		oveq2 7368	. . . . . . . . . . . 12 ⊢ (𝑚 = 1 → (𝑁 − 𝑚) = (𝑁 − 1))
5	4	fveq2d 6838	. . . . . . . . . . 11 ⊢ (𝑚 = 1 → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚)) = ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))
6	5	fveq1d 6836	. . . . . . . . . 10 ⊢ (𝑚 = 1 → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) = (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥))
7	4	fveq2d 6838	. . . . . . . . . . 11 ⊢ (𝑚 = 1 → ((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚)) = ((ℂ D^𝑛 𝑇)‘(𝑁 − 1)))
8	7	fveq1d 6836	. . . . . . . . . 10 ⊢ (𝑚 = 1 → (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥) = (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥))
9	6, 8	oveq12d 7378	. . . . . . . . 9 ⊢ (𝑚 = 1 → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) = ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)))
10		oveq2 7368	. . . . . . . . 9 ⊢ (𝑚 = 1 → ((𝑥 − 𝐵)↑𝑚) = ((𝑥 − 𝐵)↑1))
11	9, 10	oveq12d 7378	. . . . . . . 8 ⊢ (𝑚 = 1 → (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚)) = (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1)))
12	11	mpteq2dv 5180	. . . . . . 7 ⊢ (𝑚 = 1 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))))
13	12	oveq1d 7375	. . . . . 6 ⊢ (𝑚 = 1 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) lim_ℂ 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))) lim_ℂ 𝐵))
14	13	eleq2d 2823	. . . . 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 7368	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑛 → (𝑁 − 𝑚) = (𝑁 − 𝑛))
17	16	fveq2d 6838	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚)) = ((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛)))
18	17	fveq1d 6836	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) = (((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥))
19	16	fveq2d 6838	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → ((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚)) = ((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛)))
20	19	fveq1d 6836	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥) = (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑥))
21	18, 20	oveq12d 7378	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) = ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑥)))
22		oveq2 7368	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → ((𝑥 − 𝐵)↑𝑚) = ((𝑥 − 𝐵)↑𝑛))
23	21, 22	oveq12d 7378	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚)) = (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑥)) / ((𝑥 − 𝐵)↑𝑛)))
24	23	mpteq2dv 5180	. . . . . . . 8 ⊢ (𝑚 = 𝑛 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑥)) / ((𝑥 − 𝐵)↑𝑛))))
25		fveq2 6834	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) = (((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦))
26		fveq2 6834	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑥) = (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑦))
27	25, 26	oveq12d 7378	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑥)) = ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑦)))
28		oveq1 7367	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑥 − 𝐵) = (𝑦 − 𝐵))
29	28	oveq1d 7375	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((𝑥 − 𝐵)↑𝑛) = ((𝑦 − 𝐵)↑𝑛))
30	27, 29	oveq12d 7378	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑥)) / ((𝑥 − 𝐵)↑𝑛)) = (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛)))
31	30	cbvmptv 5190	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑥)) / ((𝑥 − 𝐵)↑𝑛))) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛)))
32	24, 31	eqtrdi 2788	. . . . . . 7 ⊢ (𝑚 = 𝑛 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))))
33	32	oveq1d 7375	. . . . . 6 ⊢ (𝑚 = 𝑛 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) lim_ℂ 𝐵) = ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) lim_ℂ 𝐵))
34	33	eleq2d 2823	. . . . 5 ⊢ (𝑚 = 𝑛 → (0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) lim_ℂ 𝐵) ↔ 0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) lim_ℂ 𝐵)))
35	34	imbi2d 340	. . . 4 ⊢ (𝑚 = 𝑛 → ((𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) lim_ℂ 𝐵)) ↔ (𝜑 → 0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) lim_ℂ 𝐵))))
36		oveq2 7368	. . . . . . . . . . . 12 ⊢ (𝑚 = (𝑛 + 1) → (𝑁 − 𝑚) = (𝑁 − (𝑛 + 1)))
37	36	fveq2d 6838	. . . . . . . . . . 11 ⊢ (𝑚 = (𝑛 + 1) → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚)) = ((𝑆 D^𝑛 𝐹)‘(𝑁 − (𝑛 + 1))))
38	37	fveq1d 6836	. . . . . . . . . 10 ⊢ (𝑚 = (𝑛 + 1) → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) = (((𝑆 D^𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥))
39	36	fveq2d 6838	. . . . . . . . . . 11 ⊢ (𝑚 = (𝑛 + 1) → ((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚)) = ((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑛 + 1))))
40	39	fveq1d 6836	. . . . . . . . . 10 ⊢ (𝑚 = (𝑛 + 1) → (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥) = (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥))
41	38, 40	oveq12d 7378	. . . . . . . . 9 ⊢ (𝑚 = (𝑛 + 1) → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) = ((((𝑆 D^𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)))
42		oveq2 7368	. . . . . . . . 9 ⊢ (𝑚 = (𝑛 + 1) → ((𝑥 − 𝐵)↑𝑚) = ((𝑥 − 𝐵)↑(𝑛 + 1)))
43	41, 42	oveq12d 7378	. . . . . . . 8 ⊢ (𝑚 = (𝑛 + 1) → (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚)) = (((((𝑆 D^𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1))))
44	43	mpteq2dv 5180	. . . . . . 7 ⊢ (𝑚 = (𝑛 + 1) → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))))
45	44	oveq1d 7375	. . . . . 6 ⊢ (𝑚 = (𝑛 + 1) → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) lim_ℂ 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))) lim_ℂ 𝐵))
46	45	eleq2d 2823	. . . . 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 7368	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑁 → (𝑁 − 𝑚) = (𝑁 − 𝑁))
49	48	fveq2d 6838	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑁 → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚)) = ((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁)))
50	49	fveq1d 6836	. . . . . . . . . 10 ⊢ (𝑚 = 𝑁 → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) = (((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥))
51	48	fveq2d 6838	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑁 → ((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚)) = ((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁)))
52	51	fveq1d 6836	. . . . . . . . . 10 ⊢ (𝑚 = 𝑁 → (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥) = (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥))
53	50, 52	oveq12d 7378	. . . . . . . . 9 ⊢ (𝑚 = 𝑁 → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) = ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)))
54		oveq2 7368	. . . . . . . . 9 ⊢ (𝑚 = 𝑁 → ((𝑥 − 𝐵)↑𝑚) = ((𝑥 − 𝐵)↑𝑁))
55	53, 54	oveq12d 7378	. . . . . . . 8 ⊢ (𝑚 = 𝑁 → (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚)) = (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁)))
56	55	mpteq2dv 5180	. . . . . . 7 ⊢ (𝑚 = 𝑁 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))))
57	56	oveq1d 7375	. . . . . 6 ⊢ (𝑚 = 𝑁 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) lim_ℂ 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) lim_ℂ 𝐵))
58	57	eleq2d 2823	. . . . 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 6834	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝐵 → (((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) = (((𝑆 D^𝑛 𝐹)‘𝑁)‘𝐵))
62		fveq2 6834	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝐵 → (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦) = (((ℂ D^𝑛 𝑇)‘𝑁)‘𝐵))
63	61, 62	oveq12d 7378	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝐵 → ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)) = ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝐵) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝐵)))
64		eqid 2737	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦))) = (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))
65		ovex 7393	. . . . . . . . . . . . 13 ⊢ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝐵) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝐵)) ∈ V
66	63, 64, 65	fvmpt 6941	. . . . . . . . . . . 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 12489	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
72		nn0uz 12817	. . . . . . . . . . . . . . 15 ⊢ ℕ₀ = (ℤ_≥‘0)
73	71, 72	eleqtrdi 2847	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘0))
74		eluzfz2b 13478	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ (ℤ_≥‘0) ↔ 𝑁 ∈ (0...𝑁))
75	73, 74	sylib 218	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ (0...𝑁))
76		taylthlem1.d	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom ((𝑆 D^𝑛 𝐹)‘𝑁) = 𝐴)
77	60, 76	eleqtrrd 2840	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D^𝑛 𝐹)‘𝑁))
78		taylthlem1.t	. . . . . . . . . . . . 13 ⊢ 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵)
79	68, 69, 70, 75, 77, 78	dvntaylp0 26349	. . . . . . . . . . . 12 ⊢ (𝜑 → (((ℂ D^𝑛 𝑇)‘𝑁)‘𝐵) = (((𝑆 D^𝑛 𝐹)‘𝑁)‘𝐵))
80	79	oveq2d 7376	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝐵) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝐵)) = ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝐵) − (((𝑆 D^𝑛 𝐹)‘𝑁)‘𝐵)))
81		cnex 11110	. . . . . . . . . . . . . . . 16 ⊢ ℂ ∈ V
82	81	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ℂ ∈ V)
83		elpm2r 8785	. . . . . . . . . . . . . . 15 ⊢ (((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆)) → 𝐹 ∈ (ℂ ↑_pm 𝑆))
84	82, 68, 69, 70, 83	syl22anc 839	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹 ∈ (ℂ ↑_pm 𝑆))
85		dvnf 25904	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ 𝑁 ∈ ℕ₀) → ((𝑆 D^𝑛 𝐹)‘𝑁):dom ((𝑆 D^𝑛 𝐹)‘𝑁)⟶ℂ)
86	68, 84, 71, 85	syl3anc 1374	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘𝑁):dom ((𝑆 D^𝑛 𝐹)‘𝑁)⟶ℂ)
87	86, 77	ffvelcdmd 7031	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑆 D^𝑛 𝐹)‘𝑁)‘𝐵) ∈ ℂ)
88	87	subidd 11484	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝐵) − (((𝑆 D^𝑛 𝐹)‘𝑁)‘𝐵)) = 0)
89	67, 80, 88	3eqtrd 2776	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))‘𝐵) = 0)
90		funmpt 6530	. . . . . . . . . . 11 ⊢ Fun (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))
91		ovex 7393	. . . . . . . . . . . . 13 ⊢ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)) ∈ V
92	91, 64	dmmpti 6636	. . . . . . . . . . . 12 ⊢ dom (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦))) = 𝐴
93	60, 92	eleqtrrdi 2848	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ dom (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦))))
94		funbrfvb 6887	. . . . . . . . . . 11 ⊢ ((Fun (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦))) ∧ 𝐵 ∈ dom (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))) → (((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))‘𝐵) = 0 ↔ 𝐵(𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))0))
95	90, 93, 94	sylancr 588	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))‘𝐵) = 0 ↔ 𝐵(𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))0))
96	89, 95	mpbid 232	. . . . . . . . 9 ⊢ (𝜑 → 𝐵(𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))0)
97		nnm1nn0 12469	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ₀)
98	1, 97	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑁 − 1) ∈ ℕ₀)
99		dvnf 25904	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ (𝑁 − 1) ∈ ℕ₀) → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)):dom ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))⟶ℂ)
100	68, 84, 98, 99	syl3anc 1374	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)):dom ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))⟶ℂ)
101		dvnbss 25905	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ (𝑁 − 1) ∈ ℕ₀) → dom ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)) ⊆ dom 𝐹)
102	68, 84, 98, 101	syl3anc 1374	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)) ⊆ dom 𝐹)
103	69, 102	fssdmd 6680	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)) ⊆ 𝐴)
104		fzo0end 13704	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ (0..^𝑁))
105		elfzofz 13621	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 − 1) ∈ (0..^𝑁) → (𝑁 − 1) ∈ (0...𝑁))
106	1, 104, 105	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑁 − 1) ∈ (0...𝑁))
107		dvn2bss 25907	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ (𝑁 − 1) ∈ (0...𝑁)) → dom ((𝑆 D^𝑛 𝐹)‘𝑁) ⊆ dom ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))
108	68, 84, 106, 107	syl3anc 1374	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom ((𝑆 D^𝑛 𝐹)‘𝑁) ⊆ dom ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))
109	76, 108	eqsstrrd 3958	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ⊆ dom ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))
110	103, 109	eqssd 3940	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)) = 𝐴)
111	110	feq2d 6646	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)):dom ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))⟶ℂ ↔ ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)):𝐴⟶ℂ))
112	100, 111	mpbid 232	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)):𝐴⟶ℂ)
113	112	ffvelcdmda 7030	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) ∈ ℂ)
114	76	feq2d 6646	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑆 D^𝑛 𝐹)‘𝑁):dom ((𝑆 D^𝑛 𝐹)‘𝑁)⟶ℂ ↔ ((𝑆 D^𝑛 𝐹)‘𝑁):𝐴⟶ℂ))
115	86, 114	mpbid 232	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘𝑁):𝐴⟶ℂ)
116	115	ffvelcdmda 7030	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) ∈ ℂ)
117	1	nncnd 12181	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ ℂ)
118		1cnd 11130	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 ∈ ℂ)
119	117, 118	npcand 11500	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
120	119	fveq2d 6838	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘((𝑁 − 1) + 1)) = ((𝑆 D^𝑛 𝐹)‘𝑁))
121		recnprss 25881	. . . . . . . . . . . . . . 15 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
122	68, 121	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
123		dvnp1 25902	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ (𝑁 − 1) ∈ ℕ₀) → ((𝑆 D^𝑛 𝐹)‘((𝑁 − 1) + 1)) = (𝑆 D ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))))
124	122, 84, 98, 123	syl3anc 1374	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘((𝑁 − 1) + 1)) = (𝑆 D ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))))
125	120, 124	eqtr3d 2774	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘𝑁) = (𝑆 D ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))))
126	115	feqmptd 6902	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘𝑁) = (𝑦 ∈ 𝐴 ↦ (((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦)))
127	112	feqmptd 6902	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)) = (𝑦 ∈ 𝐴 ↦ (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦)))
128	127	oveq2d 7376	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆 D ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))) = (𝑆 D (𝑦 ∈ 𝐴 ↦ (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦))))
129	125, 126, 128	3eqtr3rd 2781	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝐴 ↦ (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦))) = (𝑦 ∈ 𝐴 ↦ (((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦)))
130	70, 122	sstrd 3933	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ⊆ ℂ)
131	130	sselda 3922	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℂ)
132		1nn0 12444	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℕ₀
133	132	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 ∈ ℕ₀)
134		elpm2r 8785	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)):𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆)) → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)) ∈ (ℂ ↑_pm 𝑆))
135	82, 68, 112, 70, 134	syl22anc 839	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)) ∈ (ℂ ↑_pm 𝑆))
136		dvn1 25903	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ⊆ ℂ ∧ ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)) ∈ (ℂ ↑_pm 𝑆)) → ((𝑆 D^𝑛 ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))‘1) = (𝑆 D ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))))
137	122, 135, 136	syl2anc 585	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑆 D^𝑛 ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))‘1) = (𝑆 D ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))))
138	124, 120	eqtr3d 2774	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑆 D ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))) = ((𝑆 D^𝑛 𝐹)‘𝑁))
139	137, 138	eqtrd 2772	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑆 D^𝑛 ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))‘1) = ((𝑆 D^𝑛 𝐹)‘𝑁))
140	139	dmeqd 5854	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom ((𝑆 D^𝑛 ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))‘1) = dom ((𝑆 D^𝑛 𝐹)‘𝑁))
141	77, 140	eleqtrrd 2840	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D^𝑛 ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))‘1))
142		eqid 2737	. . . . . . . . . . . . . . 15 ⊢ (1(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))𝐵) = (1(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))𝐵)
143	68, 112, 70, 133, 141, 142	taylpf 26342	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))𝐵):ℂ⟶ℂ)
144	118, 117	pncan3d 11499	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (1 + (𝑁 − 1)) = 𝑁)
145	144	oveq1d 7375	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵) = (𝑁(𝑆 Tayl 𝐹)𝐵))
146	78, 145	eqtr4id 2791	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑇 = ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵))
147	146	oveq2d 7376	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (ℂ D^𝑛 𝑇) = (ℂ D^𝑛 ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵)))
148	147	fveq1d 6836	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘(𝑁 − 1)) = ((ℂ D^𝑛 ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵))‘(𝑁 − 1)))
149	144	fveq2d 6838	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘(1 + (𝑁 − 1))) = ((𝑆 D^𝑛 𝐹)‘𝑁))
150	149	dmeqd 5854	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → dom ((𝑆 D^𝑛 𝐹)‘(1 + (𝑁 − 1))) = dom ((𝑆 D^𝑛 𝐹)‘𝑁))
151	77, 150	eleqtrrd 2840	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D^𝑛 𝐹)‘(1 + (𝑁 − 1))))
152	68, 69, 70, 98, 133, 151	dvntaylp 26348	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((ℂ D^𝑛 ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵))‘(𝑁 − 1)) = (1(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))𝐵))
153	148, 152	eqtrd 2772	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘(𝑁 − 1)) = (1(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))𝐵))
154	153	feq1d 6644	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((ℂ D^𝑛 𝑇)‘(𝑁 − 1)):ℂ⟶ℂ ↔ (1(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))𝐵):ℂ⟶ℂ))
155	143, 154	mpbird 257	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘(𝑁 − 1)):ℂ⟶ℂ)
156	155	ffvelcdmda 7030	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦) ∈ ℂ)
157	131, 156	syldan 592	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦) ∈ ℂ)
158		0nn0 12443	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℕ₀
159	158	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 0 ∈ ℕ₀)
160		elpm2r 8785	. . . . . . . . . . . . . . . . . . 19 ⊢ (((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (((𝑆 D^𝑛 𝐹)‘𝑁):𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆)) → ((𝑆 D^𝑛 𝐹)‘𝑁) ∈ (ℂ ↑_pm 𝑆))
161	82, 68, 115, 70, 160	syl22anc 839	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘𝑁) ∈ (ℂ ↑_pm 𝑆))
162		dvn0 25901	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑆 ⊆ ℂ ∧ ((𝑆 D^𝑛 𝐹)‘𝑁) ∈ (ℂ ↑_pm 𝑆)) → ((𝑆 D^𝑛 ((𝑆 D^𝑛 𝐹)‘𝑁))‘0) = ((𝑆 D^𝑛 𝐹)‘𝑁))
163	122, 161, 162	syl2anc 585	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑆 D^𝑛 ((𝑆 D^𝑛 𝐹)‘𝑁))‘0) = ((𝑆 D^𝑛 𝐹)‘𝑁))
164	163	dmeqd 5854	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom ((𝑆 D^𝑛 ((𝑆 D^𝑛 𝐹)‘𝑁))‘0) = dom ((𝑆 D^𝑛 𝐹)‘𝑁))
165	77, 164	eleqtrrd 2840	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D^𝑛 ((𝑆 D^𝑛 𝐹)‘𝑁))‘0))
166		eqid 2737	. . . . . . . . . . . . . . 15 ⊢ (0(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘𝑁))𝐵) = (0(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘𝑁))𝐵)
167	68, 115, 70, 159, 165, 166	taylpf 26342	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘𝑁))𝐵):ℂ⟶ℂ)
168	117	addlidd 11338	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (0 + 𝑁) = 𝑁)
169	168	oveq1d 7375	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵) = (𝑁(𝑆 Tayl 𝐹)𝐵))
170	169, 78	eqtr4di 2790	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵) = 𝑇)
171	170	oveq2d 7376	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (ℂ D^𝑛 ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵)) = (ℂ D^𝑛 𝑇))
172	171	fveq1d 6836	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((ℂ D^𝑛 ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵))‘𝑁) = ((ℂ D^𝑛 𝑇)‘𝑁))
173	168	fveq2d 6838	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘(0 + 𝑁)) = ((𝑆 D^𝑛 𝐹)‘𝑁))
174	173	dmeqd 5854	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → dom ((𝑆 D^𝑛 𝐹)‘(0 + 𝑁)) = dom ((𝑆 D^𝑛 𝐹)‘𝑁))
175	77, 174	eleqtrrd 2840	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D^𝑛 𝐹)‘(0 + 𝑁)))
176	68, 69, 70, 71, 159, 175	dvntaylp 26348	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((ℂ D^𝑛 ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵))‘𝑁) = (0(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘𝑁))𝐵))
177	172, 176	eqtr3d 2774	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘𝑁) = (0(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘𝑁))𝐵))
178	177	feq1d 6644	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((ℂ D^𝑛 𝑇)‘𝑁):ℂ⟶ℂ ↔ (0(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘𝑁))𝐵):ℂ⟶ℂ))
179	167, 178	mpbird 257	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘𝑁):ℂ⟶ℂ)
180	179	ffvelcdmda 7030	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦) ∈ ℂ)
181	131, 180	syldan 592	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦) ∈ ℂ)
182	122	sselda 3922	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ ℂ)
183	182, 156	syldan 592	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦) ∈ ℂ)
184	182, 180	syldan 592	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦) ∈ ℂ)
185		eqid 2737	. . . . . . . . . . . . 13 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
186	185	cnfldtopon 24757	. . . . . . . . . . . . . 14 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
187		toponmax 22901	. . . . . . . . . . . . . 14 ⊢ ((TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ) → ℂ ∈ (TopOpen‘ℂ_fld))
188	186, 187	mp1i 13	. . . . . . . . . . . . 13 ⊢ (𝜑 → ℂ ∈ (TopOpen‘ℂ_fld))
189		dfss2 3908	. . . . . . . . . . . . . 14 ⊢ (𝑆 ⊆ ℂ ↔ (𝑆 ∩ ℂ) = 𝑆)
190	122, 189	sylib 218	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆 ∩ ℂ) = 𝑆)
191		ssid 3945	. . . . . . . . . . . . . . . . 17 ⊢ ℂ ⊆ ℂ
192	191	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ℂ ⊆ ℂ)
193		mapsspm 8817	. . . . . . . . . . . . . . . . 17 ⊢ (ℂ ↑_m ℂ) ⊆ (ℂ ↑_pm ℂ)
194	68, 69, 70, 71, 77, 78	taylpf 26342	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑇:ℂ⟶ℂ)
195	81, 81	elmap 8812	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑇 ∈ (ℂ ↑_m ℂ) ↔ 𝑇:ℂ⟶ℂ)
196	194, 195	sylibr 234	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑇 ∈ (ℂ ↑_m ℂ))
197	193, 196	sselid 3920	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑇 ∈ (ℂ ↑_pm ℂ))
198		dvnp1 25902	. . . . . . . . . . . . . . . 16 ⊢ ((ℂ ⊆ ℂ ∧ 𝑇 ∈ (ℂ ↑_pm ℂ) ∧ (𝑁 − 1) ∈ ℕ₀) → ((ℂ D^𝑛 𝑇)‘((𝑁 − 1) + 1)) = (ℂ D ((ℂ D^𝑛 𝑇)‘(𝑁 − 1))))
199	192, 197, 98, 198	syl3anc 1374	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘((𝑁 − 1) + 1)) = (ℂ D ((ℂ D^𝑛 𝑇)‘(𝑁 − 1))))
200	119	fveq2d 6838	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘((𝑁 − 1) + 1)) = ((ℂ D^𝑛 𝑇)‘𝑁))
201	199, 200	eqtr3d 2774	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℂ D ((ℂ D^𝑛 𝑇)‘(𝑁 − 1))) = ((ℂ D^𝑛 𝑇)‘𝑁))
202	155	feqmptd 6902	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘(𝑁 − 1)) = (𝑦 ∈ ℂ ↦ (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))
203	202	oveq2d 7376	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℂ D ((ℂ D^𝑛 𝑇)‘(𝑁 − 1))) = (ℂ D (𝑦 ∈ ℂ ↦ (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦))))
204	179	feqmptd 6902	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘𝑁) = (𝑦 ∈ ℂ ↦ (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))
205	201, 203, 204	3eqtr3d 2780	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦))) = (𝑦 ∈ ℂ ↦ (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))
206	185, 68, 188, 190, 156, 180, 205	dvmptres3 25933	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝑆 ↦ (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦))) = (𝑦 ∈ 𝑆 ↦ (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))
207		eqid 2737	. . . . . . . . . . . 12 ⊢ ((TopOpen‘ℂ_fld) ↾_t 𝑆) = ((TopOpen‘ℂ_fld) ↾_t 𝑆)
208		resttopon 23136	. . . . . . . . . . . . . . . 16 ⊢ (((TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ) ∧ 𝑆 ⊆ ℂ) → ((TopOpen‘ℂ_fld) ↾_t 𝑆) ∈ (TopOn‘𝑆))
209	186, 122, 208	sylancr 588	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((TopOpen‘ℂ_fld) ↾_t 𝑆) ∈ (TopOn‘𝑆))
210		topontop 22888	. . . . . . . . . . . . . . 15 ⊢ (((TopOpen‘ℂ_fld) ↾_t 𝑆) ∈ (TopOn‘𝑆) → ((TopOpen‘ℂ_fld) ↾_t 𝑆) ∈ Top)
211	209, 210	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((TopOpen‘ℂ_fld) ↾_t 𝑆) ∈ Top)
212		toponuni 22889	. . . . . . . . . . . . . . . 16 ⊢ (((TopOpen‘ℂ_fld) ↾_t 𝑆) ∈ (TopOn‘𝑆) → 𝑆 = ∪ ((TopOpen‘ℂ_fld) ↾_t 𝑆))
213	209, 212	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑆 = ∪ ((TopOpen‘ℂ_fld) ↾_t 𝑆))
214	70, 213	sseqtrd 3959	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ⊆ ∪ ((TopOpen‘ℂ_fld) ↾_t 𝑆))
215		eqid 2737	. . . . . . . . . . . . . . 15 ⊢ ∪ ((TopOpen‘ℂ_fld) ↾_t 𝑆) = ∪ ((TopOpen‘ℂ_fld) ↾_t 𝑆)
216	215	ntrss2 23032	. . . . . . . . . . . . . 14 ⊢ ((((TopOpen‘ℂ_fld) ↾_t 𝑆) ∈ Top ∧ 𝐴 ⊆ ∪ ((TopOpen‘ℂ_fld) ↾_t 𝑆)) → ((int‘((TopOpen‘ℂ_fld) ↾_t 𝑆))‘𝐴) ⊆ 𝐴)
217	211, 214, 216	syl2anc 585	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((int‘((TopOpen‘ℂ_fld) ↾_t 𝑆))‘𝐴) ⊆ 𝐴)
218	138	dmeqd 5854	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom (𝑆 D ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))) = dom ((𝑆 D^𝑛 𝐹)‘𝑁))
219	218, 76	eqtrd 2772	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom (𝑆 D ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))) = 𝐴)
220	122, 112, 70, 207, 185	dvbssntr 25877	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom (𝑆 D ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))) ⊆ ((int‘((TopOpen‘ℂ_fld) ↾_t 𝑆))‘𝐴))
221	219, 220	eqsstrrd 3958	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ⊆ ((int‘((TopOpen‘ℂ_fld) ↾_t 𝑆))‘𝐴))
222	217, 221	eqssd 3940	. . . . . . . . . . . 12 ⊢ (𝜑 → ((int‘((TopOpen‘ℂ_fld) ↾_t 𝑆))‘𝐴) = 𝐴)
223	68, 183, 184, 206, 70, 207, 185, 222	dvmptres2 25939	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝐴 ↦ (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦))) = (𝑦 ∈ 𝐴 ↦ (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))
224	68, 113, 116, 129, 157, 181, 223	dvmptsub 25944	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))) = (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦))))
225	224	breqd 5097	. . . . . . . . 9 ⊢ (𝜑 → (𝐵(𝑆 D (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦))))0 ↔ 𝐵(𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))0))
226	96, 225	mpbird 257	. . . . . . . 8 ⊢ (𝜑 → 𝐵(𝑆 D (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦))))0)
227		eqid 2737	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵)))
228	113, 157	subcld 11496	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)) ∈ ℂ)
229	228	fmpttd 7061	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦))):𝐴⟶ℂ)
230	207, 185, 227, 122, 229, 70	eldv 25875	. . . . . . . 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 4072	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐴 ∖ {𝐵}) → 𝑥 ∈ 𝐴)
234		fveq2 6834	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑥 → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) = (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥))
235		fveq2 6834	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑥 → (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦) = (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥))
236	234, 235	oveq12d 7378	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑥 → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)) = ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)))
237		eqid 2737	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦))) = (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))
238		ovex 7393	. . . . . . . . . . . . 13 ⊢ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) ∈ V
239	236, 237, 238	fvmpt 6941	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) = ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)))
240		fveq2 6834	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝐵 → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) = (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝐵))
241		fveq2 6834	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝐵 → (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦) = (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝐵))
242	240, 241	oveq12d 7378	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝐵 → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)) = ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝐵)))
243		ovex 7393	. . . . . . . . . . . . . . 15 ⊢ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝐵)) ∈ V
244	242, 237, 243	fvmpt 6941	. . . . . . . . . . . . . 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 26349	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝐵) = (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝐵))
247	246	oveq2d 7376	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝐵)) = ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝐵)))
248	112, 60	ffvelcdmd 7031	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝐵) ∈ ℂ)
249	248	subidd 11484	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝐵)) = 0)
250	245, 247, 249	3eqtrd 2776	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵) = 0)
251	239, 250	oveqan12rd 7380	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) = (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) − 0))
252	112	ffvelcdmda 7030	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) ∈ ℂ)
253	130	sselda 3922	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℂ)
254	155	ffvelcdmda 7030	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥) ∈ ℂ)
255	253, 254	syldan 592	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥) ∈ ℂ)
256	252, 255	subcld 11496	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) ∈ ℂ)
257	256	subid1d 11485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) − 0) = ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)))
258	251, 257	eqtr2d 2773	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) = (((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)))
259	233, 258	sylan2 594	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) = (((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)))
260	130	ssdifssd 4088	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 ∖ {𝐵}) ⊆ ℂ)
261	260	sselda 3922	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ ℂ)
262	130, 60	sseldd 3923	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ ℂ)
263	262	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝐵 ∈ ℂ)
264	261, 263	subcld 11496	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑥 − 𝐵) ∈ ℂ)
265	264	exp1d 14094	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑥 − 𝐵)↑1) = (𝑥 − 𝐵))
266	259, 265	oveq12d 7378	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1)) = ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵)))
267	266	mpteq2dva 5179	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵))))
268	267	oveq1d 7375	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))) lim_ℂ 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵))) lim_ℂ 𝐵))
269	232, 268	eleqtrrd 2840	. . . . 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 13734	. . 3 ⊢ (𝑁 ∈ (1...𝑁) → (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) lim_ℂ 𝐵)))
276	3, 275	mpcom 38	. 2 ⊢ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) lim_ℂ 𝐵))
277	117	subidd 11484	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 − 𝑁) = 0)
278	277	fveq2d 6838	. . . . . . . . 9 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁)) = ((𝑆 D^𝑛 𝐹)‘0))
279		dvn0 25901	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆)) → ((𝑆 D^𝑛 𝐹)‘0) = 𝐹)
280	122, 84, 279	syl2anc 585	. . . . . . . . 9 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘0) = 𝐹)
281	278, 280	eqtrd 2772	. . . . . . . 8 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁)) = 𝐹)
282	281	fveq1d 6836	. . . . . . 7 ⊢ (𝜑 → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) = (𝐹‘𝑥))
283	277	fveq2d 6838	. . . . . . . . 9 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁)) = ((ℂ D^𝑛 𝑇)‘0))
284		dvn0 25901	. . . . . . . . . 10 ⊢ ((ℂ ⊆ ℂ ∧ 𝑇 ∈ (ℂ ↑_pm ℂ)) → ((ℂ D^𝑛 𝑇)‘0) = 𝑇)
285	191, 197, 284	sylancr 588	. . . . . . . . 9 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘0) = 𝑇)
286	283, 285	eqtrd 2772	. . . . . . . 8 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁)) = 𝑇)
287	286	fveq1d 6836	. . . . . . 7 ⊢ (𝜑 → (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥) = (𝑇‘𝑥))
288	282, 287	oveq12d 7378	. . . . . 6 ⊢ (𝜑 → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) = ((𝐹‘𝑥) − (𝑇‘𝑥)))
289	288	oveq1d 7375	. . . . 5 ⊢ (𝜑 → (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁)) = (((𝐹‘𝑥) − (𝑇‘𝑥)) / ((𝑥 − 𝐵)↑𝑁)))
290	289	mpteq2dv 5180	. . . 4 ⊢ (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝐹‘𝑥) − (𝑇‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))))
291		taylthlem1.r	. . . 4 ⊢ 𝑅 = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝐹‘𝑥) − (𝑇‘𝑥)) / ((𝑥 − 𝐵)↑𝑁)))
292	290, 291	eqtr4di 2790	. . 3 ⊢ (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) = 𝑅)
293	292	oveq1d 7375	. 2 ⊢ (𝜑 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) lim_ℂ 𝐵) = (𝑅 lim_ℂ 𝐵))
294	276, 293	eleqtrd 2839	1 ⊢ (𝜑 → 0 ∈ (𝑅 lim_ℂ 𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1542 ∈ wcel 2114 Vcvv 3430 ∖ cdif 3887 ∩ cin 3889 ⊆ wss 3890 {csn 4568 {cpr 4570 ∪ cuni 4851 class class class wbr 5086 ↦ cmpt 5167 dom cdm 5624 Fun wfun 6486 ⟶wf 6488 ‘cfv 6492 (class class class)co 7360 ↑_m cmap 8766 ↑_pm cpm 8767 ℂcc 11027 ℝcr 11028 0cc0 11029 1c1 11030 + caddc 11032 − cmin 11368 / cdiv 11798 ℕcn 12165 ℕ₀cn0 12428 ℤ_≥cuz 12779 ...cfz 13452 ..^cfzo 13599 ↑cexp 14014 ↾_t crest 17374 TopOpenctopn 17375 ℂ_fldccnfld 21344 Topctop 22868 TopOnctopon 22885 intcnt 22992 lim_ℂ climc 25839 D cdv 25840 D^𝑛 cdvn 25841 Tayl ctayl 26329

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5302 ax-pr 5370 ax-un 7682 ax-inf2 9553 ax-cnex 11085 ax-resscn 11086 ax-1cn 11087 ax-icn 11088 ax-addcl 11089 ax-addrcl 11090 ax-mulcl 11091 ax-mulrcl 11092 ax-mulcom 11093 ax-addass 11094 ax-mulass 11095 ax-distr 11096 ax-i2m1 11097 ax-1ne0 11098 ax-1rid 11099 ax-rnegex 11100 ax-rrecex 11101 ax-cnre 11102 ax-pre-lttri 11103 ax-pre-lttrn 11104 ax-pre-ltadd 11105 ax-pre-mulgt0 11106 ax-pre-sup 11107 ax-addf 11108

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-tp 4573 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-iin 4937 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-se 5578 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-isom 6501 df-riota 7317 df-ov 7363 df-oprab 7364 df-mpo 7365 df-of 7624 df-om 7811 df-1st 7935 df-2nd 7936 df-supp 8104 df-frecs 8224 df-wrecs 8255 df-recs 8304 df-rdg 8342 df-1o 8398 df-2o 8399 df-er 8636 df-map 8768 df-pm 8769 df-ixp 8839 df-en 8887 df-dom 8888 df-sdom 8889 df-fin 8890 df-fsupp 9268 df-fi 9317 df-sup 9348 df-inf 9349 df-oi 9418 df-card 9854 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-sub 11370 df-neg 11371 df-div 11799 df-nn 12166 df-2 12235 df-3 12236 df-4 12237 df-5 12238 df-6 12239 df-7 12240 df-8 12241 df-9 12242 df-n0 12429 df-xnn0 12502 df-z 12516 df-dec 12636 df-uz 12780 df-q 12890 df-rp 12934 df-xneg 13054 df-xadd 13055 df-xmul 13056 df-icc 13296 df-fz 13453 df-fzo 13600 df-seq 13955 df-exp 14015 df-fac 14227 df-hash 14284 df-cj 15052 df-re 15053 df-im 15054 df-sqrt 15188 df-abs 15189 df-clim 15441 df-sum 15640 df-struct 17108 df-sets 17125 df-slot 17143 df-ndx 17155 df-base 17171 df-ress 17192 df-plusg 17224 df-mulr 17225 df-starv 17226 df-sca 17227 df-vsca 17228 df-ip 17229 df-tset 17230 df-ple 17231 df-ds 17233 df-unif 17234 df-hom 17235 df-cco 17236 df-rest 17376 df-topn 17377 df-0g 17395 df-gsum 17396 df-topgen 17397 df-pt 17398 df-prds 17401 df-xrs 17457 df-qtop 17462 df-imas 17463 df-xps 17465 df-mre 17539 df-mrc 17540 df-acs 17542 df-mgm 18599 df-sgrp 18678 df-mnd 18694 df-submnd 18743 df-grp 18903 df-minusg 18904 df-mulg 19035 df-cntz 19283 df-cmn 19748 df-abl 19749 df-mgp 20113 df-ur 20154 df-ring 20207 df-cring 20208 df-psmet 21336 df-xmet 21337 df-met 21338 df-bl 21339 df-mopn 21340 df-fbas 21341 df-fg 21342 df-cnfld 21345 df-top 22869 df-topon 22886 df-topsp 22908 df-bases 22921 df-cld 22994 df-ntr 22995 df-cls 22996 df-nei 23073 df-lp 23111 df-perf 23112 df-cn 23202 df-cnp 23203 df-haus 23290 df-tx 23537 df-hmeo 23730 df-fil 23821 df-fm 23913 df-flim 23914 df-flf 23915 df-tsms 24102 df-xms 24295 df-ms 24296 df-tms 24297 df-cncf 24855 df-limc 25843 df-dv 25844 df-dvn 25845 df-tayl 26331

This theorem is referenced by: taylth 26353

W3C validator