Metamath Proof Explorer


Theorem 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 φ S
taylthlem1.f φ F : A
taylthlem1.a φ A S
taylthlem1.d φ dom S D n F N = A
taylthlem1.n φ N
taylthlem1.b φ B A
taylthlem1.t T = N S Tayl F B
taylthlem1.r R = x A B F x T x x B N
taylthlem1.i φ n 1 ..^ N 0 y A B S D n F N n y D n T N n y y B n lim B 0 x A B S D n F N n + 1 x D n T N n + 1 x x B n + 1 lim B
Assertion taylthlem1 φ 0 R lim B

Proof

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