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 26757

Description: Lemma for taylth 26759. 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 26759 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 13728	. . . 4 ⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈ (1...𝑁))
3	1, 2	sylib 221	. . 3 ⊢ (𝜑 → 𝑁 ∈ (1...𝑁))
4		oveq2 7459	. . . . . . . . . . . 12 ⊢ (𝑚 = 1 → (𝑁 − 𝑚) = (𝑁 − 1))
5	4	fveq2d 6920	. . . . . . . . . . 11 ⊢ (𝑚 = 1 → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚)) = ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))
6	5	fveq1d 6918	. . . . . . . . . 10 ⊢ (𝑚 = 1 → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) = (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥))
7	4	fveq2d 6920	. . . . . . . . . . 11 ⊢ (𝑚 = 1 → ((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚)) = ((ℂ D^𝑛 𝑇)‘(𝑁 − 1)))
8	7	fveq1d 6918	. . . . . . . . . 10 ⊢ (𝑚 = 1 → (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥) = (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥))
9	6, 8	oveq12d 7469	. . . . . . . . 9 ⊢ (𝑚 = 1 → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) = ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)))
10		oveq2 7459	. . . . . . . . 9 ⊢ (𝑚 = 1 → ((𝑥 − 𝐵)↑𝑚) = ((𝑥 − 𝐵)↑1))
11	9, 10	oveq12d 7469	. . . . . . . 8 ⊢ (𝑚 = 1 → (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚)) = (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1)))
12	11	mpteq2dv 5205	. . . . . . 7 ⊢ (𝑚 = 1 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))))
13	12	oveq1d 7466	. . . . . 6 ⊢ (𝑚 = 1 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) lim_ℂ 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))) lim_ℂ 𝐵))
14	13	eleq2d 2850	. . . . 5 ⊢ (𝑚 = 1 → (0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) lim_ℂ 𝐵) ↔ 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))) lim_ℂ 𝐵)))
15	14	imbi2d 343	. . . 4 ⊢ (𝑚 = 1 → ((𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) lim_ℂ 𝐵)) ↔ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))) lim_ℂ 𝐵))))
16		oveq2 7459	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑛 → (𝑁 − 𝑚) = (𝑁 − 𝑛))
17	16	fveq2d 6920	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚)) = ((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛)))
18	17	fveq1d 6918	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) = (((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥))
19	16	fveq2d 6920	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → ((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚)) = ((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛)))
20	19	fveq1d 6918	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥) = (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑥))
21	18, 20	oveq12d 7469	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) = ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑥)))
22		oveq2 7459	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → ((𝑥 − 𝐵)↑𝑚) = ((𝑥 − 𝐵)↑𝑛))
23	21, 22	oveq12d 7469	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚)) = (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑥)) / ((𝑥 − 𝐵)↑𝑛)))
24	23	mpteq2dv 5205	. . . . . . . 8 ⊢ (𝑚 = 𝑛 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑥)) / ((𝑥 − 𝐵)↑𝑛))))
25		fveq2 6916	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) = (((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦))
26		fveq2 6916	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑥) = (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑦))
27	25, 26	oveq12d 7469	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑥)) = ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑦)))
28		oveq1 7458	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑥 − 𝐵) = (𝑦 − 𝐵))
29	28	oveq1d 7466	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((𝑥 − 𝐵)↑𝑛) = ((𝑦 − 𝐵)↑𝑛))
30	27, 29	oveq12d 7469	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑥)) / ((𝑥 − 𝐵)↑𝑛)) = (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛)))
31	30	cbvmptv 5215	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑥)) / ((𝑥 − 𝐵)↑𝑛))) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛)))
32	24, 31	eqtrdi 2814	. . . . . . 7 ⊢ (𝑚 = 𝑛 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))))
33	32	oveq1d 7466	. . . . . 6 ⊢ (𝑚 = 𝑛 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) lim_ℂ 𝐵) = ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) lim_ℂ 𝐵))
34	33	eleq2d 2850	. . . . 5 ⊢ (𝑚 = 𝑛 → (0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) lim_ℂ 𝐵) ↔ 0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) lim_ℂ 𝐵)))
35	34	imbi2d 343	. . . 4 ⊢ (𝑚 = 𝑛 → ((𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) lim_ℂ 𝐵)) ↔ (𝜑 → 0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) lim_ℂ 𝐵))))
36		oveq2 7459	. . . . . . . . . . . 12 ⊢ (𝑚 = (𝑛 + 1) → (𝑁 − 𝑚) = (𝑁 − (𝑛 + 1)))
37	36	fveq2d 6920	. . . . . . . . . . 11 ⊢ (𝑚 = (𝑛 + 1) → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚)) = ((𝑆 D^𝑛 𝐹)‘(𝑁 − (𝑛 + 1))))
38	37	fveq1d 6918	. . . . . . . . . 10 ⊢ (𝑚 = (𝑛 + 1) → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) = (((𝑆 D^𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥))
39	36	fveq2d 6920	. . . . . . . . . . 11 ⊢ (𝑚 = (𝑛 + 1) → ((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚)) = ((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑛 + 1))))
40	39	fveq1d 6918	. . . . . . . . . 10 ⊢ (𝑚 = (𝑛 + 1) → (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥) = (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥))
41	38, 40	oveq12d 7469	. . . . . . . . 9 ⊢ (𝑚 = (𝑛 + 1) → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) = ((((𝑆 D^𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)))
42		oveq2 7459	. . . . . . . . 9 ⊢ (𝑚 = (𝑛 + 1) → ((𝑥 − 𝐵)↑𝑚) = ((𝑥 − 𝐵)↑(𝑛 + 1)))
43	41, 42	oveq12d 7469	. . . . . . . 8 ⊢ (𝑚 = (𝑛 + 1) → (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚)) = (((((𝑆 D^𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1))))
44	43	mpteq2dv 5205	. . . . . . 7 ⊢ (𝑚 = (𝑛 + 1) → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))))
45	44	oveq1d 7466	. . . . . 6 ⊢ (𝑚 = (𝑛 + 1) → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) lim_ℂ 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))) lim_ℂ 𝐵))
46	45	eleq2d 2850	. . . . 5 ⊢ (𝑚 = (𝑛 + 1) → (0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) lim_ℂ 𝐵) ↔ 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))) lim_ℂ 𝐵)))
47	46	imbi2d 343	. . . 4 ⊢ (𝑚 = (𝑛 + 1) → ((𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) lim_ℂ 𝐵)) ↔ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))) lim_ℂ 𝐵))))
48		oveq2 7459	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑁 → (𝑁 − 𝑚) = (𝑁 − 𝑁))
49	48	fveq2d 6920	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑁 → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚)) = ((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁)))
50	49	fveq1d 6918	. . . . . . . . . 10 ⊢ (𝑚 = 𝑁 → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) = (((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥))
51	48	fveq2d 6920	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑁 → ((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚)) = ((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁)))
52	51	fveq1d 6918	. . . . . . . . . 10 ⊢ (𝑚 = 𝑁 → (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥) = (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥))
53	50, 52	oveq12d 7469	. . . . . . . . 9 ⊢ (𝑚 = 𝑁 → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) = ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)))
54		oveq2 7459	. . . . . . . . 9 ⊢ (𝑚 = 𝑁 → ((𝑥 − 𝐵)↑𝑚) = ((𝑥 − 𝐵)↑𝑁))
55	53, 54	oveq12d 7469	. . . . . . . 8 ⊢ (𝑚 = 𝑁 → (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚)) = (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁)))
56	55	mpteq2dv 5205	. . . . . . 7 ⊢ (𝑚 = 𝑁 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))))
57	56	oveq1d 7466	. . . . . 6 ⊢ (𝑚 = 𝑁 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) lim_ℂ 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) lim_ℂ 𝐵))
58	57	eleq2d 2850	. . . . 5 ⊢ (𝑚 = 𝑁 → (0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) lim_ℂ 𝐵) ↔ 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) lim_ℂ 𝐵)))
59	58	imbi2d 343	. . . 4 ⊢ (𝑚 = 𝑁 → ((𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) lim_ℂ 𝐵)) ↔ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) lim_ℂ 𝐵))))
60		taylthlem1.b	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ 𝐴)
61		fveq2 6916	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝐵 → (((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) = (((𝑆 D^𝑛 𝐹)‘𝑁)‘𝐵))
62		fveq2 6916	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝐵 → (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦) = (((ℂ D^𝑛 𝑇)‘𝑁)‘𝐵))
63	61, 62	oveq12d 7469	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝐵 → ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)) = ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝐵) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝐵)))
64		eqid 2763	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦))) = (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))
65		ovex 7484	. . . . . . . . . . . . 13 ⊢ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝐵) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝐵)) ∈ V
66	63, 64, 65	fvmpt 7024	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))‘𝐵) = ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝐵) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝐵)))
67	60, 66	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))‘𝐵) = ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝐵) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝐵)))
68		taylthlem1.s	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})
69		taylthlem1.f	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)
70		taylthlem1.a	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ⊆ 𝑆)
71	1	nnnn0d 12707	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
72		nn0uz 13043	. . . . . . . . . . . . . . 15 ⊢ ℕ₀ = (ℤ_≥‘0)
73	71, 72	eleqtrdi 2874	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘0))
74		eluzfz2b 13706	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ (ℤ_≥‘0) ↔ 𝑁 ∈ (0...𝑁))
75	73, 74	sylib 221	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ (0...𝑁))
76		taylthlem1.d	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom ((𝑆 D^𝑛 𝐹)‘𝑁) = 𝐴)
77	60, 76	eleqtrrd 2867	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D^𝑛 𝐹)‘𝑁))
78		taylthlem1.t	. . . . . . . . . . . . 13 ⊢ 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵)
79	68, 69, 70, 75, 77, 78	dvntaylp0 26756	. . . . . . . . . . . 12 ⊢ (𝜑 → (((ℂ D^𝑛 𝑇)‘𝑁)‘𝐵) = (((𝑆 D^𝑛 𝐹)‘𝑁)‘𝐵))
80	79	oveq2d 7467	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝐵) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝐵)) = ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝐵) − (((𝑆 D^𝑛 𝐹)‘𝑁)‘𝐵)))
81		cnex 11320	. . . . . . . . . . . . . . . 16 ⊢ ℂ ∈ V
82	81	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ℂ ∈ V)
83		elpm2r 8903	. . . . . . . . . . . . . . 15 ⊢ (((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆)) → 𝐹 ∈ (ℂ ↑_pm 𝑆))
84	82, 68, 69, 70, 83	syl22anc 852	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹 ∈ (ℂ ↑_pm 𝑆))
85		dvnf 26302	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ 𝑁 ∈ ℕ₀) → ((𝑆 D^𝑛 𝐹)‘𝑁):dom ((𝑆 D^𝑛 𝐹)‘𝑁)⟶ℂ)
86	68, 84, 71, 85	syl3anc 1399	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘𝑁):dom ((𝑆 D^𝑛 𝐹)‘𝑁)⟶ℂ)
87	86, 77	ffvelcdmd 7117	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑆 D^𝑛 𝐹)‘𝑁)‘𝐵) ∈ ℂ)
88	87	subidd 11696	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝐵) − (((𝑆 D^𝑛 𝐹)‘𝑁)‘𝐵)) = 0)
89	67, 80, 88	3eqtrd 2802	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))‘𝐵) = 0)
90		funmpt 6606	. . . . . . . . . . 11 ⊢ Fun (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))
91		ovex 7484	. . . . . . . . . . . . 13 ⊢ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)) ∈ V
92	91, 64	dmmpti 6713	. . . . . . . . . . . 12 ⊢ dom (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦))) = 𝐴
93	60, 92	eleqtrrdi 2875	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ dom (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦))))
94		funbrfvb 6969	. . . . . . . . . . 11 ⊢ ((Fun (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦))) ∧ 𝐵 ∈ dom (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))) → (((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))‘𝐵) = 0 ↔ 𝐵(𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))0))
95	90, 93, 94	sylancr 599	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))‘𝐵) = 0 ↔ 𝐵(𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))0))
96	89, 95	mpbid 235	. . . . . . . . 9 ⊢ (𝜑 → 𝐵(𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))0)
97		nnm1nn0 12687	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ₀)
98	1, 97	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑁 − 1) ∈ ℕ₀)
99		dvnf 26302	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ (𝑁 − 1) ∈ ℕ₀) → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)):dom ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))⟶ℂ)
100	68, 84, 98, 99	syl3anc 1399	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)):dom ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))⟶ℂ)
101		dvnbss 26303	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ (𝑁 − 1) ∈ ℕ₀) → dom ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)) ⊆ dom 𝐹)
102	68, 84, 98, 101	syl3anc 1399	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)) ⊆ dom 𝐹)
103	69, 102	fssdmd 6758	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)) ⊆ 𝐴)
104		fzo0end 13933	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ (0..^𝑁))
105		elfzofz 13850	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 − 1) ∈ (0..^𝑁) → (𝑁 − 1) ∈ (0...𝑁))
106	1, 104, 105	3syl 19	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑁 − 1) ∈ (0...𝑁))
107		dvn2bss 26305	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ (𝑁 − 1) ∈ (0...𝑁)) → dom ((𝑆 D^𝑛 𝐹)‘𝑁) ⊆ dom ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))
108	68, 84, 106, 107	syl3anc 1399	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom ((𝑆 D^𝑛 𝐹)‘𝑁) ⊆ dom ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))
109	76, 108	eqsstrrd 3948	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ⊆ dom ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))
110	103, 109	eqssd 3930	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)) = 𝐴)
111	110	feq2d 6723	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)):dom ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))⟶ℂ ↔ ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)):𝐴⟶ℂ))
112	100, 111	mpbid 235	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)):𝐴⟶ℂ)
113	112	ffvelcdmda 7116	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) ∈ ℂ)
114	76	feq2d 6723	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑆 D^𝑛 𝐹)‘𝑁):dom ((𝑆 D^𝑛 𝐹)‘𝑁)⟶ℂ ↔ ((𝑆 D^𝑛 𝐹)‘𝑁):𝐴⟶ℂ))
115	86, 114	mpbid 235	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘𝑁):𝐴⟶ℂ)
116	115	ffvelcdmda 7116	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) ∈ ℂ)
117	1	nncnd 12391	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ ℂ)
118		1cnd 11341	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 ∈ ℂ)
119	117, 118	npcand 11712	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
120	119	fveq2d 6920	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘((𝑁 − 1) + 1)) = ((𝑆 D^𝑛 𝐹)‘𝑁))
121		recnprss 26279	. . . . . . . . . . . . . . 15 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
122	68, 121	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
123		dvnp1 26300	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ (𝑁 − 1) ∈ ℕ₀) → ((𝑆 D^𝑛 𝐹)‘((𝑁 − 1) + 1)) = (𝑆 D ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))))
124	122, 84, 98, 123	syl3anc 1399	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘((𝑁 − 1) + 1)) = (𝑆 D ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))))
125	120, 124	eqtr3d 2800	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘𝑁) = (𝑆 D ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))))
126	115	feqmptd 6984	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘𝑁) = (𝑦 ∈ 𝐴 ↦ (((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦)))
127	112	feqmptd 6984	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)) = (𝑦 ∈ 𝐴 ↦ (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦)))
128	127	oveq2d 7467	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆 D ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))) = (𝑆 D (𝑦 ∈ 𝐴 ↦ (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦))))
129	125, 126, 128	3eqtr3rd 2807	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝐴 ↦ (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦))) = (𝑦 ∈ 𝐴 ↦ (((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦)))
130	70, 122	sstrd 3923	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ⊆ ℂ)
131	130	sselda 3913	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℂ)
132		1nn0 12662	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℕ₀
133	132	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 ∈ ℕ₀)
134		elpm2r 8903	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)):𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆)) → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)) ∈ (ℂ ↑_pm 𝑆))
135	82, 68, 112, 70, 134	syl22anc 852	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)) ∈ (ℂ ↑_pm 𝑆))
136		dvn1 26301	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ⊆ ℂ ∧ ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)) ∈ (ℂ ↑_pm 𝑆)) → ((𝑆 D^𝑛 ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))‘1) = (𝑆 D ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))))
137	122, 135, 136	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑆 D^𝑛 ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))‘1) = (𝑆 D ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))))
138	124, 120	eqtr3d 2800	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑆 D ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))) = ((𝑆 D^𝑛 𝐹)‘𝑁))
139	137, 138	eqtrd 2798	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑆 D^𝑛 ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))‘1) = ((𝑆 D^𝑛 𝐹)‘𝑁))
140	139	dmeqd 5899	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom ((𝑆 D^𝑛 ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))‘1) = dom ((𝑆 D^𝑛 𝐹)‘𝑁))
141	77, 140	eleqtrrd 2867	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D^𝑛 ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))‘1))
142		eqid 2763	. . . . . . . . . . . . . . 15 ⊢ (1(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))𝐵) = (1(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))𝐵)
143	68, 112, 70, 133, 141, 142	taylpf 26750	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))𝐵):ℂ⟶ℂ)
144	118, 117	pncan3d 11711	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (1 + (𝑁 − 1)) = 𝑁)
145	144	oveq1d 7466	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵) = (𝑁(𝑆 Tayl 𝐹)𝐵))
146	78, 145	eqtr4id 2817	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑇 = ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵))
147	146	oveq2d 7467	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (ℂ D^𝑛 𝑇) = (ℂ D^𝑛 ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵)))
148	147	fveq1d 6918	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘(𝑁 − 1)) = ((ℂ D^𝑛 ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵))‘(𝑁 − 1)))
149	144	fveq2d 6920	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘(1 + (𝑁 − 1))) = ((𝑆 D^𝑛 𝐹)‘𝑁))
150	149	dmeqd 5899	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → dom ((𝑆 D^𝑛 𝐹)‘(1 + (𝑁 − 1))) = dom ((𝑆 D^𝑛 𝐹)‘𝑁))
151	77, 150	eleqtrrd 2867	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D^𝑛 𝐹)‘(1 + (𝑁 − 1))))
152	68, 69, 70, 98, 133, 151	dvntaylp 26755	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((ℂ D^𝑛 ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵))‘(𝑁 − 1)) = (1(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))𝐵))
153	148, 152	eqtrd 2798	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘(𝑁 − 1)) = (1(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))𝐵))
154	153	feq1d 6721	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((ℂ D^𝑛 𝑇)‘(𝑁 − 1)):ℂ⟶ℂ ↔ (1(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))𝐵):ℂ⟶ℂ))
155	143, 154	mpbird 260	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘(𝑁 − 1)):ℂ⟶ℂ)
156	155	ffvelcdmda 7116	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦) ∈ ℂ)
157	131, 156	syldan 603	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦) ∈ ℂ)
158		0nn0 12661	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℕ₀
159	158	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 0 ∈ ℕ₀)
160		elpm2r 8903	. . . . . . . . . . . . . . . . . . 19 ⊢ (((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (((𝑆 D^𝑛 𝐹)‘𝑁):𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆)) → ((𝑆 D^𝑛 𝐹)‘𝑁) ∈ (ℂ ↑_pm 𝑆))
161	82, 68, 115, 70, 160	syl22anc 852	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘𝑁) ∈ (ℂ ↑_pm 𝑆))
162		dvn0 26299	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑆 ⊆ ℂ ∧ ((𝑆 D^𝑛 𝐹)‘𝑁) ∈ (ℂ ↑_pm 𝑆)) → ((𝑆 D^𝑛 ((𝑆 D^𝑛 𝐹)‘𝑁))‘0) = ((𝑆 D^𝑛 𝐹)‘𝑁))
163	122, 161, 162	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑆 D^𝑛 ((𝑆 D^𝑛 𝐹)‘𝑁))‘0) = ((𝑆 D^𝑛 𝐹)‘𝑁))
164	163	dmeqd 5899	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom ((𝑆 D^𝑛 ((𝑆 D^𝑛 𝐹)‘𝑁))‘0) = dom ((𝑆 D^𝑛 𝐹)‘𝑁))
165	77, 164	eleqtrrd 2867	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D^𝑛 ((𝑆 D^𝑛 𝐹)‘𝑁))‘0))
166		eqid 2763	. . . . . . . . . . . . . . 15 ⊢ (0(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘𝑁))𝐵) = (0(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘𝑁))𝐵)
167	68, 115, 70, 159, 165, 166	taylpf 26750	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘𝑁))𝐵):ℂ⟶ℂ)
168	117	addlidd 11550	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (0 + 𝑁) = 𝑁)
169	168	oveq1d 7466	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵) = (𝑁(𝑆 Tayl 𝐹)𝐵))
170	169, 78	eqtr4di 2816	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵) = 𝑇)
171	170	oveq2d 7467	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (ℂ D^𝑛 ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵)) = (ℂ D^𝑛 𝑇))
172	171	fveq1d 6918	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((ℂ D^𝑛 ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵))‘𝑁) = ((ℂ D^𝑛 𝑇)‘𝑁))
173	168	fveq2d 6920	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘(0 + 𝑁)) = ((𝑆 D^𝑛 𝐹)‘𝑁))
174	173	dmeqd 5899	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → dom ((𝑆 D^𝑛 𝐹)‘(0 + 𝑁)) = dom ((𝑆 D^𝑛 𝐹)‘𝑁))
175	77, 174	eleqtrrd 2867	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D^𝑛 𝐹)‘(0 + 𝑁)))
176	68, 69, 70, 71, 159, 175	dvntaylp 26755	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((ℂ D^𝑛 ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵))‘𝑁) = (0(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘𝑁))𝐵))
177	172, 176	eqtr3d 2800	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘𝑁) = (0(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘𝑁))𝐵))
178	177	feq1d 6721	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((ℂ D^𝑛 𝑇)‘𝑁):ℂ⟶ℂ ↔ (0(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘𝑁))𝐵):ℂ⟶ℂ))
179	167, 178	mpbird 260	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘𝑁):ℂ⟶ℂ)
180	179	ffvelcdmda 7116	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦) ∈ ℂ)
181	131, 180	syldan 603	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦) ∈ ℂ)
182	122	sselda 3913	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ ℂ)
183	182, 156	syldan 603	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦) ∈ ℂ)
184	182, 180	syldan 603	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦) ∈ ℂ)
185		eqid 2763	. . . . . . . . . . . . 13 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
186	185	cnfldtopon 25156	. . . . . . . . . . . . . 14 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
187		toponmax 23299	. . . . . . . . . . . . . 14 ⊢ ((TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ) → ℂ ∈ (TopOpen‘ℂ_fld))
188	186, 187	mp1i 14	. . . . . . . . . . . . 13 ⊢ (𝜑 → ℂ ∈ (TopOpen‘ℂ_fld))
189		dfss2 4097	. . . . . . . . . . . . . 14 ⊢ (𝑆 ⊆ ℂ ↔ (𝑆 ∩ ℂ) = 𝑆)
190	122, 189	sylib 221	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆 ∩ ℂ) = 𝑆)
191		ssid 3935	. . . . . . . . . . . . . . . . 17 ⊢ ℂ ⊆ ℂ
192	191	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ℂ ⊆ ℂ)
193		mapsspm 8942	. . . . . . . . . . . . . . . . 17 ⊢ (ℂ ↑_m ℂ) ⊆ (ℂ ↑_pm ℂ)
194	68, 69, 70, 71, 77, 78	taylpf 26750	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑇:ℂ⟶ℂ)
195	81, 81	elmap 8937	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑇 ∈ (ℂ ↑_m ℂ) ↔ 𝑇:ℂ⟶ℂ)
196	194, 195	sylibr 237	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑇 ∈ (ℂ ↑_m ℂ))
197	193, 196	sselid 3911	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑇 ∈ (ℂ ↑_pm ℂ))
198		dvnp1 26300	. . . . . . . . . . . . . . . 16 ⊢ ((ℂ ⊆ ℂ ∧ 𝑇 ∈ (ℂ ↑_pm ℂ) ∧ (𝑁 − 1) ∈ ℕ₀) → ((ℂ D^𝑛 𝑇)‘((𝑁 − 1) + 1)) = (ℂ D ((ℂ D^𝑛 𝑇)‘(𝑁 − 1))))
199	192, 197, 98, 198	syl3anc 1399	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘((𝑁 − 1) + 1)) = (ℂ D ((ℂ D^𝑛 𝑇)‘(𝑁 − 1))))
200	119	fveq2d 6920	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘((𝑁 − 1) + 1)) = ((ℂ D^𝑛 𝑇)‘𝑁))
201	199, 200	eqtr3d 2800	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℂ D ((ℂ D^𝑛 𝑇)‘(𝑁 − 1))) = ((ℂ D^𝑛 𝑇)‘𝑁))
202	155	feqmptd 6984	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘(𝑁 − 1)) = (𝑦 ∈ ℂ ↦ (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))
203	202	oveq2d 7467	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℂ D ((ℂ D^𝑛 𝑇)‘(𝑁 − 1))) = (ℂ D (𝑦 ∈ ℂ ↦ (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦))))
204	179	feqmptd 6984	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘𝑁) = (𝑦 ∈ ℂ ↦ (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))
205	201, 203, 204	3eqtr3d 2806	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦))) = (𝑦 ∈ ℂ ↦ (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))
206	185, 68, 188, 190, 156, 180, 205	dvmptres3 26331	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝑆 ↦ (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦))) = (𝑦 ∈ 𝑆 ↦ (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))
207		eqid 2763	. . . . . . . . . . . 12 ⊢ ((TopOpen‘ℂ_fld) ↾_t 𝑆) = ((TopOpen‘ℂ_fld) ↾_t 𝑆)
208		resttopon 23534	. . . . . . . . . . . . . . . 16 ⊢ (((TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ) ∧ 𝑆 ⊆ ℂ) → ((TopOpen‘ℂ_fld) ↾_t 𝑆) ∈ (TopOn‘𝑆))
209	186, 122, 208	sylancr 599	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((TopOpen‘ℂ_fld) ↾_t 𝑆) ∈ (TopOn‘𝑆))
210		topontop 23286	. . . . . . . . . . . . . . 15 ⊢ (((TopOpen‘ℂ_fld) ↾_t 𝑆) ∈ (TopOn‘𝑆) → ((TopOpen‘ℂ_fld) ↾_t 𝑆) ∈ Top)
211	209, 210	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((TopOpen‘ℂ_fld) ↾_t 𝑆) ∈ Top)
212		toponuni 23287	. . . . . . . . . . . . . . . 16 ⊢ (((TopOpen‘ℂ_fld) ↾_t 𝑆) ∈ (TopOn‘𝑆) → 𝑆 = ∪ ((TopOpen‘ℂ_fld) ↾_t 𝑆))
213	209, 212	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑆 = ∪ ((TopOpen‘ℂ_fld) ↾_t 𝑆))
214	70, 213	sseqtrd 3949	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ⊆ ∪ ((TopOpen‘ℂ_fld) ↾_t 𝑆))
215		eqid 2763	. . . . . . . . . . . . . . 15 ⊢ ∪ ((TopOpen‘ℂ_fld) ↾_t 𝑆) = ∪ ((TopOpen‘ℂ_fld) ↾_t 𝑆)
216	215	ntrss2 23430	. . . . . . . . . . . . . 14 ⊢ ((((TopOpen‘ℂ_fld) ↾_t 𝑆) ∈ Top ∧ 𝐴 ⊆ ∪ ((TopOpen‘ℂ_fld) ↾_t 𝑆)) → ((int‘((TopOpen‘ℂ_fld) ↾_t 𝑆))‘𝐴) ⊆ 𝐴)
217	211, 214, 216	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((int‘((TopOpen‘ℂ_fld) ↾_t 𝑆))‘𝐴) ⊆ 𝐴)
218	138	dmeqd 5899	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom (𝑆 D ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))) = dom ((𝑆 D^𝑛 𝐹)‘𝑁))
219	218, 76	eqtrd 2798	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom (𝑆 D ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))) = 𝐴)
220	122, 112, 70, 207, 185	dvbssntr 26275	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom (𝑆 D ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))) ⊆ ((int‘((TopOpen‘ℂ_fld) ↾_t 𝑆))‘𝐴))
221	219, 220	eqsstrrd 3948	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ⊆ ((int‘((TopOpen‘ℂ_fld) ↾_t 𝑆))‘𝐴))
222	217, 221	eqssd 3930	. . . . . . . . . . . 12 ⊢ (𝜑 → ((int‘((TopOpen‘ℂ_fld) ↾_t 𝑆))‘𝐴) = 𝐴)
223	68, 183, 184, 206, 70, 207, 185, 222	dvmptres2 26337	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝐴 ↦ (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦))) = (𝑦 ∈ 𝐴 ↦ (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))
224	68, 113, 116, 129, 157, 181, 223	dvmptsub 26342	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))) = (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦))))
225	224	breqd 5119	. . . . . . . . 9 ⊢ (𝜑 → (𝐵(𝑆 D (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦))))0 ↔ 𝐵(𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))0))
226	96, 225	mpbird 260	. . . . . . . 8 ⊢ (𝜑 → 𝐵(𝑆 D (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦))))0)
227		eqid 2763	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵)))
228	113, 157	subcld 11708	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)) ∈ ℂ)
229	228	fmpttd 7147	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦))):𝐴⟶ℂ)
230	207, 185, 227, 122, 229, 70	eldv 26273	. . . . . . . 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 235	. . . . . . 7 ⊢ (𝜑 → (𝐵 ∈ ((int‘((TopOpen‘ℂ_fld) ↾_t 𝑆))‘𝐴) ∧ 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵))) lim_ℂ 𝐵)))
232	231	simprd 501	. . . . . 6 ⊢ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵))) lim_ℂ 𝐵))
233		eldifi 4070	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐴 ∖ {𝐵}) → 𝑥 ∈ 𝐴)
234		fveq2 6916	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑥 → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) = (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥))
235		fveq2 6916	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑥 → (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦) = (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥))
236	234, 235	oveq12d 7469	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑥 → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)) = ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)))
237		eqid 2763	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦))) = (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))
238		ovex 7484	. . . . . . . . . . . . 13 ⊢ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) ∈ V
239	236, 237, 238	fvmpt 7024	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) = ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)))
240		fveq2 6916	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝐵 → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) = (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝐵))
241		fveq2 6916	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝐵 → (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦) = (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝐵))
242	240, 241	oveq12d 7469	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝐵 → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)) = ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝐵)))
243		ovex 7484	. . . . . . . . . . . . . . 15 ⊢ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝐵)) ∈ V
244	242, 237, 243	fvmpt 7024	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵) = ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝐵)))
245	60, 244	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵) = ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝐵)))
246	68, 69, 70, 106, 77, 78	dvntaylp0 26756	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝐵) = (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝐵))
247	246	oveq2d 7467	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝐵)) = ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝐵)))
248	112, 60	ffvelcdmd 7117	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝐵) ∈ ℂ)
249	248	subidd 11696	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝐵)) = 0)
250	245, 247, 249	3eqtrd 2802	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵) = 0)
251	239, 250	oveqan12rd 7471	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) = (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) − 0))
252	112	ffvelcdmda 7116	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) ∈ ℂ)
253	130	sselda 3913	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℂ)
254	155	ffvelcdmda 7116	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥) ∈ ℂ)
255	253, 254	syldan 603	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥) ∈ ℂ)
256	252, 255	subcld 11708	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) ∈ ℂ)
257	256	subid1d 11697	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) − 0) = ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)))
258	251, 257	eqtr2d 2799	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) = (((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)))
259	233, 258	sylan2 605	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) = (((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)))
260	130	ssdifssd 4086	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 ∖ {𝐵}) ⊆ ℂ)
261	260	sselda 3913	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ ℂ)
262	130, 60	sseldd 3914	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ ℂ)
263	262	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝐵 ∈ ℂ)
264	261, 263	subcld 11708	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑥 − 𝐵) ∈ ℂ)
265	264	exp1d 14324	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑥 − 𝐵)↑1) = (𝑥 − 𝐵))
266	259, 265	oveq12d 7469	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1)) = ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵)))
267	266	mpteq2dva 5204	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵))))
268	267	oveq1d 7466	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))) lim_ℂ 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵))) lim_ℂ 𝐵))
269	232, 268	eleqtrrd 2867	. . . . 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 462	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1..^𝑁)) → (0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) lim_ℂ 𝐵) → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))) lim_ℂ 𝐵)))
273	272	expcom 419	. . . . 5 ⊢ (𝑛 ∈ (1..^𝑁) → (𝜑 → (0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) lim_ℂ 𝐵) → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))) lim_ℂ 𝐵))))
274	273	a2d 30	. . . 4 ⊢ (𝑛 ∈ (1..^𝑁) → ((𝜑 → 0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) lim_ℂ 𝐵)) → (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))) lim_ℂ 𝐵))))
275	15, 35, 47, 59, 270, 274	fzind2 13963	. . 3 ⊢ (𝑁 ∈ (1...𝑁) → (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) lim_ℂ 𝐵)))
276	3, 275	mpcom 39	. 2 ⊢ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) lim_ℂ 𝐵))
277	117	subidd 11696	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 − 𝑁) = 0)
278	277	fveq2d 6920	. . . . . . . . 9 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁)) = ((𝑆 D^𝑛 𝐹)‘0))
279		dvn0 26299	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆)) → ((𝑆 D^𝑛 𝐹)‘0) = 𝐹)
280	122, 84, 279	syl2anc 596	. . . . . . . . 9 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘0) = 𝐹)
281	278, 280	eqtrd 2798	. . . . . . . 8 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁)) = 𝐹)
282	281	fveq1d 6918	. . . . . . 7 ⊢ (𝜑 → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) = (𝐹‘𝑥))
283	277	fveq2d 6920	. . . . . . . . 9 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁)) = ((ℂ D^𝑛 𝑇)‘0))
284		dvn0 26299	. . . . . . . . . 10 ⊢ ((ℂ ⊆ ℂ ∧ 𝑇 ∈ (ℂ ↑_pm ℂ)) → ((ℂ D^𝑛 𝑇)‘0) = 𝑇)
285	191, 197, 284	sylancr 599	. . . . . . . . 9 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘0) = 𝑇)
286	283, 285	eqtrd 2798	. . . . . . . 8 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁)) = 𝑇)
287	286	fveq1d 6918	. . . . . . 7 ⊢ (𝜑 → (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥) = (𝑇‘𝑥))
288	282, 287	oveq12d 7469	. . . . . 6 ⊢ (𝜑 → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) = ((𝐹‘𝑥) − (𝑇‘𝑥)))
289	288	oveq1d 7466	. . . . 5 ⊢ (𝜑 → (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁)) = (((𝐹‘𝑥) − (𝑇‘𝑥)) / ((𝑥 − 𝐵)↑𝑁)))
290	289	mpteq2dv 5205	. . . 4 ⊢ (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝐹‘𝑥) − (𝑇‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))))
291		taylthlem1.r	. . . 4 ⊢ 𝑅 = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝐹‘𝑥) − (𝑇‘𝑥)) / ((𝑥 − 𝐵)↑𝑁)))
292	290, 291	eqtr4di 2816	. . 3 ⊢ (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) = 𝑅)
293	292	oveq1d 7466	. 2 ⊢ (𝜑 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) lim_ℂ 𝐵) = (𝑅 lim_ℂ 𝐵))
294	276, 293	eleqtrd 2866	1 ⊢ (𝜑 → 0 ∈ (𝑅 lim_ℂ 𝐵))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2147 Vcvv 3454 ⊆ wss 3900 ∖ cdif 4048 ∩ cin 4092 {csn 4588 {cpr 4590 ∪ cuni 4872 class class class wbr 5108 ↦ cmpt 5192 dom cdm 5658 Fun wfun 6560 ⟶wf 6562 ‘cfv 6566 (class class class)co 7451 ↑_m cmap 8885 ↑_pm cpm 8886 ℂcc 11237 ℝcr 11238 0cc0 11239 1c1 11240 + caddc 11242 − cmin 11580 / cdiv 12013 ℕcn 12375 ℕ₀cn0 12646 ℤ_≥cuz 13005 ...cfz 13679 ..^cfzo 13828 ↑cexp 14244 ↾_t crest 17641 TopOpenctopn 17642 ℂ_fldccnfld 21729 Topctop 23266 TopOnctopon 23283 intcnt 23390 lim_ℂ climc 26237 D cdv 26238 D^𝑛 cdvn 26239 Tayl ctayl 26737

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 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5238 ax-sep 5255 ax-nul 5266 ax-pow 5334 ax-pr 5398 ax-un 7783 ax-inf2 9679 ax-cnex 11295 ax-resscn 11296 ax-1cn 11297 ax-icn 11298 ax-addcl 11299 ax-addrcl 11300 ax-mulcl 11301 ax-mulrcl 11302 ax-mulcom 11303 ax-addass 11304 ax-mulass 11305 ax-distr 11306 ax-i2m1 11307 ax-1ne0 11308 ax-1rid 11309 ax-rnegex 11310 ax-rrecex 11311 ax-cnre 11312 ax-pre-lttri 11313 ax-pre-lttrn 11314 ax-pre-ltadd 11315 ax-pre-mulgt0 11316 ax-pre-sup 11317 ax-addf 11318

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 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4841 df-uni 4873 df-int 4913 df-iun 4958 df-iin 4959 df-br 5109 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-se 5612 df-we 5613 df-xp 5664 df-rel 5665 df-cnv 5666 df-co 5667 df-dm 5668 df-rn 5669 df-res 5670 df-ima 5671 df-pred 6330 df-ord 6391 df-on 6392 df-lim 6393 df-suc 6394 df-iota 6520 df-fun 6568 df-fn 6569 df-f 6570 df-f1 6571 df-fo 6572 df-f1o 6573 df-fv 6574 df-isom 6575 df-riota 7408 df-ov 7454 df-oprab 7455 df-mpo 7456 df-of 7725 df-om 7912 df-1st 8035 df-2nd 8036 df-supp 8215 df-frecs 8337 df-wrecs 8368 df-recs 8417 df-rdg 8456 df-1o 8514 df-2o 8515 df-er 8755 df-map 8887 df-pm 8888 df-ixp 8964 df-en 9012 df-dom 9013 df-sdom 9014 df-fin 9015 df-fsupp 9392 df-fi 9440 df-sup 9471 df-inf 9472 df-oi 9541 df-card 10057 df-pnf 11384 df-mnf 11385 df-xr 11386 df-ltxr 11387 df-le 11388 df-sub 11582 df-neg 11583 df-div 12014 df-nn 12376 df-2 12445 df-3 12446 df-4 12447 df-5 12448 df-6 12449 df-7 12450 df-8 12451 df-9 12452 df-n0 12647 df-xnn0 12720 df-z 12734 df-dec 12855 df-uz 13006 df-q 13116 df-rp 13161 df-xneg 13281 df-xadd 13282 df-xmul 13283 df-icc 13523 df-fz 13680 df-fzo 13829 df-seq 14185 df-exp 14245 df-fac 14459 df-hash 14516 df-cj 15309 df-re 15310 df-im 15311 df-sqrt 15445 df-abs 15446 df-clim 15699 df-sum 15898 df-struct 17369 df-sets 17386 df-slot 17404 df-ndx 17416 df-base 17432 df-ress 17453 df-plusg 17486 df-mulr 17487 df-starv 17488 df-sca 17489 df-vsca 17490 df-ip 17491 df-tset 17492 df-ple 17493 df-ds 17495 df-unif 17496 df-hom 17497 df-cco 17498 df-euf 17499 df-rest 17643 df-topn 17644 df-0g 17662 df-gsum 17663 df-topgen 17664 df-pt 17665 df-prds 17668 df-xrs 17724 df-qtop 17729 df-imas 17730 df-xps 17732 df-mre 17806 df-mrc 17807 df-acs 17809 df-mgm 18866 df-sgrp 18958 df-mnd 18974 df-submnd 19029 df-grp 19197 df-minusg 19198 df-mulg 19328 df-cntz 19582 df-cmn 20047 df-abl 20048 df-mgp 20412 df-ur 20459 df-ring 20512 df-cring 20513 df-psmet 21721 df-xmet 21722 df-met 21723 df-bl 21724 df-mopn 21725 df-fbas 21726 df-fg 21727 df-cnfld 21730 df-top 23267 df-topon 23284 df-topsp 23306 df-bases 23319 df-cld 23392 df-ntr 23393 df-cls 23394 df-nei 23471 df-lp 23509 df-perf 23510 df-cn 23600 df-cnp 23601 df-haus 23688 df-tx 23936 df-hmeo 24129 df-fil 24220 df-fm 24312 df-flim 24313 df-flf 24314 df-tsms 24501 df-xms 24694 df-ms 24695 df-tms 24696 df-cncf 25254 df-limc 26241 df-dv 26242 df-dvn 26243 df-tayl 26739

This theorem is used by: taylth 26759

W3C validator