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 φAS
taylthlem1.d φdomSDnFN=A
taylthlem1.n φN
taylthlem1.b φBA
taylthlem1.t T=NSTaylFB
taylthlem1.r R=xABFxTxxBN
taylthlem1.i φn1..^N0yABSDnFNnyDnTNnyyBnlimB0xABSDnFNn+1xDnTNn+1xxBn+1limB
Assertion taylthlem1 φ0RlimB

Proof

Step Hyp Ref Expression
1 taylthlem1.s φS
2 taylthlem1.f φF:A
3 taylthlem1.a φAS
4 taylthlem1.d φdomSDnFN=A
5 taylthlem1.n φN
6 taylthlem1.b φBA
7 taylthlem1.t T=NSTaylFB
8 taylthlem1.r R=xABFxTxxBN
9 taylthlem1.i φn1..^N0yABSDnFNnyDnTNnyyBnlimB0xABSDnFNn+1xDnTNn+1xxBn+1limB
10 elfz1end NN1N
11 5 10 sylib φN1N
12 oveq2 m=1Nm=N1
13 12 fveq2d m=1SDnFNm=SDnFN1
14 13 fveq1d m=1SDnFNmx=SDnFN1x
15 12 fveq2d m=1DnTNm=DnTN1
16 15 fveq1d m=1DnTNmx=DnTN1x
17 14 16 oveq12d m=1SDnFNmxDnTNmx=SDnFN1xDnTN1x
18 oveq2 m=1xBm=xB1
19 17 18 oveq12d m=1SDnFNmxDnTNmxxBm=SDnFN1xDnTN1xxB1
20 19 mpteq2dv m=1xABSDnFNmxDnTNmxxBm=xABSDnFN1xDnTN1xxB1
21 20 oveq1d m=1xABSDnFNmxDnTNmxxBmlimB=xABSDnFN1xDnTN1xxB1limB
22 21 eleq2d m=10xABSDnFNmxDnTNmxxBmlimB0xABSDnFN1xDnTN1xxB1limB
23 22 imbi2d m=1φ0xABSDnFNmxDnTNmxxBmlimBφ0xABSDnFN1xDnTN1xxB1limB
24 oveq2 m=nNm=Nn
25 24 fveq2d m=nSDnFNm=SDnFNn
26 25 fveq1d m=nSDnFNmx=SDnFNnx
27 24 fveq2d m=nDnTNm=DnTNn
28 27 fveq1d m=nDnTNmx=DnTNnx
29 26 28 oveq12d m=nSDnFNmxDnTNmx=SDnFNnxDnTNnx
30 oveq2 m=nxBm=xBn
31 29 30 oveq12d m=nSDnFNmxDnTNmxxBm=SDnFNnxDnTNnxxBn
32 31 mpteq2dv m=nxABSDnFNmxDnTNmxxBm=xABSDnFNnxDnTNnxxBn
33 fveq2 x=ySDnFNnx=SDnFNny
34 fveq2 x=yDnTNnx=DnTNny
35 33 34 oveq12d x=ySDnFNnxDnTNnx=SDnFNnyDnTNny
36 oveq1 x=yxB=yB
37 36 oveq1d x=yxBn=yBn
38 35 37 oveq12d x=ySDnFNnxDnTNnxxBn=SDnFNnyDnTNnyyBn
39 38 cbvmptv xABSDnFNnxDnTNnxxBn=yABSDnFNnyDnTNnyyBn
40 32 39 eqtrdi m=nxABSDnFNmxDnTNmxxBm=yABSDnFNnyDnTNnyyBn
41 40 oveq1d m=nxABSDnFNmxDnTNmxxBmlimB=yABSDnFNnyDnTNnyyBnlimB
42 41 eleq2d m=n0xABSDnFNmxDnTNmxxBmlimB0yABSDnFNnyDnTNnyyBnlimB
43 42 imbi2d m=nφ0xABSDnFNmxDnTNmxxBmlimBφ0yABSDnFNnyDnTNnyyBnlimB
44 oveq2 m=n+1Nm=Nn+1
45 44 fveq2d m=n+1SDnFNm=SDnFNn+1
46 45 fveq1d m=n+1SDnFNmx=SDnFNn+1x
47 44 fveq2d m=n+1DnTNm=DnTNn+1
48 47 fveq1d m=n+1DnTNmx=DnTNn+1x
49 46 48 oveq12d m=n+1SDnFNmxDnTNmx=SDnFNn+1xDnTNn+1x
50 oveq2 m=n+1xBm=xBn+1
51 49 50 oveq12d m=n+1SDnFNmxDnTNmxxBm=SDnFNn+1xDnTNn+1xxBn+1
52 51 mpteq2dv m=n+1xABSDnFNmxDnTNmxxBm=xABSDnFNn+1xDnTNn+1xxBn+1
53 52 oveq1d m=n+1xABSDnFNmxDnTNmxxBmlimB=xABSDnFNn+1xDnTNn+1xxBn+1limB
54 53 eleq2d m=n+10xABSDnFNmxDnTNmxxBmlimB0xABSDnFNn+1xDnTNn+1xxBn+1limB
55 54 imbi2d m=n+1φ0xABSDnFNmxDnTNmxxBmlimBφ0xABSDnFNn+1xDnTNn+1xxBn+1limB
56 oveq2 m=NNm=NN
57 56 fveq2d m=NSDnFNm=SDnFNN
58 57 fveq1d m=NSDnFNmx=SDnFNNx
59 56 fveq2d m=NDnTNm=DnTNN
60 59 fveq1d m=NDnTNmx=DnTNNx
61 58 60 oveq12d m=NSDnFNmxDnTNmx=SDnFNNxDnTNNx
62 oveq2 m=NxBm=xBN
63 61 62 oveq12d m=NSDnFNmxDnTNmxxBm=SDnFNNxDnTNNxxBN
64 63 mpteq2dv m=NxABSDnFNmxDnTNmxxBm=xABSDnFNNxDnTNNxxBN
65 64 oveq1d m=NxABSDnFNmxDnTNmxxBmlimB=xABSDnFNNxDnTNNxxBNlimB
66 65 eleq2d m=N0xABSDnFNmxDnTNmxxBmlimB0xABSDnFNNxDnTNNxxBNlimB
67 66 imbi2d m=Nφ0xABSDnFNmxDnTNmxxBmlimBφ0xABSDnFNNxDnTNNxxBNlimB
68 fveq2 y=BSDnFNy=SDnFNB
69 fveq2 y=BDnTNy=DnTNB
70 68 69 oveq12d y=BSDnFNyDnTNy=SDnFNBDnTNB
71 eqid yASDnFNyDnTNy=yASDnFNyDnTNy
72 ovex SDnFNBDnTNBV
73 70 71 72 fvmpt BAyASDnFNyDnTNyB=SDnFNBDnTNB
74 6 73 syl φyASDnFNyDnTNyB=SDnFNBDnTNB
75 5 nnnn0d φN0
76 nn0uz 0=0
77 75 76 eleqtrdi φN0
78 eluzfz2b N0N0N
79 77 78 sylib φN0N
80 6 4 eleqtrrd φBdomSDnFN
81 1 2 3 79 80 7 dvntaylp0 φDnTNB=SDnFNB
82 81 oveq2d φSDnFNBDnTNB=SDnFNBSDnFNB
83 cnex V
84 83 a1i φV
85 elpm2r VSF:AASF𝑝𝑚S
86 84 1 2 3 85 syl22anc φF𝑝𝑚S
87 dvnf SF𝑝𝑚SN0SDnFN:domSDnFN
88 1 86 75 87 syl3anc φSDnFN:domSDnFN
89 88 80 ffvelrnd φSDnFNB
90 89 subidd φSDnFNBSDnFNB=0
91 74 82 90 3eqtrd φyASDnFNyDnTNyB=0
92 funmpt FunyASDnFNyDnTNy
93 ovex SDnFNyDnTNyV
94 93 71 dmmpti domyASDnFNyDnTNy=A
95 6 94 eleqtrrdi φBdomyASDnFNyDnTNy
96 funbrfvb FunyASDnFNyDnTNyBdomyASDnFNyDnTNyyASDnFNyDnTNyB=0ByASDnFNyDnTNy0
97 92 95 96 sylancr φyASDnFNyDnTNyB=0ByASDnFNyDnTNy0
98 91 97 mpbid φByASDnFNyDnTNy0
99 nnm1nn0 NN10
100 5 99 syl φN10
101 dvnf SF𝑝𝑚SN10SDnFN1:domSDnFN1
102 1 86 100 101 syl3anc φSDnFN1:domSDnFN1
103 dvnbss SF𝑝𝑚SN10domSDnFN1domF
104 1 86 100 103 syl3anc φdomSDnFN1domF
105 2 104 fssdmd φdomSDnFN1A
106 fzo0end NN10..^N
107 elfzofz N10..^NN10N
108 5 106 107 3syl φN10N
109 dvn2bss SF𝑝𝑚SN10NdomSDnFNdomSDnFN1
110 1 86 108 109 syl3anc φdomSDnFNdomSDnFN1
111 4 110 eqsstrrd φAdomSDnFN1
112 105 111 eqssd φdomSDnFN1=A
113 112 feq2d φSDnFN1:domSDnFN1SDnFN1:A
114 102 113 mpbid φSDnFN1:A
115 114 ffvelrnda φyASDnFN1y
116 4 feq2d φSDnFN:domSDnFNSDnFN:A
117 88 116 mpbid φSDnFN:A
118 117 ffvelrnda φyASDnFNy
119 5 nncnd φN
120 1cnd φ1
121 119 120 npcand φN-1+1=N
122 121 fveq2d φSDnFN-1+1=SDnFN
123 recnprss SS
124 1 123 syl φS
125 dvnp1 SF𝑝𝑚SN10SDnFN-1+1=SDSDnFN1
126 124 86 100 125 syl3anc φSDnFN-1+1=SDSDnFN1
127 122 126 eqtr3d φSDnFN=SDSDnFN1
128 117 feqmptd φSDnFN=yASDnFNy
129 114 feqmptd φSDnFN1=yASDnFN1y
130 129 oveq2d φSDSDnFN1=dyASDnFN1ydSy
131 127 128 130 3eqtr3rd φdyASDnFN1ydSy=yASDnFNy
132 3 124 sstrd φA
133 132 sselda φyAy
134 1nn0 10
135 134 a1i φ10
136 elpm2r VSSDnFN1:AASSDnFN1𝑝𝑚S
137 84 1 114 3 136 syl22anc φSDnFN1𝑝𝑚S
138 dvn1 SSDnFN1𝑝𝑚SSDnSDnFN11=SDSDnFN1
139 124 137 138 syl2anc φSDnSDnFN11=SDSDnFN1
140 126 122 eqtr3d φSDSDnFN1=SDnFN
141 139 140 eqtrd φSDnSDnFN11=SDnFN
142 141 dmeqd φdomSDnSDnFN11=domSDnFN
143 80 142 eleqtrrd φBdomSDnSDnFN11
144 eqid 1STaylSDnFN1B=1STaylSDnFN1B
145 1 114 3 135 143 144 taylpf φ1STaylSDnFN1B:
146 120 119 pncan3d φ1+N-1=N
147 146 oveq1d φ1+N-1STaylFB=NSTaylFB
148 7 147 eqtr4id φT=1+N-1STaylFB
149 148 oveq2d φDnT=Dn1+N-1STaylFB
150 149 fveq1d φDnTN1=Dn1+N-1STaylFBN1
151 146 fveq2d φSDnF1+N-1=SDnFN
152 151 dmeqd φdomSDnF1+N-1=domSDnFN
153 80 152 eleqtrrd φBdomSDnF1+N-1
154 1 2 3 100 135 153 dvntaylp φDn1+N-1STaylFBN1=1STaylSDnFN1B
155 150 154 eqtrd φDnTN1=1STaylSDnFN1B
156 155 feq1d φDnTN1:1STaylSDnFN1B:
157 145 156 mpbird φDnTN1:
158 157 ffvelrnda φyDnTN1y
159 133 158 syldan φyADnTN1y
160 0nn0 00
161 160 a1i φ00
162 elpm2r VSSDnFN:AASSDnFN𝑝𝑚S
163 84 1 117 3 162 syl22anc φSDnFN𝑝𝑚S
164 dvn0 SSDnFN𝑝𝑚SSDnSDnFN0=SDnFN
165 124 163 164 syl2anc φSDnSDnFN0=SDnFN
166 165 dmeqd φdomSDnSDnFN0=domSDnFN
167 80 166 eleqtrrd φBdomSDnSDnFN0
168 eqid 0STaylSDnFNB=0STaylSDnFNB
169 1 117 3 161 167 168 taylpf φ0STaylSDnFNB:
170 119 addid2d φ0+N=N
171 170 oveq1d φ0+NSTaylFB=NSTaylFB
172 171 7 eqtr4di φ0+NSTaylFB=T
173 172 oveq2d φDn0+NSTaylFB=DnT
174 173 fveq1d φDn0+NSTaylFBN=DnTN
175 170 fveq2d φSDnF0+N=SDnFN
176 175 dmeqd φdomSDnF0+N=domSDnFN
177 80 176 eleqtrrd φBdomSDnF0+N
178 1 2 3 75 161 177 dvntaylp φDn0+NSTaylFBN=0STaylSDnFNB
179 174 178 eqtr3d φDnTN=0STaylSDnFNB
180 179 feq1d φDnTN:0STaylSDnFNB:
181 169 180 mpbird φDnTN:
182 181 ffvelrnda φyDnTNy
183 133 182 syldan φyADnTNy
184 124 sselda φySy
185 184 158 syldan φySDnTN1y
186 184 182 syldan φySDnTNy
187 eqid TopOpenfld=TopOpenfld
188 187 cnfldtopon TopOpenfldTopOn
189 toponmax TopOpenfldTopOnTopOpenfld
190 188 189 mp1i φTopOpenfld
191 df-ss SS=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 TT:
198 196 197 sylibr φT
199 195 198 sselid φT𝑝𝑚
200 dvnp1 T𝑝𝑚N10DnTN-1+1=DDnTN1
201 194 199 100 200 syl3anc φDnTN-1+1=DDnTN1
202 121 fveq2d φDnTN-1+1=DnTN
203 201 202 eqtr3d φDDnTN1=DnTN
204 157 feqmptd φDnTN1=yDnTN1y
205 204 oveq2d φDDnTN1=dyDnTN1ydy
206 181 feqmptd φDnTN=yDnTNy
207 203 205 206 3eqtr3d φdyDnTN1ydy=yDnTNy
208 187 1 190 192 158 182 207 dvmptres3 φdySDnTN1ydSy=ySDnTNy
209 eqid TopOpenfld𝑡S=TopOpenfld𝑡S
210 resttopon TopOpenfldTopOnSTopOpenfld𝑡STopOnS
211 188 124 210 sylancr φTopOpenfld𝑡STopOnS
212 topontop TopOpenfld𝑡STopOnSTopOpenfld𝑡STop
213 211 212 syl φTopOpenfld𝑡STop
214 toponuni TopOpenfld𝑡STopOnSS=TopOpenfld𝑡S
215 211 214 syl φS=TopOpenfld𝑡S
216 3 215 sseqtrd φATopOpenfld𝑡S
217 eqid TopOpenfld𝑡S=TopOpenfld𝑡S
218 217 ntrss2 TopOpenfld𝑡STopATopOpenfld𝑡SintTopOpenfld𝑡SAA
219 213 216 218 syl2anc φintTopOpenfld𝑡SAA
220 140 dmeqd φdomSDnFN1S=domSDnFN
221 220 4 eqtrd φdomSDnFN1S=A
222 124 114 3 209 187 dvbssntr φdomSDnFN1SintTopOpenfld𝑡SA
223 221 222 eqsstrrd φAintTopOpenfld𝑡SA
224 219 223 eqssd φintTopOpenfld𝑡SA=A
225 1 185 186 208 3 209 187 224 dvmptres2 φdyADnTN1ydSy=yADnTNy
226 1 115 118 131 159 183 225 dvmptsub φdyASDnFN1yDnTN1ydSy=yASDnFNyDnTNy
227 226 breqd φBdyASDnFN1yDnTN1ydSy0ByASDnFNyDnTNy0
228 98 227 mpbird φBdyASDnFN1yDnTN1ydSy0
229 eqid xAByASDnFN1yDnTN1yxyASDnFN1yDnTN1yBxB=xAByASDnFN1yDnTN1yxyASDnFN1yDnTN1yBxB
230 115 159 subcld φyASDnFN1yDnTN1y
231 230 fmpttd φyASDnFN1yDnTN1y:A
232 209 187 229 124 231 3 eldv φBdyASDnFN1yDnTN1ydSy0BintTopOpenfld𝑡SA0xAByASDnFN1yDnTN1yxyASDnFN1yDnTN1yBxBlimB
233 228 232 mpbid φBintTopOpenfld𝑡SA0xAByASDnFN1yDnTN1yxyASDnFN1yDnTN1yBxBlimB
234 233 simprd φ0xAByASDnFN1yDnTN1yxyASDnFN1yDnTN1yBxBlimB
235 eldifi xABxA
236 fveq2 y=xSDnFN1y=SDnFN1x
237 fveq2 y=xDnTN1y=DnTN1x
238 236 237 oveq12d y=xSDnFN1yDnTN1y=SDnFN1xDnTN1x
239 eqid yASDnFN1yDnTN1y=yASDnFN1yDnTN1y
240 ovex SDnFN1xDnTN1xV
241 238 239 240 fvmpt xAyASDnFN1yDnTN1yx=SDnFN1xDnTN1x
242 fveq2 y=BSDnFN1y=SDnFN1B
243 fveq2 y=BDnTN1y=DnTN1B
244 242 243 oveq12d y=BSDnFN1yDnTN1y=SDnFN1BDnTN1B
245 ovex SDnFN1BDnTN1BV
246 244 239 245 fvmpt BAyASDnFN1yDnTN1yB=SDnFN1BDnTN1B
247 6 246 syl φyASDnFN1yDnTN1yB=SDnFN1BDnTN1B
248 1 2 3 108 80 7 dvntaylp0 φDnTN1B=SDnFN1B
249 248 oveq2d φSDnFN1BDnTN1B=SDnFN1BSDnFN1B
250 114 6 ffvelrnd φSDnFN1B
251 250 subidd φSDnFN1BSDnFN1B=0
252 247 249 251 3eqtrd φyASDnFN1yDnTN1yB=0
253 241 252 oveqan12rd φxAyASDnFN1yDnTN1yxyASDnFN1yDnTN1yB=SDnFN1x-DnTN1x-0
254 114 ffvelrnda φxASDnFN1x
255 132 sselda φxAx
256 157 ffvelrnda φxDnTN1x
257 255 256 syldan φxADnTN1x
258 254 257 subcld φxASDnFN1xDnTN1x
259 258 subid1d φxASDnFN1x-DnTN1x-0=SDnFN1xDnTN1x
260 253 259 eqtr2d φxASDnFN1xDnTN1x=yASDnFN1yDnTN1yxyASDnFN1yDnTN1yB
261 235 260 sylan2 φxABSDnFN1xDnTN1x=yASDnFN1yDnTN1yxyASDnFN1yDnTN1yB
262 132 ssdifssd φAB
263 262 sselda φxABx
264 132 6 sseldd φB
265 264 adantr φxABB
266 263 265 subcld φxABxB
267 266 exp1d φxABxB1=xB
268 261 267 oveq12d φxABSDnFN1xDnTN1xxB1=yASDnFN1yDnTN1yxyASDnFN1yDnTN1yBxB
269 268 mpteq2dva φxABSDnFN1xDnTN1xxB1=xAByASDnFN1yDnTN1yxyASDnFN1yDnTN1yBxB
270 269 oveq1d φxABSDnFN1xDnTN1xxB1limB=xAByASDnFN1yDnTN1yxyASDnFN1yDnTN1yBxBlimB
271 234 270 eleqtrrd φ0xABSDnFN1xDnTN1xxB1limB
272 271 a1i N1φ0xABSDnFN1xDnTN1xxB1limB
273 9 expr φn1..^N0yABSDnFNnyDnTNnyyBnlimB0xABSDnFNn+1xDnTNn+1xxBn+1limB
274 273 expcom n1..^Nφ0yABSDnFNnyDnTNnyyBnlimB0xABSDnFNn+1xDnTNn+1xxBn+1limB
275 274 a2d n1..^Nφ0yABSDnFNnyDnTNnyyBnlimBφ0xABSDnFNn+1xDnTNn+1xxBn+1limB
276 23 43 55 67 272 275 fzind2 N1Nφ0xABSDnFNNxDnTNNxxBNlimB
277 11 276 mpcom φ0xABSDnFNNxDnTNNxxBNlimB
278 119 subidd φNN=0
279 278 fveq2d φSDnFNN=SDnF0
280 dvn0 SF𝑝𝑚SSDnF0=F
281 124 86 280 syl2anc φSDnF0=F
282 279 281 eqtrd φSDnFNN=F
283 282 fveq1d φSDnFNNx=Fx
284 278 fveq2d φDnTNN=DnT0
285 dvn0 T𝑝𝑚DnT0=T
286 193 199 285 sylancr φDnT0=T
287 284 286 eqtrd φDnTNN=T
288 287 fveq1d φDnTNNx=Tx
289 283 288 oveq12d φSDnFNNxDnTNNx=FxTx
290 289 oveq1d φSDnFNNxDnTNNxxBN=FxTxxBN
291 290 mpteq2dv φxABSDnFNNxDnTNNxxBN=xABFxTxxBN
292 291 8 eqtr4di φxABSDnFNNxDnTNNxxBN=R
293 292 oveq1d φxABSDnFNNxDnTNNxxBNlimB=RlimB
294 277 293 eleqtrd φ0RlimB