taylthlem1

Description: Lemma for taylth . 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 S = RR , we can only do this part generically, and for taylth itself we must restrict to RR . (Contributed by Mario Carneiro, 1-Jan-2017)

	Ref	Expression
Hypotheses	taylthlem1.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
	taylthlem1.f	$⊢ φ \to F : A ⟶ ℂ$
	taylthlem1.a	$⊢ φ \to A \subseteq S$
	taylthlem1.d	$⊢ φ \to dom (S D^{n} F) (N) = A$
	taylthlem1.n	$⊢ φ \to N \in ℕ$
	taylthlem1.b	$⊢ φ \to B \in A$
	taylthlem1.t	$⊢ T = N (S Tayl F) B$
	taylthlem1.r	$⊢ R = (x \in (A ∖ \{B\}) ⟼ \frac{F (x) - T (x)}{{(x - B)}^{N}})$
	taylthlem1.i	$⊢ (φ \land (n \in (1 ..^N) \land 0 \in ((y \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - n) (y) - (ℂ D^{n} T) (N - n) (y)}{{(y - B)}^{n}}) {lim}_{ℂ} B))) \to 0 \in ((x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - (n + 1)) (x) - (ℂ D^{n} T) (N - (n + 1)) (x)}{{(x - B)}^{n + 1}}) {lim}_{ℂ} B)$
Assertion	taylthlem1	$⊢ φ \to 0 \in (R {lim}_{ℂ} B)$

Proof

Step	Hyp	Ref	Expression
1		taylthlem1.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
2		taylthlem1.f	$⊢ φ \to F : A ⟶ ℂ$
3		taylthlem1.a	$⊢ φ \to A \subseteq S$
4		taylthlem1.d	$⊢ φ \to dom (S D^{n} F) (N) = A$
5		taylthlem1.n	$⊢ φ \to N \in ℕ$
6		taylthlem1.b	$⊢ φ \to B \in A$
7		taylthlem1.t	$⊢ T = N (S Tayl F) B$
8		taylthlem1.r	$⊢ R = (x \in (A ∖ \{B\}) ⟼ \frac{F (x) - T (x)}{{(x - B)}^{N}})$
9		taylthlem1.i	$⊢ (φ \land (n \in (1 ..^N) \land 0 \in ((y \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - n) (y) - (ℂ D^{n} T) (N - n) (y)}{{(y - B)}^{n}}) {lim}_{ℂ} B))) \to 0 \in ((x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - (n + 1)) (x) - (ℂ D^{n} T) (N - (n + 1)) (x)}{{(x - B)}^{n + 1}}) {lim}_{ℂ} B)$
10		elfz1end	$⊢ N \in ℕ \leftrightarrow N \in (1 \dots N)$
11	5 10	sylib	$⊢ φ \to N \in (1 \dots N)$
12		oveq2	$⊢ m = 1 \to N - m = N - 1$
13	12	fveq2d	$⊢ m = 1 \to (S D^{n} F) (N - m) = (S D^{n} F) (N - 1)$
14	13	fveq1d	$⊢ m = 1 \to (S D^{n} F) (N - m) (x) = (S D^{n} F) (N - 1) (x)$
15	12	fveq2d	$⊢ m = 1 \to (ℂ D^{n} T) (N - m) = (ℂ D^{n} T) (N - 1)$
16	15	fveq1d	$⊢ m = 1 \to (ℂ D^{n} T) (N - m) (x) = (ℂ D^{n} T) (N - 1) (x)$
17	14 16	oveq12d	$⊢ m = 1 \to (S D^{n} F) (N - m) (x) - (ℂ D^{n} T) (N - m) (x) = (S D^{n} F) (N - 1) (x) - (ℂ D^{n} T) (N - 1) (x)$
18		oveq2	$⊢ m = 1 \to {(x - B)}^{m} = {(x - B)}^{1}$
19	17 18	oveq12d	$⊢ m = 1 \to \frac{(S D^{n} F) (N - m) (x) - (ℂ D^{n} T) (N - m) (x)}{{(x - B)}^{m}} = \frac{(S D^{n} F) (N - 1) (x) - (ℂ D^{n} T) (N - 1) (x)}{{(x - B)}^{1}}$
20	19	mpteq2dv	$⊢ m = 1 \to (x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - m) (x) - (ℂ D^{n} T) (N - m) (x)}{{(x - B)}^{m}}) = (x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - 1) (x) - (ℂ D^{n} T) (N - 1) (x)}{{(x - B)}^{1}})$
21	20	oveq1d	$⊢ m = 1 \to (x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - m) (x) - (ℂ D^{n} T) (N - m) (x)}{{(x - B)}^{m}}) {lim}_{ℂ} B = (x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - 1) (x) - (ℂ D^{n} T) (N - 1) (x)}{{(x - B)}^{1}}) {lim}_{ℂ} B$
22	21	eleq2d	$⊢ m = 1 \to (0 \in ((x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - m) (x) - (ℂ D^{n} T) (N - m) (x)}{{(x - B)}^{m}}) {lim}_{ℂ} B) \leftrightarrow 0 \in ((x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - 1) (x) - (ℂ D^{n} T) (N - 1) (x)}{{(x - B)}^{1}}) {lim}_{ℂ} B))$
23	22	imbi2d	$⊢ m = 1 \to ((φ \to 0 \in ((x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - m) (x) - (ℂ D^{n} T) (N - m) (x)}{{(x - B)}^{m}}) {lim}_{ℂ} B)) \leftrightarrow (φ \to 0 \in ((x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - 1) (x) - (ℂ D^{n} T) (N - 1) (x)}{{(x - B)}^{1}}) {lim}_{ℂ} B)))$
24		oveq2	$⊢ m = n \to N - m = N - n$
25	24	fveq2d	$⊢ m = n \to (S D^{n} F) (N - m) = (S D^{n} F) (N - n)$
26	25	fveq1d	$⊢ m = n \to (S D^{n} F) (N - m) (x) = (S D^{n} F) (N - n) (x)$
27	24	fveq2d	$⊢ m = n \to (ℂ D^{n} T) (N - m) = (ℂ D^{n} T) (N - n)$
28	27	fveq1d	$⊢ m = n \to (ℂ D^{n} T) (N - m) (x) = (ℂ D^{n} T) (N - n) (x)$
29	26 28	oveq12d	$⊢ m = n \to (S D^{n} F) (N - m) (x) - (ℂ D^{n} T) (N - m) (x) = (S D^{n} F) (N - n) (x) - (ℂ D^{n} T) (N - n) (x)$
30		oveq2	$⊢ m = n \to {(x - B)}^{m} = {(x - B)}^{n}$
31	29 30	oveq12d	$⊢ m = n \to \frac{(S D^{n} F) (N - m) (x) - (ℂ D^{n} T) (N - m) (x)}{{(x - B)}^{m}} = \frac{(S D^{n} F) (N - n) (x) - (ℂ D^{n} T) (N - n) (x)}{{(x - B)}^{n}}$
32	31	mpteq2dv	$⊢ m = n \to (x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - m) (x) - (ℂ D^{n} T) (N - m) (x)}{{(x - B)}^{m}}) = (x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - n) (x) - (ℂ D^{n} T) (N - n) (x)}{{(x - B)}^{n}})$
33		fveq2	$⊢ x = y \to (S D^{n} F) (N - n) (x) = (S D^{n} F) (N - n) (y)$
34		fveq2	$⊢ x = y \to (ℂ D^{n} T) (N - n) (x) = (ℂ D^{n} T) (N - n) (y)$
35	33 34	oveq12d	$⊢ x = y \to (S D^{n} F) (N - n) (x) - (ℂ D^{n} T) (N - n) (x) = (S D^{n} F) (N - n) (y) - (ℂ D^{n} T) (N - n) (y)$
36		oveq1	$⊢ x = y \to x - B = y - B$
37	36	oveq1d	$⊢ x = y \to {(x - B)}^{n} = {(y - B)}^{n}$
38	35 37	oveq12d	$⊢ x = y \to \frac{(S D^{n} F) (N - n) (x) - (ℂ D^{n} T) (N - n) (x)}{{(x - B)}^{n}} = \frac{(S D^{n} F) (N - n) (y) - (ℂ D^{n} T) (N - n) (y)}{{(y - B)}^{n}}$
39	38	cbvmptv	$⊢ (x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - n) (x) - (ℂ D^{n} T) (N - n) (x)}{{(x - B)}^{n}}) = (y \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - n) (y) - (ℂ D^{n} T) (N - n) (y)}{{(y - B)}^{n}})$
40	32 39	eqtrdi	$⊢ m = n \to (x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - m) (x) - (ℂ D^{n} T) (N - m) (x)}{{(x - B)}^{m}}) = (y \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - n) (y) - (ℂ D^{n} T) (N - n) (y)}{{(y - B)}^{n}})$
41	40	oveq1d	$⊢ m = n \to (x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - m) (x) - (ℂ D^{n} T) (N - m) (x)}{{(x - B)}^{m}}) {lim}_{ℂ} B = (y \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - n) (y) - (ℂ D^{n} T) (N - n) (y)}{{(y - B)}^{n}}) {lim}_{ℂ} B$
42	41	eleq2d	$⊢ m = n \to (0 \in ((x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - m) (x) - (ℂ D^{n} T) (N - m) (x)}{{(x - B)}^{m}}) {lim}_{ℂ} B) \leftrightarrow 0 \in ((y \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - n) (y) - (ℂ D^{n} T) (N - n) (y)}{{(y - B)}^{n}}) {lim}_{ℂ} B))$
43	42	imbi2d	$⊢ m = n \to ((φ \to 0 \in ((x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - m) (x) - (ℂ D^{n} T) (N - m) (x)}{{(x - B)}^{m}}) {lim}_{ℂ} B)) \leftrightarrow (φ \to 0 \in ((y \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - n) (y) - (ℂ D^{n} T) (N - n) (y)}{{(y - B)}^{n}}) {lim}_{ℂ} B)))$
44		oveq2	$⊢ m = n + 1 \to N - m = N - (n + 1)$
45	44	fveq2d	$⊢ m = n + 1 \to (S D^{n} F) (N - m) = (S D^{n} F) (N - (n + 1))$
46	45	fveq1d	$⊢ m = n + 1 \to (S D^{n} F) (N - m) (x) = (S D^{n} F) (N - (n + 1)) (x)$
47	44	fveq2d	$⊢ m = n + 1 \to (ℂ D^{n} T) (N - m) = (ℂ D^{n} T) (N - (n + 1))$
48	47	fveq1d	$⊢ m = n + 1 \to (ℂ D^{n} T) (N - m) (x) = (ℂ D^{n} T) (N - (n + 1)) (x)$
49	46 48	oveq12d	$⊢ m = n + 1 \to (S D^{n} F) (N - m) (x) - (ℂ D^{n} T) (N - m) (x) = (S D^{n} F) (N - (n + 1)) (x) - (ℂ D^{n} T) (N - (n + 1)) (x)$
50		oveq2	$⊢ m = n + 1 \to {(x - B)}^{m} = {(x - B)}^{n + 1}$
51	49 50	oveq12d	$⊢ m = n + 1 \to \frac{(S D^{n} F) (N - m) (x) - (ℂ D^{n} T) (N - m) (x)}{{(x - B)}^{m}} = \frac{(S D^{n} F) (N - (n + 1)) (x) - (ℂ D^{n} T) (N - (n + 1)) (x)}{{(x - B)}^{n + 1}}$
52	51	mpteq2dv	$⊢ m = n + 1 \to (x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - m) (x) - (ℂ D^{n} T) (N - m) (x)}{{(x - B)}^{m}}) = (x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - (n + 1)) (x) - (ℂ D^{n} T) (N - (n + 1)) (x)}{{(x - B)}^{n + 1}})$
53	52	oveq1d	$⊢ m = n + 1 \to (x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - m) (x) - (ℂ D^{n} T) (N - m) (x)}{{(x - B)}^{m}}) {lim}_{ℂ} B = (x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - (n + 1)) (x) - (ℂ D^{n} T) (N - (n + 1)) (x)}{{(x - B)}^{n + 1}}) {lim}_{ℂ} B$
54	53	eleq2d	$⊢ m = n + 1 \to (0 \in ((x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - m) (x) - (ℂ D^{n} T) (N - m) (x)}{{(x - B)}^{m}}) {lim}_{ℂ} B) \leftrightarrow 0 \in ((x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - (n + 1)) (x) - (ℂ D^{n} T) (N - (n + 1)) (x)}{{(x - B)}^{n + 1}}) {lim}_{ℂ} B))$
55	54	imbi2d	$⊢ m = n + 1 \to ((φ \to 0 \in ((x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - m) (x) - (ℂ D^{n} T) (N - m) (x)}{{(x - B)}^{m}}) {lim}_{ℂ} B)) \leftrightarrow (φ \to 0 \in ((x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - (n + 1)) (x) - (ℂ D^{n} T) (N - (n + 1)) (x)}{{(x - B)}^{n + 1}}) {lim}_{ℂ} B)))$
56		oveq2	$⊢ m = N \to N - m = N - N$
57	56	fveq2d	$⊢ m = N \to (S D^{n} F) (N - m) = (S D^{n} F) (N - N)$
58	57	fveq1d	$⊢ m = N \to (S D^{n} F) (N - m) (x) = (S D^{n} F) (N - N) (x)$
59	56	fveq2d	$⊢ m = N \to (ℂ D^{n} T) (N - m) = (ℂ D^{n} T) (N - N)$
60	59	fveq1d	$⊢ m = N \to (ℂ D^{n} T) (N - m) (x) = (ℂ D^{n} T) (N - N) (x)$
61	58 60	oveq12d	$⊢ m = N \to (S D^{n} F) (N - m) (x) - (ℂ D^{n} T) (N - m) (x) = (S D^{n} F) (N - N) (x) - (ℂ D^{n} T) (N - N) (x)$
62		oveq2	$⊢ m = N \to {(x - B)}^{m} = {(x - B)}^{N}$
63	61 62	oveq12d	$⊢ m = N \to \frac{(S D^{n} F) (N - m) (x) - (ℂ D^{n} T) (N - m) (x)}{{(x - B)}^{m}} = \frac{(S D^{n} F) (N - N) (x) - (ℂ D^{n} T) (N - N) (x)}{{(x - B)}^{N}}$
64	63	mpteq2dv	$⊢ m = N \to (x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - m) (x) - (ℂ D^{n} T) (N - m) (x)}{{(x - B)}^{m}}) = (x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - N) (x) - (ℂ D^{n} T) (N - N) (x)}{{(x - B)}^{N}})$
65	64	oveq1d	$⊢ m = N \to (x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - m) (x) - (ℂ D^{n} T) (N - m) (x)}{{(x - B)}^{m}}) {lim}_{ℂ} B = (x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - N) (x) - (ℂ D^{n} T) (N - N) (x)}{{(x - B)}^{N}}) {lim}_{ℂ} B$
66	65	eleq2d	$⊢ m = N \to (0 \in ((x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - m) (x) - (ℂ D^{n} T) (N - m) (x)}{{(x - B)}^{m}}) {lim}_{ℂ} B) \leftrightarrow 0 \in ((x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - N) (x) - (ℂ D^{n} T) (N - N) (x)}{{(x - B)}^{N}}) {lim}_{ℂ} B))$
67	66	imbi2d	$⊢ m = N \to ((φ \to 0 \in ((x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - m) (x) - (ℂ D^{n} T) (N - m) (x)}{{(x - B)}^{m}}) {lim}_{ℂ} B)) \leftrightarrow (φ \to 0 \in ((x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - N) (x) - (ℂ D^{n} T) (N - N) (x)}{{(x - B)}^{N}}) {lim}_{ℂ} B)))$
68		fveq2	$⊢ y = B \to (S D^{n} F) (N) (y) = (S D^{n} F) (N) (B)$
69		fveq2	$⊢ y = B \to (ℂ D^{n} T) (N) (y) = (ℂ D^{n} T) (N) (B)$
70	68 69	oveq12d	$⊢ y = B \to (S D^{n} F) (N) (y) - (ℂ D^{n} T) (N) (y) = (S D^{n} F) (N) (B) - (ℂ D^{n} T) (N) (B)$
71		eqid	$⊢ (y \in A ⟼ (S D^{n} F) (N) (y) - (ℂ D^{n} T) (N) (y)) = (y \in A ⟼ (S D^{n} F) (N) (y) - (ℂ D^{n} T) (N) (y))$
72		ovex	$⊢ (S D^{n} F) (N) (B) - (ℂ D^{n} T) (N) (B) \in V$
73	70 71 72	fvmpt	$⊢ B \in A \to (y \in A ⟼ (S D^{n} F) (N) (y) - (ℂ D^{n} T) (N) (y)) (B) = (S D^{n} F) (N) (B) - (ℂ D^{n} T) (N) (B)$
74	6 73	syl	$⊢ φ \to (y \in A ⟼ (S D^{n} F) (N) (y) - (ℂ D^{n} T) (N) (y)) (B) = (S D^{n} F) (N) (B) - (ℂ D^{n} T) (N) (B)$
75	5	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
76		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
77	75 76	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq 0}$
78		eluzfz2b	$⊢ N \in ℤ_{\geq 0} \leftrightarrow N \in (0 \dots N)$
79	77 78	sylib	$⊢ φ \to N \in (0 \dots N)$
80	6 4	eleqtrrd	$⊢ φ \to B \in dom (S D^{n} F) (N)$
81	1 2 3 79 80 7	dvntaylp0	$⊢ φ \to (ℂ D^{n} T) (N) (B) = (S D^{n} F) (N) (B)$
82	81	oveq2d	$⊢ φ \to (S D^{n} F) (N) (B) - (ℂ D^{n} T) (N) (B) = (S D^{n} F) (N) (B) - (S D^{n} F) (N) (B)$
83		cnex	$⊢ ℂ \in V$
84	83	a1i	$⊢ φ \to ℂ \in V$
85		elpm2r	$⊢ ((ℂ \in V \land S \in \{ℝ, ℂ\}) \land (F : A ⟶ ℂ \land A \subseteq S)) \to F \in (ℂ ↑_{𝑝𝑚} S)$
86	84 1 2 3 85	syl22anc	$⊢ φ \to F \in (ℂ ↑_{𝑝𝑚} S)$
87		dvnf	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land N \in ℕ_{0}) \to (S D^{n} F) (N) : dom (S D^{n} F) (N) ⟶ ℂ$
88	1 86 75 87	syl3anc	$⊢ φ \to (S D^{n} F) (N) : dom (S D^{n} F) (N) ⟶ ℂ$
89	88 80	ffvelrnd	$⊢ φ \to (S D^{n} F) (N) (B) \in ℂ$
90	89	subidd	$⊢ φ \to (S D^{n} F) (N) (B) - (S D^{n} F) (N) (B) = 0$
91	74 82 90	3eqtrd	$⊢ φ \to (y \in A ⟼ (S D^{n} F) (N) (y) - (ℂ D^{n} T) (N) (y)) (B) = 0$
92		funmpt	$⊢ Fun (y \in A ⟼ (S D^{n} F) (N) (y) - (ℂ D^{n} T) (N) (y))$
93		ovex	$⊢ (S D^{n} F) (N) (y) - (ℂ D^{n} T) (N) (y) \in V$
94	93 71	dmmpti	$⊢ dom (y \in A ⟼ (S D^{n} F) (N) (y) - (ℂ D^{n} T) (N) (y)) = A$
95	6 94	eleqtrrdi	$⊢ φ \to B \in dom (y \in A ⟼ (S D^{n} F) (N) (y) - (ℂ D^{n} T) (N) (y))$
96		funbrfvb	$⊢ (Fun (y \in A ⟼ (S D^{n} F) (N) (y) - (ℂ D^{n} T) (N) (y)) \land B \in dom (y \in A ⟼ (S D^{n} F) (N) (y) - (ℂ D^{n} T) (N) (y))) \to ((y \in A ⟼ (S D^{n} F) (N) (y) - (ℂ D^{n} T) (N) (y)) (B) = 0 \leftrightarrow B (y \in A ⟼ (S D^{n} F) (N) (y) - (ℂ D^{n} T) (N) (y)) 0)$
97	92 95 96	sylancr	$⊢ φ \to ((y \in A ⟼ (S D^{n} F) (N) (y) - (ℂ D^{n} T) (N) (y)) (B) = 0 \leftrightarrow B (y \in A ⟼ (S D^{n} F) (N) (y) - (ℂ D^{n} T) (N) (y)) 0)$
98	91 97	mpbid	$⊢ φ \to B (y \in A ⟼ (S D^{n} F) (N) (y) - (ℂ D^{n} T) (N) (y)) 0$
99		nnm1nn0	$⊢ N \in ℕ \to N - 1 \in ℕ_{0}$
100	5 99	syl	$⊢ φ \to N - 1 \in ℕ_{0}$
101		dvnf	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land N - 1 \in ℕ_{0}) \to (S D^{n} F) (N - 1) : dom (S D^{n} F) (N - 1) ⟶ ℂ$
102	1 86 100 101	syl3anc	$⊢ φ \to (S D^{n} F) (N - 1) : dom (S D^{n} F) (N - 1) ⟶ ℂ$
103		dvnbss	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land N - 1 \in ℕ_{0}) \to dom (S D^{n} F) (N - 1) \subseteq dom F$
104	1 86 100 103	syl3anc	$⊢ φ \to dom (S D^{n} F) (N - 1) \subseteq dom F$
105	2 104	fssdmd	$⊢ φ \to dom (S D^{n} F) (N - 1) \subseteq A$
106		fzo0end	$⊢ N \in ℕ \to N - 1 \in (0 ..^N)$
107		elfzofz	$⊢ N - 1 \in (0 ..^N) \to N - 1 \in (0 \dots N)$
108	5 106 107	3syl	$⊢ φ \to N - 1 \in (0 \dots N)$
109		dvn2bss	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land N - 1 \in (0 \dots N)) \to dom (S D^{n} F) (N) \subseteq dom (S D^{n} F) (N - 1)$
110	1 86 108 109	syl3anc	$⊢ φ \to dom (S D^{n} F) (N) \subseteq dom (S D^{n} F) (N - 1)$
111	4 110	eqsstrrd	$⊢ φ \to A \subseteq dom (S D^{n} F) (N - 1)$
112	105 111	eqssd	$⊢ φ \to dom (S D^{n} F) (N - 1) = A$
113	112	feq2d	$⊢ φ \to ((S D^{n} F) (N - 1) : dom (S D^{n} F) (N - 1) ⟶ ℂ \leftrightarrow (S D^{n} F) (N - 1) : A ⟶ ℂ)$
114	102 113	mpbid	$⊢ φ \to (S D^{n} F) (N - 1) : A ⟶ ℂ$
115	114	ffvelrnda	$⊢ (φ \land y \in A) \to (S D^{n} F) (N - 1) (y) \in ℂ$
116	4	feq2d	$⊢ φ \to ((S D^{n} F) (N) : dom (S D^{n} F) (N) ⟶ ℂ \leftrightarrow (S D^{n} F) (N) : A ⟶ ℂ)$
117	88 116	mpbid	$⊢ φ \to (S D^{n} F) (N) : A ⟶ ℂ$
118	117	ffvelrnda	$⊢ (φ \land y \in A) \to (S D^{n} F) (N) (y) \in ℂ$
119	5	nncnd	$⊢ φ \to N \in ℂ$
120		1cnd	$⊢ φ \to 1 \in ℂ$
121	119 120	npcand	$⊢ φ \to N - 1 + 1 = N$
122	121	fveq2d	$⊢ φ \to (S D^{n} F) (N - 1 + 1) = (S D^{n} F) (N)$
123		recnprss	$⊢ S \in \{ℝ, ℂ\} \to S \subseteq ℂ$
124	1 123	syl	$⊢ φ \to S \subseteq ℂ$
125		dvnp1	$⊢ (S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S) \land N - 1 \in ℕ_{0}) \to (S D^{n} F) (N - 1 + 1) = S D (S D^{n} F) (N - 1)$
126	124 86 100 125	syl3anc	$⊢ φ \to (S D^{n} F) (N - 1 + 1) = S D (S D^{n} F) (N - 1)$
127	122 126	eqtr3d	$⊢ φ \to (S D^{n} F) (N) = S D (S D^{n} F) (N - 1)$
128	117	feqmptd	$⊢ φ \to (S D^{n} F) (N) = (y \in A ⟼ (S D^{n} F) (N) (y))$
129	114	feqmptd	$⊢ φ \to (S D^{n} F) (N - 1) = (y \in A ⟼ (S D^{n} F) (N - 1) (y))$
130	129	oveq2d	$⊢ φ \to S D (S D^{n} F) (N - 1) = \frac{d (y \in A⟼ (S D^{n} F) (N - 1) (y))}{d_{S} y}$
131	127 128 130	3eqtr3rd	$⊢ φ \to \frac{d (y \in A⟼ (S D^{n} F) (N - 1) (y))}{d_{S} y} = (y \in A ⟼ (S D^{n} F) (N) (y))$
132	3 124	sstrd	$⊢ φ \to A \subseteq ℂ$
133	132	sselda	$⊢ (φ \land y \in A) \to y \in ℂ$
134		1nn0	$⊢ 1 \in ℕ_{0}$
135	134	a1i	$⊢ φ \to 1 \in ℕ_{0}$
136		elpm2r	$⊢ ((ℂ \in V \land S \in \{ℝ, ℂ\}) \land ((S D^{n} F) (N - 1) : A ⟶ ℂ \land A \subseteq S)) \to (S D^{n} F) (N - 1) \in (ℂ ↑_{𝑝𝑚} S)$
137	84 1 114 3 136	syl22anc	$⊢ φ \to (S D^{n} F) (N - 1) \in (ℂ ↑_{𝑝𝑚} S)$
138		dvn1	$⊢ (S \subseteq ℂ \land (S D^{n} F) (N - 1) \in (ℂ ↑_{𝑝𝑚} S)) \to (S D^{n} (S D^{n} F) (N - 1)) (1) = S D (S D^{n} F) (N - 1)$
139	124 137 138	syl2anc	$⊢ φ \to (S D^{n} (S D^{n} F) (N - 1)) (1) = S D (S D^{n} F) (N - 1)$
140	126 122	eqtr3d	$⊢ φ \to S D (S D^{n} F) (N - 1) = (S D^{n} F) (N)$
141	139 140	eqtrd	$⊢ φ \to (S D^{n} (S D^{n} F) (N - 1)) (1) = (S D^{n} F) (N)$
142	141	dmeqd	$⊢ φ \to dom (S D^{n} (S D^{n} F) (N - 1)) (1) = dom (S D^{n} F) (N)$
143	80 142	eleqtrrd	$⊢ φ \to B \in dom (S D^{n} (S D^{n} F) (N - 1)) (1)$
144		eqid	$⊢ 1 (S Tayl (S D^{n} F) (N - 1)) B = 1 (S Tayl (S D^{n} F) (N - 1)) B$
145	1 114 3 135 143 144	taylpf	$⊢ φ \to (1 (S Tayl (S D^{n} F) (N - 1)) B) : ℂ ⟶ ℂ$
146	120 119	pncan3d	$⊢ φ \to 1 + N - 1 = N$
147	146	oveq1d	$⊢ φ \to (1 + N - 1) (S Tayl F) B = N (S Tayl F) B$
148	7 147	eqtr4id	$⊢ φ \to T = (1 + N - 1) (S Tayl F) B$
149	148	oveq2d	$⊢ φ \to ℂ D^{n} T = ℂ D^{n} ((1 + N - 1) (S Tayl F) B)$
150	149	fveq1d	$⊢ φ \to (ℂ D^{n} T) (N - 1) = (ℂ D^{n} ((1 + N - 1) (S Tayl F) B)) (N - 1)$
151	146	fveq2d	$⊢ φ \to (S D^{n} F) (1 + N - 1) = (S D^{n} F) (N)$
152	151	dmeqd	$⊢ φ \to dom (S D^{n} F) (1 + N - 1) = dom (S D^{n} F) (N)$
153	80 152	eleqtrrd	$⊢ φ \to B \in dom (S D^{n} F) (1 + N - 1)$
154	1 2 3 100 135 153	dvntaylp	$⊢ φ \to (ℂ D^{n} ((1 + N - 1) (S Tayl F) B)) (N - 1) = 1 (S Tayl (S D^{n} F) (N - 1)) B$
155	150 154	eqtrd	$⊢ φ \to (ℂ D^{n} T) (N - 1) = 1 (S Tayl (S D^{n} F) (N - 1)) B$
156	155	feq1d	$⊢ φ \to ((ℂ D^{n} T) (N - 1) : ℂ ⟶ ℂ \leftrightarrow (1 (S Tayl (S D^{n} F) (N - 1)) B) : ℂ ⟶ ℂ)$
157	145 156	mpbird	$⊢ φ \to (ℂ D^{n} T) (N - 1) : ℂ ⟶ ℂ$
158	157	ffvelrnda	$⊢ (φ \land y \in ℂ) \to (ℂ D^{n} T) (N - 1) (y) \in ℂ$
159	133 158	syldan	$⊢ (φ \land y \in A) \to (ℂ D^{n} T) (N - 1) (y) \in ℂ$
160		0nn0	$⊢ 0 \in ℕ_{0}$
161	160	a1i	$⊢ φ \to 0 \in ℕ_{0}$
162		elpm2r	$⊢ ((ℂ \in V \land S \in \{ℝ, ℂ\}) \land ((S D^{n} F) (N) : A ⟶ ℂ \land A \subseteq S)) \to (S D^{n} F) (N) \in (ℂ ↑_{𝑝𝑚} S)$
163	84 1 117 3 162	syl22anc	$⊢ φ \to (S D^{n} F) (N) \in (ℂ ↑_{𝑝𝑚} S)$
164		dvn0	$⊢ (S \subseteq ℂ \land (S D^{n} F) (N) \in (ℂ ↑_{𝑝𝑚} S)) \to (S D^{n} (S D^{n} F) (N)) (0) = (S D^{n} F) (N)$
165	124 163 164	syl2anc	$⊢ φ \to (S D^{n} (S D^{n} F) (N)) (0) = (S D^{n} F) (N)$
166	165	dmeqd	$⊢ φ \to dom (S D^{n} (S D^{n} F) (N)) (0) = dom (S D^{n} F) (N)$
167	80 166	eleqtrrd	$⊢ φ \to B \in dom (S D^{n} (S D^{n} F) (N)) (0)$
168		eqid	$⊢ 0 (S Tayl (S D^{n} F) (N)) B = 0 (S Tayl (S D^{n} F) (N)) B$
169	1 117 3 161 167 168	taylpf	$⊢ φ \to (0 (S Tayl (S D^{n} F) (N)) B) : ℂ ⟶ ℂ$
170	119	addid2d	$⊢ φ \to 0 + N = N$
171	170	oveq1d	$⊢ φ \to (0 + N) (S Tayl F) B = N (S Tayl F) B$
172	171 7	eqtr4di	$⊢ φ \to (0 + N) (S Tayl F) B = T$
173	172	oveq2d	$⊢ φ \to ℂ D^{n} ((0 + N) (S Tayl F) B) = ℂ D^{n} T$
174	173	fveq1d	$⊢ φ \to (ℂ D^{n} ((0 + N) (S Tayl F) B)) (N) = (ℂ D^{n} T) (N)$
175	170	fveq2d	$⊢ φ \to (S D^{n} F) (0 + N) = (S D^{n} F) (N)$
176	175	dmeqd	$⊢ φ \to dom (S D^{n} F) (0 + N) = dom (S D^{n} F) (N)$
177	80 176	eleqtrrd	$⊢ φ \to B \in dom (S D^{n} F) (0 + N)$
178	1 2 3 75 161 177	dvntaylp	$⊢ φ \to (ℂ D^{n} ((0 + N) (S Tayl F) B)) (N) = 0 (S Tayl (S D^{n} F) (N)) B$
179	174 178	eqtr3d	$⊢ φ \to (ℂ D^{n} T) (N) = 0 (S Tayl (S D^{n} F) (N)) B$
180	179	feq1d	$⊢ φ \to ((ℂ D^{n} T) (N) : ℂ ⟶ ℂ \leftrightarrow (0 (S Tayl (S D^{n} F) (N)) B) : ℂ ⟶ ℂ)$
181	169 180	mpbird	$⊢ φ \to (ℂ D^{n} T) (N) : ℂ ⟶ ℂ$
182	181	ffvelrnda	$⊢ (φ \land y \in ℂ) \to (ℂ D^{n} T) (N) (y) \in ℂ$
183	133 182	syldan	$⊢ (φ \land y \in A) \to (ℂ D^{n} T) (N) (y) \in ℂ$
184	124	sselda	$⊢ (φ \land y \in S) \to y \in ℂ$
185	184 158	syldan	$⊢ (φ \land y \in S) \to (ℂ D^{n} T) (N - 1) (y) \in ℂ$
186	184 182	syldan	$⊢ (φ \land y \in S) \to (ℂ D^{n} T) (N) (y) \in ℂ$
187		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
188	187	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
189		toponmax	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ) \to ℂ \in TopOpen (ℂ_{fld})$
190	188 189	mp1i	$⊢ φ \to ℂ \in TopOpen (ℂ_{fld})$
191		df-ss	$⊢ S \subseteq ℂ \leftrightarrow S \cap ℂ = S$
192	124 191	sylib	$⊢ φ \to S \cap ℂ = S$
193		ssid	$⊢ ℂ \subseteq ℂ$
194	193	a1i	$⊢ φ \to ℂ \subseteq ℂ$
195		mapsspm	$⊢ ℂ^{ℂ} \subseteq ℂ ↑_{𝑝𝑚} ℂ$
196	1 2 3 75 80 7	taylpf	$⊢ φ \to T : ℂ ⟶ ℂ$
197	83 83	elmap	$⊢ T \in (ℂ^{ℂ}) \leftrightarrow T : ℂ ⟶ ℂ$
198	196 197	sylibr	$⊢ φ \to T \in (ℂ^{ℂ})$
199	195 198	sseldi	$⊢ φ \to T \in (ℂ ↑_{𝑝𝑚} ℂ)$
200		dvnp1	$⊢ (ℂ \subseteq ℂ \land T \in (ℂ ↑_{𝑝𝑚} ℂ) \land N - 1 \in ℕ_{0}) \to (ℂ D^{n} T) (N - 1 + 1) = ℂ D (ℂ D^{n} T) (N - 1)$
201	194 199 100 200	syl3anc	$⊢ φ \to (ℂ D^{n} T) (N - 1 + 1) = ℂ D (ℂ D^{n} T) (N - 1)$
202	121	fveq2d	$⊢ φ \to (ℂ D^{n} T) (N - 1 + 1) = (ℂ D^{n} T) (N)$
203	201 202	eqtr3d	$⊢ φ \to ℂ D (ℂ D^{n} T) (N - 1) = (ℂ D^{n} T) (N)$
204	157	feqmptd	$⊢ φ \to (ℂ D^{n} T) (N - 1) = (y \in ℂ ⟼ (ℂ D^{n} T) (N - 1) (y))$
205	204	oveq2d	$⊢ φ \to ℂ D (ℂ D^{n} T) (N - 1) = \frac{d (y \in ℂ⟼ (ℂ D^{n} T) (N - 1) (y))}{d_{ℂ} y}$
206	181	feqmptd	$⊢ φ \to (ℂ D^{n} T) (N) = (y \in ℂ ⟼ (ℂ D^{n} T) (N) (y))$
207	203 205 206	3eqtr3d	$⊢ φ \to \frac{d (y \in ℂ⟼ (ℂ D^{n} T) (N - 1) (y))}{d_{ℂ} y} = (y \in ℂ ⟼ (ℂ D^{n} T) (N) (y))$
208	187 1 190 192 158 182 207	dvmptres3	$⊢ φ \to \frac{d (y \in S⟼ (ℂ D^{n} T) (N - 1) (y))}{d_{S} y} = (y \in S ⟼ (ℂ D^{n} T) (N) (y))$
209		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} S = TopOpen (ℂ_{fld}) ↾_{𝑡} S$
210		resttopon	$⊢ (TopOpen (ℂ_{fld}) \in TopOn (ℂ) \land S \subseteq ℂ) \to TopOpen (ℂ_{fld}) ↾_{𝑡} S \in TopOn (S)$
211	188 124 210	sylancr	$⊢ φ \to TopOpen (ℂ_{fld}) ↾_{𝑡} S \in TopOn (S)$
212		topontop	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} S \in TopOn (S) \to TopOpen (ℂ_{fld}) ↾_{𝑡} S \in Top$
213	211 212	syl	$⊢ φ \to TopOpen (ℂ_{fld}) ↾_{𝑡} S \in Top$
214		toponuni	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} S \in TopOn (S) \to S = ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
215	211 214	syl	$⊢ φ \to S = ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
216	3 215	sseqtrd	$⊢ φ \to A \subseteq ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
217		eqid	$⊢ ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} S) = ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
218	217	ntrss2	$⊢ (TopOpen (ℂ_{fld}) ↾_{𝑡} S \in Top \land A \subseteq ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} S)) \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} S) (A) \subseteq A$
219	213 216 218	syl2anc	$⊢ φ \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} S) (A) \subseteq A$
220	140	dmeqd	$⊢ φ \to dom {(S D^{n} F) (N - 1)}_{S}^{'} = dom (S D^{n} F) (N)$
221	220 4	eqtrd	$⊢ φ \to dom {(S D^{n} F) (N - 1)}_{S}^{'} = A$
222	124 114 3 209 187	dvbssntr	$⊢ φ \to dom {(S D^{n} F) (N - 1)}_{S}^{'} \subseteq int (TopOpen (ℂ_{fld}) ↾_{𝑡} S) (A)$
223	221 222	eqsstrrd	$⊢ φ \to A \subseteq int (TopOpen (ℂ_{fld}) ↾_{𝑡} S) (A)$
224	219 223	eqssd	$⊢ φ \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} S) (A) = A$
225	1 185 186 208 3 209 187 224	dvmptres2	$⊢ φ \to \frac{d (y \in A⟼ (ℂ D^{n} T) (N - 1) (y))}{d_{S} y} = (y \in A ⟼ (ℂ D^{n} T) (N) (y))$
226	1 115 118 131 159 183 225	dvmptsub	$⊢ φ \to \frac{d (y \in A⟼ (S D^{n} F) (N - 1) (y) - (ℂ D^{n} T) (N - 1) (y))}{d_{S} y} = (y \in A ⟼ (S D^{n} F) (N) (y) - (ℂ D^{n} T) (N) (y))$
227	226	breqd	$⊢ φ \to (B \frac{d (y \in A⟼ (S D^{n} F) (N - 1) (y) - (ℂ D^{n} T) (N - 1) (y))}{d_{S} y} 0 \leftrightarrow B (y \in A ⟼ (S D^{n} F) (N) (y) - (ℂ D^{n} T) (N) (y)) 0)$
228	98 227	mpbird	$⊢ φ \to B \frac{d (y \in A⟼ (S D^{n} F) (N - 1) (y) - (ℂ D^{n} T) (N - 1) (y))}{d_{S} y} 0$
229		eqid	$⊢ (x \in (A ∖ \{B\}) ⟼ \frac{(y \in A ⟼ (S D^{n} F) (N - 1) (y) - (ℂ D^{n} T) (N - 1) (y)) (x) - (y \in A ⟼ (S D^{n} F) (N - 1) (y) - (ℂ D^{n} T) (N - 1) (y)) (B)}{x - B}) = (x \in (A ∖ \{B\}) ⟼ \frac{(y \in A ⟼ (S D^{n} F) (N - 1) (y) - (ℂ D^{n} T) (N - 1) (y)) (x) - (y \in A ⟼ (S D^{n} F) (N - 1) (y) - (ℂ D^{n} T) (N - 1) (y)) (B)}{x - B})$
230	115 159	subcld	$⊢ (φ \land y \in A) \to (S D^{n} F) (N - 1) (y) - (ℂ D^{n} T) (N - 1) (y) \in ℂ$
231	230	fmpttd	$⊢ φ \to (y \in A ⟼ (S D^{n} F) (N - 1) (y) - (ℂ D^{n} T) (N - 1) (y)) : A ⟶ ℂ$
232	209 187 229 124 231 3	eldv	$⊢ φ \to (B \frac{d (y \in A⟼ (S D^{n} F) (N - 1) (y) - (ℂ D^{n} T) (N - 1) (y))}{d_{S} y} 0 \leftrightarrow (B \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} S) (A) \land 0 \in ((x \in (A ∖ \{B\}) ⟼ \frac{(y \in A ⟼ (S D^{n} F) (N - 1) (y) - (ℂ D^{n} T) (N - 1) (y)) (x) - (y \in A ⟼ (S D^{n} F) (N - 1) (y) - (ℂ D^{n} T) (N - 1) (y)) (B)}{x - B}) {lim}_{ℂ} B)))$
233	228 232	mpbid	$⊢ φ \to (B \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} S) (A) \land 0 \in ((x \in (A ∖ \{B\}) ⟼ \frac{(y \in A ⟼ (S D^{n} F) (N - 1) (y) - (ℂ D^{n} T) (N - 1) (y)) (x) - (y \in A ⟼ (S D^{n} F) (N - 1) (y) - (ℂ D^{n} T) (N - 1) (y)) (B)}{x - B}) {lim}_{ℂ} B))$
234	233	simprd	$⊢ φ \to 0 \in ((x \in (A ∖ \{B\}) ⟼ \frac{(y \in A ⟼ (S D^{n} F) (N - 1) (y) - (ℂ D^{n} T) (N - 1) (y)) (x) - (y \in A ⟼ (S D^{n} F) (N - 1) (y) - (ℂ D^{n} T) (N - 1) (y)) (B)}{x - B}) {lim}_{ℂ} B)$
235		eldifi	$⊢ x \in (A ∖ \{B\}) \to x \in A$
236		fveq2	$⊢ y = x \to (S D^{n} F) (N - 1) (y) = (S D^{n} F) (N - 1) (x)$
237		fveq2	$⊢ y = x \to (ℂ D^{n} T) (N - 1) (y) = (ℂ D^{n} T) (N - 1) (x)$
238	236 237	oveq12d	$⊢ y = x \to (S D^{n} F) (N - 1) (y) - (ℂ D^{n} T) (N - 1) (y) = (S D^{n} F) (N - 1) (x) - (ℂ D^{n} T) (N - 1) (x)$
239		eqid	$⊢ (y \in A ⟼ (S D^{n} F) (N - 1) (y) - (ℂ D^{n} T) (N - 1) (y)) = (y \in A ⟼ (S D^{n} F) (N - 1) (y) - (ℂ D^{n} T) (N - 1) (y))$
240		ovex	$⊢ (S D^{n} F) (N - 1) (x) - (ℂ D^{n} T) (N - 1) (x) \in V$
241	238 239 240	fvmpt	$⊢ x \in A \to (y \in A ⟼ (S D^{n} F) (N - 1) (y) - (ℂ D^{n} T) (N - 1) (y)) (x) = (S D^{n} F) (N - 1) (x) - (ℂ D^{n} T) (N - 1) (x)$
242		fveq2	$⊢ y = B \to (S D^{n} F) (N - 1) (y) = (S D^{n} F) (N - 1) (B)$
243		fveq2	$⊢ y = B \to (ℂ D^{n} T) (N - 1) (y) = (ℂ D^{n} T) (N - 1) (B)$
244	242 243	oveq12d	$⊢ y = B \to (S D^{n} F) (N - 1) (y) - (ℂ D^{n} T) (N - 1) (y) = (S D^{n} F) (N - 1) (B) - (ℂ D^{n} T) (N - 1) (B)$
245		ovex	$⊢ (S D^{n} F) (N - 1) (B) - (ℂ D^{n} T) (N - 1) (B) \in V$
246	244 239 245	fvmpt	$⊢ B \in A \to (y \in A ⟼ (S D^{n} F) (N - 1) (y) - (ℂ D^{n} T) (N - 1) (y)) (B) = (S D^{n} F) (N - 1) (B) - (ℂ D^{n} T) (N - 1) (B)$
247	6 246	syl	$⊢ φ \to (y \in A ⟼ (S D^{n} F) (N - 1) (y) - (ℂ D^{n} T) (N - 1) (y)) (B) = (S D^{n} F) (N - 1) (B) - (ℂ D^{n} T) (N - 1) (B)$
248	1 2 3 108 80 7	dvntaylp0	$⊢ φ \to (ℂ D^{n} T) (N - 1) (B) = (S D^{n} F) (N - 1) (B)$
249	248	oveq2d	$⊢ φ \to (S D^{n} F) (N - 1) (B) - (ℂ D^{n} T) (N - 1) (B) = (S D^{n} F) (N - 1) (B) - (S D^{n} F) (N - 1) (B)$
250	114 6	ffvelrnd	$⊢ φ \to (S D^{n} F) (N - 1) (B) \in ℂ$
251	250	subidd	$⊢ φ \to (S D^{n} F) (N - 1) (B) - (S D^{n} F) (N - 1) (B) = 0$
252	247 249 251	3eqtrd	$⊢ φ \to (y \in A ⟼ (S D^{n} F) (N - 1) (y) - (ℂ D^{n} T) (N - 1) (y)) (B) = 0$
253	241 252	oveqan12rd	$⊢ (φ \land x \in A) \to (y \in A ⟼ (S D^{n} F) (N - 1) (y) - (ℂ D^{n} T) (N - 1) (y)) (x) - (y \in A ⟼ (S D^{n} F) (N - 1) (y) - (ℂ D^{n} T) (N - 1) (y)) (B) = (S D^{n} F) (N - 1) (x) - (ℂ D^{n} T) (N - 1) (x) - 0$
254	114	ffvelrnda	$⊢ (φ \land x \in A) \to (S D^{n} F) (N - 1) (x) \in ℂ$
255	132	sselda	$⊢ (φ \land x \in A) \to x \in ℂ$
256	157	ffvelrnda	$⊢ (φ \land x \in ℂ) \to (ℂ D^{n} T) (N - 1) (x) \in ℂ$
257	255 256	syldan	$⊢ (φ \land x \in A) \to (ℂ D^{n} T) (N - 1) (x) \in ℂ$
258	254 257	subcld	$⊢ (φ \land x \in A) \to (S D^{n} F) (N - 1) (x) - (ℂ D^{n} T) (N - 1) (x) \in ℂ$
259	258	subid1d	$⊢ (φ \land x \in A) \to (S D^{n} F) (N - 1) (x) - (ℂ D^{n} T) (N - 1) (x) - 0 = (S D^{n} F) (N - 1) (x) - (ℂ D^{n} T) (N - 1) (x)$
260	253 259	eqtr2d	$⊢ (φ \land x \in A) \to (S D^{n} F) (N - 1) (x) - (ℂ D^{n} T) (N - 1) (x) = (y \in A ⟼ (S D^{n} F) (N - 1) (y) - (ℂ D^{n} T) (N - 1) (y)) (x) - (y \in A ⟼ (S D^{n} F) (N - 1) (y) - (ℂ D^{n} T) (N - 1) (y)) (B)$
261	235 260	sylan2	$⊢ (φ \land x \in (A ∖ \{B\})) \to (S D^{n} F) (N - 1) (x) - (ℂ D^{n} T) (N - 1) (x) = (y \in A ⟼ (S D^{n} F) (N - 1) (y) - (ℂ D^{n} T) (N - 1) (y)) (x) - (y \in A ⟼ (S D^{n} F) (N - 1) (y) - (ℂ D^{n} T) (N - 1) (y)) (B)$
262	132	ssdifssd	$⊢ φ \to A ∖ \{B\} \subseteq ℂ$
263	262	sselda	$⊢ (φ \land x \in (A ∖ \{B\})) \to x \in ℂ$
264	132 6	sseldd	$⊢ φ \to B \in ℂ$
265	264	adantr	$⊢ (φ \land x \in (A ∖ \{B\})) \to B \in ℂ$
266	263 265	subcld	$⊢ (φ \land x \in (A ∖ \{B\})) \to x - B \in ℂ$
267	266	exp1d	$⊢ (φ \land x \in (A ∖ \{B\})) \to {(x - B)}^{1} = x - B$
268	261 267	oveq12d	$⊢ (φ \land x \in (A ∖ \{B\})) \to \frac{(S D^{n} F) (N - 1) (x) - (ℂ D^{n} T) (N - 1) (x)}{{(x - B)}^{1}} = \frac{(y \in A ⟼ (S D^{n} F) (N - 1) (y) - (ℂ D^{n} T) (N - 1) (y)) (x) - (y \in A ⟼ (S D^{n} F) (N - 1) (y) - (ℂ D^{n} T) (N - 1) (y)) (B)}{x - B}$
269	268	mpteq2dva	$⊢ φ \to (x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - 1) (x) - (ℂ D^{n} T) (N - 1) (x)}{{(x - B)}^{1}}) = (x \in (A ∖ \{B\}) ⟼ \frac{(y \in A ⟼ (S D^{n} F) (N - 1) (y) - (ℂ D^{n} T) (N - 1) (y)) (x) - (y \in A ⟼ (S D^{n} F) (N - 1) (y) - (ℂ D^{n} T) (N - 1) (y)) (B)}{x - B})$
270	269	oveq1d	$⊢ φ \to (x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - 1) (x) - (ℂ D^{n} T) (N - 1) (x)}{{(x - B)}^{1}}) {lim}_{ℂ} B = (x \in (A ∖ \{B\}) ⟼ \frac{(y \in A ⟼ (S D^{n} F) (N - 1) (y) - (ℂ D^{n} T) (N - 1) (y)) (x) - (y \in A ⟼ (S D^{n} F) (N - 1) (y) - (ℂ D^{n} T) (N - 1) (y)) (B)}{x - B}) {lim}_{ℂ} B$
271	234 270	eleqtrrd	$⊢ φ \to 0 \in ((x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - 1) (x) - (ℂ D^{n} T) (N - 1) (x)}{{(x - B)}^{1}}) {lim}_{ℂ} B)$
272	271	a1i	$⊢ N \in ℤ_{\geq 1} \to (φ \to 0 \in ((x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - 1) (x) - (ℂ D^{n} T) (N - 1) (x)}{{(x - B)}^{1}}) {lim}_{ℂ} B))$
273	9	expr	$⊢ (φ \land n \in (1 ..^N)) \to (0 \in ((y \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - n) (y) - (ℂ D^{n} T) (N - n) (y)}{{(y - B)}^{n}}) {lim}_{ℂ} B) \to 0 \in ((x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - (n + 1)) (x) - (ℂ D^{n} T) (N - (n + 1)) (x)}{{(x - B)}^{n + 1}}) {lim}_{ℂ} B))$
274	273	expcom	$⊢ n \in (1 ..^N) \to (φ \to (0 \in ((y \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - n) (y) - (ℂ D^{n} T) (N - n) (y)}{{(y - B)}^{n}}) {lim}_{ℂ} B) \to 0 \in ((x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - (n + 1)) (x) - (ℂ D^{n} T) (N - (n + 1)) (x)}{{(x - B)}^{n + 1}}) {lim}_{ℂ} B)))$
275	274	a2d	$⊢ n \in (1 ..^N) \to ((φ \to 0 \in ((y \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - n) (y) - (ℂ D^{n} T) (N - n) (y)}{{(y - B)}^{n}}) {lim}_{ℂ} B)) \to (φ \to 0 \in ((x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - (n + 1)) (x) - (ℂ D^{n} T) (N - (n + 1)) (x)}{{(x - B)}^{n + 1}}) {lim}_{ℂ} B)))$
276	23 43 55 67 272 275	fzind2	$⊢ N \in (1 \dots N) \to (φ \to 0 \in ((x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - N) (x) - (ℂ D^{n} T) (N - N) (x)}{{(x - B)}^{N}}) {lim}_{ℂ} B))$
277	11 276	mpcom	$⊢ φ \to 0 \in ((x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - N) (x) - (ℂ D^{n} T) (N - N) (x)}{{(x - B)}^{N}}) {lim}_{ℂ} B)$
278	119	subidd	$⊢ φ \to N - N = 0$
279	278	fveq2d	$⊢ φ \to (S D^{n} F) (N - N) = (S D^{n} F) (0)$
280		dvn0	$⊢ (S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S)) \to (S D^{n} F) (0) = F$
281	124 86 280	syl2anc	$⊢ φ \to (S D^{n} F) (0) = F$
282	279 281	eqtrd	$⊢ φ \to (S D^{n} F) (N - N) = F$
283	282	fveq1d	$⊢ φ \to (S D^{n} F) (N - N) (x) = F (x)$
284	278	fveq2d	$⊢ φ \to (ℂ D^{n} T) (N - N) = (ℂ D^{n} T) (0)$
285		dvn0	$⊢ (ℂ \subseteq ℂ \land T \in (ℂ ↑_{𝑝𝑚} ℂ)) \to (ℂ D^{n} T) (0) = T$
286	193 199 285	sylancr	$⊢ φ \to (ℂ D^{n} T) (0) = T$
287	284 286	eqtrd	$⊢ φ \to (ℂ D^{n} T) (N - N) = T$
288	287	fveq1d	$⊢ φ \to (ℂ D^{n} T) (N - N) (x) = T (x)$
289	283 288	oveq12d	$⊢ φ \to (S D^{n} F) (N - N) (x) - (ℂ D^{n} T) (N - N) (x) = F (x) - T (x)$
290	289	oveq1d	$⊢ φ \to \frac{(S D^{n} F) (N - N) (x) - (ℂ D^{n} T) (N - N) (x)}{{(x - B)}^{N}} = \frac{F (x) - T (x)}{{(x - B)}^{N}}$
291	290	mpteq2dv	$⊢ φ \to (x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - N) (x) - (ℂ D^{n} T) (N - N) (x)}{{(x - B)}^{N}}) = (x \in (A ∖ \{B\}) ⟼ \frac{F (x) - T (x)}{{(x - B)}^{N}})$
292	291 8	eqtr4di	$⊢ φ \to (x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - N) (x) - (ℂ D^{n} T) (N - N) (x)}{{(x - B)}^{N}}) = R$
293	292	oveq1d	$⊢ φ \to (x \in (A ∖ \{B\}) ⟼ \frac{(S D^{n} F) (N - N) (x) - (ℂ D^{n} T) (N - N) (x)}{{(x - B)}^{N}}) {lim}_{ℂ} B = R {lim}_{ℂ} B$
294	277 293	eleqtrd	$⊢ φ \to 0 \in (R {lim}_{ℂ} B)$

Metamath Proof Explorer

Theorem taylthlem1

Proof