Step | Hyp | Ref
| Expression |
1 | | fourierdlem112.23 |
. . . . 5
                             |
2 | | fveq2 5865 |
. . . . . . . 8
           |
3 | | oveq1 6297 |
. . . . . . . . 9
       |
4 | 3 | fveq2d 5869 |
. . . . . . . 8
               |
5 | 2, 4 | oveq12d 6308 |
. . . . . . 7
                           |
6 | | fveq2 5865 |
. . . . . . . 8
           |
7 | 3 | fveq2d 5869 |
. . . . . . . 8
               |
8 | 6, 7 | oveq12d 6308 |
. . . . . . 7
                           |
9 | 5, 8 | oveq12d 6308 |
. . . . . 6
                                                       |
10 | 9 | cbvmptv 4495 |
. . . . 5
                                                         |
11 | 1, 10 | eqtri 2473 |
. . . 4
                             |
12 | | seqeq3 12218 |
. . . 4
                            
                                    |
13 | 11, 12 | mp1i 13 |
. . 3
                                     |
14 | | nnuz 11194 |
. . . . 5
     |
15 | | 1zzd 10968 |
. . . . 5
   |
16 | | nfv 1761 |
. . . . . . 7
   |
17 | | nfcv 2592 |
. . . . . . . 8
   |
18 | | nfcv 2592 |
. . . . . . . . 9
        |
19 | | nfcv 2592 |
. . . . . . . . . 10
     
   |
20 | | nfcv 2592 |
. . . . . . . . . 10
  |
21 | | nfcv 2592 |
. . . . . . . . . 10
           |
22 | 19, 20, 21 | nfov 6316 |
. . . . . . . . 9
      
            |
23 | 18, 22 | nfitg 22732 |
. . . . . . . 8
                           |
24 | 17, 23 | nfmpt 4491 |
. . . . . . 7
                             |
25 | | nfcv 2592 |
. . . . . . . . 9
       |
26 | 25, 22 | nfitg 22732 |
. . . . . . . 8
                          |
27 | 17, 26 | nfmpt 4491 |
. . . . . . 7
                            |
28 | | fourierdlem112.z |
. . . . . . . 8
                                           |
29 | | fourierdlem112.a |
. . . . . . . . . . . . 13
                         |
30 | | nfmpt1 4492 |
. . . . . . . . . . . . 13
                           |
31 | 29, 30 | nfcxfr 2590 |
. . . . . . . . . . . 12
   |
32 | | nfcv 2592 |
. . . . . . . . . . . 12
   |
33 | 31, 32 | nffv 5872 |
. . . . . . . . . . 11
       |
34 | | nfcv 2592 |
. . . . . . . . . . 11
  |
35 | | nfcv 2592 |
. . . . . . . . . . 11
   |
36 | 33, 34, 35 | nfov 6316 |
. . . . . . . . . 10
         |
37 | | nfcv 2592 |
. . . . . . . . . 10
  |
38 | | nfcv 2592 |
. . . . . . . . . . 11
       |
39 | 38 | nfsum1 13756 |
. . . . . . . . . 10
                                   |
40 | 36, 37, 39 | nfov 6316 |
. . . . . . . . 9
                                           |
41 | 17, 40 | nfmpt 4491 |
. . . . . . . 8
                                             |
42 | 28, 41 | nfcxfr 2590 |
. . . . . . 7
   |
43 | | fourierdlem112.f |
. . . . . . . 8
       |
44 | | fourierdlem112.25 |
. . . . . . . 8
   |
45 | | eqid 2451 |
. . . . . . . 8
                          ..^                                         ..^                |
46 | | picn 23414 |
. . . . . . . . . . . . 13
 |
47 | 46 | 2timesi 10730 |
. . . . . . . . . . . 12
     |
48 | | fourierdlem112.t |
. . . . . . . . . . . 12
   |
49 | 46, 46 | subnegi 9953 |
. . . . . . . . . . . 12
      |
50 | 47, 48, 49 | 3eqtr4i 2483 |
. . . . . . . . . . 11
    |
51 | | fourierdlem112.p |
. . . . . . . . . . 11
 
                  
 ..^                |
52 | | fourierdlem112.m |
. . . . . . . . . . 11
   |
53 | | fourierdlem112.q |
. . . . . . . . . . 11
       |
54 | | pire 23413 |
. . . . . . . . . . . . . 14
 |
55 | 54 | a1i 11 |
. . . . . . . . . . . . 13
   |
56 | 55 | renegcld 10046 |
. . . . . . . . . . . 12
    |
57 | 56, 44 | readdcld 9670 |
. . . . . . . . . . 11
      |
58 | 55, 44 | readdcld 9670 |
. . . . . . . . . . 11
     |
59 | | negpilt0 37490 |
. . . . . . . . . . . . . 14
  |
60 | | pipos 23415 |
. . . . . . . . . . . . . 14
 |
61 | 54 | renegcli 9935 |
. . . . . . . . . . . . . . 15
  |
62 | | 0re 9643 |
. . . . . . . . . . . . . . 15
 |
63 | 61, 62, 54 | lttri 9760 |
. . . . . . . . . . . . . 14
  
    |
64 | 59, 60, 63 | mp2an 678 |
. . . . . . . . . . . . 13
  |
65 | 64 | a1i 11 |
. . . . . . . . . . . 12
    |
66 | 56, 55, 44, 65 | ltadd1dd 10224 |
. . . . . . . . . . 11
        |
67 | | oveq1 6297 |
. . . . . . . . . . . . . . 15
           |
68 | 67 | eleq1d 2513 |
. . . . . . . . . . . . . 14
             |
69 | 68 | rexbidv 2901 |
. . . . . . . . . . . . 13
  
            |
70 | 69 | cbvrabv 3044 |
. . . . . . . . . . . 12
      ![[,] [,]](_icc.gif)    
           ![[,] [,]](_icc.gif)           |
71 | 70 | uneq2i 3585 |
. . . . . . . . . . 11
               ![[,] [,]](_icc.gif)    
                     ![[,] [,]](_icc.gif)            |
72 | | fourierdlem112.n |
. . . . . . . . . . 11
                   ![[,] [,]](_icc.gif)    
         |
73 | | fourierdlem112.v |
. . . . . . . . . . 11
                        ![[,] [,]](_icc.gif)    
         |
74 | 50, 51, 52, 53, 57, 58, 66, 45, 71, 72, 73 | fourierdlem54 38024 |
. . . . . . . . . 10
                              ..^                                        ![[,] [,]](_icc.gif)               |
75 | 74 | simpld 461 |
. . . . . . . . 9
                             ..^                     |
76 | 75 | simpld 461 |
. . . . . . . 8
   |
77 | 75 | simprd 465 |
. . . . . . . 8
                            ..^                    |
78 | | fourierdlem112.xran |
. . . . . . . 8
   |
79 | 43 | adantr 467 |
. . . . . . . . 9
 
 ..^        |
80 | | fveq2 5865 |
. . . . . . . . . . . . . . . 16
           |
81 | | oveq1 6297 |
. . . . . . . . . . . . . . . . 17
       |
82 | 81 | fveq2d 5869 |
. . . . . . . . . . . . . . . 16
               |
83 | 80, 82 | breq12d 4415 |
. . . . . . . . . . . . . . 15
     
     
             |
84 | 83 | cbvralv 3019 |
. . . . . . . . . . . . . 14
 
 ..^              ..^              |
85 | 84 | anbi2i 700 |
. . . . . . . . . . . . 13
               ..^     
      
              ..^     
         |
86 | 85 | a1i 11 |
. . . . . . . . . . . 12
                    
 ..^            
              ..^     
          |
87 | 86 | rabbiia 3033 |
. . . . . . . . . . 11
                   
 ..^              
                  
 ..^               |
88 | 87 | mpteq2i 4486 |
. . . . . . . . . 10
                    
 ..^                                   
 ..^                |
89 | 51, 88 | eqtri 2473 |
. . . . . . . . 9
 
                  
 ..^                |
90 | 52 | adantr 467 |
. . . . . . . . 9
 
 ..^    |
91 | 53 | adantr 467 |
. . . . . . . . 9
 
 ..^        |
92 | | fourierdlem112.fper |
. . . . . . . . . 10
 

            |
93 | 92 | adantlr 721 |
. . . . . . . . 9
    ..^               |
94 | | eleq1 2517 |
. . . . . . . . . . . . 13
   ..^
 ..^    |
95 | 94 | anbi2d 710 |
. . . . . . . . . . . 12
  
 ..^  
 ..^     |
96 | | fveq2 5865 |
. . . . . . . . . . . . . . 15
           |
97 | 81 | fveq2d 5869 |
. . . . . . . . . . . . . . 15
               |
98 | 96, 97 | oveq12d 6308 |
. . . . . . . . . . . . . 14
                               |
99 | 98 | reseq2d 5105 |
. . . . . . . . . . . . 13
                                   |
100 | 98 | oveq1d 6305 |
. . . . . . . . . . . . 13
                                       |
101 | 99, 100 | eleq12d 2523 |
. . . . . . . . . . . 12
                                   
                                     |
102 | 95, 101 | imbi12d 322 |
. . . . . . . . . . 11
   
 ..^                                    
   ..^                                        |
103 | | fourierdlem112.fcn |
. . . . . . . . . . 11
 
 ..^                                      |
104 | 102, 103 | chvarv 2107 |
. . . . . . . . . 10
 
 ..^                                      |
105 | 104 | adantlr 721 |
. . . . . . . . 9
    ..^   ..^ 
                                    |
106 | 57 | adantr 467 |
. . . . . . . . 9
 
 ..^       |
107 | 57 | rexrd 9690 |
. . . . . . . . . . 11
      |
108 | | pnfxr 11412 |
. . . . . . . . . . . 12
 |
109 | 108 | a1i 11 |
. . . . . . . . . . 11
   |
110 | 58 | ltpnfd 11423 |
. . . . . . . . . . 11
  
  |
111 | 107, 109,
58, 66, 110 | eliood 37595 |
. . . . . . . . . 10
       
   |
112 | 111 | adantr 467 |
. . . . . . . . 9
 
 ..^            |
113 | | id 22 |
. . . . . . . . . . 11
  ..^
 ..^   |
114 | 72 | oveq2i 6301 |
. . . . . . . . . . 11
 ..^  ..^                   ![[,] [,]](_icc.gif)               |
115 | 113, 114 | syl6eleq 2539 |
. . . . . . . . . 10
  ..^
 ..^                   ![[,] [,]](_icc.gif)                |
116 | 115 | adantl 468 |
. . . . . . . . 9
 
 ..^   ..^                   ![[,] [,]](_icc.gif)                |
117 | 72 | oveq2i 6301 |
. . . . . . . . . . . 12
                          ![[,] [,]](_icc.gif)    
          |
118 | | isoeq4 6213 |
. . . . . . . . . . . 12
                           ![[,] [,]](_icc.gif)    
         
                     ![[,] [,]](_icc.gif)    
      
                       ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)               |
119 | 117, 118 | ax-mp 5 |
. . . . . . . . . . 11
                      ![[,] [,]](_icc.gif)    
      
                       ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)              |
120 | 119 | iotabii 5568 |
. . . . . . . . . 10
                        ![[,] [,]](_icc.gif)               
                       ![[,] [,]](_icc.gif)    
                         ![[,] [,]](_icc.gif)    
         |
121 | 73, 120 | eqtri 2473 |
. . . . . . . . 9
                          ![[,] [,]](_icc.gif)    
                         ![[,] [,]](_icc.gif)    
         |
122 | 79, 89, 50, 90, 91, 93, 105, 106, 112, 116, 121 | fourierdlem98 38068 |
. . . . . . . 8
 
 ..^                                      |
123 | | fourierdlem112.fbd |
. . . . . . . . . 10
             |
124 | 123 | adantr 467 |
. . . . . . . . 9
 
 ..^              |
125 | | nfra1 2769 |
. . . . . . . . . . 11
            |
126 | | elioore 11666 |
. . . . . . . . . . . . 13
                 |
127 | | rspa 2755 |
. . . . . . . . . . . . 13
                      |
128 | 126, 127 | sylan2 477 |
. . . . . . . . . . . 12
                                    |
129 | 128 | ex 436 |
. . . . . . . . . . 11
 
                      
           |
130 | 125, 129 | ralrimi 2788 |
. . . . . . . . . 10
 
                               
  |
131 | 130 | reximi 2855 |
. . . . . . . . 9
  
                                   |
132 | 124, 131 | syl 17 |
. . . . . . . 8
 
 ..^                             |
133 | | ssid 3451 |
. . . . . . . . . . . 12
 |
134 | | dvfre 22905 |
. . . . . . . . . . . 12
                 |
135 | 43, 133, 134 | sylancl 668 |
. . . . . . . . . . 11
           |
136 | 135 | adantr 467 |
. . . . . . . . . 10
 
 ..^      
     |
137 | | eqid 2451 |
. . . . . . . . . . . . 13
     |
138 | 54 | a1i 11 |
. . . . . . . . . . . . 13
 
 ..^    |
139 | 61 | a1i 11 |
. . . . . . . . . . . . 13
 
 ..^     |
140 | 98 | reseq2d 5105 |
. . . . . . . . . . . . . . . . 17
                                       |
141 | 140, 100 | eleq12d 2523 |
. . . . . . . . . . . . . . . 16
                                     
                                       |
142 | 95, 141 | imbi12d 322 |
. . . . . . . . . . . . . . 15
   
 ..^                                      
   ..^                                          |
143 | | fourierdlem112.fdvcn |
. . . . . . . . . . . . . . 15
 
 ..^                                        |
144 | 142, 143 | chvarv 2107 |
. . . . . . . . . . . . . 14
 
 ..^                                        |
145 | 144 | adantlr 721 |
. . . . . . . . . . . . 13
    ..^   ..^ 
                                      |
146 | | fourierdlem112.x |
. . . . . . . . . . . . . . 15
   |
147 | 56, 146 | readdcld 9670 |
. . . . . . . . . . . . . 14
      |
148 | 147 | adantr 467 |
. . . . . . . . . . . . 13
 
 ..^       |
149 | 147 | rexrd 9690 |
. . . . . . . . . . . . . . 15
      |
150 | 55, 146 | readdcld 9670 |
. . . . . . . . . . . . . . 15
     |
151 | 56, 55, 146, 65 | ltadd1dd 10224 |
. . . . . . . . . . . . . . 15
        |
152 | 150 | ltpnfd 11423 |
. . . . . . . . . . . . . . 15
  
  |
153 | 149, 109,
150, 151, 152 | eliood 37595 |
. . . . . . . . . . . . . 14
       
   |
154 | 153 | adantr 467 |
. . . . . . . . . . . . 13
 
 ..^            |
155 | | oveq1 6297 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
156 | 155 | oveq2d 6306 |
. . . . . . . . . . . . . . . . . . . . 21
           |
157 | 156 | eleq1d 2513 |
. . . . . . . . . . . . . . . . . . . 20
             |
158 | 157 | cbvrexv 3020 |
. . . . . . . . . . . . . . . . . . 19
     
       |
159 | 158 | rgenw 2749 |
. . . . . . . . . . . . . . . . . 18
      ![[,] [,]](_icc.gif)           
      |
160 | | rabbi 2969 |
. . . . . . . . . . . . . . . . . 18
 
     ![[,] [,]](_icc.gif)                       ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)    
       |
161 | 159, 160 | mpbi 212 |
. . . . . . . . . . . . . . . . 17
      ![[,] [,]](_icc.gif)    
           ![[,] [,]](_icc.gif)           |
162 | 161 | uneq2i 3585 |
. . . . . . . . . . . . . . . 16
               ![[,] [,]](_icc.gif)    
                     ![[,] [,]](_icc.gif)    
       |
163 | | isoeq5 6214 |
. . . . . . . . . . . . . . . 16
                ![[,] [,]](_icc.gif)    
                     ![[,] [,]](_icc.gif)    
     
                        ![[,] [,]](_icc.gif)    
                         ![[,] [,]](_icc.gif)    
      
                       ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)               |
164 | 162, 163 | ax-mp 5 |
. . . . . . . . . . . . . . 15
                        ![[,] [,]](_icc.gif)    
                         ![[,] [,]](_icc.gif)    
      
                       ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)              |
165 | 164 | iotabii 5568 |
. . . . . . . . . . . . . 14
                          ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)               
                       ![[,] [,]](_icc.gif)    
                         ![[,] [,]](_icc.gif)    
         |
166 | 121, 165 | eqtri 2473 |
. . . . . . . . . . . . 13
                          ![[,] [,]](_icc.gif)    
                         ![[,] [,]](_icc.gif)    
         |
167 | | eleq1 2517 |
. . . . . . . . . . . . . . 15
   
     |
168 | | fveq2 5865 |
. . . . . . . . . . . . . . 15
               |
169 | 167, 168 | ifbieq1d 3904 |
. . . . . . . . . . . . . 14
   
            
            |
170 | 169 | cbvmptv 4495 |
. . . . . . . . . . . . 13
                               |
171 | 79, 137, 89, 138, 139, 50, 90, 91, 93, 145, 148, 154, 116, 166, 170 | fourierdlem97 38067 |
. . . . . . . . . . . 12
 
 ..^                                        |
172 | | cncff 21925 |
. . . . . . . . . . . 12
                                                                           |
173 | | fdm 5733 |
. . . . . . . . . . . 12
                                                                       |
174 | 171, 172,
173 | 3syl 18 |
. . . . . . . . . . 11
 
 ..^ 
                                  |
175 | | ssdmres 5126 |
. . . . . . . . . . 11
              
 
                                  |
176 | 174, 175 | sylibr 216 |
. . . . . . . . . 10
 
 ..^                
   |
177 | 136, 176 | fssresd 5750 |
. . . . . . . . 9
 
 ..^                                        |
178 | | ax-resscn 9596 |
. . . . . . . . . . 11
 |
179 | 178 | a1i 11 |
. . . . . . . . . 10
 
 ..^    |
180 | | cncffvrn 21930 |
. . . . . . . . . 10
 
                                    
                                                                            |
181 | 179, 171,
180 | syl2anc 667 |
. . . . . . . . 9
 
 ..^                                      
                                       |
182 | 177, 181 | mpbird 236 |
. . . . . . . 8
 
 ..^                                        |
183 | | fourierdlem112.fdvbd |
. . . . . . . . . . 11
                  |
184 | 183 | adantr 467 |
. . . . . . . . . 10
 
 ..^                   |
185 | | nfv 1761 |
. . . . . . . . . . . . . 14
    ..^   |
186 | | nfra1 2769 |
. . . . . . . . . . . . . 14
   
           
 |
187 | 185, 186 | nfan 2011 |
. . . . . . . . . . . . 13
   
 ..^                  |
188 | | fvres 5879 |
. . . . . . . . . . . . . . . . . 18
                                             |
189 | 188 | adantl 468 |
. . . . . . . . . . . . . . . . 17
    ..^                                               |
190 | 189 | fveq2d 5869 |
. . . . . . . . . . . . . . . 16
    ..^                                                       |
191 | 190 | adantlr 721 |
. . . . . . . . . . . . . . 15
   
 ..^                
                                                     |
192 | | simplr 762 |
. . . . . . . . . . . . . . . 16
   
 ..^                
               

           
  |
193 | 176 | sselda 3432 |
. . . . . . . . . . . . . . . . 17
    ..^                     |
194 | 193 | adantlr 721 |
. . . . . . . . . . . . . . . 16
   
 ..^                
                   |
195 | | rspa 2755 |
. . . . . . . . . . . . . . . 16
   
           
            
  |
196 | 192, 194,
195 | syl2anc 667 |
. . . . . . . . . . . . . . 15
   
 ..^                
                        
  |
197 | 191, 196 | eqbrtrd 4423 |
. . . . . . . . . . . . . 14
   
 ..^                
                                        
  |
198 | 197 | ex 436 |
. . . . . . . . . . . . 13
    ..^                
              
                             |
199 | 187, 198 | ralrimi 2788 |
. . . . . . . . . . . 12
    ..^                
                                         
  |
200 | 199 | ex 436 |
. . . . . . . . . . 11
 
 ..^                                                          
   |
201 | 200 | reximdv 2861 |
. . . . . . . . . 10
 
 ..^                                                                |
202 | 184, 201 | mpd 15 |
. . . . . . . . 9
 
 ..^                                               |
203 | | nfra1 2769 |
. . . . . . . . . . . 12
                                           
 |
204 | 188 | eqcomd 2457 |
. . . . . . . . . . . . . . . 16
                                             |
205 | 204 | fveq2d 5869 |
. . . . . . . . . . . . . . 15
                                                     |
206 | 205 | adantl 468 |
. . . . . . . . . . . . . 14
                                           
                                                     |
207 | | rspa 2755 |
. . . . . . . . . . . . . 14
                                           
                                        
  |
208 | 206, 207 | eqbrtrd 4423 |
. . . . . . . . . . . . 13
                                           
                        
  |
209 | 208 | ex 436 |
. . . . . . . . . . . 12
 
                                                                 
   |
210 | 203, 209 | ralrimi 2788 |
. . . . . . . . . . 11
 
                                                                  
  |
211 | 210 | a1i 11 |
. . . . . . . . . 10
 
 ..^                                            
                             |
212 | 211 | reximdv 2861 |
. . . . . . . . 9
 
 ..^                                             
 
                            |
213 | 202, 212 | mpd 15 |
. . . . . . . 8
 
 ..^                               |
214 | | nfv 1761 |
. . . . . . . . . . . 12
    ..^   |
215 | | nfcsb1v 3379 |
. . . . . . . . . . . . 13
  
 ![]_ ]_](_urbrack.gif)  |
216 | 215 | nfel1 2606 |
. . . . . . . . . . . 12
    ![]_ ]_](_urbrack.gif)
                 lim       |
217 | 214, 216 | nfim 2003 |
. . . . . . . . . . 11
   
 ..^  
 ![]_ ]_](_urbrack.gif)
                 lim        |
218 | | csbeq1a 3372 |
. . . . . . . . . . . . 13
   ![]_ ]_](_urbrack.gif)   |
219 | 99, 96 | oveq12d 6308 |
. . . . . . . . . . . . 13
                  lim                       lim        |
220 | 218, 219 | eleq12d 2523 |
. . . . . . . . . . . 12
 
                 lim        ![]_ ]_](_urbrack.gif)
                 lim         |
221 | 95, 220 | imbi12d 322 |
. . . . . . . . . . 11
   
 ..^ 
                 lim      
   ..^    ![]_ ]_](_urbrack.gif)
                 lim          |
222 | | fourierdlem112.c |
. . . . . . . . . . 11
 
 ..^                   lim        |
223 | 217, 221,
222 | chvar 2106 |
. . . . . . . . . 10
 
 ..^    ![]_ ]_](_urbrack.gif)
                 lim        |
224 | 223 | adantlr 721 |
. . . . . . . . 9
    ..^   ..^ 
  ![]_ ]_](_urbrack.gif)                  lim        |
225 | 79, 89, 50, 90, 91, 93, 105, 224, 106, 112, 116, 121 | fourierdlem96 38066 |
. . . . . . . 8
 
 ..^         ![(,] (,]](_ioc.gif)      
                                    ..^    
     ![(,] (,]](_ioc.gif)                                
             ..^   ![]_ ]_](_urbrack.gif)          ..^          ![(,] (,]](_ioc.gif)      
                                            ![(,] (,]](_ioc.gif)                                                     lim        |
226 | | nfcsb1v 3379 |
. . . . . . . . . . . . 13
  
 ![]_ ]_](_urbrack.gif)  |
227 | 226 | nfel1 2606 |
. . . . . . . . . . . 12
    ![]_ ]_](_urbrack.gif)
                 lim         |
228 | 214, 227 | nfim 2003 |
. . . . . . . . . . 11
   
 ..^  
 ![]_ ]_](_urbrack.gif)
                 lim          |
229 | | csbeq1a 3372 |
. . . . . . . . . . . . 13
   ![]_ ]_](_urbrack.gif)   |
230 | 99, 97 | oveq12d 6308 |
. . . . . . . . . . . . 13
                  lim                         lim          |
231 | 229, 230 | eleq12d 2523 |
. . . . . . . . . . . 12
 
                 lim          ![]_ ]_](_urbrack.gif)
                 lim           |
232 | 95, 231 | imbi12d 322 |
. . . . . . . . . . 11
   
 ..^ 
                 lim        
   ..^    ![]_ ]_](_urbrack.gif)
                 lim            |
233 | | fourierdlem112.u |
. . . . . . . . . . 11
 
 ..^                   lim          |
234 | 228, 232,
233 | chvar 2106 |
. . . . . . . . . 10
 
 ..^    ![]_ ]_](_urbrack.gif)
                 lim          |
235 | 234 | adantlr 721 |
. . . . . . . . 9
    ..^   ..^ 
  ![]_ ]_](_urbrack.gif)                  lim          |
236 | 79, 89, 50, 90, 91, 93, 105, 235, 148, 154, 116, 121 | fourierdlem99 38069 |
. . . . . . . 8
 
 ..^                                      ..^          ![(,] (,]](_ioc.gif)      
                                        ..^   ![]_ ]_](_urbrack.gif)          ..^          ![(,] (,]](_ioc.gif)      
                                                                                  lim          |
237 | | eqeq1 2455 |
. . . . . . . . . 10
     |
238 | | oveq2 6298 |
. . . . . . . . . . . . 13
 
     |
239 | 238 | fveq2d 5869 |
. . . . . . . . . . . 12
          
    |
240 | | breq2 4406 |
. . . . . . . . . . . . 13
 
   |
241 | 240 | ifbid 3903 |
. . . . . . . . . . . 12
             |
242 | 239, 241 | oveq12d 6308 |
. . . . . . . . . . 11
     
                       |
243 | | id 22 |
. . . . . . . . . . 11
   |
244 | 242, 243 | oveq12d 6308 |
. . . . . . . . . 10
      
                          |
245 | 237, 244 | ifbieq2d 3906 |
. . . . . . . . 9
          
                   
            |
246 | 245 | cbvmptv 4495 |
. . . . . . . 8
    ![[,] [,]](_icc.gif)           
               ![[,] [,]](_icc.gif)           
            |
247 | | eqeq1 2455 |
. . . . . . . . . 10
     |
248 | | id 22 |
. . . . . . . . . . 11
   |
249 | | oveq1 6297 |
. . . . . . . . . . . . 13
       |
250 | 249 | fveq2d 5869 |
. . . . . . . . . . . 12
               |
251 | 250 | oveq2d 6306 |
. . . . . . . . . . 11
                   |
252 | 248, 251 | oveq12d 6308 |
. . . . . . . . . 10
                       |
253 | 247, 252 | ifbieq2d 3906 |
. . . . . . . . 9
                                 |
254 | 253 | cbvmptv 4495 |
. . . . . . . 8
    ![[,] [,]](_icc.gif)                      ![[,] [,]](_icc.gif)                   |
255 | | fveq2 5865 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif)                               ![[,] [,]](_icc.gif) 
         
                |
256 | | fveq2 5865 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif)                          ![[,] [,]](_icc.gif)                       |
257 | 255, 256 | oveq12d 6308 |
. . . . . . . . 9
       ![[,] [,]](_icc.gif) 
         
                   ![[,] [,]](_icc.gif)                            ![[,] [,]](_icc.gif)                               ![[,] [,]](_icc.gif) 
                      |
258 | 257 | cbvmptv 4495 |
. . . . . . . 8
    ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)                               ![[,] [,]](_icc.gif) 
                         ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif) 
         
                   ![[,] [,]](_icc.gif)                        |
259 | | oveq2 6298 |
. . . . . . . . . 10
               |
260 | 259 | fveq2d 5869 |
. . . . . . . . 9
                       |
261 | 260 | cbvmptv 4495 |
. . . . . . . 8
    ![[,] [,]](_icc.gif)                 ![[,] [,]](_icc.gif)              |
262 | | fveq2 5865 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)           
                   ![[,] [,]](_icc.gif)                               ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif) 
         
                   ![[,] [,]](_icc.gif)                            |
263 | | fveq2 5865 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif)                     ![[,] [,]](_icc.gif)                  |
264 | 262, 263 | oveq12d 6308 |
. . . . . . . . 9
       ![[,] [,]](_icc.gif) 
      ![[,] [,]](_icc.gif)                               ![[,] [,]](_icc.gif) 
                             ![[,] [,]](_icc.gif)                       ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)           
                   ![[,] [,]](_icc.gif)                               ![[,] [,]](_icc.gif)                   |
265 | 264 | cbvmptv 4495 |
. . . . . . . 8
    ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)           
                   ![[,] [,]](_icc.gif)                               ![[,] [,]](_icc.gif)                      ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif) 
      ![[,] [,]](_icc.gif)                               ![[,] [,]](_icc.gif) 
                             ![[,] [,]](_icc.gif)                   |
266 | | fveq2 5865 |
. . . . . . . . . . . . 13
           |
267 | 266 | fveq1d 5867 |
. . . . . . . . . . . 12
                   |
268 | 267 | |