Step | Hyp | Ref
| Expression |
1 | | fourierdlem46.h |
. . . . . . . . 9
          ![[,] [,]](_icc.gif)     |
2 | | pire 23406 |
. . . . . . . . . . . . 13
 |
3 | 2 | a1i 11 |
. . . . . . . . . . . 12
   |
4 | 3 | renegcld 10043 |
. . . . . . . . . . 11
    |
5 | | fourierdlem46.c |
. . . . . . . . . . 11
   |
6 | | tpssi 4137 |
. . . . . . . . . . 11
  
    
   |
7 | 4, 3, 5, 6 | syl3anc 1267 |
. . . . . . . . . 10
    
   |
8 | 4, 3 | iccssred 37596 |
. . . . . . . . . . 11
    ![[,] [,]](_icc.gif) 
  |
9 | 8 | ssdifssd 3570 |
. . . . . . . . . 10
     ![[,] [,]](_icc.gif)  
  |
10 | 7, 9 | unssd 3609 |
. . . . . . . . 9
           ![[,] [,]](_icc.gif)      |
11 | 1, 10 | syl5eqss 3475 |
. . . . . . . 8

  |
12 | | fourierdlem46.qf |
. . . . . . . . 9
           |
13 | | fourierdlem46.i |
. . . . . . . . . 10
  ..^   |
14 | | elfzofz 11932 |
. . . . . . . . . 10
  ..^
      |
15 | 13, 14 | syl 17 |
. . . . . . . . 9
       |
16 | 12, 15 | ffvelrnd 6021 |
. . . . . . . 8
       |
17 | 11, 16 | sseldd 3432 |
. . . . . . 7
       |
18 | 17 | adantr 467 |
. . . . . 6
 
    
      |
19 | | fzofzp1 12005 |
. . . . . . . . . . 11
  ..^
        |
20 | 13, 19 | syl 17 |
. . . . . . . . . 10
         |
21 | 12, 20 | ffvelrnd 6021 |
. . . . . . . . 9
         |
22 | 11, 21 | sseldd 3432 |
. . . . . . . 8
         |
23 | 22 | rexrd 9687 |
. . . . . . 7
         |
24 | 23 | adantr 467 |
. . . . . 6
 
    
        |
25 | | fourierdlem46.10 |
. . . . . . 7
    
        |
26 | 25 | adantr 467 |
. . . . . 6
 
    
            |
27 | | simpr 463 |
. . . . . . . . . . . . 13
     
    
      |
28 | | simpl 459 |
. . . . . . . . . . . . 13
     
    
      |
29 | 27, 28 | eqeltrd 2528 |
. . . . . . . . . . . 12
     
    
  |
30 | 29 | adantll 719 |
. . . . . . . . . . 11
       
    
  |
31 | 30 | adantlr 720 |
. . . . . . . . . 10
                               |
32 | | ssun2 3597 |
. . . . . . . . . . . . . . . . . . 19
    ![[,] [,]](_icc.gif)      
 
    ![[,] [,]](_icc.gif)     |
33 | 32, 1 | sseqtr4i 3464 |
. . . . . . . . . . . . . . . . . 18
    ![[,] [,]](_icc.gif)    |
34 | | fourierdlem46.qiss |
. . . . . . . . . . . . . . . . . . . . . 22
              
       |
35 | | ioossicc 11717 |
. . . . . . . . . . . . . . . . . . . . . 22
        ![[,] [,]](_icc.gif)   |
36 | 34, 35 | syl6ss 3443 |
. . . . . . . . . . . . . . . . . . . . 21
              
   ![[,] [,]](_icc.gif)    |
37 | 36 | sselda 3431 |
. . . . . . . . . . . . . . . . . . . 20
 
                  ![[,] [,]](_icc.gif)    |
38 | 37 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
                 
    ![[,] [,]](_icc.gif)    |
39 | | simpr 463 |
. . . . . . . . . . . . . . . . . . 19
                 

  |
40 | 38, 39 | eldifd 3414 |
. . . . . . . . . . . . . . . . . 18
                 
     ![[,] [,]](_icc.gif) 
   |
41 | 33, 40 | sseldi 3429 |
. . . . . . . . . . . . . . . . 17
                 
   |
42 | | fourierdlem46.ranq |
. . . . . . . . . . . . . . . . . . 19
   |
43 | 42 | eqcomd 2456 |
. . . . . . . . . . . . . . . . . 18
   |
44 | 43 | ad2antrr 731 |
. . . . . . . . . . . . . . . . 17
                 
   |
45 | 41, 44 | eleqtrd 2530 |
. . . . . . . . . . . . . . . 16
                 
   |
46 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
47 | | ffn 5726 |
. . . . . . . . . . . . . . . . . . . . . . 23
        
      |
48 | 12, 47 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
49 | 48 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . 21
 
       |
50 | | fvelrnb 5910 |
. . . . . . . . . . . . . . . . . . . . 21
                   |
51 | 49, 50 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
 
               |
52 | 46, 51 | mpbid 214 |
. . . . . . . . . . . . . . . . . . 19
 
             |
53 | 52 | adantlr 720 |
. . . . . . . . . . . . . . . . . 18
                   
           |
54 | | elfzelz 11797 |
. . . . . . . . . . . . . . . . . . . . 21
       |
55 | 54 | ad2antlr 732 |
. . . . . . . . . . . . . . . . . . . 20
               
                 |
56 | | simplll 767 |
. . . . . . . . . . . . . . . . . . . . . 22
   
              
         
  |
57 | | simplr 761 |
. . . . . . . . . . . . . . . . . . . . . 22
   
              
         
      |
58 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                             |
59 | | simplr 761 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                       |
60 | 58, 59 | eqeltrd 2528 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                           |
61 | 60 | adantlr 720 |
. . . . . . . . . . . . . . . . . . . . . 22
   
              
         
                    |
62 | | elfzoelz 11917 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  ..^
  |
63 | 13, 62 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
64 | 63 | ad2antrr 731 |
. . . . . . . . . . . . . . . . . . . . . . 23
                             |
65 | 17 | rexrd 9687 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       |
66 | 65 | ad2antrr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                                 |
67 | 23 | ad2antrr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                                   |
68 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                                               |
69 | | ioogtlb 37586 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
           
                             |
70 | 66, 67, 68, 69 | syl3anc 1267 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                     |
71 | | fourierdlem46.qiso |
. . . . . . . . . . . . . . . . . . . . . . . . . 26

         |
72 | 71 | ad2antrr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                                    |
73 | 15 | ad2antrr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                                 |
74 | | simplr 761 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                                 |
75 | | isorel 6215 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
           
                  |
76 | 72, 73, 74, 75 | syl12anc 1265 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                           
           |
77 | 70, 76 | mpbird 236 |
. . . . . . . . . . . . . . . . . . . . . . 23
                             |
78 | | iooltub 37604 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
           
                               |
79 | 66, 67, 68, 78 | syl3anc 1267 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                       |
80 | 20 | ad2antrr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                                   |
81 | | isorel 6215 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
           
              
         |
82 | 72, 74, 80, 81 | syl12anc 1265 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                           
 
             |
83 | 79, 82 | mpbird 236 |
. . . . . . . . . . . . . . . . . . . . . . 23
                               |
84 | | btwnnz 11009 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
  |
85 | 64, 77, 83, 84 | syl3anc 1267 |
. . . . . . . . . . . . . . . . . . . . . 22
                          
  |
86 | 56, 57, 61, 85 | syl21anc 1266 |
. . . . . . . . . . . . . . . . . . . . 21
   
              
         
  |
87 | 86 | adantllr 724 |
. . . . . . . . . . . . . . . . . . . 20
               
              
  |
88 | 55, 87 | pm2.65da 579 |
. . . . . . . . . . . . . . . . . . 19
   
              
     
      |
89 | 88 | nrexdv 2842 |
. . . . . . . . . . . . . . . . . 18
                               |
90 | 53, 89 | pm2.65da 579 |
. . . . . . . . . . . . . . . . 17
 
              
  |
91 | 90 | adantr 467 |
. . . . . . . . . . . . . . . 16
                 

  |
92 | 45, 91 | condan 802 |
. . . . . . . . . . . . . . 15
 
                 |
93 | 92 | ralrimiva 2801 |
. . . . . . . . . . . . . 14
                   |
94 | | dfss3 3421 |
. . . . . . . . . . . . . 14
              
                  |
95 | 93, 94 | sylibr 216 |
. . . . . . . . . . . . 13
              
  |
96 | 95 | ad2antrr 731 |
. . . . . . . . . . . 12
                 
                  
  |
97 | 65 | ad2antrr 731 |
. . . . . . . . . . . . 13
                 
           |
98 | 23 | ad2antrr 731 |
. . . . . . . . . . . . 13
                 
             |
99 | | icossre 11712 |
. . . . . . . . . . . . . . . 16
                             |
100 | 17, 23, 99 | syl2anc 666 |
. . . . . . . . . . . . . . 15
              
  |
101 | 100 | sselda 3431 |
. . . . . . . . . . . . . 14
 
                 |
102 | 101 | adantr 467 |
. . . . . . . . . . . . 13
                 
    
  |
103 | 17 | ad2antrr 731 |
. . . . . . . . . . . . . 14
                 
           |
104 | 65 | adantr 467 |
. . . . . . . . . . . . . . . 16
 
                     |
105 | 23 | adantr 467 |
. . . . . . . . . . . . . . . 16
 
                       |
106 | | simpr 463 |
. . . . . . . . . . . . . . . 16
 
                               |
107 | | icogelb 11683 |
. . . . . . . . . . . . . . . 16
           
                     |
108 | 104, 105,
106, 107 | syl3anc 1267 |
. . . . . . . . . . . . . . 15
 
                     |
109 | 108 | adantr 467 |
. . . . . . . . . . . . . 14
                 
        
  |
110 | | neqne 37368 |
. . . . . . . . . . . . . . 15
           |
111 | 110 | adantl 468 |
. . . . . . . . . . . . . 14
                 
           |
112 | 103, 102,
109, 111 | leneltd 9786 |
. . . . . . . . . . . . 13
                 
        
  |
113 | | icoltub 37601 |
. . . . . . . . . . . . . . 15
           
                       |
114 | 104, 105,
106, 113 | syl3anc 1267 |
. . . . . . . . . . . . . 14
 
                       |
115 | 114 | adantr 467 |
. . . . . . . . . . . . 13
                 
        
    |
116 | 97, 98, 102, 112, 115 | eliood 37589 |
. . . . . . . . . . . 12
                 
    
                |
117 | 96, 116 | sseldd 3432 |
. . . . . . . . . . 11
                 
    
  |
118 | 117 | adantllr 724 |
. . . . . . . . . 10
                            
  |
119 | 31, 118 | pm2.61dan 799 |
. . . . . . . . 9
       
              
  |
120 | 119 | ralrimiva 2801 |
. . . . . . . 8
 
    
                  |
121 | | dfss3 3421 |
. . . . . . . 8
              
                  |
122 | 120, 121 | sylibr 216 |
. . . . . . 7
 
    
                |
123 | | fourierdlem46.cn |
. . . . . . . 8
       |
124 | 123 | adantr 467 |
. . . . . . 7
 
    
      |
125 | | rescncf 21922 |
. . . . . . 7
              
                                          |
126 | 122, 124,
125 | sylc 62 |
. . . . . 6
 
    
                                    |
127 | 18, 24, 26, 126 | icocncflimc 37761 |
. . . . 5
 
    
                                         
               lim        |
128 | 17 | leidd 10177 |
. . . . . . . . 9
    
      |
129 | 65, 23, 65, 128, 25 | elicod 11682 |
. . . . . . . 8
               
     |
130 | | fvres 5877 |
. . . . . . . 8
                                                     |
131 | 129, 130 | syl 17 |
. . . . . . 7
                                   |
132 | 131 | eqcomd 2456 |
. . . . . 6
          
                        |
133 | 132 | adantr 467 |
. . . . 5
 
    
                                  |
134 | | ioossico 11720 |
. . . . . . . . 9
          
                  |
135 | 134 | a1i 11 |
. . . . . . . 8
 
    
                              |
136 | 135 | resabs1d 5133 |
. . . . . . 7
 
    
                                
                 |
137 | 136 | eqcomd 2456 |
. . . . . 6
 
    
                                
                 |
138 | 137 | oveq1d 6303 |
. . . . 5
 
    
                 lim                       
               lim        |
139 | 127, 133,
138 | 3eltr4d 2543 |
. . . 4
 
    
                         lim        |
140 | | ne0i 3736 |
. . . 4
                          lim     
                 lim        |
141 | 139, 140 | syl 17 |
. . 3
 
    
                 lim        |
142 | | pnfxr 11409 |
. . . . . . . . 9
 |
143 | 142 | a1i 11 |
. . . . . . . . . 10
   |
144 | 22 | ltpnfd 11420 |
. . . . . . . . . 10
         |
145 | 23, 143, 144 | xrltled 37478 |
. . . . . . . . 9
      
  |
146 | | iooss2 11669 |
. . . . . . . . 9
                               |
147 | 142, 145,
146 | sylancr 668 |
. . . . . . . 8
              
         |
148 | 147 | resabs1d 5133 |
. . . . . . 7
                                            |
149 | 148 | oveq1d 6303 |
. . . . . 6
                           lim                       lim        |
150 | 149 | eqcomd 2456 |
. . . . 5
                  lim              
                 lim        |
151 | 150 | adantr 467 |
. . . 4
 
                      lim              
                 lim        |
152 | | limcresi 22833 |
. . . . 5
 
        lim     
        
                 lim       |
153 | 17 | adantr 467 |
. . . . . 6
 
           |
154 | | simpl 459 |
. . . . . . 7
 
       |
155 | 2 | renegcli 9932 |
. . . . . . . . . . . 12
  |
156 | 155 | rexri 9690 |
. . . . . . . . . . 11
  |
157 | 156 | a1i 11 |
. . . . . . . . . 10
    |
158 | 2 | rexri 9690 |
. . . . . . . . . . 11
 |
159 | 158 | a1i 11 |
. . . . . . . . . 10
   |
160 | 4, 3, 17, 22, 25, 34 | fourierdlem10 37973 |
. . . . . . . . . . 11
          
     |
161 | 160 | simpld 461 |
. . . . . . . . . 10
        |
162 | 160 | simprd 465 |
. . . . . . . . . . 11
      
  |
163 | 17, 22, 3, 25, 162 | ltletrd 9792 |
. . . . . . . . . 10
    
  |
164 | 157, 159,
65, 161, 163 | elicod 11682 |
. . . . . . . . 9
            |
165 | 164 | adantr 467 |
. . . . . . . 8
 
                |
166 | | simpr 463 |
. . . . . . . 8
 
           |
167 | 165, 166 | eldifd 3414 |
. . . . . . 7
 
                  |
168 | 154, 167 | jca 535 |
. . . . . 6
 
     
              |
169 | | eleq1 2516 |
. . . . . . . . 9
                           |
170 | 169 | anbi2d 709 |
. . . . . . . 8
      
       
                |
171 | | oveq1 6295 |
. . . . . . . . . . 11
      
          |
172 | 171 | reseq2d 5104 |
. . . . . . . . . 10
          
          |
173 | | id 22 |
. . . . . . . . . 10
           |
174 | 172, 173 | oveq12d 6306 |
. . . . . . . . 9
        
  lim
          
lim        |
175 | 174 | neeq1d 2682 |
. . . . . . . 8
           
lim           
lim         |
176 | 170, 175 | imbi12d 322 |
. . . . . . 7
       
     
 
      lim  
           
         
  lim
         |
177 | | fourierdlem46.rlim |
. . . . . . 7
 
           
  lim
   |
178 | 176, 177 | vtoclg 3106 |
. . . . . 6
      
                   
  lim
        |
179 | 153, 168,
178 | sylc 62 |
. . . . 5
 
              
lim        |
180 | | ssn0 3766 |
. . . . 5
           
lim        
                       lim     
          lim                                 lim        |
181 | 152, 179,
180 | sylancr 668 |
. . . 4
 
                               lim        |
182 | 151, 181 | eqnetrd 2690 |
. . 3
 
                      lim        |
183 | 141, 182 | pm2.61dan 799 |
. 2
                  lim        |
184 | 65 | adantr 467 |
. . . . . 6
 
      
      |
185 | 22 | adantr 467 |
. . . . . 6
 
      
        |
186 | 25 | adantr 467 |
. . . . . 6
 
      
            |
187 | | simpr 463 |
. . . . . . . . . . . . 13
       
      
        |
188 | | simpl 459 |
. . . . . . . . . . . . 13
       
      
        |
189 | 187, 188 | eqeltrd 2528 |
. . . . . . . . . . . 12
       
      
  |
190 | 189 | adantll 719 |
. . . . . . . . . . 11
                
  |
191 | 190 | adantlr 720 |
. . . . . . . . . 10
                 ![(,] (,]](_ioc.gif)                  |
192 | 95 | ad2antrr 731 |
. . . . . . . . . . . 12
         ![(,] (,]](_ioc.gif)        
                    
  |
193 | 65 | ad2antrr 731 |
. . . . . . . . . . . . 13
         ![(,] (,]](_ioc.gif)        
             |
194 | 23 | ad2antrr 731 |
. . . . . . . . . . . . 13
         ![(,] (,]](_ioc.gif)        
               |
195 | 65 | adantr 467 |
. . . . . . . . . . . . . . . 16
 
      ![(,] (,]](_ioc.gif)               |
196 | 22 | adantr 467 |
. . . . . . . . . . . . . . . 16
 
      ![(,] (,]](_ioc.gif)                 |
197 | | iocssre 11711 |
. . . . . . . . . . . . . . . 16
                   ![(,] (,]](_ioc.gif)       
  |
198 | 195, 196,
197 | syl2anc 666 |
. . . . . . . . . . . . . . 15
 
      ![(,] (,]](_ioc.gif)               ![(,] (,]](_ioc.gif)          |
199 | | simpr 463 |
. . . . . . . . . . . . . . 15
 
      ![(,] (,]](_ioc.gif)               ![(,] (,]](_ioc.gif)          |
200 | 198, 199 | sseldd 3432 |
. . . . . . . . . . . . . 14
 
      ![(,] (,]](_ioc.gif)           |
201 | 200 | adantr 467 |
. . . . . . . . . . . . 13
         ![(,] (,]](_ioc.gif)        
      
  |
202 | 23 | adantr 467 |
. . . . . . . . . . . . . . 15
 
      ![(,] (,]](_ioc.gif)                 |
203 | | iocgtlb 37593 |
. . . . . . . . . . . . . . 15
           
      ![(,] (,]](_ioc.gif)               |
204 | 195, 202,
199, 203 | syl3anc 1267 |
. . . . . . . . . . . . . 14
 
      ![(,] (,]](_ioc.gif)               |
205 | 204 | adantr 467 |
. . . . . . . . . . . . 13
         ![(,] (,]](_ioc.gif)        
          
  |
206 | 22 | ad2antrr 731 |
. . . . . . . . . . . . . 14
         ![(,] (,]](_ioc.gif)        
               |
207 | | iocleub 37594 |
. . . . . . . . . . . . . . . 16
           
      ![(,] (,]](_ioc.gif)                 |
208 | 195, 202,
199, 207 | syl3anc 1267 |
. . . . . . . . . . . . . . 15
 
      ![(,] (,]](_ioc.gif)                 |
209 | 208 | adantr 467 |
. . . . . . . . . . . . . 14
         ![(,] (,]](_ioc.gif)        
          
    |
210 | | neqne 37368 |
. . . . . . . . . . . . . . . 16
          
    |
211 | 210 | necomd 2678 |
. . . . . . . . . . . . . . 15
               |
212 | 211 | adantl 468 |
. . . . . . . . . . . . . 14
         ![(,] (,]](_ioc.gif)        
               |
213 | 201, 206,
209, 212 | leneltd 9786 |
. . . . . . . . . . . . 13
         ![(,] (,]](_ioc.gif)        
          
    |
214 | 193, 194,
201, 205, 213 | eliood 37589 |
. . . . . . . . . . . 12
         ![(,] (,]](_ioc.gif)        
      
                |
215 | 192, 214 | sseldd 3432 |
. . . . . . . . . . 11
         ![(,] (,]](_ioc.gif)        
      
  |
216 | 215 | adantllr 724 |
. . . . . . . . . 10
                 ![(,] (,]](_ioc.gif)            
  
  |
217 | 191, 216 | pm2.61dan 799 |
. . . . . . . . 9
                ![(,] (,]](_ioc.gif)        
  |
218 | 217 | ralrimiva 2801 |
. . . . . . . 8
 
      
       ![(,] (,]](_ioc.gif)           |
219 | | dfss3 3421 |
. . . . . . . 8
       ![(,] (,]](_ioc.gif)       
       ![(,] (,]](_ioc.gif)           |
220 | 218, 219 | sylibr 216 |
. . . . . . 7
 
      
      ![(,] (,]](_ioc.gif)          |
221 | 123 | adantr 467 |
. . . . . . 7
 
      
      |
222 | | rescncf 21922 |
. . . . . . 7
       ![(,] (,]](_ioc.gif)       
            ![(,] (,]](_ioc.gif)                ![(,] (,]](_ioc.gif)              |
223 | 220, 221,
222 | sylc 62 |
. . . . . 6
 
      
       ![(,] (,]](_ioc.gif)                ![(,] (,]](_ioc.gif)             |
224 | 184, 185,
186, 223 | ioccncflimc 37757 |
. . . . 5
 
      
        ![(,] (,]](_ioc.gif)                           ![(,] (,]](_ioc.gif)        
               lim          |
225 | 22 | leidd 10177 |
. . . . . . . . . 10
      
        |
226 | 65, 23, 23, 25, 225 | eliocd 37599 |
. . . . . . . . 9
             ![(,] (,]](_ioc.gif)    
     |
227 | | fvres 5877 |
. . . . . . . . 9
             ![(,] (,]](_ioc.gif)                ![(,] (,]](_ioc.gif)                              |
228 | 226, 227 | syl 17 |
. . . . . . . 8
         ![(,] (,]](_ioc.gif)                        
     |
229 | 228 | eqcomd 2456 |
. . . . . . 7
            
      ![(,] (,]](_ioc.gif)                    |
230 | | ioossioc 37582 |
. . . . . . . . . . 11
          
         ![(,] (,]](_ioc.gif)         |
231 | | resabs1 5132 |
. . . . . . . . . . 11
                     ![(,] (,]](_ioc.gif)                ![(,] (,]](_ioc.gif)        
                                 |
232 | 230, 231 | ax-mp 5 |
. . . . . . . . . 10
 
      ![(,] (,]](_ioc.gif)                        
                |
233 | 232 | eqcomi 2459 |
. . . . . . . . 9
                        ![(,] (,]](_ioc.gif)        
                |
234 | 233 | oveq1i 6298 |
. . . . . . . 8
 
               lim                 ![(,] (,]](_ioc.gif)        
               lim         |
235 | 234 | a1i 11 |
. . . . . . 7
                  lim                 ![(,] (,]](_ioc.gif)        
               lim          |
236 | 229, 235 | eleq12d 2522 |
. . . . . 6
             
               lim                ![(,] (,]](_ioc.gif)                           ![(,] (,]](_ioc.gif)        
               lim           |
237 | 236 | adantr 467 |
. . . . 5
 
      
                            lim                ![(,] (,]](_ioc.gif)                           ![(,] (,]](_ioc.gif)        
               lim           |
238 | 224, 237 | mpbird 236 |
. . . 4
 
      
                           lim          |
239 | | ne0i 3736 |
. . . 4
                            lim       
                 lim          |
240 | 238, 239 | syl 17 |
. . 3
 
      
                 lim          |
241 | | mnfxr 11411 |
. . . . . . . . 9
 |
242 | 241 | a1i 11 |
. . . . . . . . . 10
   |
243 | 17 | mnfltd 11423 |
. . . . . . . . . 10

      |
244 | 242, 65, 243 | xrltled 37478 |
. . . . . . . . 9

      |
245 | | iooss1 11668 |
. . . . . . . . 9
                               |
246 | 241, 244,
245 | sylancr 668 |
. . . . . . . 8
              
           |
247 | 246 | resabs1d 5133 |
. . . . . . 7
            
                                 |
248 | 247 | eqcomd 2456 |
. . . . . 6
                  
                           |
249 | 248 | adantr 467 |
. . . . 5
 
                              
                     |
250 | 249 | oveq1d 6303 |
. . . 4
 
                        lim                
                   lim          |
251 | | limcresi 22833 |
. . . . 5
 
          lim       
        
                   lim         |
252 | 22 | adantr 467 |
. . . . . 6
 
          
    |
253 | | simpl 459 |
. . . . . . 7
 
         |
254 | 156 | a1i 11 |
. . . . . . . . 9
 
          |
255 | 158 | a1i 11 |
. . . . . . . . 9
 
         |
256 | 23 | adantr 467 |
. . . . . . . . 9
 
          
    |
257 | 4, 17, 22, 161, 25 | lelttrd 9790 |
. . . . . . . . . 10
          |
258 | 257 | adantr 467 |
. . . . . . . . 9
 
                |
259 | 162 | adantr 467 |
. . . . . . . . 9
 
          
    |
260 | 254, 255,
256, 258, 259 | eliocd 37599 |
. . . . . . . 8
 
          
     ![(,] (,]](_ioc.gif)    |
261 | | simpr 463 |
. . . . . . . 8
 
      
        |
262 | 260, 261 | eldifd 3414 |
. . . . . . 7
 
          
      ![(,] (,]](_ioc.gif) 
   |
263 | 253, 262 | jca 535 |
. . . . . 6
 
                  ![(,] (,]](_ioc.gif)      |
264 | | eleq1 2516 |
. . . . . . . . 9
    
       ![(,] (,]](_ioc.gif)             ![(,] (,]](_ioc.gif)      |
265 | 264 | anbi2d 709 |
. . . . . . . 8
    
   
    ![(,] (,]](_ioc.gif)   
           ![(,] (,]](_ioc.gif)       |
266 | | oveq2 6296 |
. . . . . . . . . . 11
    
                |
267 | 266 | reseq2d 5104 |
. . . . . . . . . 10
    
             
      |
268 | | id 22 |
. . . . . . . . . 10
    
     
    |
269 | 267, 268 | oveq12d 6306 |
. . . . . . . . 9
    
        lim              lim          |
270 | 269 | neeq1d 2682 |
. . . . . . . 8
    
         lim   
          lim           |
271 | 265, 270 | imbi12d 322 |
. . . . . . 7
    
    
    ![(,] (,]](_ioc.gif) 
 
      lim  
     
      ![(,] (,]](_ioc.gif) 
         
    lim    
       |
272 | | fourierdlem46.llim |
. . . . . . 7
 
    ![(,] (,]](_ioc.gif)          lim    |
273 | 271, 272 | vtoclg 3106 |
. . . . . 6
        
          ![(,] (,]](_ioc.gif)                lim           |
274 | 252, 263,
273 | sylc 62 |
. . . . 5
 
        
          lim          |
275 | | ssn0 3766 |
. . . . 5
              lim          
                         lim         
          lim           
                         lim          |
276 | 251, 274,
275 | sylancr 668 |
. . . 4
 
         
                         lim          |
277 | 250, 276 | eqnetrd 2690 |
. . 3
 
                        lim          |
278 | 240, 277 | pm2.61dan 799 |
. 2
                  lim          |
279 | 183, 278 | jca 535 |
1
                   lim                       lim           |