Step | Hyp | Ref
| Expression |
1 | | taylthlem1.n |
. . . 4
   |
2 | | elfz1end 11829 |
. . . 4

      |
3 | 1, 2 | sylib 200 |
. . 3
       |
4 | | oveq2 6298 |
. . . . . . . . . . . 12
 
     |
5 | 4 | fveq2d 5869 |
. . . . . . . . . . 11
        
              |
6 | 5 | fveq1d 5867 |
. . . . . . . . . 10
         
             
       |
7 | 4 | fveq2d 5869 |
. . . . . . . . . . 11
        
              |
8 | 7 | fveq1d 5867 |
. . . . . . . . . 10
         
             
       |
9 | 6, 8 | oveq12d 6308 |
. . . . . . . . 9
                        
                             
        |
10 | | oveq2 6298 |
. . . . . . . . 9
               |
11 | 9, 10 | oveq12d 6308 |
. . . . . . . 8
                                                                               |
12 | 11 | mpteq2dv 4490 |
. . . . . . 7
                
             
                                                            |
13 | 12 | oveq1d 6305 |
. . . . . 6
                               
              lim                  
             
              lim    |
14 | 13 | eleq2d 2514 |
. . . . 5
                  
             
              lim                  
             
              lim     |
15 | 14 | imbi2d 318 |
. . . 4
  
                              
              lim  
                 
             
              lim      |
16 | | oveq2 6298 |
. . . . . . . . . . . . 13
 
     |
17 | 16 | fveq2d 5869 |
. . . . . . . . . . . 12
        
              |
18 | 17 | fveq1d 5867 |
. . . . . . . . . . 11
         
             
       |
19 | 16 | fveq2d 5869 |
. . . . . . . . . . . 12
        
              |
20 | 19 | fveq1d 5867 |
. . . . . . . . . . 11
         
             
       |
21 | 18, 20 | oveq12d 6308 |
. . . . . . . . . 10
                        
                             
        |
22 | | oveq2 6298 |
. . . . . . . . . 10
               |
23 | 21, 22 | oveq12d 6308 |
. . . . . . . . 9
                                                                               |
24 | 23 | mpteq2dv 4490 |
. . . . . . . 8
                
             
                                                            |
25 | | fveq2 5865 |
. . . . . . . . . . 11
         
             
       |
26 | | fveq2 5865 |
. . . . . . . . . . 11
         
             
       |
27 | 25, 26 | oveq12d 6308 |
. . . . . . . . . 10
                        
                             
        |
28 | | oveq1 6297 |
. . . . . . . . . . 11
       |
29 | 28 | oveq1d 6305 |
. . . . . . . . . 10
               |
30 | 27, 29 | oveq12d 6308 |
. . . . . . . . 9
                                                                               |
31 | 30 | cbvmptv 4495 |
. . . . . . . 8
                                                                         
               |
32 | 24, 31 | syl6eq 2501 |
. . . . . . 7
                
             
                                                            |
33 | 32 | oveq1d 6305 |
. . . . . 6
                               
              lim                  
             
              lim    |
34 | 33 | eleq2d 2514 |
. . . . 5
                  
             
              lim                  
             
              lim     |
35 | 34 | imbi2d 318 |
. . . 4
  
                              
              lim  
                 
             
              lim      |
36 | | oveq2 6298 |
. . . . . . . . . . . 12
   
  
    |
37 | 36 | fveq2d 5869 |
. . . . . . . . . . 11
          
                |
38 | 37 | fveq1d 5867 |
. . . . . . . . . 10
           
             
         |
39 | 36 | fveq2d 5869 |
. . . . . . . . . . 11
          
                |
40 | 39 | fveq1d 5867 |
. . . . . . . . . 10
           
             
         |
41 | 38, 40 | oveq12d 6308 |
. . . . . . . . 9
                          
                
              
          |
42 | | oveq2 6298 |
. . . . . . . . 9
                   |
43 | 41, 42 | oveq12d 6308 |
. . . . . . . 8
                                                                    
                  |
44 | 43 | mpteq2dv 4490 |
. . . . . . 7
                  
             
                                              
                   |
45 | 44 | oveq1d 6305 |
. . . . . 6
                                 
              lim                  
               
                  lim    |
46 | 45 | eleq2d 2514 |
. . . . 5
                    
             
              lim                  
               
                  lim     |
47 | 46 | imbi2d 318 |
. . . 4
    
                              
              lim  
                 
               
                  lim      |
48 | | oveq2 6298 |
. . . . . . . . . . . 12
 
     |
49 | 48 | fveq2d 5869 |
. . . . . . . . . . 11
        
              |
50 | 49 | fveq1d 5867 |
. . . . . . . . . 10
         
             
       |
51 | 48 | fveq2d 5869 |
. . . . . . . . . . 11
        
              |
52 | 51 | fveq1d 5867 |
. . . . . . . . . 10
         
             
       |
53 | 50, 52 | oveq12d 6308 |
. . . . . . . . 9
                        
                             
        |
54 | | oveq2 6298 |
. . . . . . . . 9
               |
55 | 53, 54 | oveq12d 6308 |
. . . . . . . 8
                                                                               |
56 | 55 | mpteq2dv 4490 |
. . . . . . 7
                
             
                                                            |
57 | 56 | oveq1d 6305 |
. . . . . 6
                               
              lim                  
             
              lim    |
58 | 57 | eleq2d 2514 |
. . . . 5
                  
             
              lim                  
             
              lim     |
59 | 58 | imbi2d 318 |
. . . 4
  
                              
              lim  
                 
             
              lim      |
60 | | taylthlem1.b |
. . . . . . . . . . . 12
   |
61 | | fveq2 5865 |
. . . . . . . . . . . . . 14
                           |
62 | | fveq2 5865 |
. . . . . . . . . . . . . 14
                           |
63 | 61, 62 | oveq12d 6308 |
. . . . . . . . . . . . 13
                                                       |
64 | | eqid 2451 |
. . . . . . . . . . . . 13
                                                         |
65 | | ovex 6318 |
. . . . . . . . . . . . 13
                           |
66 | 63, 64, 65 | fvmpt 5948 |
. . . . . . . . . . . 12
                                                             |
67 | 60, 66 | syl 17 |
. . . . . . . . . . 11
                                                             |
68 | | taylthlem1.s |
. . . . . . . . . . . . 13
      |
69 | | taylthlem1.f |
. . . . . . . . . . . . 13
       |
70 | | taylthlem1.a |
. . . . . . . . . . . . 13

  |
71 | 1 | nnnn0d 10925 |
. . . . . . . . . . . . . . 15
   |
72 | | nn0uz 11193 |
. . . . . . . . . . . . . . 15
     |
73 | 71, 72 | syl6eleq 2539 |
. . . . . . . . . . . . . 14
       |
74 | | eluzfz2b 11808 |
. . . . . . . . . . . . . 14
    
      |
75 | 73, 74 | sylib 200 |
. . . . . . . . . . . . 13
       |
76 | | taylthlem1.d |
. . . . . . . . . . . . . 14
           |
77 | 60, 76 | eleqtrrd 2532 |
. . . . . . . . . . . . 13
           |
78 | | taylthlem1.t |
. . . . . . . . . . . . 13
   Tayl     |
79 | 68, 69, 70, 75, 77, 78 | dvntaylp0 23327 |
. . . . . . . . . . . 12
                           |
80 | 79 | oveq2d 6306 |
. . . . . . . . . . 11
                                                       |
81 | | cnex 9620 |
. . . . . . . . . . . . . . . 16
 |
82 | 81 | a1i 11 |
. . . . . . . . . . . . . . 15
   |
83 | | elpm2r 7489 |
. . . . . . . . . . . . . . 15
              
   |
84 | 82, 68, 69, 70, 83 | syl22anc 1269 |
. . . . . . . . . . . . . 14
     |
85 | | dvnf 22881 |
. . . . . . . . . . . . . 14
      

                      |
86 | 68, 84, 71, 85 | syl3anc 1268 |
. . . . . . . . . . . . 13
                       |
87 | 86, 77 | ffvelrnd 6023 |
. . . . . . . . . . . 12
               |
88 | 87 | subidd 9974 |
. . . . . . . . . . 11
                             |
89 | 67, 80, 88 | 3eqtrd 2489 |
. . . . . . . . . 10
                                   |
90 | | funmpt 5618 |
. . . . . . . . . . 11
                             |
91 | | ovex 6318 |
. . . . . . . . . . . . 13
                           |
92 | 91, 64 | dmmpti 5707 |
. . . . . . . . . . . 12
                             |
93 | 60, 92 | syl6eleqr 2540 |
. . . . . . . . . . 11
                               |
94 | | funbrfvb 5907 |
. . . . . . . . . . 11
                                                                                           
                                 |
95 | 90, 93, 94 | sylancr 669 |
. . . . . . . . . 10
                                                                   |
96 | 89, 95 | mpbid 214 |
. . . . . . . . 9
                                 |
97 | | nnm1nn0 10911 |
. . . . . . . . . . . . . . 15
 
   |
98 | 1, 97 | syl 17 |
. . . . . . . . . . . . . 14
     |
99 | | dvnf 22881 |
. . . . . . . . . . . . . 14
      
          
           
      |
100 | 68, 84, 98, 99 | syl3anc 1268 |
. . . . . . . . . . . . 13
        
           
      |
101 | | dvnbss 22882 |
. . . . . . . . . . . . . . . . 17
      
          
    |
102 | 68, 84, 98, 101 | syl3anc 1268 |
. . . . . . . . . . . . . . . 16
             |
103 | | fdm 5733 |
. . . . . . . . . . . . . . . . 17
       |
104 | 69, 103 | syl 17 |
. . . . . . . . . . . . . . . 16
   |
105 | 102, 104 | sseqtrd 3468 |
. . . . . . . . . . . . . . 15
             |
106 | | fzo0end 12003 |
. . . . . . . . . . . . . . . . . 18
 
  ..^   |
107 | | elfzofz 11935 |
. . . . . . . . . . . . . . . . . 18
    ..^
        |
108 | 1, 106, 107 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
         |
109 | | dvn2bss 22884 |
. . . . . . . . . . . . . . . . 17
      
                      
    |
110 | 68, 84, 108, 109 | syl3anc 1268 |
. . . . . . . . . . . . . . . 16
                
    |
111 | 76, 110 | eqsstr3d 3467 |
. . . . . . . . . . . . . . 15

            |
112 | 105, 111 | eqssd 3449 |
. . . . . . . . . . . . . 14
             |
113 | 112 | feq2d 5715 |
. . . . . . . . . . . . 13
                                 
         |
114 | 100, 113 | mpbid 214 |
. . . . . . . . . . . 12
        
        |
115 | 114 | ffvelrnda 6022 |
. . . . . . . . . . 11
 
         
       |
116 | 76 | feq2d 5715 |
. . . . . . . . . . . . 13
                                     |
117 | 86, 116 | mpbid 214 |
. . . . . . . . . . . 12
               |
118 | 117 | ffvelrnda 6022 |
. . . . . . . . . . 11
 
               |
119 | 1 | nncnd 10625 |
. . . . . . . . . . . . . . 15
   |
120 | | 1cnd 9659 |
. . . . . . . . . . . . . . 15
   |
121 | 119, 120 | npcand 9990 |
. . . . . . . . . . . . . 14
       |
122 | 121 | fveq2d 5869 |
. . . . . . . . . . . . 13
                       |
123 | | recnprss 22859 |
. . . . . . . . . . . . . . 15
   
  |
124 | 68, 123 | syl 17 |
. . . . . . . . . . . . . 14

  |
125 | | dvnp1 22879 |
. . . . . . . . . . . . . 14
 
 
                             |
126 | 124, 84, 98, 125 | syl3anc 1268 |
. . . . . . . . . . . . 13
                           |
127 | 122, 126 | eqtr3d 2487 |
. . . . . . . . . . . 12
                       |
128 | 117 | feqmptd 5918 |
. . . . . . . . . . . 12
                         |
129 | 114 | feqmptd 5918 |
. . . . . . . . . . . . 13
        
           
        |
130 | 129 | oveq2d 6306 |
. . . . . . . . . . . 12
         
             
         |
131 | 127, 128,
130 | 3eqtr3rd 2494 |
. . . . . . . . . . 11
           
                       |
132 | 70, 124 | sstrd 3442 |
. . . . . . . . . . . . 13

  |
133 | 132 | sselda 3432 |
. . . . . . . . . . . 12
 
   |
134 | | 1nn0 10885 |
. . . . . . . . . . . . . . . 16
 |
135 | 134 | a1i 11 |
. . . . . . . . . . . . . . 15
   |
136 | | elpm2r 7489 |
. . . . . . . . . . . . . . . . . . . 20
                               
  
   |
137 | 82, 68, 114, 70, 136 | syl22anc 1269 |
. . . . . . . . . . . . . . . . . . 19
        
  
   |
138 | | dvn1 22880 |
. . . . . . . . . . . . . . . . . . 19
 
       
                               
     |
139 | 124, 137,
138 | syl2anc 667 |
. . . . . . . . . . . . . . . . . 18
                           
     |
140 | 126, 122 | eqtr3d 2487 |
. . . . . . . . . . . . . . . . . 18
         
             |
141 | 139, 140 | eqtrd 2485 |
. . . . . . . . . . . . . . . . 17
                             |
142 | 141 | dmeqd 5037 |
. . . . . . . . . . . . . . . 16
                             |
143 | 77, 142 | eleqtrrd 2532 |
. . . . . . . . . . . . . . 15
            
        |
144 | | eqid 2451 |
. . . . . . . . . . . . . . 15
   Tayl                 Tayl        
      |
145 | 68, 114, 70, 135, 143, 144 | taylpf 23321 |
. . . . . . . . . . . . . 14
    Tayl        
           |
146 | 120, 119 | pncan3d 9989 |
. . . . . . . . . . . . . . . . . . . 20
       |
147 | 146 | oveq1d 6305 |
. . . . . . . . . . . . . . . . . . 19
        Tayl       Tayl      |
148 | 147, 78 | syl6reqr 2504 |
. . . . . . . . . . . . . . . . . 18
        Tayl      |
149 | 148 | oveq2d 6306 |
. . . . . . . . . . . . . . . . 17
               Tayl       |
150 | 149 | fveq1d 5867 |
. . . . . . . . . . . . . . . 16
        
             Tayl            |
151 | 146 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . 19
                       |
152 | 151 | dmeqd 5037 |
. . . . . . . . . . . . . . . . . 18
                       |
153 | 77, 152 | eleqtrrd 2532 |
. . . . . . . . . . . . . . . . 17
               |
154 | 68, 69, 70, 98, 135, 153 | dvntaylp 23326 |
. . . . . . . . . . . . . . . 16
            Tayl       
     Tayl                |
155 | 150, 154 | eqtrd 2485 |
. . . . . . . . . . . . . . 15
        
     Tayl        
       |
156 | 155 | feq1d 5714 |
. . . . . . . . . . . . . 14
               
   Tayl                     |
157 | 145, 156 | mpbird 236 |
. . . . . . . . . . . . 13
        
        |
158 | 157 | ffvelrnda 6022 |
. . . . . . . . . . . 12
 

        
       |
159 | 133, 158 | syldan 473 |
. . . . . . . . . . 11
 
         
       |
160 | | 0nn0 10884 |
. . . . . . . . . . . . . . . 16
 |
161 | 160 | a1i 11 |
. . . . . . . . . . . . . . 15
   |
162 | | elpm2r 7489 |
. . . . . . . . . . . . . . . . . . 19
                              
   |
163 | 82, 68, 117, 70, 162 | syl22anc 1269 |
. . . . . . . . . . . . . . . . . 18
         
   |
164 | | dvn0 22878 |
. . . . . . . . . . . . . . . . . 18
 
                                     |
165 | 124, 163,
164 | syl2anc 667 |
. . . . . . . . . . . . . . . . 17
                           |
166 | 165 | dmeqd 5037 |
. . . . . . . . . . . . . . . 16
                           |
167 | 77, 166 | eleqtrrd 2532 |
. . . . . . . . . . . . . . 15
                   |
168 | | eqid 2451 |
. . . . . . . . . . . . . . 15
   Tayl               Tayl             |
169 | 68, 117, 70, 161, 167, 168 | taylpf 23321 |
. . . . . . . . . . . . . 14
    Tayl                  |
170 | 119 | addid2d 9834 |
. . . . . . . . . . . . . . . . . . . 20
     |
171 | 170 | oveq1d 6305 |
. . . . . . . . . . . . . . . . . . 19
      Tayl       Tayl      |
172 | 171, 78 | syl6eqr 2503 |
. . . . . . . . . . . . . . . . . 18
      Tayl      |
173 | 172 | oveq2d 6306 |
. . . . . . . . . . . . . . . . 17
         Tayl           |
174 | 173 | fveq1d 5867 |
. . . . . . . . . . . . . . . 16
          Tayl                  |
175 | 170 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . 19
                     |
176 | 175 | dmeqd 5037 |
. . . . . . . . . . . . . . . . . 18
                     |
177 | 77, 176 | eleqtrrd 2532 |
. . . . . . . . . . . . . . . . 17
             |
178 | 68, 69, 70, 71, 161, 177 | dvntaylp 23326 |
. . . . . . . . . . . . . . . 16
          Tayl           Tayl              |
179 | 174, 178 | eqtr3d 2487 |
. . . . . . . . . . . . . . 15
            Tayl              |
180 | 179 | feq1d 5714 |
. . . . . . . . . . . . . 14
             
   Tayl                   |
181 | 169, 180 | mpbird 236 |
. . . . . . . . . . . . 13
               |
182 | 181 | ffvelrnda 6022 |
. . . . . . . . . . . 12
 

              |
183 | 133, 182 | syldan 473 |
. . . . . . . . . . 11
 
               |
184 | 124 | sselda 3432 |
. . . . . . . . . . . . 13
 
   |
185 | 184, 158 | syldan 473 |
. . . . . . . . . . . 12
 
         
       |
186 | 184, 182 | syldan 473 |
. . . . . . . . . . . 12
 
               |
187 | | eqid 2451 |
. . . . . . . . . . . . 13
  ℂfld   ℂfld |
188 | 187 | cnfldtopon 21803 |
. . . . . . . . . . . . . 14
  ℂfld TopOn   |
189 | | toponmax 19943 |
. . . . . . . . . . . . . 14
   ℂfld TopOn 
  ℂfld  |
190 | 188, 189 | mp1i 13 |
. . . . . . . . . . . . 13
   ℂfld  |
191 | | df-ss 3418 |
. . . . . . . . . . . . . 14

    |
192 | 124, 191 | sylib 200 |
. . . . . . . . . . . . 13
  
  |
193 | | ssid 3451 |
. . . . . . . . . . . . . . . . 17
 |
194 | 193 | a1i 11 |
. . . . . . . . . . . . . . . 16

  |
195 | | mapsspm 7505 |
. . . . . . . . . . . . . . . . 17
  
  |
196 | 68, 69, 70, 71, 77, 78 | taylpf 23321 |
. . . . . . . . . . . . . . . . . 18
       |
197 | 81, 81 | elmap 7500 |
. . . . . . . . . . . . . . . . . 18
  
      |
198 | 196, 197 | sylibr 216 |
. . . . . . . . . . . . . . . . 17
     |
199 | 195, 198 | sseldi 3430 |
. . . . . . . . . . . . . . . 16
     |
200 | | dvnp1 22879 |
. . . . . . . . . . . . . . . 16
 
                         
     |
201 | 194, 199,
98, 200 | syl3anc 1268 |
. . . . . . . . . . . . . . 15
                           |
202 | 121 | fveq2d 5869 |
. . . . . . . . . . . . . . 15
                       |
203 | 201, 202 | eqtr3d 2487 |
. . . . . . . . . . . . . 14
         
             |
204 | 157 | feqmptd 5918 |
. . . . . . . . . . . . . . 15
        
           
        |
205 | 204 | oveq2d 6306 |
. . . . . . . . . . . . . 14
         
             
         |
206 | 181 | feqmptd 5918 |
. . . . . . . . . . . . . 14
                         |
207 | 203, 205,
206 | 3eqtr3d 2493 |
. . . . . . . . . . . . 13
           
                       |
208 | 187, 68, 190, 192, 158, 182, 207 | dvmptres3 22910 |
. . . . . . . . . . . 12
           
                       |
209 | | eqid 2451 |
. . . . . . . . . . . 12
   ℂfld ↾t     ℂfld
↾t   |
210 | | resttopon 20177 |
. . . . . . . . . . . . . . . 16
    ℂfld
TopOn      ℂfld
↾t  TopOn    |
211 | 188, 124,
210 | sylancr 669 |
. . . . . . . . . . . . . . 15
    ℂfld
↾t  TopOn    |
212 | | topontop 19941 |
. . . . . . . . . . . . . . 15
    ℂfld
↾t  TopOn     ℂfld
↾t    |
213 | 211, 212 | syl 17 |
. . . . . . . . . . . . . 14
    ℂfld
↾t    |
214 | | toponuni 19942 |
. . . . . . . . . . . . . . . 16
    ℂfld
↾t  TopOn      ℂfld ↾t    |
215 | 211, 214 | syl 17 |
. . . . . . . . . . . . . . 15
     ℂfld
↾t    |
216 | 70, 215 | sseqtrd 3468 |
. . . . . . . . . . . . . 14

    ℂfld
↾t    |
217 | | eqid 2451 |
. . . . . . . . . . . . . . 15
    ℂfld
↾t      ℂfld
↾t   |
218 | 217 | ntrss2 20072 |
. . . . . . . . . . . . . 14
     ℂfld
↾t 
    ℂfld
↾t          ℂfld
↾t        |
219 | 213, 216,
218 | syl2anc 667 |
. . . . . . . . . . . . 13
        ℂfld
↾t        |
220 | 140 | dmeqd 5037 |
. . . . . . . . . . . . . . 15
         
             |
221 | 220, 76 | eqtrd 2485 |
. . . . . . . . . . . . . 14
         
     |
222 | 124, 114,
70, 209, 187 | dvbssntr 22855 |
. . . . . . . . . . . . . 14
         
          ℂfld
↾t        |
223 | 221, 222 | eqsstr3d 3467 |
. . . . . . . . . . . . 13

       ℂfld ↾t        |
224 | 219, 223 | eqssd 3449 |
. . . . . . . . . . . 12
        ℂfld
↾t        |
225 | 68, 185, 186, 208, 70, 209, 187, 224 | dvmptres2 22916 |
. . . . . . . . . . 11
           
                       |
226 | 68, 115, 118, 131, 159, 183, 225 | dvmptsub 22921 |
. . . . . . . . . 10
                          
                                      |
227 | 226 | breqd 4413 |
. . . . . . . . 9
              
                                                        |
228 | 96, 227 | mpbird 236 |
. . . . . . . 8
                                       |
229 | | eqid 2451 |
. . . . . . . . 9
                  
             
                                   
                                 
                                   
             
                |
230 | 115, 159 | subcld 9986 |
. . . . . . . . . 10
 
                        
        |
231 | | eqid 2451 |
. . . . . . . . . 10
          
             
                               
        |
232 | 230, 231 | fmptd 6046 |
. . . . . . . . 9
                                       |
233 | 209, 187,
229, 124, 232, 70 | eldv 22853 |
. . . . . . . 8
              
                       
       ℂfld ↾t     
                   
                                   
             
               lim      |
234 | 228, 233 | mpbid 214 |
. . . . . . 7
         ℂfld
↾t                         
                                   
             
               lim     |
235 | 234 | simprd 465 |
. . . . . 6
                                                        
                             lim    |
236 | | eldifi 3555 |
. . . . . . . . . 10
    
  |
237 | | fveq2 5865 |
. . . . . . . . . . . . . 14
         
             
       |
238 | | fveq2 5865 |
. . . . . . . . . . . . . 14
         
             
       |
239 | 237, 238 | oveq12d 6308 |
. . . . . . . . . . . . 13
                        
                             
        |
240 | | ovex 6318 |
. . . . . . . . . . . . 13
         
             
       |
241 | 239, 231,
240 | fvmpt 5948 |
. . . . . . . . . . . 12
                                                                     |
242 | | fveq2 5865 |
. . . . . . . . . . . . . . . 16
         
             
       |
243 | | fveq2 5865 |
. . . . . . . . . . . . . . . 16
         
             
       |
244 | 242, 243 | oveq12d 6308 |
. . . . . . . . . . . . . . 15
                        
                             
        |
245 | | ovex 6318 |
. . . . . . . . . . . . . . 15
         
             
       |
246 | 244, 231,
245 | fvmpt 5948 |
. . . . . . . . . . . . . 14
                                                                     |
247 | 60, 246 | syl 17 |
. . . . . . . . . . . . 13
            
                                 
                      |
248 | 68, 69, 70, 108, 77, 78 | dvntaylp0 23327 |
. . . . . . . . . . . . . 14
                       
       |
249 | 248 | oveq2d 6306 |
. . . . . . . . . . . . 13
                                                               |
250 | 114, 60 | ffvelrnd 6023 |
. . . . . . . . . . . . . 14
                 |
251 | 250 | subidd 9974 |
. . . . . . . . . . . . 13
                                 |
252 | 247, 249,
251 | 3eqtrd 2489 |
. . . . . . . . . . . 12
            
                          |
253 | 241, 252 | oveqan12rd 6310 |
. . . . . . . . . . 11
 
             
                                   
             
                                             |
254 | 114 | ffvelrnda 6022 |
. . . . . . . . . . . . 13
 
         
       |
255 | 132 | sselda 3432 |
. . . . . . . . . . . . . 14
 
   |
256 | 157 | ffvelrnda 6022 |
. . . . . . . . . . . . . 14
 

        
       |
257 | 255, 256 | syldan 473 |
. . . . . . . . . . . . 13
 
         
       |
258 | 254, 257 | subcld 9986 |
. . . . . . . . . . . 12
 
                        
        |
259 | 258 | subid1d 9975 |
. . . . . . . . . . 11
 
                                                        
        |
260 | 253, 259 | eqtr2d 2486 |
. . . . . . . . . 10
 
                        
                  
                                   
             
             |
261 | 236, 260 | sylan2 477 |
. . . . . . . . 9
 

                                              
             
                                   
             |
262 | 132 | ssdifssd 3571 |
. . . . . . . . . . . 12
       |
263 | 262 | sselda 3432 |
. . . . . . . . . . 11
 

   
  |
264 | 132, 60 | sseldd 3433 |
. . . . . . . . . . . 12
   |
265 | 264 | adantr 467 |
. . . . . . . . . . 11
 

   
  |
266 | 263, 265 | subcld 9986 |
. . . . . . . . . 10
 

        |
267 | 266 | exp1d 12411 |
. . . . . . . . 9
 

              |
268 | 261, 267 | oveq12d 6308 |
. . . . . . . 8
 

              
                                                      
                                                    |
269 | 268 | mpteq2dva 4489 |
. . . . . . 7
                              
                                                                    
                               |
270 | 269 | oveq1d 6305 |
. . . . . 6
                               
              lim                                                         
                             lim    |
271 | 235, 270 | eleqtrrd 2532 |
. . . . 5
                 
             
              lim    |
272 | 271 | a1i 11 |
. . . 4
    
                 
             
              lim     |
273 | | taylthlem1.i |
. . . . . . 7
 
  ..^                               
              lim                    
               
                  lim    |
274 | 273 | expr 620 |
. . . . . 6
 
 ..^                                 
              lim 
                 
              
                  lim     |
275 | 274 | expcom 437 |
. . . . 5
  ..^
                                
              lim 
                 
              
                  lim      |
276 | 275 | a2d 29 |
. . . 4
  ..^
                                
              lim                     
              
                  lim      |
277 | 15, 35, 47, 59, 272, 276 | fzind2 12023 |
. . 3
                                    
              lim     |
278 | 3, 277 | mpcom 37 |
. 2
                 
             
              lim    |
279 | 119 | subidd 9974 |
. . . . . . . . . 10
     |
280 | 279 | fveq2d 5869 |
. . . . . . . . 9
        
            |
281 | | dvn0 22878 |
. . . . . . . . . 10
 
             |
282 | 124, 84, 281 | syl2anc 667 |
. . . . . . . . 9
           |
283 | 280, 282 | eqtrd 2485 |
. . . . . . . 8
        
    |
284 | 283 | fveq1d 5867 |
. . . . . . 7
                     |
285 | 279 | fveq2d 5869 |
. . . . . . . . 9
        
            |
286 | | dvn0 22878 |
. . . . . . . . . 10
 
             |
287 | 193, 199,
286 | sylancr 669 |
. . . . . . . . 9
           |
288 | 285, 287 | eqtrd 2485 |
. . . . . . . 8
        
    |
289 | 288 | fveq1d 5867 |
. . . . . . 7
                     |
290 | 284, 289 | oveq12d 6308 |
. . . . . 6
                                           |
291 | 290 | oveq1d 6305 |
. . . . 5
           
                                               |
292 | 291 | mpteq2dv 4490 |
. . . 4
                              
                                        |
293 | | taylthlem1.r |
. . . 4
                         |
294 | 292, 293 | syl6eqr 2503 |
. . 3
                              
                |
295 | 294 | oveq1d 6305 |
. 2
                               
              lim   lim    |
296 | 278, 295 | eleqtrd 2531 |
1
  lim    |