taylthlem2

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

Proof

Step	Hyp	Ref	Expression
1		taylth.f	$⊢ φ \to F : A ⟶ ℝ$
2		taylth.a	$⊢ φ \to A \subseteq ℝ$
3		taylth.d	$⊢ φ \to dom (ℝ D^{n} F) (N) = A$
4		taylth.n	$⊢ φ \to N \in ℕ$
5		taylth.b	$⊢ φ \to B \in A$
6		taylth.t	$⊢ T = N (ℝ Tayl F) B$
7		taylthlem2.m	$⊢ φ \to M \in (1 ..^N)$
8		taylthlem2.i	$⊢ φ \to 0 \in ((x \in (A ∖ \{B\}) ⟼ \frac{(ℝ D^{n} F) (N - M) (x) - (ℂ D^{n} T) (N - M) (x)}{{(x - B)}^{M}}) {lim}_{ℂ} B)$
9		fz1ssfz0	$⊢ (1 \dots N) \subseteq (0 \dots N)$
10		fzofzp1	$⊢ M \in (1 ..^N) \to M + 1 \in (1 \dots N)$
11	7 10	syl	$⊢ φ \to M + 1 \in (1 \dots N)$
12	9 11	sselid	$⊢ φ \to M + 1 \in (0 \dots N)$
13		fznn0sub2	$⊢ M + 1 \in (0 \dots N) \to N - (M + 1) \in (0 \dots N)$
14	12 13	syl	$⊢ φ \to N - (M + 1) \in (0 \dots N)$
15		elfznn0	$⊢ N - (M + 1) \in (0 \dots N) \to N - (M + 1) \in ℕ_{0}$
16	14 15	syl	$⊢ φ \to N - (M + 1) \in ℕ_{0}$
17		dvnfre	$⊢ (F : A ⟶ ℝ \land A \subseteq ℝ \land N - (M + 1) \in ℕ_{0}) \to (ℝ D^{n} F) (N - (M + 1)) : dom (ℝ D^{n} F) (N - (M + 1)) ⟶ ℝ$
18	1 2 16 17	syl3anc	$⊢ φ \to (ℝ D^{n} F) (N - (M + 1)) : dom (ℝ D^{n} F) (N - (M + 1)) ⟶ ℝ$
19		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
20	19	a1i	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
21		cnex	$⊢ ℂ \in V$
22	21	a1i	$⊢ φ \to ℂ \in V$
23		reex	$⊢ ℝ \in V$
24	23	a1i	$⊢ φ \to ℝ \in V$
25		ax-resscn	$⊢ ℝ \subseteq ℂ$
26		fss	$⊢ (F : A ⟶ ℝ \land ℝ \subseteq ℂ) \to F : A ⟶ ℂ$
27	1 25 26	sylancl	$⊢ φ \to F : A ⟶ ℂ$
28		elpm2r	$⊢ ((ℂ \in V \land ℝ \in V) \land (F : A ⟶ ℂ \land A \subseteq ℝ)) \to F \in (ℂ ↑_{𝑝𝑚} ℝ)$
29	22 24 27 2 28	syl22anc	$⊢ φ \to F \in (ℂ ↑_{𝑝𝑚} ℝ)$
30		dvnbss	$⊢ (ℝ \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℝ) \land N - (M + 1) \in ℕ_{0}) \to dom (ℝ D^{n} F) (N - (M + 1)) \subseteq dom F$
31	20 29 16 30	syl3anc	$⊢ φ \to dom (ℝ D^{n} F) (N - (M + 1)) \subseteq dom F$
32	1 31	fssdmd	$⊢ φ \to dom (ℝ D^{n} F) (N - (M + 1)) \subseteq A$
33		dvn2bss	$⊢ (ℝ \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℝ) \land N - (M + 1) \in (0 \dots N)) \to dom (ℝ D^{n} F) (N) \subseteq dom (ℝ D^{n} F) (N - (M + 1))$
34	20 29 14 33	syl3anc	$⊢ φ \to dom (ℝ D^{n} F) (N) \subseteq dom (ℝ D^{n} F) (N - (M + 1))$
35	3 34	eqsstrrd	$⊢ φ \to A \subseteq dom (ℝ D^{n} F) (N - (M + 1))$
36	32 35	eqssd	$⊢ φ \to dom (ℝ D^{n} F) (N - (M + 1)) = A$
37	36	feq2d	$⊢ φ \to ((ℝ D^{n} F) (N - (M + 1)) : dom (ℝ D^{n} F) (N - (M + 1)) ⟶ ℝ \leftrightarrow (ℝ D^{n} F) (N - (M + 1)) : A ⟶ ℝ)$
38	18 37	mpbid	$⊢ φ \to (ℝ D^{n} F) (N - (M + 1)) : A ⟶ ℝ$
39	38	ffvelrnda	$⊢ (φ \land y \in A) \to (ℝ D^{n} F) (N - (M + 1)) (y) \in ℝ$
40	2	sselda	$⊢ (φ \land y \in A) \to y \in ℝ$
41		fvres	$⊢ y \in ℝ \to ({(ℂ D^{n} T) (N - (M + 1)) ↾}_{ℝ}) (y) = (ℂ D^{n} T) (N - (M + 1)) (y)$
42	41	adantl	$⊢ (φ \land y \in ℝ) \to ({(ℂ D^{n} T) (N - (M + 1)) ↾}_{ℝ}) (y) = (ℂ D^{n} T) (N - (M + 1)) (y)$
43		resubdrg	$⊢ (ℝ \in SubRing (ℂ_{fld}) \land ℝ_{fld} \in DivRing)$
44	43	simpli	$⊢ ℝ \in SubRing (ℂ_{fld})$
45	44	a1i	$⊢ φ \to ℝ \in SubRing (ℂ_{fld})$
46	4	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
47	5 3	eleqtrrd	$⊢ φ \to B \in dom (ℝ D^{n} F) (N)$
48	2 5	sseldd	$⊢ φ \to B \in ℝ$
49		elfznn0	$⊢ k \in (0 \dots N) \to k \in ℕ_{0}$
50		dvnfre	$⊢ (F : A ⟶ ℝ \land A \subseteq ℝ \land k \in ℕ_{0}) \to (ℝ D^{n} F) (k) : dom (ℝ D^{n} F) (k) ⟶ ℝ$
51	1 2 49 50	syl2an3an	$⊢ (φ \land k \in (0 \dots N)) \to (ℝ D^{n} F) (k) : dom (ℝ D^{n} F) (k) ⟶ ℝ$
52		simpr	$⊢ (φ \land k \in (0 \dots N)) \to k \in (0 \dots N)$
53		dvn2bss	$⊢ (ℝ \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℝ) \land k \in (0 \dots N)) \to dom (ℝ D^{n} F) (N) \subseteq dom (ℝ D^{n} F) (k)$
54	19 29 52 53	mp3an2ani	$⊢ (φ \land k \in (0 \dots N)) \to dom (ℝ D^{n} F) (N) \subseteq dom (ℝ D^{n} F) (k)$
55	47	adantr	$⊢ (φ \land k \in (0 \dots N)) \to B \in dom (ℝ D^{n} F) (N)$
56	54 55	sseldd	$⊢ (φ \land k \in (0 \dots N)) \to B \in dom (ℝ D^{n} F) (k)$
57	51 56	ffvelrnd	$⊢ (φ \land k \in (0 \dots N)) \to (ℝ D^{n} F) (k) (B) \in ℝ$
58	49	adantl	$⊢ (φ \land k \in (0 \dots N)) \to k \in ℕ_{0}$
59	58	faccld	$⊢ (φ \land k \in (0 \dots N)) \to k! \in ℕ$
60	57 59	nndivred	$⊢ (φ \land k \in (0 \dots N)) \to \frac{(ℝ D^{n} F) (k) (B)}{k!} \in ℝ$
61	20 27 2 46 47 6 45 48 60	taylply2	$⊢ φ \to (T \in Poly (ℝ) \land \deg (T) \leq N)$
62	61	simpld	$⊢ φ \to T \in Poly (ℝ)$
63		dvnply2	$⊢ (ℝ \in SubRing (ℂ_{fld}) \land T \in Poly (ℝ) \land N - (M + 1) \in ℕ_{0}) \to (ℂ D^{n} T) (N - (M + 1)) \in Poly (ℝ)$
64	45 62 16 63	syl3anc	$⊢ φ \to (ℂ D^{n} T) (N - (M + 1)) \in Poly (ℝ)$
65		plyreres	$⊢ (ℂ D^{n} T) (N - (M + 1)) \in Poly (ℝ) \to ({(ℂ D^{n} T) (N - (M + 1)) ↾}_{ℝ}) : ℝ ⟶ ℝ$
66	64 65	syl	$⊢ φ \to ({(ℂ D^{n} T) (N - (M + 1)) ↾}_{ℝ}) : ℝ ⟶ ℝ$
67	66	ffvelrnda	$⊢ (φ \land y \in ℝ) \to ({(ℂ D^{n} T) (N - (M + 1)) ↾}_{ℝ}) (y) \in ℝ$
68	42 67	eqeltrrd	$⊢ (φ \land y \in ℝ) \to (ℂ D^{n} T) (N - (M + 1)) (y) \in ℝ$
69	40 68	syldan	$⊢ (φ \land y \in A) \to (ℂ D^{n} T) (N - (M + 1)) (y) \in ℝ$
70	39 69	resubcld	$⊢ (φ \land y \in A) \to (ℝ D^{n} F) (N - (M + 1)) (y) - (ℂ D^{n} T) (N - (M + 1)) (y) \in ℝ$
71	70	fmpttd	$⊢ φ \to (y \in A ⟼ (ℝ D^{n} F) (N - (M + 1)) (y) - (ℂ D^{n} T) (N - (M + 1)) (y)) : A ⟶ ℝ$
72	48	adantr	$⊢ (φ \land y \in A) \to B \in ℝ$
73	40 72	resubcld	$⊢ (φ \land y \in A) \to y - B \in ℝ$
74		elfzouz	$⊢ M \in (1 ..^N) \to M \in ℤ_{\geq 1}$
75	7 74	syl	$⊢ φ \to M \in ℤ_{\geq 1}$
76		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
77	75 76	eleqtrrdi	$⊢ φ \to M \in ℕ$
78	77	nnnn0d	$⊢ φ \to M \in ℕ_{0}$
79	78	adantr	$⊢ (φ \land y \in A) \to M \in ℕ_{0}$
80		1nn0	$⊢ 1 \in ℕ_{0}$
81	80	a1i	$⊢ (φ \land y \in A) \to 1 \in ℕ_{0}$
82	79 81	nn0addcld	$⊢ (φ \land y \in A) \to M + 1 \in ℕ_{0}$
83	73 82	reexpcld	$⊢ (φ \land y \in A) \to {(y - B)}^{M + 1} \in ℝ$
84	83	fmpttd	$⊢ φ \to (y \in A ⟼ {(y - B)}^{M + 1}) : A ⟶ ℝ$
85		retop	$⊢ topGen (ran (.)) \in Top$
86		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
87	86	ntrss2	$⊢ (topGen (ran (.)) \in Top \land A \subseteq ℝ) \to int (topGen (ran (.))) (A) \subseteq A$
88	85 2 87	sylancr	$⊢ φ \to int (topGen (ran (.))) (A) \subseteq A$
89	4	nncnd	$⊢ φ \to N \in ℂ$
90	77	nncnd	$⊢ φ \to M \in ℂ$
91		1cnd	$⊢ φ \to 1 \in ℂ$
92	89 90 91	nppcan2d	$⊢ φ \to N - (M + 1) + 1 = N - M$
93	92	fveq2d	$⊢ φ \to (ℝ D^{n} F) (N - (M + 1) + 1) = (ℝ D^{n} F) (N - M)$
94	25	a1i	$⊢ φ \to ℝ \subseteq ℂ$
95		dvnp1	$⊢ (ℝ \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} ℝ) \land N - (M + 1) \in ℕ_{0}) \to (ℝ D^{n} F) (N - (M + 1) + 1) = ℝ D (ℝ D^{n} F) (N - (M + 1))$
96	94 29 16 95	syl3anc	$⊢ φ \to (ℝ D^{n} F) (N - (M + 1) + 1) = ℝ D (ℝ D^{n} F) (N - (M + 1))$
97	93 96	eqtr3d	$⊢ φ \to (ℝ D^{n} F) (N - M) = ℝ D (ℝ D^{n} F) (N - (M + 1))$
98	97	dmeqd	$⊢ φ \to dom (ℝ D^{n} F) (N - M) = dom {(ℝ D^{n} F) (N - (M + 1))}_{ℝ}^{'}$
99		fzonnsub	$⊢ M \in (1 ..^N) \to N - M \in ℕ$
100	7 99	syl	$⊢ φ \to N - M \in ℕ$
101	100	nnnn0d	$⊢ φ \to N - M \in ℕ_{0}$
102		dvnbss	$⊢ (ℝ \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℝ) \land N - M \in ℕ_{0}) \to dom (ℝ D^{n} F) (N - M) \subseteq dom F$
103	20 29 101 102	syl3anc	$⊢ φ \to dom (ℝ D^{n} F) (N - M) \subseteq dom F$
104	1 103	fssdmd	$⊢ φ \to dom (ℝ D^{n} F) (N - M) \subseteq A$
105		elfzofz	$⊢ M \in (1 ..^N) \to M \in (1 \dots N)$
106	7 105	syl	$⊢ φ \to M \in (1 \dots N)$
107	9 106	sselid	$⊢ φ \to M \in (0 \dots N)$
108		fznn0sub2	$⊢ M \in (0 \dots N) \to N - M \in (0 \dots N)$
109	107 108	syl	$⊢ φ \to N - M \in (0 \dots N)$
110		dvn2bss	$⊢ (ℝ \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℝ) \land N - M \in (0 \dots N)) \to dom (ℝ D^{n} F) (N) \subseteq dom (ℝ D^{n} F) (N - M)$
111	20 29 109 110	syl3anc	$⊢ φ \to dom (ℝ D^{n} F) (N) \subseteq dom (ℝ D^{n} F) (N - M)$
112	3 111	eqsstrrd	$⊢ φ \to A \subseteq dom (ℝ D^{n} F) (N - M)$
113	104 112	eqssd	$⊢ φ \to dom (ℝ D^{n} F) (N - M) = A$
114	98 113	eqtr3d	$⊢ φ \to dom {(ℝ D^{n} F) (N - (M + 1))}_{ℝ}^{'} = A$
115		fss	$⊢ ((ℝ D^{n} F) (N - (M + 1)) : A ⟶ ℝ \land ℝ \subseteq ℂ) \to (ℝ D^{n} F) (N - (M + 1)) : A ⟶ ℂ$
116	38 25 115	sylancl	$⊢ φ \to (ℝ D^{n} F) (N - (M + 1)) : A ⟶ ℂ$
117		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
118	117	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
119	94 116 2 118 117	dvbssntr	$⊢ φ \to dom {(ℝ D^{n} F) (N - (M + 1))}_{ℝ}^{'} \subseteq int (topGen (ran (.))) (A)$
120	114 119	eqsstrrd	$⊢ φ \to A \subseteq int (topGen (ran (.))) (A)$
121	88 120	eqssd	$⊢ φ \to int (topGen (ran (.))) (A) = A$
122	86	isopn3	$⊢ (topGen (ran (.)) \in Top \land A \subseteq ℝ) \to (A \in topGen (ran (.)) \leftrightarrow int (topGen (ran (.))) (A) = A)$
123	85 2 122	sylancr	$⊢ φ \to (A \in topGen (ran (.)) \leftrightarrow int (topGen (ran (.))) (A) = A)$
124	121 123	mpbird	$⊢ φ \to A \in topGen (ran (.))$
125		eqid	$⊢ A ∖ \{B\} = A ∖ \{B\}$
126		difss	$⊢ A ∖ \{B\} \subseteq A$
127	39	recnd	$⊢ (φ \land y \in A) \to (ℝ D^{n} F) (N - (M + 1)) (y) \in ℂ$
128		dvnf	$⊢ (ℝ \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} ℝ) \land N - M \in ℕ_{0}) \to (ℝ D^{n} F) (N - M) : dom (ℝ D^{n} F) (N - M) ⟶ ℂ$
129	20 29 101 128	syl3anc	$⊢ φ \to (ℝ D^{n} F) (N - M) : dom (ℝ D^{n} F) (N - M) ⟶ ℂ$
130	113	feq2d	$⊢ φ \to ((ℝ D^{n} F) (N - M) : dom (ℝ D^{n} F) (N - M) ⟶ ℂ \leftrightarrow (ℝ D^{n} F) (N - M) : A ⟶ ℂ)$
131	129 130	mpbid	$⊢ φ \to (ℝ D^{n} F) (N - M) : A ⟶ ℂ$
132	131	ffvelrnda	$⊢ (φ \land y \in A) \to (ℝ D^{n} F) (N - M) (y) \in ℂ$
133		dvnfre	$⊢ (F : A ⟶ ℝ \land A \subseteq ℝ \land N - M \in ℕ_{0}) \to (ℝ D^{n} F) (N - M) : dom (ℝ D^{n} F) (N - M) ⟶ ℝ$
134	1 2 101 133	syl3anc	$⊢ φ \to (ℝ D^{n} F) (N - M) : dom (ℝ D^{n} F) (N - M) ⟶ ℝ$
135	113	feq2d	$⊢ φ \to ((ℝ D^{n} F) (N - M) : dom (ℝ D^{n} F) (N - M) ⟶ ℝ \leftrightarrow (ℝ D^{n} F) (N - M) : A ⟶ ℝ)$
136	134 135	mpbid	$⊢ φ \to (ℝ D^{n} F) (N - M) : A ⟶ ℝ$
137	136	feqmptd	$⊢ φ \to (ℝ D^{n} F) (N - M) = (y \in A ⟼ (ℝ D^{n} F) (N - M) (y))$
138	38	feqmptd	$⊢ φ \to (ℝ D^{n} F) (N - (M + 1)) = (y \in A ⟼ (ℝ D^{n} F) (N - (M + 1)) (y))$
139	138	oveq2d	$⊢ φ \to ℝ D (ℝ D^{n} F) (N - (M + 1)) = \frac{d (y \in A⟼ (ℝ D^{n} F) (N - (M + 1)) (y))}{d_{ℝ} y}$
140	97 137 139	3eqtr3rd	$⊢ φ \to \frac{d (y \in A⟼ (ℝ D^{n} F) (N - (M + 1)) (y))}{d_{ℝ} y} = (y \in A ⟼ (ℝ D^{n} F) (N - M) (y))$
141	69	recnd	$⊢ (φ \land y \in A) \to (ℂ D^{n} T) (N - (M + 1)) (y) \in ℂ$
142		fvexd	$⊢ (φ \land y \in A) \to (ℂ D^{n} T) (N - M) (y) \in V$
143	68	recnd	$⊢ (φ \land y \in ℝ) \to (ℂ D^{n} T) (N - (M + 1)) (y) \in ℂ$
144		recn	$⊢ y \in ℝ \to y \in ℂ$
145		dvnply2	$⊢ (ℝ \in SubRing (ℂ_{fld}) \land T \in Poly (ℝ) \land N - M \in ℕ_{0}) \to (ℂ D^{n} T) (N - M) \in Poly (ℝ)$
146	45 62 101 145	syl3anc	$⊢ φ \to (ℂ D^{n} T) (N - M) \in Poly (ℝ)$
147		plyf	$⊢ (ℂ D^{n} T) (N - M) \in Poly (ℝ) \to (ℂ D^{n} T) (N - M) : ℂ ⟶ ℂ$
148	146 147	syl	$⊢ φ \to (ℂ D^{n} T) (N - M) : ℂ ⟶ ℂ$
149	148	ffvelrnda	$⊢ (φ \land y \in ℂ) \to (ℂ D^{n} T) (N - M) (y) \in ℂ$
150	144 149	sylan2	$⊢ (φ \land y \in ℝ) \to (ℂ D^{n} T) (N - M) (y) \in ℂ$
151	117	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
152		toponmax	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ) \to ℂ \in TopOpen (ℂ_{fld})$
153	151 152	mp1i	$⊢ φ \to ℂ \in TopOpen (ℂ_{fld})$
154		df-ss	$⊢ ℝ \subseteq ℂ \leftrightarrow ℝ \cap ℂ = ℝ$
155	94 154	sylib	$⊢ φ \to ℝ \cap ℂ = ℝ$
156		plyf	$⊢ (ℂ D^{n} T) (N - (M + 1)) \in Poly (ℝ) \to (ℂ D^{n} T) (N - (M + 1)) : ℂ ⟶ ℂ$
157	64 156	syl	$⊢ φ \to (ℂ D^{n} T) (N - (M + 1)) : ℂ ⟶ ℂ$
158	157	ffvelrnda	$⊢ (φ \land y \in ℂ) \to (ℂ D^{n} T) (N - (M + 1)) (y) \in ℂ$
159	92	fveq2d	$⊢ φ \to (ℂ D^{n} T) (N - (M + 1) + 1) = (ℂ D^{n} T) (N - M)$
160		ssid	$⊢ ℂ \subseteq ℂ$
161	160	a1i	$⊢ φ \to ℂ \subseteq ℂ$
162		mapsspm	$⊢ ℂ^{ℂ} \subseteq ℂ ↑_{𝑝𝑚} ℂ$
163		plyf	$⊢ T \in Poly (ℝ) \to T : ℂ ⟶ ℂ$
164	62 163	syl	$⊢ φ \to T : ℂ ⟶ ℂ$
165	21 21	elmap	$⊢ T \in (ℂ^{ℂ}) \leftrightarrow T : ℂ ⟶ ℂ$
166	164 165	sylibr	$⊢ φ \to T \in (ℂ^{ℂ})$
167	162 166	sselid	$⊢ φ \to T \in (ℂ ↑_{𝑝𝑚} ℂ)$
168		dvnp1	$⊢ (ℂ \subseteq ℂ \land T \in (ℂ ↑_{𝑝𝑚} ℂ) \land N - (M + 1) \in ℕ_{0}) \to (ℂ D^{n} T) (N - (M + 1) + 1) = ℂ D (ℂ D^{n} T) (N - (M + 1))$
169	161 167 16 168	syl3anc	$⊢ φ \to (ℂ D^{n} T) (N - (M + 1) + 1) = ℂ D (ℂ D^{n} T) (N - (M + 1))$
170	159 169	eqtr3d	$⊢ φ \to (ℂ D^{n} T) (N - M) = ℂ D (ℂ D^{n} T) (N - (M + 1))$
171	148	feqmptd	$⊢ φ \to (ℂ D^{n} T) (N - M) = (y \in ℂ ⟼ (ℂ D^{n} T) (N - M) (y))$
172	157	feqmptd	$⊢ φ \to (ℂ D^{n} T) (N - (M + 1)) = (y \in ℂ ⟼ (ℂ D^{n} T) (N - (M + 1)) (y))$
173	172	oveq2d	$⊢ φ \to ℂ D (ℂ D^{n} T) (N - (M + 1)) = \frac{d (y \in ℂ⟼ (ℂ D^{n} T) (N - (M + 1)) (y))}{d_{ℂ} y}$
174	170 171 173	3eqtr3rd	$⊢ φ \to \frac{d (y \in ℂ⟼ (ℂ D^{n} T) (N - (M + 1)) (y))}{d_{ℂ} y} = (y \in ℂ ⟼ (ℂ D^{n} T) (N - M) (y))$
175	117 20 153 155 158 149 174	dvmptres3	$⊢ φ \to \frac{d (y \in ℝ⟼ (ℂ D^{n} T) (N - (M + 1)) (y))}{d_{ℝ} y} = (y \in ℝ ⟼ (ℂ D^{n} T) (N - M) (y))$
176	20 143 150 175 2 118 117 124	dvmptres	$⊢ φ \to \frac{d (y \in A⟼ (ℂ D^{n} T) (N - (M + 1)) (y))}{d_{ℝ} y} = (y \in A ⟼ (ℂ D^{n} T) (N - M) (y))$
177	20 127 132 140 141 142 176	dvmptsub	$⊢ φ \to \frac{d (y \in A⟼ (ℝ D^{n} F) (N - (M + 1)) (y) - (ℂ D^{n} T) (N - (M + 1)) (y))}{d_{ℝ} y} = (y \in A ⟼ (ℝ D^{n} F) (N - M) (y) - (ℂ D^{n} T) (N - M) (y))$
178	177	dmeqd	$⊢ φ \to dom \frac{d (y \in A⟼ (ℝ D^{n} F) (N - (M + 1)) (y) - (ℂ D^{n} T) (N - (M + 1)) (y))}{d_{ℝ} y} = dom (y \in A ⟼ (ℝ D^{n} F) (N - M) (y) - (ℂ D^{n} T) (N - M) (y))$
179		ovex	$⊢ (ℝ D^{n} F) (N - M) (y) - (ℂ D^{n} T) (N - M) (y) \in V$
180		eqid	$⊢ (y \in A ⟼ (ℝ D^{n} F) (N - M) (y) - (ℂ D^{n} T) (N - M) (y)) = (y \in A ⟼ (ℝ D^{n} F) (N - M) (y) - (ℂ D^{n} T) (N - M) (y))$
181	179 180	dmmpti	$⊢ dom (y \in A ⟼ (ℝ D^{n} F) (N - M) (y) - (ℂ D^{n} T) (N - M) (y)) = A$
182	178 181	eqtrdi	$⊢ φ \to dom \frac{d (y \in A⟼ (ℝ D^{n} F) (N - (M + 1)) (y) - (ℂ D^{n} T) (N - (M + 1)) (y))}{d_{ℝ} y} = A$
183	126 182	sseqtrrid	$⊢ φ \to A ∖ \{B\} \subseteq dom \frac{d (y \in A⟼ (ℝ D^{n} F) (N - (M + 1)) (y) - (ℂ D^{n} T) (N - (M + 1)) (y))}{d_{ℝ} y}$
184		simpr	$⊢ (φ \land y \in ℂ) \to y \in ℂ$
185	48	adantr	$⊢ (φ \land y \in ℂ) \to B \in ℝ$
186	185	recnd	$⊢ (φ \land y \in ℂ) \to B \in ℂ$
187	184 186	subcld	$⊢ (φ \land y \in ℂ) \to y - B \in ℂ$
188	78	adantr	$⊢ (φ \land y \in ℂ) \to M \in ℕ_{0}$
189	80	a1i	$⊢ (φ \land y \in ℂ) \to 1 \in ℕ_{0}$
190	188 189	nn0addcld	$⊢ (φ \land y \in ℂ) \to M + 1 \in ℕ_{0}$
191	187 190	expcld	$⊢ (φ \land y \in ℂ) \to {(y - B)}^{M + 1} \in ℂ$
192	144 191	sylan2	$⊢ (φ \land y \in ℝ) \to {(y - B)}^{M + 1} \in ℂ$
193	90	adantr	$⊢ (φ \land y \in ℂ) \to M \in ℂ$
194		1cnd	$⊢ (φ \land y \in ℂ) \to 1 \in ℂ$
195	193 194	addcld	$⊢ (φ \land y \in ℂ) \to M + 1 \in ℂ$
196	187 188	expcld	$⊢ (φ \land y \in ℂ) \to {(y - B)}^{M} \in ℂ$
197	195 196	mulcld	$⊢ (φ \land y \in ℂ) \to (M + 1) {(y - B)}^{M} \in ℂ$
198	144 197	sylan2	$⊢ (φ \land y \in ℝ) \to (M + 1) {(y - B)}^{M} \in ℂ$
199	21	prid2	$⊢ ℂ \in \{ℝ, ℂ\}$
200	199	a1i	$⊢ φ \to ℂ \in \{ℝ, ℂ\}$
201		simpr	$⊢ (φ \land x \in ℂ) \to x \in ℂ$
202		elfznn	$⊢ M + 1 \in (1 \dots N) \to M + 1 \in ℕ$
203	11 202	syl	$⊢ φ \to M + 1 \in ℕ$
204	203	nnnn0d	$⊢ φ \to M + 1 \in ℕ_{0}$
205	204	adantr	$⊢ (φ \land x \in ℂ) \to M + 1 \in ℕ_{0}$
206	201 205	expcld	$⊢ (φ \land x \in ℂ) \to x^{M + 1} \in ℂ$
207		ovexd	$⊢ (φ \land x \in ℂ) \to (M + 1) x^{M} \in V$
208	200	dvmptid	$⊢ φ \to \frac{d (y \in ℂ⟼ y)}{d_{ℂ} y} = (y \in ℂ ⟼ 1)$
209		0cnd	$⊢ (φ \land y \in ℂ) \to 0 \in ℂ$
210	48	recnd	$⊢ φ \to B \in ℂ$
211	200 210	dvmptc	$⊢ φ \to \frac{d (y \in ℂ⟼ B)}{d_{ℂ} y} = (y \in ℂ ⟼ 0)$
212	200 184 194 208 186 209 211	dvmptsub	$⊢ φ \to \frac{d (y \in ℂ⟼ y - B)}{d_{ℂ} y} = (y \in ℂ ⟼ 1 - 0)$
213		1m0e1	$⊢ 1 - 0 = 1$
214	213	mpteq2i	$⊢ (y \in ℂ ⟼ 1 - 0) = (y \in ℂ ⟼ 1)$
215	212 214	eqtrdi	$⊢ φ \to \frac{d (y \in ℂ⟼ y - B)}{d_{ℂ} y} = (y \in ℂ ⟼ 1)$
216		dvexp	$⊢ M + 1 \in ℕ \to \frac{d (x \in ℂ⟼ x^{M + 1})}{d_{ℂ} x} = (x \in ℂ ⟼ (M + 1) x^{M + 1 - 1})$
217	203 216	syl	$⊢ φ \to \frac{d (x \in ℂ⟼ x^{M + 1})}{d_{ℂ} x} = (x \in ℂ ⟼ (M + 1) x^{M + 1 - 1})$
218	90 91	pncand	$⊢ φ \to M + 1 - 1 = M$
219	218	oveq2d	$⊢ φ \to x^{M + 1 - 1} = x^{M}$
220	219	oveq2d	$⊢ φ \to (M + 1) x^{M + 1 - 1} = (M + 1) x^{M}$
221	220	mpteq2dv	$⊢ φ \to (x \in ℂ ⟼ (M + 1) x^{M + 1 - 1}) = (x \in ℂ ⟼ (M + 1) x^{M})$
222	217 221	eqtrd	$⊢ φ \to \frac{d (x \in ℂ⟼ x^{M + 1})}{d_{ℂ} x} = (x \in ℂ ⟼ (M + 1) x^{M})$
223		oveq1	$⊢ x = y - B \to x^{M + 1} = {(y - B)}^{M + 1}$
224		oveq1	$⊢ x = y - B \to x^{M} = {(y - B)}^{M}$
225	224	oveq2d	$⊢ x = y - B \to (M + 1) x^{M} = (M + 1) {(y - B)}^{M}$
226	200 200 187 194 206 207 215 222 223 225	dvmptco	$⊢ φ \to \frac{d (y \in ℂ⟼ {(y - B)}^{M + 1})}{d_{ℂ} y} = (y \in ℂ ⟼ (M + 1) {(y - B)}^{M} \cdot 1)$
227	197	mulid1d	$⊢ (φ \land y \in ℂ) \to (M + 1) {(y - B)}^{M} \cdot 1 = (M + 1) {(y - B)}^{M}$
228	227	mpteq2dva	$⊢ φ \to (y \in ℂ ⟼ (M + 1) {(y - B)}^{M} \cdot 1) = (y \in ℂ ⟼ (M + 1) {(y - B)}^{M})$
229	226 228	eqtrd	$⊢ φ \to \frac{d (y \in ℂ⟼ {(y - B)}^{M + 1})}{d_{ℂ} y} = (y \in ℂ ⟼ (M + 1) {(y - B)}^{M})$
230	117 20 153 155 191 197 229	dvmptres3	$⊢ φ \to \frac{d (y \in ℝ⟼ {(y - B)}^{M + 1})}{d_{ℝ} y} = (y \in ℝ ⟼ (M + 1) {(y - B)}^{M})$
231	20 192 198 230 2 118 117 124	dvmptres	$⊢ φ \to \frac{d (y \in A⟼ {(y - B)}^{M + 1})}{d_{ℝ} y} = (y \in A ⟼ (M + 1) {(y - B)}^{M})$
232	231	dmeqd	$⊢ φ \to dom \frac{d (y \in A⟼ {(y - B)}^{M + 1})}{d_{ℝ} y} = dom (y \in A ⟼ (M + 1) {(y - B)}^{M})$
233		ovex	$⊢ (M + 1) {(y - B)}^{M} \in V$
234		eqid	$⊢ (y \in A ⟼ (M + 1) {(y - B)}^{M}) = (y \in A ⟼ (M + 1) {(y - B)}^{M})$
235	233 234	dmmpti	$⊢ dom (y \in A ⟼ (M + 1) {(y - B)}^{M}) = A$
236	232 235	eqtrdi	$⊢ φ \to dom \frac{d (y \in A⟼ {(y - B)}^{M + 1})}{d_{ℝ} y} = A$
237	126 236	sseqtrrid	$⊢ φ \to A ∖ \{B\} \subseteq dom \frac{d (y \in A⟼ {(y - B)}^{M + 1})}{d_{ℝ} y}$
238	20 27 2 14 47 6	dvntaylp0	$⊢ φ \to (ℂ D^{n} T) (N - (M + 1)) (B) = (ℝ D^{n} F) (N - (M + 1)) (B)$
239	238	oveq2d	$⊢ φ \to (ℝ D^{n} F) (N - (M + 1)) (B) - (ℂ D^{n} T) (N - (M + 1)) (B) = (ℝ D^{n} F) (N - (M + 1)) (B) - (ℝ D^{n} F) (N - (M + 1)) (B)$
240	116 5	ffvelrnd	$⊢ φ \to (ℝ D^{n} F) (N - (M + 1)) (B) \in ℂ$
241	240	subidd	$⊢ φ \to (ℝ D^{n} F) (N - (M + 1)) (B) - (ℝ D^{n} F) (N - (M + 1)) (B) = 0$
242	239 241	eqtrd	$⊢ φ \to (ℝ D^{n} F) (N - (M + 1)) (B) - (ℂ D^{n} T) (N - (M + 1)) (B) = 0$
243	117	subcn	$⊢ - \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
244	243	a1i	$⊢ φ \to - \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
245		dvcn	$⊢ ((ℝ \subseteq ℂ \land (ℝ D^{n} F) (N - (M + 1)) : A ⟶ ℂ \land A \subseteq ℝ) \land dom {(ℝ D^{n} F) (N - (M + 1))}_{ℝ}^{'} = A) \to (ℝ D^{n} F) (N - (M + 1)) : A \underset{cn}{⟶} ℂ$
246	94 116 2 114 245	syl31anc	$⊢ φ \to (ℝ D^{n} F) (N - (M + 1)) : A \underset{cn}{⟶} ℂ$
247	138 246	eqeltrrd	$⊢ φ \to (y \in A ⟼ (ℝ D^{n} F) (N - (M + 1)) (y)) : A \underset{cn}{⟶} ℂ$
248		plycn	$⊢ (ℂ D^{n} T) (N - (M + 1)) \in Poly (ℝ) \to (ℂ D^{n} T) (N - (M + 1)) : ℂ \underset{cn}{⟶} ℂ$
249	64 248	syl	$⊢ φ \to (ℂ D^{n} T) (N - (M + 1)) : ℂ \underset{cn}{⟶} ℂ$
250	2 25	sstrdi	$⊢ φ \to A \subseteq ℂ$
251		cncfmptid	$⊢ (A \subseteq ℂ \land ℂ \subseteq ℂ) \to (y \in A ⟼ y) : A \underset{cn}{⟶} ℂ$
252	250 160 251	sylancl	$⊢ φ \to (y \in A ⟼ y) : A \underset{cn}{⟶} ℂ$
253	249 252	cncfmpt1f	$⊢ φ \to (y \in A ⟼ (ℂ D^{n} T) (N - (M + 1)) (y)) : A \underset{cn}{⟶} ℂ$
254	117 244 247 253	cncfmpt2f	$⊢ φ \to (y \in A ⟼ (ℝ D^{n} F) (N - (M + 1)) (y) - (ℂ D^{n} T) (N - (M + 1)) (y)) : A \underset{cn}{⟶} ℂ$
255		fveq2	$⊢ y = B \to (ℝ D^{n} F) (N - (M + 1)) (y) = (ℝ D^{n} F) (N - (M + 1)) (B)$
256		fveq2	$⊢ y = B \to (ℂ D^{n} T) (N - (M + 1)) (y) = (ℂ D^{n} T) (N - (M + 1)) (B)$
257	255 256	oveq12d	$⊢ y = B \to (ℝ D^{n} F) (N - (M + 1)) (y) - (ℂ D^{n} T) (N - (M + 1)) (y) = (ℝ D^{n} F) (N - (M + 1)) (B) - (ℂ D^{n} T) (N - (M + 1)) (B)$
258	254 5 257	cnmptlimc	$⊢ φ \to (ℝ D^{n} F) (N - (M + 1)) (B) - (ℂ D^{n} T) (N - (M + 1)) (B) \in ((y \in A ⟼ (ℝ D^{n} F) (N - (M + 1)) (y) - (ℂ D^{n} T) (N - (M + 1)) (y)) {lim}_{ℂ} B)$
259	242 258	eqeltrrd	$⊢ φ \to 0 \in ((y \in A ⟼ (ℝ D^{n} F) (N - (M + 1)) (y) - (ℂ D^{n} T) (N - (M + 1)) (y)) {lim}_{ℂ} B)$
260	210	subidd	$⊢ φ \to B - B = 0$
261	260	oveq1d	$⊢ φ \to {(B - B)}^{M + 1} = 0^{M + 1}$
262	203	0expd	$⊢ φ \to 0^{M + 1} = 0$
263	261 262	eqtrd	$⊢ φ \to {(B - B)}^{M + 1} = 0$
264	250	sselda	$⊢ (φ \land y \in A) \to y \in ℂ$
265	264 191	syldan	$⊢ (φ \land y \in A) \to {(y - B)}^{M + 1} \in ℂ$
266	265	fmpttd	$⊢ φ \to (y \in A ⟼ {(y - B)}^{M + 1}) : A ⟶ ℂ$
267		dvcn	$⊢ ((ℝ \subseteq ℂ \land (y \in A ⟼ {(y - B)}^{M + 1}) : A ⟶ ℂ \land A \subseteq ℝ) \land dom \frac{d (y \in A⟼ {(y - B)}^{M + 1})}{d_{ℝ} y} = A) \to (y \in A ⟼ {(y - B)}^{M + 1}) : A \underset{cn}{⟶} ℂ$
268	94 266 2 236 267	syl31anc	$⊢ φ \to (y \in A ⟼ {(y - B)}^{M + 1}) : A \underset{cn}{⟶} ℂ$
269		oveq1	$⊢ y = B \to y - B = B - B$
270	269	oveq1d	$⊢ y = B \to {(y - B)}^{M + 1} = {(B - B)}^{M + 1}$
271	268 5 270	cnmptlimc	$⊢ φ \to {(B - B)}^{M + 1} \in ((y \in A ⟼ {(y - B)}^{M + 1}) {lim}_{ℂ} B)$
272	263 271	eqeltrrd	$⊢ φ \to 0 \in ((y \in A ⟼ {(y - B)}^{M + 1}) {lim}_{ℂ} B)$
273	250	ssdifssd	$⊢ φ \to A ∖ \{B\} \subseteq ℂ$
274	273	sselda	$⊢ (φ \land y \in (A ∖ \{B\})) \to y \in ℂ$
275	210	adantr	$⊢ (φ \land y \in (A ∖ \{B\})) \to B \in ℂ$
276	274 275	subcld	$⊢ (φ \land y \in (A ∖ \{B\})) \to y - B \in ℂ$
277		eldifsni	$⊢ y \in (A ∖ \{B\}) \to y \neq B$
278	277	adantl	$⊢ (φ \land y \in (A ∖ \{B\})) \to y \neq B$
279	274 275 278	subne0d	$⊢ (φ \land y \in (A ∖ \{B\})) \to y - B \neq 0$
280	203	adantr	$⊢ (φ \land y \in (A ∖ \{B\})) \to M + 1 \in ℕ$
281	280	nnzd	$⊢ (φ \land y \in (A ∖ \{B\})) \to M + 1 \in ℤ$
282	276 279 281	expne0d	$⊢ (φ \land y \in (A ∖ \{B\})) \to {(y - B)}^{M + 1} \neq 0$
283	282	necomd	$⊢ (φ \land y \in (A ∖ \{B\})) \to 0 \neq {(y - B)}^{M + 1}$
284	283	neneqd	$⊢ (φ \land y \in (A ∖ \{B\})) \to \neg 0 = {(y - B)}^{M + 1}$
285	284	nrexdv	$⊢ φ \to \neg \exists y \in (A ∖ \{B\}) 0 = {(y - B)}^{M + 1}$
286		df-ima	$⊢ (y \in A ⟼ {(y - B)}^{M + 1}) [A ∖ \{B\}] = ran ({(y \in A ⟼ {(y - B)}^{M + 1}) ↾}_{(A ∖ \{B\})})$
287	286	eleq2i	$⊢ 0 \in (y \in A ⟼ {(y - B)}^{M + 1}) [A ∖ \{B\}] \leftrightarrow 0 \in ran ({(y \in A ⟼ {(y - B)}^{M + 1}) ↾}_{(A ∖ \{B\})})$
288		resmpt	$⊢ A ∖ \{B\} \subseteq A \to {(y \in A ⟼ {(y - B)}^{M + 1}) ↾}_{(A ∖ \{B\})} = (y \in (A ∖ \{B\}) ⟼ {(y - B)}^{M + 1})$
289	126 288	ax-mp	$⊢ {(y \in A ⟼ {(y - B)}^{M + 1}) ↾}_{(A ∖ \{B\})} = (y \in (A ∖ \{B\}) ⟼ {(y - B)}^{M + 1})$
290		ovex	$⊢ {(y - B)}^{M + 1} \in V$
291	289 290	elrnmpti	$⊢ 0 \in ran ({(y \in A ⟼ {(y - B)}^{M + 1}) ↾}_{(A ∖ \{B\})}) \leftrightarrow \exists y \in (A ∖ \{B\}) 0 = {(y - B)}^{M + 1}$
292	287 291	bitri	$⊢ 0 \in (y \in A ⟼ {(y - B)}^{M + 1}) [A ∖ \{B\}] \leftrightarrow \exists y \in (A ∖ \{B\}) 0 = {(y - B)}^{M + 1}$
293	285 292	sylnibr	$⊢ φ \to \neg 0 \in (y \in A ⟼ {(y - B)}^{M + 1}) [A ∖ \{B\}]$
294	90	adantr	$⊢ (φ \land y \in (A ∖ \{B\})) \to M \in ℂ$
295		1cnd	$⊢ (φ \land y \in (A ∖ \{B\})) \to 1 \in ℂ$
296	294 295	addcld	$⊢ (φ \land y \in (A ∖ \{B\})) \to M + 1 \in ℂ$
297	274 196	syldan	$⊢ (φ \land y \in (A ∖ \{B\})) \to {(y - B)}^{M} \in ℂ$
298	280	nnne0d	$⊢ (φ \land y \in (A ∖ \{B\})) \to M + 1 \neq 0$
299	77	adantr	$⊢ (φ \land y \in (A ∖ \{B\})) \to M \in ℕ$
300	299	nnzd	$⊢ (φ \land y \in (A ∖ \{B\})) \to M \in ℤ$
301	276 279 300	expne0d	$⊢ (φ \land y \in (A ∖ \{B\})) \to {(y - B)}^{M} \neq 0$
302	296 297 298 301	mulne0d	$⊢ (φ \land y \in (A ∖ \{B\})) \to (M + 1) {(y - B)}^{M} \neq 0$
303	302	necomd	$⊢ (φ \land y \in (A ∖ \{B\})) \to 0 \neq (M + 1) {(y - B)}^{M}$
304	303	neneqd	$⊢ (φ \land y \in (A ∖ \{B\})) \to \neg 0 = (M + 1) {(y - B)}^{M}$
305	304	nrexdv	$⊢ φ \to \neg \exists y \in (A ∖ \{B\}) 0 = (M + 1) {(y - B)}^{M}$
306	231	imaeq1d	$⊢ φ \to \frac{d (y \in A⟼ {(y - B)}^{M + 1})}{d_{ℝ} y} [A ∖ \{B\}] = (y \in A ⟼ (M + 1) {(y - B)}^{M}) [A ∖ \{B\}]$
307		df-ima	$⊢ (y \in A ⟼ (M + 1) {(y - B)}^{M}) [A ∖ \{B\}] = ran ({(y \in A ⟼ (M + 1) {(y - B)}^{M}) ↾}_{(A ∖ \{B\})})$
308	306 307	eqtrdi	$⊢ φ \to \frac{d (y \in A⟼ {(y - B)}^{M + 1})}{d_{ℝ} y} [A ∖ \{B\}] = ran ({(y \in A ⟼ (M + 1) {(y - B)}^{M}) ↾}_{(A ∖ \{B\})})$
309	308	eleq2d	$⊢ φ \to (0 \in \frac{d (y \in A⟼ {(y - B)}^{M + 1})}{d_{ℝ} y} [A ∖ \{B\}] \leftrightarrow 0 \in ran ({(y \in A ⟼ (M + 1) {(y - B)}^{M}) ↾}_{(A ∖ \{B\})}))$
310		resmpt	$⊢ A ∖ \{B\} \subseteq A \to {(y \in A ⟼ (M + 1) {(y - B)}^{M}) ↾}_{(A ∖ \{B\})} = (y \in (A ∖ \{B\}) ⟼ (M + 1) {(y - B)}^{M})$
311	126 310	ax-mp	$⊢ {(y \in A ⟼ (M + 1) {(y - B)}^{M}) ↾}_{(A ∖ \{B\})} = (y \in (A ∖ \{B\}) ⟼ (M + 1) {(y - B)}^{M})$
312	311 233	elrnmpti	$⊢ 0 \in ran ({(y \in A ⟼ (M + 1) {(y - B)}^{M}) ↾}_{(A ∖ \{B\})}) \leftrightarrow \exists y \in (A ∖ \{B\}) 0 = (M + 1) {(y - B)}^{M}$
313	309 312	bitrdi	$⊢ φ \to (0 \in \frac{d (y \in A⟼ {(y - B)}^{M + 1})}{d_{ℝ} y} [A ∖ \{B\}] \leftrightarrow \exists y \in (A ∖ \{B\}) 0 = (M + 1) {(y - B)}^{M})$
314	305 313	mtbird	$⊢ φ \to \neg 0 \in \frac{d (y \in A⟼ {(y - B)}^{M + 1})}{d_{ℝ} y} [A ∖ \{B\}]$
315		eldifi	$⊢ x \in (A ∖ \{B\}) \to x \in A$
316	131	ffvelrnda	$⊢ (φ \land x \in A) \to (ℝ D^{n} F) (N - M) (x) \in ℂ$
317	315 316	sylan2	$⊢ (φ \land x \in (A ∖ \{B\})) \to (ℝ D^{n} F) (N - M) (x) \in ℂ$
318	2	ssdifssd	$⊢ φ \to A ∖ \{B\} \subseteq ℝ$
319	318	sselda	$⊢ (φ \land x \in (A ∖ \{B\})) \to x \in ℝ$
320	319	recnd	$⊢ (φ \land x \in (A ∖ \{B\})) \to x \in ℂ$
321	148	ffvelrnda	$⊢ (φ \land x \in ℂ) \to (ℂ D^{n} T) (N - M) (x) \in ℂ$
322	320 321	syldan	$⊢ (φ \land x \in (A ∖ \{B\})) \to (ℂ D^{n} T) (N - M) (x) \in ℂ$
323	317 322	subcld	$⊢ (φ \land x \in (A ∖ \{B\})) \to (ℝ D^{n} F) (N - M) (x) - (ℂ D^{n} T) (N - M) (x) \in ℂ$
324	48	adantr	$⊢ (φ \land x \in (A ∖ \{B\})) \to B \in ℝ$
325	319 324	resubcld	$⊢ (φ \land x \in (A ∖ \{B\})) \to x - B \in ℝ$
326	78	adantr	$⊢ (φ \land x \in (A ∖ \{B\})) \to M \in ℕ_{0}$
327	325 326	reexpcld	$⊢ (φ \land x \in (A ∖ \{B\})) \to {(x - B)}^{M} \in ℝ$
328	327	recnd	$⊢ (φ \land x \in (A ∖ \{B\})) \to {(x - B)}^{M} \in ℂ$
329	324	recnd	$⊢ (φ \land x \in (A ∖ \{B\})) \to B \in ℂ$
330	320 329	subcld	$⊢ (φ \land x \in (A ∖ \{B\})) \to x - B \in ℂ$
331		eldifsni	$⊢ x \in (A ∖ \{B\}) \to x \neq B$
332	331	adantl	$⊢ (φ \land x \in (A ∖ \{B\})) \to x \neq B$
333	320 329 332	subne0d	$⊢ (φ \land x \in (A ∖ \{B\})) \to x - B \neq 0$
334	326	nn0zd	$⊢ (φ \land x \in (A ∖ \{B\})) \to M \in ℤ$
335	330 333 334	expne0d	$⊢ (φ \land x \in (A ∖ \{B\})) \to {(x - B)}^{M} \neq 0$
336	323 328 335	divcld	$⊢ (φ \land x \in (A ∖ \{B\})) \to \frac{(ℝ D^{n} F) (N - M) (x) - (ℂ D^{n} T) (N - M) (x)}{{(x - B)}^{M}} \in ℂ$
337	203	nnrecred	$⊢ φ \to \frac{1}{M + 1} \in ℝ$
338	337	recnd	$⊢ φ \to \frac{1}{M + 1} \in ℂ$
339	338	adantr	$⊢ (φ \land x \in (A ∖ \{B\})) \to \frac{1}{M + 1} \in ℂ$
340		txtopon	$⊢ (TopOpen (ℂ_{fld}) \in TopOn (ℂ) \land TopOpen (ℂ_{fld}) \in TopOn (ℂ)) \to TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld}) \in TopOn (ℂ \times ℂ)$
341	151 151 340	mp2an	$⊢ TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld}) \in TopOn (ℂ \times ℂ)$
342	341	toponrestid	$⊢ TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld}) = (TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) ↾_{𝑡} (ℂ \times ℂ)$
343		limcresi	$⊢ (x \in A ⟼ \frac{1}{M + 1}) {lim}_{ℂ} B \subseteq ({(x \in A ⟼ \frac{1}{M + 1}) ↾}_{(A ∖ \{B\})}) {lim}_{ℂ} B$
344		resmpt	$⊢ A ∖ \{B\} \subseteq A \to {(x \in A ⟼ \frac{1}{M + 1}) ↾}_{(A ∖ \{B\})} = (x \in (A ∖ \{B\}) ⟼ \frac{1}{M + 1})$
345	126 344	ax-mp	$⊢ {(x \in A ⟼ \frac{1}{M + 1}) ↾}_{(A ∖ \{B\})} = (x \in (A ∖ \{B\}) ⟼ \frac{1}{M + 1})$
346	345	oveq1i	$⊢ ({(x \in A ⟼ \frac{1}{M + 1}) ↾}_{(A ∖ \{B\})}) {lim}_{ℂ} B = (x \in (A ∖ \{B\}) ⟼ \frac{1}{M + 1}) {lim}_{ℂ} B$
347	343 346	sseqtri	$⊢ (x \in A ⟼ \frac{1}{M + 1}) {lim}_{ℂ} B \subseteq (x \in (A ∖ \{B\}) ⟼ \frac{1}{M + 1}) {lim}_{ℂ} B$
348		cncfmptc	$⊢ (\frac{1}{M + 1} \in ℝ \land A \subseteq ℂ \land ℝ \subseteq ℂ) \to (x \in A ⟼ \frac{1}{M + 1}) : A \underset{cn}{⟶} ℝ$
349	337 250 94 348	syl3anc	$⊢ φ \to (x \in A ⟼ \frac{1}{M + 1}) : A \underset{cn}{⟶} ℝ$
350		eqidd	$⊢ x = B \to \frac{1}{M + 1} = \frac{1}{M + 1}$
351	349 5 350	cnmptlimc	$⊢ φ \to \frac{1}{M + 1} \in ((x \in A ⟼ \frac{1}{M + 1}) {lim}_{ℂ} B)$
352	347 351	sselid	$⊢ φ \to \frac{1}{M + 1} \in ((x \in (A ∖ \{B\}) ⟼ \frac{1}{M + 1}) {lim}_{ℂ} B)$
353	117	mulcn	$⊢ \times \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
354		0cn	$⊢ 0 \in ℂ$
355		opelxpi	$⊢ (0 \in ℂ \land \frac{1}{M + 1} \in ℂ) \to ⟨0, \frac{1}{M + 1}⟩ \in (ℂ \times ℂ)$
356	354 338 355	sylancr	$⊢ φ \to ⟨0, \frac{1}{M + 1}⟩ \in (ℂ \times ℂ)$
357	341	toponunii	$⊢ ℂ \times ℂ = ⋃ (TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld}))$
358	357	cncnpi	$⊢ (\times \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld})) \land ⟨0, \frac{1}{M + 1}⟩ \in (ℂ \times ℂ)) \to \times \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) CnP TopOpen (ℂ_{fld})) (⟨0, \frac{1}{M + 1}⟩)$
359	353 356 358	sylancr	$⊢ φ \to \times \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) CnP TopOpen (ℂ_{fld})) (⟨0, \frac{1}{M + 1}⟩)$
360	336 339 161 161 117 342 8 352 359	limccnp2	$⊢ φ \to 0 \cdot (\frac{1}{M + 1}) \in ((x \in (A ∖ \{B\}) ⟼ (\frac{(ℝ D^{n} F) (N - M) (x) - (ℂ D^{n} T) (N - M) (x)}{{(x - B)}^{M}}) (\frac{1}{M + 1})) {lim}_{ℂ} B)$
361	338	mul02d	$⊢ φ \to 0 \cdot (\frac{1}{M + 1}) = 0$
362	177	fveq1d	$⊢ φ \to \frac{d (y \in A⟼ (ℝ D^{n} F) (N - (M + 1)) (y) - (ℂ D^{n} T) (N - (M + 1)) (y))}{d_{ℝ} y} (x) = (y \in A ⟼ (ℝ D^{n} F) (N - M) (y) - (ℂ D^{n} T) (N - M) (y)) (x)$
363		fveq2	$⊢ y = x \to (ℝ D^{n} F) (N - M) (y) = (ℝ D^{n} F) (N - M) (x)$
364		fveq2	$⊢ y = x \to (ℂ D^{n} T) (N - M) (y) = (ℂ D^{n} T) (N - M) (x)$
365	363 364	oveq12d	$⊢ y = x \to (ℝ D^{n} F) (N - M) (y) - (ℂ D^{n} T) (N - M) (y) = (ℝ D^{n} F) (N - M) (x) - (ℂ D^{n} T) (N - M) (x)$
366		ovex	$⊢ (ℝ D^{n} F) (N - M) (x) - (ℂ D^{n} T) (N - M) (x) \in V$
367	365 180 366	fvmpt	$⊢ x \in A \to (y \in A ⟼ (ℝ D^{n} F) (N - M) (y) - (ℂ D^{n} T) (N - M) (y)) (x) = (ℝ D^{n} F) (N - M) (x) - (ℂ D^{n} T) (N - M) (x)$
368	315 367	syl	$⊢ x \in (A ∖ \{B\}) \to (y \in A ⟼ (ℝ D^{n} F) (N - M) (y) - (ℂ D^{n} T) (N - M) (y)) (x) = (ℝ D^{n} F) (N - M) (x) - (ℂ D^{n} T) (N - M) (x)$
369	362 368	sylan9eq	$⊢ (φ \land x \in (A ∖ \{B\})) \to \frac{d (y \in A⟼ (ℝ D^{n} F) (N - (M + 1)) (y) - (ℂ D^{n} T) (N - (M + 1)) (y))}{d_{ℝ} y} (x) = (ℝ D^{n} F) (N - M) (x) - (ℂ D^{n} T) (N - M) (x)$
370	231	fveq1d	$⊢ φ \to \frac{d (y \in A⟼ {(y - B)}^{M + 1})}{d_{ℝ} y} (x) = (y \in A ⟼ (M + 1) {(y - B)}^{M}) (x)$
371		oveq1	$⊢ y = x \to y - B = x - B$
372	371	oveq1d	$⊢ y = x \to {(y - B)}^{M} = {(x - B)}^{M}$
373	372	oveq2d	$⊢ y = x \to (M + 1) {(y - B)}^{M} = (M + 1) {(x - B)}^{M}$
374		ovex	$⊢ (M + 1) {(x - B)}^{M} \in V$
375	373 234 374	fvmpt	$⊢ x \in A \to (y \in A ⟼ (M + 1) {(y - B)}^{M}) (x) = (M + 1) {(x - B)}^{M}$
376	315 375	syl	$⊢ x \in (A ∖ \{B\}) \to (y \in A ⟼ (M + 1) {(y - B)}^{M}) (x) = (M + 1) {(x - B)}^{M}$
377	370 376	sylan9eq	$⊢ (φ \land x \in (A ∖ \{B\})) \to \frac{d (y \in A⟼ {(y - B)}^{M + 1})}{d_{ℝ} y} (x) = (M + 1) {(x - B)}^{M}$
378	203	adantr	$⊢ (φ \land x \in (A ∖ \{B\})) \to M + 1 \in ℕ$
379	378	nncnd	$⊢ (φ \land x \in (A ∖ \{B\})) \to M + 1 \in ℂ$
380	379 328	mulcomd	$⊢ (φ \land x \in (A ∖ \{B\})) \to (M + 1) {(x - B)}^{M} = {(x - B)}^{M} (M + 1)$
381	377 380	eqtrd	$⊢ (φ \land x \in (A ∖ \{B\})) \to \frac{d (y \in A⟼ {(y - B)}^{M + 1})}{d_{ℝ} y} (x) = {(x - B)}^{M} (M + 1)$
382	369 381	oveq12d	$⊢ (φ \land x \in (A ∖ \{B\})) \to \frac{\frac{d (y \in A⟼ (ℝ D^{n} F) (N - (M + 1)) (y) - (ℂ D^{n} T) (N - (M + 1)) (y))}{d_{ℝ} y} (x)}{\frac{d (y \in A⟼ {(y - B)}^{M + 1})}{d_{ℝ} y} (x)} = \frac{(ℝ D^{n} F) (N - M) (x) - (ℂ D^{n} T) (N - M) (x)}{{(x - B)}^{M} (M + 1)}$
383	378	nnne0d	$⊢ (φ \land x \in (A ∖ \{B\})) \to M + 1 \neq 0$
384	323 328 379 335 383	divdiv1d	$⊢ (φ \land x \in (A ∖ \{B\})) \to \frac{\frac{(ℝ D^{n} F) (N - M) (x) - (ℂ D^{n} T) (N - M) (x)}{{(x - B)}^{M}}}{M + 1} = \frac{(ℝ D^{n} F) (N - M) (x) - (ℂ D^{n} T) (N - M) (x)}{{(x - B)}^{M} (M + 1)}$
385	336 379 383	divrecd	$⊢ (φ \land x \in (A ∖ \{B\})) \to \frac{\frac{(ℝ D^{n} F) (N - M) (x) - (ℂ D^{n} T) (N - M) (x)}{{(x - B)}^{M}}}{M + 1} = (\frac{(ℝ D^{n} F) (N - M) (x) - (ℂ D^{n} T) (N - M) (x)}{{(x - B)}^{M}}) (\frac{1}{M + 1})$
386	382 384 385	3eqtr2rd	$⊢ (φ \land x \in (A ∖ \{B\})) \to (\frac{(ℝ D^{n} F) (N - M) (x) - (ℂ D^{n} T) (N - M) (x)}{{(x - B)}^{M}}) (\frac{1}{M + 1}) = \frac{\frac{d (y \in A⟼ (ℝ D^{n} F) (N - (M + 1)) (y) - (ℂ D^{n} T) (N - (M + 1)) (y))}{d_{ℝ} y} (x)}{\frac{d (y \in A⟼ {(y - B)}^{M + 1})}{d_{ℝ} y} (x)}$
387	386	mpteq2dva	$⊢ φ \to (x \in (A ∖ \{B\}) ⟼ (\frac{(ℝ D^{n} F) (N - M) (x) - (ℂ D^{n} T) (N - M) (x)}{{(x - B)}^{M}}) (\frac{1}{M + 1})) = (x \in (A ∖ \{B\}) ⟼ \frac{\frac{d (y \in A⟼ (ℝ D^{n} F) (N - (M + 1)) (y) - (ℂ D^{n} T) (N - (M + 1)) (y))}{d_{ℝ} y} (x)}{\frac{d (y \in A⟼ {(y - B)}^{M + 1})}{d_{ℝ} y} (x)})$
388	387	oveq1d	$⊢ φ \to (x \in (A ∖ \{B\}) ⟼ (\frac{(ℝ D^{n} F) (N - M) (x) - (ℂ D^{n} T) (N - M) (x)}{{(x - B)}^{M}}) (\frac{1}{M + 1})) {lim}_{ℂ} B = (x \in (A ∖ \{B\}) ⟼ \frac{\frac{d (y \in A⟼ (ℝ D^{n} F) (N - (M + 1)) (y) - (ℂ D^{n} T) (N - (M + 1)) (y))}{d_{ℝ} y} (x)}{\frac{d (y \in A⟼ {(y - B)}^{M + 1})}{d_{ℝ} y} (x)}) {lim}_{ℂ} B$
389	360 361 388	3eltr3d	$⊢ φ \to 0 \in ((x \in (A ∖ \{B\}) ⟼ \frac{\frac{d (y \in A⟼ (ℝ D^{n} F) (N - (M + 1)) (y) - (ℂ D^{n} T) (N - (M + 1)) (y))}{d_{ℝ} y} (x)}{\frac{d (y \in A⟼ {(y - B)}^{M + 1})}{d_{ℝ} y} (x)}) {lim}_{ℂ} B)$
390	2 71 84 124 5 125 183 237 259 272 293 314 389	lhop	$⊢ φ \to 0 \in ((x \in (A ∖ \{B\}) ⟼ \frac{(y \in A ⟼ (ℝ D^{n} F) (N - (M + 1)) (y) - (ℂ D^{n} T) (N - (M + 1)) (y)) (x)}{(y \in A ⟼ {(y - B)}^{M + 1}) (x)}) {lim}_{ℂ} B)$
391	315	adantl	$⊢ (φ \land x \in (A ∖ \{B\})) \to x \in A$
392		fveq2	$⊢ y = x \to (ℝ D^{n} F) (N - (M + 1)) (y) = (ℝ D^{n} F) (N - (M + 1)) (x)$
393		fveq2	$⊢ y = x \to (ℂ D^{n} T) (N - (M + 1)) (y) = (ℂ D^{n} T) (N - (M + 1)) (x)$
394	392 393	oveq12d	$⊢ y = x \to (ℝ D^{n} F) (N - (M + 1)) (y) - (ℂ D^{n} T) (N - (M + 1)) (y) = (ℝ D^{n} F) (N - (M + 1)) (x) - (ℂ D^{n} T) (N - (M + 1)) (x)$
395		eqid	$⊢ (y \in A ⟼ (ℝ D^{n} F) (N - (M + 1)) (y) - (ℂ D^{n} T) (N - (M + 1)) (y)) = (y \in A ⟼ (ℝ D^{n} F) (N - (M + 1)) (y) - (ℂ D^{n} T) (N - (M + 1)) (y))$
396		ovex	$⊢ (ℝ D^{n} F) (N - (M + 1)) (x) - (ℂ D^{n} T) (N - (M + 1)) (x) \in V$
397	394 395 396	fvmpt	$⊢ x \in A \to (y \in A ⟼ (ℝ D^{n} F) (N - (M + 1)) (y) - (ℂ D^{n} T) (N - (M + 1)) (y)) (x) = (ℝ D^{n} F) (N - (M + 1)) (x) - (ℂ D^{n} T) (N - (M + 1)) (x)$
398	391 397	syl	$⊢ (φ \land x \in (A ∖ \{B\})) \to (y \in A ⟼ (ℝ D^{n} F) (N - (M + 1)) (y) - (ℂ D^{n} T) (N - (M + 1)) (y)) (x) = (ℝ D^{n} F) (N - (M + 1)) (x) - (ℂ D^{n} T) (N - (M + 1)) (x)$
399	371	oveq1d	$⊢ y = x \to {(y - B)}^{M + 1} = {(x - B)}^{M + 1}$
400		eqid	$⊢ (y \in A ⟼ {(y - B)}^{M + 1}) = (y \in A ⟼ {(y - B)}^{M + 1})$
401		ovex	$⊢ {(x - B)}^{M + 1} \in V$
402	399 400 401	fvmpt	$⊢ x \in A \to (y \in A ⟼ {(y - B)}^{M + 1}) (x) = {(x - B)}^{M + 1}$
403	391 402	syl	$⊢ (φ \land x \in (A ∖ \{B\})) \to (y \in A ⟼ {(y - B)}^{M + 1}) (x) = {(x - B)}^{M + 1}$
404	398 403	oveq12d	$⊢ (φ \land x \in (A ∖ \{B\})) \to \frac{(y \in A ⟼ (ℝ D^{n} F) (N - (M + 1)) (y) - (ℂ D^{n} T) (N - (M + 1)) (y)) (x)}{(y \in A ⟼ {(y - B)}^{M + 1}) (x)} = \frac{(ℝ D^{n} F) (N - (M + 1)) (x) - (ℂ D^{n} T) (N - (M + 1)) (x)}{{(x - B)}^{M + 1}}$
405	404	mpteq2dva	$⊢ φ \to (x \in (A ∖ \{B\}) ⟼ \frac{(y \in A ⟼ (ℝ D^{n} F) (N - (M + 1)) (y) - (ℂ D^{n} T) (N - (M + 1)) (y)) (x)}{(y \in A ⟼ {(y - B)}^{M + 1}) (x)}) = (x \in (A ∖ \{B\}) ⟼ \frac{(ℝ D^{n} F) (N - (M + 1)) (x) - (ℂ D^{n} T) (N - (M + 1)) (x)}{{(x - B)}^{M + 1}})$
406	405	oveq1d	$⊢ φ \to (x \in (A ∖ \{B\}) ⟼ \frac{(y \in A ⟼ (ℝ D^{n} F) (N - (M + 1)) (y) - (ℂ D^{n} T) (N - (M + 1)) (y)) (x)}{(y \in A ⟼ {(y - B)}^{M + 1}) (x)}) {lim}_{ℂ} B = (x \in (A ∖ \{B\}) ⟼ \frac{(ℝ D^{n} F) (N - (M + 1)) (x) - (ℂ D^{n} T) (N - (M + 1)) (x)}{{(x - B)}^{M + 1}}) {lim}_{ℂ} B$
407	390 406	eleqtrd	$⊢ φ \to 0 \in ((x \in (A ∖ \{B\}) ⟼ \frac{(ℝ D^{n} F) (N - (M + 1)) (x) - (ℂ D^{n} T) (N - (M + 1)) (x)}{{(x - B)}^{M + 1}}) {lim}_{ℂ} B)$

Metamath Proof Explorer

Theorem taylthlem2

Proof