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 26609

Description: Lemma for taylth 26611. 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 26611 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 13609	. . . 4 ⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈ (1...𝑁))
3	1, 2	sylib 221	. . 3 ⊢ (𝜑 → 𝑁 ∈ (1...𝑁))
4		oveq2 7421	. . . . . . . . . . . 12 ⊢ (𝑚 = 1 → (𝑁 − 𝑚) = (𝑁 − 1))
5	4	fveq2d 6882	. . . . . . . . . . 11 ⊢ (𝑚 = 1 → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚)) = ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))
6	5	fveq1d 6880	. . . . . . . . . 10 ⊢ (𝑚 = 1 → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) = (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥))
7	4	fveq2d 6882	. . . . . . . . . . 11 ⊢ (𝑚 = 1 → ((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚)) = ((ℂ D^𝑛 𝑇)‘(𝑁 − 1)))
8	7	fveq1d 6880	. . . . . . . . . 10 ⊢ (𝑚 = 1 → (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥) = (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥))
9	6, 8	oveq12d 7431	. . . . . . . . 9 ⊢ (𝑚 = 1 → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) = ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)))
10		oveq2 7421	. . . . . . . . 9 ⊢ (𝑚 = 1 → ((𝑥 − 𝐵)↑𝑚) = ((𝑥 − 𝐵)↑1))
11	9, 10	oveq12d 7431	. . . . . . . 8 ⊢ (𝑚 = 1 → (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚)) = (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1)))
12	11	mpteq2dv 5199	. . . . . . 7 ⊢ (𝑚 = 1 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))))
13	12	oveq1d 7428	. . . . . 6 ⊢ (𝑚 = 1 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) lim_ℂ 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))) lim_ℂ 𝐵))
14	13	eleq2d 2846	. . . . 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 7421	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑛 → (𝑁 − 𝑚) = (𝑁 − 𝑛))
17	16	fveq2d 6882	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚)) = ((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛)))
18	17	fveq1d 6880	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) = (((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥))
19	16	fveq2d 6882	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → ((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚)) = ((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛)))
20	19	fveq1d 6880	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥) = (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑥))
21	18, 20	oveq12d 7431	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) = ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑥)))
22		oveq2 7421	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → ((𝑥 − 𝐵)↑𝑚) = ((𝑥 − 𝐵)↑𝑛))
23	21, 22	oveq12d 7431	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚)) = (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑥)) / ((𝑥 − 𝐵)↑𝑛)))
24	23	mpteq2dv 5199	. . . . . . . 8 ⊢ (𝑚 = 𝑛 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑥)) / ((𝑥 − 𝐵)↑𝑛))))
25		fveq2 6878	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) = (((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦))
26		fveq2 6878	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑥) = (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑦))
27	25, 26	oveq12d 7431	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑥)) = ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑦)))
28		oveq1 7420	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑥 − 𝐵) = (𝑦 − 𝐵))
29	28	oveq1d 7428	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((𝑥 − 𝐵)↑𝑛) = ((𝑦 − 𝐵)↑𝑛))
30	27, 29	oveq12d 7431	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑥)) / ((𝑥 − 𝐵)↑𝑛)) = (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛)))
31	30	cbvmptv 5209	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑥)) / ((𝑥 − 𝐵)↑𝑛))) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛)))
32	24, 31	eqtrdi 2811	. . . . . . 7 ⊢ (𝑚 = 𝑛 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) = (𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))))
33	32	oveq1d 7428	. . . . . 6 ⊢ (𝑚 = 𝑛 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) lim_ℂ 𝐵) = ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) lim_ℂ 𝐵))
34	33	eleq2d 2846	. . . . 5 ⊢ (𝑚 = 𝑛 → (0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) lim_ℂ 𝐵) ↔ 0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) lim_ℂ 𝐵)))
35	34	imbi2d 343	. . . 4 ⊢ (𝑚 = 𝑛 → ((𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) lim_ℂ 𝐵)) ↔ (𝜑 → 0 ∈ ((𝑦 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑛))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑛))‘𝑦)) / ((𝑦 − 𝐵)↑𝑛))) lim_ℂ 𝐵))))
36		oveq2 7421	. . . . . . . . . . . 12 ⊢ (𝑚 = (𝑛 + 1) → (𝑁 − 𝑚) = (𝑁 − (𝑛 + 1)))
37	36	fveq2d 6882	. . . . . . . . . . 11 ⊢ (𝑚 = (𝑛 + 1) → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚)) = ((𝑆 D^𝑛 𝐹)‘(𝑁 − (𝑛 + 1))))
38	37	fveq1d 6880	. . . . . . . . . 10 ⊢ (𝑚 = (𝑛 + 1) → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) = (((𝑆 D^𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥))
39	36	fveq2d 6882	. . . . . . . . . . 11 ⊢ (𝑚 = (𝑛 + 1) → ((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚)) = ((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑛 + 1))))
40	39	fveq1d 6880	. . . . . . . . . 10 ⊢ (𝑚 = (𝑛 + 1) → (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥) = (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥))
41	38, 40	oveq12d 7431	. . . . . . . . 9 ⊢ (𝑚 = (𝑛 + 1) → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) = ((((𝑆 D^𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)))
42		oveq2 7421	. . . . . . . . 9 ⊢ (𝑚 = (𝑛 + 1) → ((𝑥 − 𝐵)↑𝑚) = ((𝑥 − 𝐵)↑(𝑛 + 1)))
43	41, 42	oveq12d 7431	. . . . . . . 8 ⊢ (𝑚 = (𝑛 + 1) → (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚)) = (((((𝑆 D^𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1))))
44	43	mpteq2dv 5199	. . . . . . 7 ⊢ (𝑚 = (𝑛 + 1) → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))))
45	44	oveq1d 7428	. . . . . 6 ⊢ (𝑚 = (𝑛 + 1) → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) lim_ℂ 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − (𝑛 + 1)))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − (𝑛 + 1)))‘𝑥)) / ((𝑥 − 𝐵)↑(𝑛 + 1)))) lim_ℂ 𝐵))
46	45	eleq2d 2846	. . . . 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 7421	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑁 → (𝑁 − 𝑚) = (𝑁 − 𝑁))
49	48	fveq2d 6882	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑁 → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚)) = ((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁)))
50	49	fveq1d 6880	. . . . . . . . . 10 ⊢ (𝑚 = 𝑁 → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) = (((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥))
51	48	fveq2d 6882	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑁 → ((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚)) = ((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁)))
52	51	fveq1d 6880	. . . . . . . . . 10 ⊢ (𝑚 = 𝑁 → (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥) = (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥))
53	50, 52	oveq12d 7431	. . . . . . . . 9 ⊢ (𝑚 = 𝑁 → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) = ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)))
54		oveq2 7421	. . . . . . . . 9 ⊢ (𝑚 = 𝑁 → ((𝑥 − 𝐵)↑𝑚) = ((𝑥 − 𝐵)↑𝑁))
55	53, 54	oveq12d 7431	. . . . . . . 8 ⊢ (𝑚 = 𝑁 → (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚)) = (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁)))
56	55	mpteq2dv 5199	. . . . . . 7 ⊢ (𝑚 = 𝑁 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))))
57	56	oveq1d 7428	. . . . . 6 ⊢ (𝑚 = 𝑁 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑚))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑚))‘𝑥)) / ((𝑥 − 𝐵)↑𝑚))) lim_ℂ 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) lim_ℂ 𝐵))
58	57	eleq2d 2846	. . . . 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 6878	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝐵 → (((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) = (((𝑆 D^𝑛 𝐹)‘𝑁)‘𝐵))
62		fveq2 6878	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝐵 → (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦) = (((ℂ D^𝑛 𝑇)‘𝑁)‘𝐵))
63	61, 62	oveq12d 7431	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝐵 → ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)) = ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝐵) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝐵)))
64		eqid 2760	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦))) = (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))
65		ovex 7446	. . . . . . . . . . . . 13 ⊢ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝐵) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝐵)) ∈ V
66	63, 64, 65	fvmpt 6986	. . . . . . . . . . . 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 12589	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
72		nn0uz 12925	. . . . . . . . . . . . . . 15 ⊢ ℕ₀ = (ℤ_≥‘0)
73	71, 72	eleqtrdi 2870	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘0))
74		eluzfz2b 13587	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ (ℤ_≥‘0) ↔ 𝑁 ∈ (0...𝑁))
75	73, 74	sylib 221	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ (0...𝑁))
76		taylthlem1.d	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom ((𝑆 D^𝑛 𝐹)‘𝑁) = 𝐴)
77	60, 76	eleqtrrd 2863	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D^𝑛 𝐹)‘𝑁))
78		taylthlem1.t	. . . . . . . . . . . . 13 ⊢ 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵)
79	68, 69, 70, 75, 77, 78	dvntaylp0 26608	. . . . . . . . . . . 12 ⊢ (𝜑 → (((ℂ D^𝑛 𝑇)‘𝑁)‘𝐵) = (((𝑆 D^𝑛 𝐹)‘𝑁)‘𝐵))
80	79	oveq2d 7429	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝐵) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝐵)) = ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝐵) − (((𝑆 D^𝑛 𝐹)‘𝑁)‘𝐵)))
81		cnex 11205	. . . . . . . . . . . . . . . 16 ⊢ ℂ ∈ V
82	81	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ℂ ∈ V)
83		elpm2r 8844	. . . . . . . . . . . . . . 15 ⊢ (((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆)) → 𝐹 ∈ (ℂ ↑_pm 𝑆))
84	82, 68, 69, 70, 83	syl22anc 852	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹 ∈ (ℂ ↑_pm 𝑆))
85		dvnf 26154	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ 𝑁 ∈ ℕ₀) → ((𝑆 D^𝑛 𝐹)‘𝑁):dom ((𝑆 D^𝑛 𝐹)‘𝑁)⟶ℂ)
86	68, 84, 71, 85	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘𝑁):dom ((𝑆 D^𝑛 𝐹)‘𝑁)⟶ℂ)
87	86, 77	ffvelcdmd 7078	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑆 D^𝑛 𝐹)‘𝑁)‘𝐵) ∈ ℂ)
88	87	subidd 11581	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝐵) − (((𝑆 D^𝑛 𝐹)‘𝑁)‘𝐵)) = 0)
89	67, 80, 88	3eqtrd 2799	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))‘𝐵) = 0)
90		funmpt 6571	. . . . . . . . . . 11 ⊢ Fun (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))
91		ovex 7446	. . . . . . . . . . . . 13 ⊢ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)) ∈ V
92	91, 64	dmmpti 6676	. . . . . . . . . . . 12 ⊢ dom (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦))) = 𝐴
93	60, 92	eleqtrrdi 2871	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ dom (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦))))
94		funbrfvb 6931	. . . . . . . . . . 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 12569	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ₀)
98	1, 97	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑁 − 1) ∈ ℕ₀)
99		dvnf 26154	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ (𝑁 − 1) ∈ ℕ₀) → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)):dom ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))⟶ℂ)
100	68, 84, 98, 99	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)):dom ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))⟶ℂ)
101		dvnbss 26155	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ (𝑁 − 1) ∈ ℕ₀) → dom ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)) ⊆ dom 𝐹)
102	68, 84, 98, 101	syl3anc 1398	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)) ⊆ dom 𝐹)
103	69, 102	fssdmd 6721	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)) ⊆ 𝐴)
104		fzo0end 13814	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ (0..^𝑁))
105		elfzofz 13731	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 − 1) ∈ (0..^𝑁) → (𝑁 − 1) ∈ (0...𝑁))
106	1, 104, 105	3syl 19	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑁 − 1) ∈ (0...𝑁))
107		dvn2bss 26157	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ (𝑁 − 1) ∈ (0...𝑁)) → dom ((𝑆 D^𝑛 𝐹)‘𝑁) ⊆ dom ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))
108	68, 84, 106, 107	syl3anc 1398	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom ((𝑆 D^𝑛 𝐹)‘𝑁) ⊆ dom ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))
109	76, 108	eqsstrrd 3966	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ⊆ dom ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))
110	103, 109	eqssd 3948	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)) = 𝐴)
111	110	feq2d 6686	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)):dom ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))⟶ℂ ↔ ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)):𝐴⟶ℂ))
112	100, 111	mpbid 235	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)):𝐴⟶ℂ)
113	112	ffvelcdmda 7077	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) ∈ ℂ)
114	76	feq2d 6686	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑆 D^𝑛 𝐹)‘𝑁):dom ((𝑆 D^𝑛 𝐹)‘𝑁)⟶ℂ ↔ ((𝑆 D^𝑛 𝐹)‘𝑁):𝐴⟶ℂ))
115	86, 114	mpbid 235	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘𝑁):𝐴⟶ℂ)
116	115	ffvelcdmda 7077	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) ∈ ℂ)
117	1	nncnd 12273	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ ℂ)
118		1cnd 11226	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 ∈ ℂ)
119	117, 118	npcand 11597	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
120	119	fveq2d 6882	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘((𝑁 − 1) + 1)) = ((𝑆 D^𝑛 𝐹)‘𝑁))
121		recnprss 26131	. . . . . . . . . . . . . . 15 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
122	68, 121	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
123		dvnp1 26152	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ (𝑁 − 1) ∈ ℕ₀) → ((𝑆 D^𝑛 𝐹)‘((𝑁 − 1) + 1)) = (𝑆 D ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))))
124	122, 84, 98, 123	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘((𝑁 − 1) + 1)) = (𝑆 D ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))))
125	120, 124	eqtr3d 2797	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘𝑁) = (𝑆 D ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))))
126	115	feqmptd 6946	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘𝑁) = (𝑦 ∈ 𝐴 ↦ (((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦)))
127	112	feqmptd 6946	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)) = (𝑦 ∈ 𝐴 ↦ (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦)))
128	127	oveq2d 7429	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆 D ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))) = (𝑆 D (𝑦 ∈ 𝐴 ↦ (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦))))
129	125, 126, 128	3eqtr3rd 2804	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝐴 ↦ (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦))) = (𝑦 ∈ 𝐴 ↦ (((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦)))
130	70, 122	sstrd 3941	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ⊆ ℂ)
131	130	sselda 3931	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℂ)
132		1nn0 12544	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℕ₀
133	132	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 ∈ ℕ₀)
134		elpm2r 8844	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)):𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆)) → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)) ∈ (ℂ ↑_pm 𝑆))
135	82, 68, 112, 70, 134	syl22anc 852	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)) ∈ (ℂ ↑_pm 𝑆))
136		dvn1 26153	. . . . . . . . . . . . . . . . . . 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 2797	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑆 D ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))) = ((𝑆 D^𝑛 𝐹)‘𝑁))
139	137, 138	eqtrd 2795	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑆 D^𝑛 ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))‘1) = ((𝑆 D^𝑛 𝐹)‘𝑁))
140	139	dmeqd 5889	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom ((𝑆 D^𝑛 ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))‘1) = dom ((𝑆 D^𝑛 𝐹)‘𝑁))
141	77, 140	eleqtrrd 2863	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D^𝑛 ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))‘1))
142		eqid 2760	. . . . . . . . . . . . . . 15 ⊢ (1(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))𝐵) = (1(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))𝐵)
143	68, 112, 70, 133, 141, 142	taylpf 26602	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))𝐵):ℂ⟶ℂ)
144	118, 117	pncan3d 11596	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (1 + (𝑁 − 1)) = 𝑁)
145	144	oveq1d 7428	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵) = (𝑁(𝑆 Tayl 𝐹)𝐵))
146	78, 145	eqtr4id 2814	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑇 = ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵))
147	146	oveq2d 7429	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (ℂ D^𝑛 𝑇) = (ℂ D^𝑛 ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵)))
148	147	fveq1d 6880	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘(𝑁 − 1)) = ((ℂ D^𝑛 ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵))‘(𝑁 − 1)))
149	144	fveq2d 6882	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘(1 + (𝑁 − 1))) = ((𝑆 D^𝑛 𝐹)‘𝑁))
150	149	dmeqd 5889	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → dom ((𝑆 D^𝑛 𝐹)‘(1 + (𝑁 − 1))) = dom ((𝑆 D^𝑛 𝐹)‘𝑁))
151	77, 150	eleqtrrd 2863	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D^𝑛 𝐹)‘(1 + (𝑁 − 1))))
152	68, 69, 70, 98, 133, 151	dvntaylp 26607	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((ℂ D^𝑛 ((1 + (𝑁 − 1))(𝑆 Tayl 𝐹)𝐵))‘(𝑁 − 1)) = (1(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))𝐵))
153	148, 152	eqtrd 2795	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘(𝑁 − 1)) = (1(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))𝐵))
154	153	feq1d 6684	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((ℂ D^𝑛 𝑇)‘(𝑁 − 1)):ℂ⟶ℂ ↔ (1(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1)))𝐵):ℂ⟶ℂ))
155	143, 154	mpbird 260	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘(𝑁 − 1)):ℂ⟶ℂ)
156	155	ffvelcdmda 7077	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦) ∈ ℂ)
157	131, 156	syldan 603	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦) ∈ ℂ)
158		0nn0 12543	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℕ₀
159	158	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 0 ∈ ℕ₀)
160		elpm2r 8844	. . . . . . . . . . . . . . . . . . 19 ⊢ (((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (((𝑆 D^𝑛 𝐹)‘𝑁):𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆)) → ((𝑆 D^𝑛 𝐹)‘𝑁) ∈ (ℂ ↑_pm 𝑆))
161	82, 68, 115, 70, 160	syl22anc 852	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘𝑁) ∈ (ℂ ↑_pm 𝑆))
162		dvn0 26151	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑆 ⊆ ℂ ∧ ((𝑆 D^𝑛 𝐹)‘𝑁) ∈ (ℂ ↑_pm 𝑆)) → ((𝑆 D^𝑛 ((𝑆 D^𝑛 𝐹)‘𝑁))‘0) = ((𝑆 D^𝑛 𝐹)‘𝑁))
163	122, 161, 162	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑆 D^𝑛 ((𝑆 D^𝑛 𝐹)‘𝑁))‘0) = ((𝑆 D^𝑛 𝐹)‘𝑁))
164	163	dmeqd 5889	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom ((𝑆 D^𝑛 ((𝑆 D^𝑛 𝐹)‘𝑁))‘0) = dom ((𝑆 D^𝑛 𝐹)‘𝑁))
165	77, 164	eleqtrrd 2863	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D^𝑛 ((𝑆 D^𝑛 𝐹)‘𝑁))‘0))
166		eqid 2760	. . . . . . . . . . . . . . 15 ⊢ (0(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘𝑁))𝐵) = (0(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘𝑁))𝐵)
167	68, 115, 70, 159, 165, 166	taylpf 26602	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘𝑁))𝐵):ℂ⟶ℂ)
168	117	addlidd 11435	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (0 + 𝑁) = 𝑁)
169	168	oveq1d 7428	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵) = (𝑁(𝑆 Tayl 𝐹)𝐵))
170	169, 78	eqtr4di 2813	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵) = 𝑇)
171	170	oveq2d 7429	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (ℂ D^𝑛 ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵)) = (ℂ D^𝑛 𝑇))
172	171	fveq1d 6880	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((ℂ D^𝑛 ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵))‘𝑁) = ((ℂ D^𝑛 𝑇)‘𝑁))
173	168	fveq2d 6882	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘(0 + 𝑁)) = ((𝑆 D^𝑛 𝐹)‘𝑁))
174	173	dmeqd 5889	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → dom ((𝑆 D^𝑛 𝐹)‘(0 + 𝑁)) = dom ((𝑆 D^𝑛 𝐹)‘𝑁))
175	77, 174	eleqtrrd 2863	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D^𝑛 𝐹)‘(0 + 𝑁)))
176	68, 69, 70, 71, 159, 175	dvntaylp 26607	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((ℂ D^𝑛 ((0 + 𝑁)(𝑆 Tayl 𝐹)𝐵))‘𝑁) = (0(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘𝑁))𝐵))
177	172, 176	eqtr3d 2797	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘𝑁) = (0(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘𝑁))𝐵))
178	177	feq1d 6684	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((ℂ D^𝑛 𝑇)‘𝑁):ℂ⟶ℂ ↔ (0(𝑆 Tayl ((𝑆 D^𝑛 𝐹)‘𝑁))𝐵):ℂ⟶ℂ))
179	167, 178	mpbird 260	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘𝑁):ℂ⟶ℂ)
180	179	ffvelcdmda 7077	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦) ∈ ℂ)
181	131, 180	syldan 603	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦) ∈ ℂ)
182	122	sselda 3931	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ ℂ)
183	182, 156	syldan 603	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦) ∈ ℂ)
184	182, 180	syldan 603	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦) ∈ ℂ)
185		eqid 2760	. . . . . . . . . . . . 13 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
186	185	cnfldtopon 25008	. . . . . . . . . . . . . 14 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
187		toponmax 23151	. . . . . . . . . . . . . 14 ⊢ ((TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ) → ℂ ∈ (TopOpen‘ℂ_fld))
188	186, 187	mp1i 14	. . . . . . . . . . . . 13 ⊢ (𝜑 → ℂ ∈ (TopOpen‘ℂ_fld))
189		dfss2 3917	. . . . . . . . . . . . . 14 ⊢ (𝑆 ⊆ ℂ ↔ (𝑆 ∩ ℂ) = 𝑆)
190	122, 189	sylib 221	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆 ∩ ℂ) = 𝑆)
191		ssid 3953	. . . . . . . . . . . . . . . . 17 ⊢ ℂ ⊆ ℂ
192	191	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ℂ ⊆ ℂ)
193		mapsspm 8883	. . . . . . . . . . . . . . . . 17 ⊢ (ℂ ↑_m ℂ) ⊆ (ℂ ↑_pm ℂ)
194	68, 69, 70, 71, 77, 78	taylpf 26602	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑇:ℂ⟶ℂ)
195	81, 81	elmap 8878	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑇 ∈ (ℂ ↑_m ℂ) ↔ 𝑇:ℂ⟶ℂ)
196	194, 195	sylibr 237	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑇 ∈ (ℂ ↑_m ℂ))
197	193, 196	sselid 3929	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑇 ∈ (ℂ ↑_pm ℂ))
198		dvnp1 26152	. . . . . . . . . . . . . . . 16 ⊢ ((ℂ ⊆ ℂ ∧ 𝑇 ∈ (ℂ ↑_pm ℂ) ∧ (𝑁 − 1) ∈ ℕ₀) → ((ℂ D^𝑛 𝑇)‘((𝑁 − 1) + 1)) = (ℂ D ((ℂ D^𝑛 𝑇)‘(𝑁 − 1))))
199	192, 197, 98, 198	syl3anc 1398	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘((𝑁 − 1) + 1)) = (ℂ D ((ℂ D^𝑛 𝑇)‘(𝑁 − 1))))
200	119	fveq2d 6882	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘((𝑁 − 1) + 1)) = ((ℂ D^𝑛 𝑇)‘𝑁))
201	199, 200	eqtr3d 2797	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℂ D ((ℂ D^𝑛 𝑇)‘(𝑁 − 1))) = ((ℂ D^𝑛 𝑇)‘𝑁))
202	155	feqmptd 6946	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘(𝑁 − 1)) = (𝑦 ∈ ℂ ↦ (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))
203	202	oveq2d 7429	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℂ D ((ℂ D^𝑛 𝑇)‘(𝑁 − 1))) = (ℂ D (𝑦 ∈ ℂ ↦ (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦))))
204	179	feqmptd 6946	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘𝑁) = (𝑦 ∈ ℂ ↦ (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))
205	201, 203, 204	3eqtr3d 2803	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦ (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦))) = (𝑦 ∈ ℂ ↦ (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))
206	185, 68, 188, 190, 156, 180, 205	dvmptres3 26183	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝑆 ↦ (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦))) = (𝑦 ∈ 𝑆 ↦ (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))
207		eqid 2760	. . . . . . . . . . . 12 ⊢ ((TopOpen‘ℂ_fld) ↾_t 𝑆) = ((TopOpen‘ℂ_fld) ↾_t 𝑆)
208		resttopon 23386	. . . . . . . . . . . . . . . 16 ⊢ (((TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ) ∧ 𝑆 ⊆ ℂ) → ((TopOpen‘ℂ_fld) ↾_t 𝑆) ∈ (TopOn‘𝑆))
209	186, 122, 208	sylancr 599	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((TopOpen‘ℂ_fld) ↾_t 𝑆) ∈ (TopOn‘𝑆))
210		topontop 23138	. . . . . . . . . . . . . . 15 ⊢ (((TopOpen‘ℂ_fld) ↾_t 𝑆) ∈ (TopOn‘𝑆) → ((TopOpen‘ℂ_fld) ↾_t 𝑆) ∈ Top)
211	209, 210	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((TopOpen‘ℂ_fld) ↾_t 𝑆) ∈ Top)
212		toponuni 23139	. . . . . . . . . . . . . . . 16 ⊢ (((TopOpen‘ℂ_fld) ↾_t 𝑆) ∈ (TopOn‘𝑆) → 𝑆 = ∪ ((TopOpen‘ℂ_fld) ↾_t 𝑆))
213	209, 212	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑆 = ∪ ((TopOpen‘ℂ_fld) ↾_t 𝑆))
214	70, 213	sseqtrd 3967	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ⊆ ∪ ((TopOpen‘ℂ_fld) ↾_t 𝑆))
215		eqid 2760	. . . . . . . . . . . . . . 15 ⊢ ∪ ((TopOpen‘ℂ_fld) ↾_t 𝑆) = ∪ ((TopOpen‘ℂ_fld) ↾_t 𝑆)
216	215	ntrss2 23282	. . . . . . . . . . . . . 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 5889	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom (𝑆 D ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))) = dom ((𝑆 D^𝑛 𝐹)‘𝑁))
219	218, 76	eqtrd 2795	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom (𝑆 D ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))) = 𝐴)
220	122, 112, 70, 207, 185	dvbssntr 26127	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom (𝑆 D ((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))) ⊆ ((int‘((TopOpen‘ℂ_fld) ↾_t 𝑆))‘𝐴))
221	219, 220	eqsstrrd 3966	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ⊆ ((int‘((TopOpen‘ℂ_fld) ↾_t 𝑆))‘𝐴))
222	217, 221	eqssd 3948	. . . . . . . . . . . 12 ⊢ (𝜑 → ((int‘((TopOpen‘ℂ_fld) ↾_t 𝑆))‘𝐴) = 𝐴)
223	68, 183, 184, 206, 70, 207, 185, 222	dvmptres2 26189	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝐴 ↦ (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦))) = (𝑦 ∈ 𝐴 ↦ (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))
224	68, 113, 116, 129, 157, 181, 223	dvmptsub 26194	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆 D (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))) = (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦))))
225	224	breqd 5114	. . . . . . . . 9 ⊢ (𝜑 → (𝐵(𝑆 D (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦))))0 ↔ 𝐵(𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘𝑁)‘𝑦) − (((ℂ D^𝑛 𝑇)‘𝑁)‘𝑦)))0))
226	96, 225	mpbird 260	. . . . . . . 8 ⊢ (𝜑 → 𝐵(𝑆 D (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦))))0)
227		eqid 2760	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵)))
228	113, 157	subcld 11593	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)) ∈ ℂ)
229	228	fmpttd 7108	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦))):𝐴⟶ℂ)
230	207, 185, 227, 122, 229, 70	eldv 26125	. . . . . . . 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 4078	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐴 ∖ {𝐵}) → 𝑥 ∈ 𝐴)
234		fveq2 6878	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑥 → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) = (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥))
235		fveq2 6878	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑥 → (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦) = (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥))
236	234, 235	oveq12d 7431	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑥 → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)) = ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)))
237		eqid 2760	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦))) = (𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))
238		ovex 7446	. . . . . . . . . . . . 13 ⊢ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) ∈ V
239	236, 237, 238	fvmpt 6986	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) = ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)))
240		fveq2 6878	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝐵 → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) = (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝐵))
241		fveq2 6878	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝐵 → (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦) = (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝐵))
242	240, 241	oveq12d 7431	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝐵 → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)) = ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝐵)))
243		ovex 7446	. . . . . . . . . . . . . . 15 ⊢ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝐵)) ∈ V
244	242, 237, 243	fvmpt 6986	. . . . . . . . . . . . . 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 26608	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝐵) = (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝐵))
247	246	oveq2d 7429	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝐵)) = ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝐵)))
248	112, 60	ffvelcdmd 7078	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝐵) ∈ ℂ)
249	248	subidd 11581	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝐵) − (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝐵)) = 0)
250	245, 247, 249	3eqtrd 2799	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵) = 0)
251	239, 250	oveqan12rd 7433	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) = (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) − 0))
252	112	ffvelcdmda 7077	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) ∈ ℂ)
253	130	sselda 3931	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℂ)
254	155	ffvelcdmda 7077	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥) ∈ ℂ)
255	253, 254	syldan 603	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥) ∈ ℂ)
256	252, 255	subcld 11593	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) ∈ ℂ)
257	256	subid1d 11582	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) − 0) = ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)))
258	251, 257	eqtr2d 2796	. . . . . . . . . 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 4094	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 ∖ {𝐵}) ⊆ ℂ)
261	260	sselda 3931	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ ℂ)
262	130, 60	sseldd 3932	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ ℂ)
263	262	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → 𝐵 ∈ ℂ)
264	261, 263	subcld 11593	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (𝑥 − 𝐵) ∈ ℂ)
265	264	exp1d 14205	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → ((𝑥 − 𝐵)↑1) = (𝑥 − 𝐵))
266	259, 265	oveq12d 7431	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝐵})) → (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1)) = ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵)))
267	266	mpteq2dva 5198	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵))))
268	267	oveq1d 7428	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑥)) / ((𝑥 − 𝐵)↑1))) lim_ℂ 𝐵) = ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ ((((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝑥) − ((𝑦 ∈ 𝐴 ↦ ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 1))‘𝑦) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 1))‘𝑦)))‘𝐵)) / (𝑥 − 𝐵))) lim_ℂ 𝐵))
269	232, 268	eleqtrrd 2863	. . . . 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 13844	. . 3 ⊢ (𝑁 ∈ (1...𝑁) → (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) lim_ℂ 𝐵)))
276	3, 275	mpcom 39	. 2 ⊢ (𝜑 → 0 ∈ ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) lim_ℂ 𝐵))
277	117	subidd 11581	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 − 𝑁) = 0)
278	277	fveq2d 6882	. . . . . . . . 9 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁)) = ((𝑆 D^𝑛 𝐹)‘0))
279		dvn0 26151	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆)) → ((𝑆 D^𝑛 𝐹)‘0) = 𝐹)
280	122, 84, 279	syl2anc 596	. . . . . . . . 9 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘0) = 𝐹)
281	278, 280	eqtrd 2795	. . . . . . . 8 ⊢ (𝜑 → ((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁)) = 𝐹)
282	281	fveq1d 6880	. . . . . . 7 ⊢ (𝜑 → (((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) = (𝐹‘𝑥))
283	277	fveq2d 6882	. . . . . . . . 9 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁)) = ((ℂ D^𝑛 𝑇)‘0))
284		dvn0 26151	. . . . . . . . . 10 ⊢ ((ℂ ⊆ ℂ ∧ 𝑇 ∈ (ℂ ↑_pm ℂ)) → ((ℂ D^𝑛 𝑇)‘0) = 𝑇)
285	191, 197, 284	sylancr 599	. . . . . . . . 9 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘0) = 𝑇)
286	283, 285	eqtrd 2795	. . . . . . . 8 ⊢ (𝜑 → ((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁)) = 𝑇)
287	286	fveq1d 6880	. . . . . . 7 ⊢ (𝜑 → (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥) = (𝑇‘𝑥))
288	282, 287	oveq12d 7431	. . . . . 6 ⊢ (𝜑 → ((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) = ((𝐹‘𝑥) − (𝑇‘𝑥)))
289	288	oveq1d 7428	. . . . 5 ⊢ (𝜑 → (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁)) = (((𝐹‘𝑥) − (𝑇‘𝑥)) / ((𝑥 − 𝐵)↑𝑁)))
290	289	mpteq2dv 5199	. . . 4 ⊢ (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝐹‘𝑥) − (𝑇‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))))
291		taylthlem1.r	. . . 4 ⊢ 𝑅 = (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((𝐹‘𝑥) − (𝑇‘𝑥)) / ((𝑥 − 𝐵)↑𝑁)))
292	290, 291	eqtr4di 2813	. . 3 ⊢ (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) = 𝑅)
293	292	oveq1d 7428	. 2 ⊢ (𝜑 → ((𝑥 ∈ (𝐴 ∖ {𝐵}) ↦ (((((𝑆 D^𝑛 𝐹)‘(𝑁 − 𝑁))‘𝑥) − (((ℂ D^𝑛 𝑇)‘(𝑁 − 𝑁))‘𝑥)) / ((𝑥 − 𝐵)↑𝑁))) lim_ℂ 𝐵) = (𝑅 lim_ℂ 𝐵))
294	276, 293	eleqtrd 2862	1 ⊢ (𝜑 → 0 ∈ (𝑅 lim_ℂ 𝐵))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2145 Vcvv 3450 ∖ cdif 3896 ∩ cin 3898 ⊆ wss 3899 {csn 4584 {cpr 4586 ∪ cuni 4867 class class class wbr 5103 ↦ cmpt 5186 dom cdm 5655 Fun wfun 6527 ⟶wf 6529 ‘cfv 6533 (class class class)co 7413 ↑_m cmap 8826 ↑_pm cpm 8827 ℂcc 11122 ℝcr 11123 0cc0 11124 1c1 11125 + caddc 11127 − cmin 11465 / cdiv 11895 ℕcn 12257 ℕ₀cn0 12528 ℤ_≥cuz 12887 ...cfz 13561 ..^cfzo 13709 ↑cexp 14125 ↾_t crest 17505 TopOpenctopn 17506 ℂ_fldccnfld 21585 Topctop 23118 TopOnctopon 23135 intcnt 23242 lim_ℂ climc 26089 D cdv 26090 D^𝑛 cdvn 26091 Tayl ctayl 26589

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-rep 5232 ax-sep 5251 ax-nul 5263 ax-pow 5330 ax-pr 5398 ax-un 7736 ax-inf2 9620 ax-cnex 11180 ax-resscn 11181 ax-1cn 11182 ax-icn 11183 ax-addcl 11184 ax-addrcl 11185 ax-mulcl 11186 ax-mulrcl 11187 ax-mulcom 11188 ax-addass 11189 ax-mulass 11190 ax-distr 11191 ax-i2m1 11192 ax-1ne0 11193 ax-1rid 11194 ax-rnegex 11195 ax-rrecex 11196 ax-cnre 11197 ax-pre-lttri 11198 ax-pre-lttrn 11199 ax-pre-ltadd 11200 ax-pre-mulgt0 11201 ax-pre-sup 11202 ax-addf 11203

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-se 5609 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6299 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-isom 6542 df-riota 7370 df-ov 7416 df-oprab 7417 df-mpo 7418 df-of 7678 df-om 7863 df-1st 7986 df-2nd 7987 df-supp 8159 df-frecs 8280 df-wrecs 8311 df-recs 8360 df-rdg 8399 df-1o 8455 df-2o 8456 df-er 8696 df-map 8828 df-pm 8829 df-ixp 8905 df-en 8953 df-dom 8954 df-sdom 8955 df-fin 8956 df-fsupp 9332 df-fi 9381 df-sup 9412 df-inf 9413 df-oi 9482 df-card 9944 df-pnf 11269 df-mnf 11270 df-xr 11271 df-ltxr 11272 df-le 11273 df-sub 11467 df-neg 11468 df-div 11896 df-nn 12258 df-2 12327 df-3 12328 df-4 12329 df-5 12330 df-6 12331 df-7 12332 df-8 12333 df-9 12334 df-n0 12529 df-xnn0 12602 df-z 12616 df-dec 12737 df-uz 12888 df-q 12998 df-rp 13043 df-xneg 13163 df-xadd 13164 df-xmul 13165 df-icc 13405 df-fz 13562 df-fzo 13710 df-seq 14066 df-exp 14126 df-fac 14338 df-hash 14395 df-cj 15186 df-re 15187 df-im 15188 df-sqrt 15322 df-abs 15323 df-clim 15575 df-sum 15774 df-struct 17239 df-sets 17256 df-slot 17274 df-ndx 17286 df-base 17302 df-ress 17323 df-plusg 17355 df-mulr 17356 df-starv 17357 df-sca 17358 df-vsca 17359 df-ip 17360 df-tset 17361 df-ple 17362 df-ds 17364 df-unif 17365 df-hom 17366 df-cco 17367 df-rest 17507 df-topn 17508 df-0g 17526 df-gsum 17527 df-topgen 17528 df-pt 17529 df-prds 17532 df-xrs 17588 df-qtop 17593 df-imas 17594 df-xps 17596 df-mre 17670 df-mrc 17671 df-acs 17673 df-mgm 18730 df-sgrp 18821 df-mnd 18837 df-submnd 18892 df-grp 19060 df-minusg 19061 df-mulg 19191 df-cntz 19444 df-cmn 19909 df-abl 19910 df-mgp 20274 df-ur 20321 df-ring 20374 df-cring 20375 df-psmet 21577 df-xmet 21578 df-met 21579 df-bl 21580 df-mopn 21581 df-fbas 21582 df-fg 21583 df-cnfld 21586 df-top 23119 df-topon 23136 df-topsp 23158 df-bases 23171 df-cld 23244 df-ntr 23245 df-cls 23246 df-nei 23323 df-lp 23361 df-perf 23362 df-cn 23452 df-cnp 23453 df-haus 23540 df-tx 23788 df-hmeo 23981 df-fil 24072 df-fm 24164 df-flim 24165 df-flf 24166 df-tsms 24353 df-xms 24546 df-ms 24547 df-tms 24548 df-cncf 25106 df-limc 26093 df-dv 26094 df-dvn 26095 df-tayl 26591

This theorem is used by: taylth 26611

W3C validator