Step | Hyp | Ref
| Expression |
1 | | fourierdlem91.q |
. . . . . . . . . . . 12
       |
2 | | fourierdlem91.m |
. . . . . . . . . . . . 13
   |
3 | | fourierdlem91.p |
. . . . . . . . . . . . . 14
 
                 
 ..^                |
4 | 3 | fourierdlem2 38008 |
. . . . . . . . . . . . 13
 
   
                  
 ..^                 |
5 | 2, 4 | syl 17 |
. . . . . . . . . . . 12
                        
 ..^                 |
6 | 1, 5 | mpbid 215 |
. . . . . . . . . . 11
                   
 ..^                |
7 | 6 | simpld 465 |
. . . . . . . . . 10
         |
8 | | elmapi 7518 |
. . . . . . . . . 10
                 |
9 | 7, 8 | syl 17 |
. . . . . . . . 9
           |
10 | | fzossfz 11968 |
. . . . . . . . . 10
 ..^      |
11 | | fourierdlem91.t |
. . . . . . . . . . . . 13
   |
12 | | fourierdlem91.e |
. . . . . . . . . . . . 13
 
             |
13 | | fourierdlem91.J |
. . . . . . . . . . . . 13
   ![(,] (,]](_ioc.gif)         |
14 | | fourierdlem91.i |
. . . . . . . . . . . . 13
     ..^                  |
15 | 3, 2, 1, 11, 12, 13, 14 | fourierdlem37 38044 |
. . . . . . . . . . . 12
       ..^ 
    ..^                  ..^                  |
16 | 15 | simpld 465 |
. . . . . . . . . . 11
      ..^   |
17 | | fourierdlem91.c |
. . . . . . . . . . . . . . . . . 18
   |
18 | | fourierdlem91.d |
. . . . . . . . . . . . . . . . . . 19
      |
19 | | elioore 11694 |
. . . . . . . . . . . . . . . . . . 19
   
  |
20 | 18, 19 | syl 17 |
. . . . . . . . . . . . . . . . . 18
   |
21 | | elioo4g 11723 |
. . . . . . . . . . . . . . . . . . . . 21
     
 
    |
22 | 18, 21 | sylib 201 |
. . . . . . . . . . . . . . . . . . . 20
  
 
    |
23 | 22 | simprd 469 |
. . . . . . . . . . . . . . . . . . 19
 
   |
24 | 23 | simpld 465 |
. . . . . . . . . . . . . . . . . 18
   |
25 | | fourierdlem91.o |
. . . . . . . . . . . . . . . . . 18
 
                 
 ..^                |
26 | | oveq1 6321 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
27 | 26 | eleq1d 2523 |
. . . . . . . . . . . . . . . . . . . . 21
             |
28 | 27 | rexbidv 2912 |
. . . . . . . . . . . . . . . . . . . 20
  
            |
29 | 28 | cbvrabv 3055 |
. . . . . . . . . . . . . . . . . . 19
   ![[,] [,]](_icc.gif)  
        ![[,] [,]](_icc.gif)         |
30 | 29 | uneq2i 3596 |
. . . . . . . . . . . . . . . . . 18
       ![[,] [,]](_icc.gif)            
   ![[,] [,]](_icc.gif)          |
31 | | fourierdlem91.n |
. . . . . . . . . . . . . . . . . . 19
       |
32 | | fourierdlem91.h |
. . . . . . . . . . . . . . . . . . . . 21
   
   ![[,] [,]](_icc.gif)  
       |
33 | 32 | fveq2i 5890 |
. . . . . . . . . . . . . . . . . . . 20
         
    ![[,] [,]](_icc.gif)           |
34 | 33 | oveq1i 6324 |
. . . . . . . . . . . . . . . . . . 19
                 ![[,] [,]](_icc.gif)            |
35 | 31, 34 | eqtri 2483 |
. . . . . . . . . . . . . . . . . 18
           ![[,] [,]](_icc.gif)            |
36 | | fourierdlem91.s |
. . . . . . . . . . . . . . . . . . 19
            |
37 | | isoeq5 6238 |
. . . . . . . . . . . . . . . . . . . . 21
        ![[,] [,]](_icc.gif)         
      
             ![[,] [,]](_icc.gif)             |
38 | 32, 37 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
       
             ![[,] [,]](_icc.gif)            |
39 | 38 | iotabii 5586 |
. . . . . . . . . . . . . . . . . . 19
                           ![[,] [,]](_icc.gif)            |
40 | 36, 39 | eqtri 2483 |
. . . . . . . . . . . . . . . . . 18
                ![[,] [,]](_icc.gif)            |
41 | 11, 3, 2, 1, 17, 20, 24, 25, 30, 35, 40 | fourierdlem54 38061 |
. . . . . . . . . . . . . . . . 17
                     ![[,] [,]](_icc.gif)             |
42 | 41 | simpld 465 |
. . . . . . . . . . . . . . . 16
         |
43 | 42 | simprd 469 |
. . . . . . . . . . . . . . 15
       |
44 | 42 | simpld 465 |
. . . . . . . . . . . . . . . 16
   |
45 | 25 | fourierdlem2 38008 |
. . . . . . . . . . . . . . . 16
 
   
                  
 ..^                 |
46 | 44, 45 | syl 17 |
. . . . . . . . . . . . . . 15
                        
 ..^                 |
47 | 43, 46 | mpbid 215 |
. . . . . . . . . . . . . 14
                   
 ..^                |
48 | 47 | simpld 465 |
. . . . . . . . . . . . 13
         |
49 | | elmapi 7518 |
. . . . . . . . . . . . 13
                 |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . 12
           |
51 | | fourierdlem91.17 |
. . . . . . . . . . . . 13
  ..^   |
52 | | elfzofz 11965 |
. . . . . . . . . . . . 13
  ..^
      |
53 | 51, 52 | syl 17 |
. . . . . . . . . . . 12
       |
54 | 50, 53 | ffvelrnd 6045 |
. . . . . . . . . . 11
       |
55 | 16, 54 | ffvelrnd 6045 |
. . . . . . . . . 10
          ..^   |
56 | 10, 55 | sseldi 3441 |
. . . . . . . . 9
               |
57 | 9, 56 | ffvelrnd 6045 |
. . . . . . . 8
               |
58 | 57 | rexrd 9715 |
. . . . . . 7
               |
59 | 58 | adantr 471 |
. . . . . 6
 
                                       |
60 | | fzofzp1 12038 |
. . . . . . . . . 10
          ..^
                |
61 | 55, 60 | syl 17 |
. . . . . . . . 9
                 |
62 | 9, 61 | ffvelrnd 6045 |
. . . . . . . 8
                 |
63 | 62 | rexrd 9715 |
. . . . . . 7
                 |
64 | 63 | adantr 471 |
. . . . . 6
 
                                         |
65 | 3, 2, 1 | fourierdlem11 38017 |
. . . . . . . . . . 11
     |
66 | 65 | simp1d 1026 |
. . . . . . . . . 10
   |
67 | 66 | rexrd 9715 |
. . . . . . . . 9
   |
68 | 65 | simp2d 1027 |
. . . . . . . . 9
   |
69 | | iocssre 11742 |
. . . . . . . . 9
     ![(,] (,]](_ioc.gif)    |
70 | 67, 68, 69 | syl2anc 671 |
. . . . . . . 8
   ![(,] (,]](_ioc.gif) 
  |
71 | 65 | simp3d 1028 |
. . . . . . . . . 10
   |
72 | 66, 68, 71, 11, 12 | fourierdlem4 38010 |
. . . . . . . . 9
       ![(,] (,]](_ioc.gif)    |
73 | | fzofzp1 12038 |
. . . . . . . . . . 11
  ..^
        |
74 | 51, 73 | syl 17 |
. . . . . . . . . 10
         |
75 | 50, 74 | ffvelrnd 6045 |
. . . . . . . . 9
    
    |
76 | 72, 75 | ffvelrnd 6045 |
. . . . . . . 8
             ![(,] (,]](_ioc.gif)    |
77 | 70, 76 | sseldd 3444 |
. . . . . . 7
             |
78 | 77 | adantr 471 |
. . . . . 6
 
                                     |
79 | 66, 68 | iccssred 37639 |
. . . . . . . . 9
   ![[,] [,]](_icc.gif) 
  |
80 | 66, 68, 71, 13 | fourierdlem17 38023 |
. . . . . . . . . 10
     ![(,] (,]](_ioc.gif)      ![[,] [,]](_icc.gif)    |
81 | 72, 54 | ffvelrnd 6045 |
. . . . . . . . . 10
           ![(,] (,]](_ioc.gif)    |
82 | 80, 81 | ffvelrnd 6045 |
. . . . . . . . 9
               ![[,] [,]](_icc.gif)    |
83 | 79, 82 | sseldd 3444 |
. . . . . . . 8
               |
84 | 47 | simprrd 772 |
. . . . . . . . . . . . . 14
   ..^              |
85 | | fveq2 5887 |
. . . . . . . . . . . . . . . 16
           |
86 | | oveq1 6321 |
. . . . . . . . . . . . . . . . 17
       |
87 | 86 | fveq2d 5891 |
. . . . . . . . . . . . . . . 16
          
    |
88 | 85, 87 | breq12d 4428 |
. . . . . . . . . . . . . . 15
     
     
             |
89 | 88 | rspccva 3160 |
. . . . . . . . . . . . . 14
    ..^             ..^ 
            |
90 | 84, 51, 89 | syl2anc 671 |
. . . . . . . . . . . . 13
    
        |
91 | 54, 75 | posdifd 10227 |
. . . . . . . . . . . . 13
                           |
92 | 90, 91 | mpbid 215 |
. . . . . . . . . . . 12
               |
93 | | eleq1 2527 |
. . . . . . . . . . . . . . . . 17
   ..^
 ..^    |
94 | 93 | anbi2d 715 |
. . . . . . . . . . . . . . . 16
  
 ..^  
 ..^     |
95 | | oveq1 6321 |
. . . . . . . . . . . . . . . . . . . 20
       |
96 | 95 | fveq2d 5891 |
. . . . . . . . . . . . . . . . . . 19
          
    |
97 | 96 | fveq2d 5891 |
. . . . . . . . . . . . . . . . . 18
                       |
98 | | fveq2 5887 |
. . . . . . . . . . . . . . . . . . . 20
           |
99 | 98 | fveq2d 5891 |
. . . . . . . . . . . . . . . . . . 19
                   |
100 | 99 | fveq2d 5891 |
. . . . . . . . . . . . . . . . . 18
                           |
101 | 97, 100 | oveq12d 6332 |
. . . . . . . . . . . . . . . . 17
                                                   |
102 | 96, 98 | oveq12d 6332 |
. . . . . . . . . . . . . . . . 17
                           |
103 | 101, 102 | eqeq12d 2476 |
. . . . . . . . . . . . . . . 16
                                             
                               |
104 | 94, 103 | imbi12d 326 |
. . . . . . . . . . . . . . 15
   
 ..^                                      
   ..^         
                                |
105 | 11 | oveq2i 6325 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
   |
106 | 105 | oveq2i 6325 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           |
107 | 106 | eleq1i 2530 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
        |
108 | 107 | rexbii 2900 |
. . . . . . . . . . . . . . . . . . . . . 22
     
   
     |
109 | 108 | rgenw 2760 |
. . . . . . . . . . . . . . . . . . . . 21
   ![[,] [,]](_icc.gif)         
        |
110 | | rabbi 2980 |
. . . . . . . . . . . . . . . . . . . . 21
 
  ![[,] [,]](_icc.gif)        
   
       ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)  
         |
111 | 109, 110 | mpbi 213 |
. . . . . . . . . . . . . . . . . . . 20
   ![[,] [,]](_icc.gif)  
        ![[,] [,]](_icc.gif)     
     |
112 | 111 | uneq2i 3596 |
. . . . . . . . . . . . . . . . . . 19
       ![[,] [,]](_icc.gif)            
   ![[,] [,]](_icc.gif)     
      |
113 | 112 | fveq2i 5890 |
. . . . . . . . . . . . . . . . . 18
      
   ![[,] [,]](_icc.gif)  
            
    ![[,] [,]](_icc.gif)     
       |
114 | 113 | oveq1i 6324 |
. . . . . . . . . . . . . . . . 17
      
    ![[,] [,]](_icc.gif)                      ![[,] [,]](_icc.gif)     
        |
115 | 35, 114 | eqtri 2483 |
. . . . . . . . . . . . . . . 16
           ![[,] [,]](_icc.gif)     
        |
116 | | isoeq5 6238 |
. . . . . . . . . . . . . . . . . . 19
    
   ![[,] [,]](_icc.gif)            
   ![[,] [,]](_icc.gif)     
     
             ![[,] [,]](_icc.gif)         
         
   ![[,] [,]](_icc.gif)  
            |
117 | 112, 116 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
              ![[,] [,]](_icc.gif)         
         
   ![[,] [,]](_icc.gif)  
           |
118 | 117 | iotabii 5586 |
. . . . . . . . . . . . . . . . 17
            
   ![[,] [,]](_icc.gif)  
                        ![[,] [,]](_icc.gif)     
        |
119 | 40, 118 | eqtri 2483 |
. . . . . . . . . . . . . . . 16
                ![[,] [,]](_icc.gif)     
        |
120 | | eqid 2461 |
. . . . . . . . . . . . . . . 16
                                 |
121 | 3, 11, 2, 1, 17, 18, 25, 115, 119, 12, 13, 120 | fourierdlem65 38072 |
. . . . . . . . . . . . . . 15
 
 ..^                                        |
122 | 104, 121 | vtoclg 3118 |
. . . . . . . . . . . . . 14
  ..^
   ..^         
                               |
123 | 122 | anabsi7 833 |
. . . . . . . . . . . . 13
 
 ..^         
                              |
124 | 51, 123 | mpdan 679 |
. . . . . . . . . . . 12
                             
         |
125 | 92, 124 | breqtrrd 4442 |
. . . . . . . . . . 11
                           |
126 | 83, 77 | posdifd 10227 |
. . . . . . . . . . 11
                    
  
                           |
127 | 125, 126 | mpbird 240 |
. . . . . . . . . 10
                         |
128 | 100, 97 | oveq12d 6332 |
. . . . . . . . . . . . . . 15
                                                       |
129 | 98 | fveq2d 5891 |
. . . . . . . . . . . . . . . . 17
                   |
130 | 129 | fveq2d 5891 |
. . . . . . . . . . . . . . . 16
                           |
131 | 129 | oveq1d 6329 |
. . . . . . . . . . . . . . . . 17
                       |
132 | 131 | fveq2d 5891 |
. . . . . . . . . . . . . . . 16
                               |
133 | 130, 132 | oveq12d 6332 |
. . . . . . . . . . . . . . 15
                                                               |
134 | 128, 133 | sseq12d 3472 |
. . . . . . . . . . . . . 14
                                                                               
                                     |
135 | 94, 134 | imbi12d 326 |
. . . . . . . . . . . . 13
   
 ..^                                                              ..^                       
                                      |
136 | 32, 30 | eqtri 2483 |
. . . . . . . . . . . . . 14
   
   ![[,] [,]](_icc.gif)          |
137 | | eqid 2461 |
. . . . . . . . . . . . . 14
                                                                                                       |
138 | 11, 3, 2, 1, 17, 20, 24, 25, 136, 31, 36, 12, 13, 137, 14 | fourierdlem79 38086 |
. . . . . . . . . . . . 13
 
 ..^                                                            |
139 | 135, 138 | vtoclg 3118 |
. . . . . . . . . . . 12
  ..^
   ..^                                                             |
140 | 139 | anabsi7 833 |
. . . . . . . . . . 11
 
 ..^                                                            |
141 | 51, 140 | mpdan 679 |
. . . . . . . . . 10
                      
                                    |
142 | 57, 62, 83, 77, 127, 141 | fourierdlem10 38016 |
. . . . . . . . 9
                                                     |
143 | 142 | simpld 465 |
. . . . . . . 8
                           |
144 | 57, 83, 77, 143, 127 | lelttrd 9818 |
. . . . . . 7
                         |
145 | 144 | adantr 471 |
. . . . . 6
 
                                                 |
146 | 62 | adantr 471 |
. . . . . . 7
 
                                         |
147 | 142 | simprd 469 |
. . . . . . . 8
          
                |
148 | 147 | adantr 471 |
. . . . . . 7
 
                                                   |
149 | | neqne 2642 |
. . . . . . . . 9
                                                   |
150 | 149 | necomd 2690 |
. . . . . . . 8
                                             
     |
151 | 150 | adantl 472 |
. . . . . . 7
 
                                                   |
152 | 78, 146, 148, 151 | leneltd 9814 |
. . . . . 6
 
                                                   |
153 | 59, 64, 78, 145, 152 | eliood 37632 |
. . . . 5
 
                                                                   |
154 | | fvres 5901 |
. . . . 5
                                                                                  
                    |
155 | 153, 154 | syl 17 |
. . . 4
 
                                                                                       |
156 | 155 | eqcomd 2467 |
. . 3
 
                                  
                                             
      |
157 | 156 | ifeq2da 3923 |
. 2
         
                                        
                                                                                      
       |
158 | | fourierdlem91.f |
. . . . . 6
       |
159 | | fdm 5755 |
. . . . . . . 8
       |
160 | 158, 159 | syl 17 |
. . . . . . 7
   |
161 | 160 | feq2d 5736 |
. . . . . 6
             |
162 | 158, 161 | mpbird 240 |
. . . . 5
       |
163 | | ioosscn 37628 |
. . . . . 6
                           |
164 | 163 | a1i 11 |
. . . . 5
                      
      |
165 | | ioossre 11724 |
. . . . . 6
                           |
166 | 165, 160 | syl5sseqr 3492 |
. . . . 5
                      
   
  |
167 | | fourierdlem91.u |
. . . . . . 7
    
              |
168 | 75, 77 | resubcld 10074 |
. . . . . . 7
     
               |
169 | 167, 168 | syl5eqel 2543 |
. . . . . 6
   |
170 | 169 | recnd 9694 |
. . . . 5
   |
171 | | eqid 2461 |
. . . . 5
                       
                               
         |
172 | 83, 77, 169 | iooshift 37660 |
. . . . . 6
                                                      
          |
173 | | ioossre 11724 |
. . . . . . 7
                             
 |
174 | 173, 160 | syl5sseqr 3492 |
. . . . . 6
                              
  |
175 | 172, 174 | eqsstr3d 3478 |
. . . . 5
                                   |
176 | | elioore 11694 |
. . . . . 6
                             |
177 | 68, 66 | resubcld 10074 |
. . . . . . . . . . . . . 14
     |
178 | 11, 177 | syl5eqel 2543 |
. . . . . . . . . . . . 13
   |
179 | 178 | recnd 9694 |
. . . . . . . . . . . 12
   |
180 | 66, 68 | posdifd 10227 |
. . . . . . . . . . . . . . 15
       |
181 | 71, 180 | mpbid 215 |
. . . . . . . . . . . . . 14
     |
182 | 181, 11 | syl6breqr 4456 |
. . . . . . . . . . . . 13
   |
183 | 182 | gt0ne0d 10205 |
. . . . . . . . . . . 12
   |
184 | 170, 179,
183 | divcan1d 10411 |
. . . . . . . . . . 11
       |
185 | 184 | eqcomd 2467 |
. . . . . . . . . 10
       |
186 | 185 | oveq2d 6330 |
. . . . . . . . 9
           |
187 | 186 | adantr 471 |
. . . . . . . 8
 

          |
188 | 187 | fveq2d 5891 |
. . . . . . 7
 

                  |
189 | 158 | adantr 471 |
. . . . . . . 8
 

      |
190 | 178 | adantr 471 |
. . . . . . . 8
 

  |
191 | 77 | recnd 9694 |
. . . . . . . . . . . . . 14
             |
192 | 75 | recnd 9694 |
. . . . . . . . . . . . . 14
    
    |
193 | 191, 192 | negsubdi2d 10027 |
. . . . . . . . . . . . 13
         
                              |
194 | 193 | eqcomd 2467 |
. . . . . . . . . . . 12
     
                     
            |
195 | 194 | oveq1d 6329 |
. . . . . . . . . . 11
                                            |
196 | 167 | oveq1i 6324 |
. . . . . . . . . . . 12
                       |
197 | 196 | a1i 11 |
. . . . . . . . . . 11
        
        
       |
198 | 12 | a1i 11 |
. . . . . . . . . . . . . . . 16
                 |
199 | | id 22 |
. . . . . . . . . . . . . . . . . 18
    
     
    |
200 | | oveq2 6322 |
. . . . . . . . . . . . . . . . . . . . 21
    
  
           |
201 | 200 | oveq1d 6329 |
. . . . . . . . . . . . . . . . . . . 20
    
           
      |
202 | 201 | fveq2d 5891 |
. . . . . . . . . . . . . . . . . . 19
    
                          |
203 | 202 | oveq1d 6329 |
. . . . . . . . . . . . . . . . . 18
    
                     
        |
204 | 199, 203 | oveq12d 6332 |
. . . . . . . . . . . . . . . . 17
    
                                        |
205 | 204 | adantl 472 |
. . . . . . . . . . . . . . . 16
 
      
                
                     |
206 | 68, 75 | resubcld 10074 |
. . . . . . . . . . . . . . . . . . . . 21
           |
207 | 206, 178,
183 | redivcld 10462 |
. . . . . . . . . . . . . . . . . . . 20
             |
208 | 207 | flcld 12065 |
. . . . . . . . . . . . . . . . . . 19
                 |
209 | 208 | zred 11068 |
. . . . . . . . . . . . . . . . . 18
                 |
210 | 209, 178 | remulcld 9696 |
. . . . . . . . . . . . . . . . 17
                   |
211 | 75, 210 | readdcld 9695 |
. . . . . . . . . . . . . . . 16
     
                     |
212 | 198, 205,
75, 211 | fvmptd 5976 |
. . . . . . . . . . . . . . 15
                           
         |
213 | 212 | oveq1d 6329 |
. . . . . . . . . . . . . 14
                                    
                |
214 | 208 | zcnd 11069 |
. . . . . . . . . . . . . . . 16
                 |
215 | 214, 179 | mulcld 9688 |
. . . . . . . . . . . . . . 15
                   |
216 | 192, 215 | pncan2d 10013 |
. . . . . . . . . . . . . 14
                                          
        |
217 | 213, 216 | eqtrd 2495 |
. . . . . . . . . . . . 13
                            
        |
218 | 217, 215 | eqeltrd 2539 |
. . . . . . . . . . . 12
                     |
219 | 218, 179,
183 | divnegd 10423 |
. . . . . . . . . . 11
                 
             
             |
220 | 195, 197,
219 | 3eqtr4d 2505 |
. . . . . . . . . 10
                          |
221 | 217 | oveq1d 6329 |
. . . . . . . . . . . . 13
         
                               |
222 | 214, 179,
183 | divcan4d 10416 |
. . . . . . . . . . . . 13
           
               
       |
223 | 221, 222 | eqtrd 2495 |
. . . . . . . . . . . 12
         
                           |
224 | 223, 208 | eqeltrd 2539 |
. . . . . . . . . . 11
         
             |
225 | 224 | znegcld 11070 |
. . . . . . . . . 10
                 
      |
226 | 220, 225 | eqeltrd 2539 |
. . . . . . . . 9
     |
227 | 226 | adantr 471 |
. . . . . . . 8
 

    |
228 | | simpr 467 |
. . . . . . . 8
 

  |
229 | | fourierdlem91.6 |
. . . . . . . . 9
 

            |
230 | 229 | adantlr 726 |
. . . . . . . 8
                 |
231 | 189, 190,
227, 228, 230 | fperiodmul 37559 |
. . . . . . 7
 

                |
232 | 188, 231 | eqtrd 2495 |
. . . . . 6
 

            |
233 | 176, 232 | sylan2 481 |
. . . . 5
 
                     
    
            |
234 | 6 | simprrd 772 |
. . . . . . . 8
   ..^              |
235 | | fveq2 5887 |
. . . . . . . . . 10
        
                  |
236 | | oveq1 6321 |
. . . . . . . . . . 11
        
              |
237 | 236 | fveq2d 5891 |
. . . . . . . . . 10
        
                      |
238 | 235, 237 | breq12d 4428 |
. . . . . . . . 9
        
                                        |
239 | 238 | rspccva 3160 |
. . . . . . . 8
    ..^                     ..^ 
                            |
240 | 234, 55, 239 | syl2anc 671 |
. . . . . . 7
                             |
241 | 55 | ancli 558 |
. . . . . . . 8
           ..^    |
242 | | eleq1 2527 |
. . . . . . . . . . 11
        
  ..^          ..^    |
243 | 242 | anbi2d 715 |
. . . . . . . . . 10
        
   ..^  
         ..^     |
244 | 235, 237 | oveq12d 6332 |
. . . . . . . . . . . 12
        
                                              |
245 | 244 | reseq2d 5123 |
. . . . . . . . . . 11
        
                
                                 |
246 | 244 | oveq1d 6329 |
. . . . . . . . . . 11
        
                                                      |
247 | 245, 246 | eleq12d 2533 |
. . . . . . . . . 10
        
                                                                                                        |
248 | 243, 247 | imbi12d 326 |
. . . . . . . . 9
        
  
 ..^ 
                                  
           ..^                                                                        |
249 | | fourierdlem91.fcn |
. . . . . . . . 9
 
 ..^                                      |
250 | 248, 249 | vtoclg 3118 |
. . . . . . . 8
          ..^
           ..^                                                                       |
251 | 55, 241, 250 | sylc 62 |
. . . . . . 7
                                                                     |
252 | | nfv 1771 |
. . . . . . . . . 10
            ..^   |
253 | | fourierdlem91.w |
. . . . . . . . . . . . 13
  ..^   |
254 | | nfmpt1 4505 |
. . . . . . . . . . . . 13
    ..^   |
255 | 253, 254 | nfcxfr 2600 |
. . . . . . . . . . . 12
   |
256 | | nfcv 2602 |
. . . . . . . . . . . 12
           |
257 | 255, 256 | nffv 5894 |
. . . . . . . . . . 11
               |
258 | 257 | nfel1 2616 |
. . . . . . . . . 10
                                               lim                 |
259 | 252, 258 | nfim 2013 |
. . . . . . . . 9
             ..^                                               lim                  |
260 | 243 | biimpar 492 |
. . . . . . . . . . . . . 14
                    ..^     ..^    |
261 | 260 | 3adant2 1033 |
. . . . . . . . . . . . 13
           
 ..^ 
                 lim                   ..^   
 ..^    |
262 | | fourierdlem91.l |
. . . . . . . . . . . . 13
 
 ..^                   lim          |
263 | 261, 262 | syl 17 |
. . . . . . . . . . . 12
           
 ..^ 
                 lim                   ..^                    lim          |
264 | | fveq2 5887 |
. . . . . . . . . . . . . . . 16
        
                  |
265 | 264 | eqcomd 2467 |
. . . . . . . . . . . . . . 15
        
                  |
266 | 265 | adantr 471 |
. . . . . . . . . . . . . 14
                    ..^                     |
267 | 260 | simprd 469 |
. . . . . . . . . . . . . . 15
                    ..^    ..^   |
268 | | elex 3065 |
. . . . . . . . . . . . . . . 16
                  lim       
  |
269 | 260, 262,
268 | 3syl 18 |
. . . . . . . . . . . . . . 15
                    ..^     |
270 | 253 | fvmpt2 5979 |
. . . . . . . . . . . . . . 15
   ..^        |
271 | 267, 269,
270 | syl2anc 671 |
. . . . . . . . . . . . . 14
                    ..^         |
272 | 266, 271 | eqtrd 2495 |
. . . . . . . . . . . . 13
                    ..^                 |
273 | 272 | 3adant2 1033 |
. . . . . . . . . . . 12
           
 ..^ 
                 lim                   ..^                 |
274 | 245, 237 | oveq12d 6332 |
. . . . . . . . . . . . . 14
        
                 lim         
                               lim                  |
275 | 274 | eqcomd 2467 |
. . . . . . . . . . . . 13
        
                                 lim                                 lim          |
276 | 275 | 3ad2ant1 1035 |
. . . . . . . . . . . 12
           
 ..^ 
                 lim                   ..^                                    lim                                 lim          |
277 | 263, 273,
276 | 3eltr4d 2554 |
. . . . . . . . . . 11
           
 ..^ 
                 lim                   ..^                                                lim                  |
278 | 277 | 3exp 1214 |
. . . . . . . . . 10
        
  
 ..^ 
                 lim          
         ..^ 
                                             lim                    |
279 | 262 | 2a1i 12 |
. . . . . . . . . 10
        
  
         ..^ 
                                             lim                  
 ..^ 
                 lim            |
280 | 278, 279 | impbid 195 |
. . . . . . . . 9
        
  
 ..^ 
                 lim        
           ..^                                               lim                    |
281 | 259, 280,
262 | vtoclg1f 3117 |
. . . . . . . 8
          ..^
           ..^                                               lim                   |
282 | 55, 241, 281 | sylc 62 |
. . . . . . 7
                                              lim                  |
283 | | eqid 2461 |
. . . . . . 7
                                                                                 
                                                                                      
      |
284 | | eqid 2461 |
. . . . . . 7
   ℂfld ↾t                                                     ℂfld
↾t                                                   |
285 | 57, 62, 240, 251, 282, 83, 77, 127, 141, 283, 284 | fourierdlem33 38040 |
. . . . . 6
         
                                                                                                               
                           lim              |
286 | 141 | resabs1d 5152 |
. . . . . . 7
                                 
                                                         |
287 | 286 | oveq1d 6329 |
. . . . . 6
                                  
                           lim             
                           lim              |
288 | 285, 287 | eleqtrd 2541 |
. . . . 5
         
                                                                                                           lim              |
289 | 162, 164,
166, 170, 171, 175, 233, 288 | limcperiod 37745 |
. . . 4
         
                                                                                                       
         lim                |
290 | 167 | oveq2i 6325 |
. . . . . 6
                                           |
291 | 191, 192 | pncan3d 10014 |
. . . . . 6
                                  
    |
292 | 290, 291 | syl5eq 2507 |
. . . . 5
                
    |
293 | 292 | oveq2d 6330 |
. . . 4
   
                                lim               
                       
         lim          |
294 | 289, 293 | eleqtrd 2541 |
. . 3
         
                                                                                                       
         lim          |
295 | 167 | oveq2i 6325 |
. . . . . . . . 9
                                               |
296 | 295 | a1i 11 |
. . . . . . . 8
                                
        
       |
297 | 17, 20 | iccssred 37639 |
. . . . . . . . . . . . . . 15
   ![[,] [,]](_icc.gif) 
  |
298 | | ax-resscn 9621 |
. . . . . . . . . . . . . . 15
 |
299 | 297, 298 | syl6ss 3455 |
. . . . . . . . . . . . . 14
   ![[,] [,]](_icc.gif) 
  |
300 | 25, 44, 43 | fourierdlem15 38021 |
. . . . . . . . . . . . . . 15
           ![[,] [,]](_icc.gif)    |
301 | 300, 53 | ffvelrnd 6045 |
. . . . . . . . . . . . . 14
       ![[,] [,]](_icc.gif)    |
302 | 299, 301 | sseldd 3444 |
. . . . . . . . . . . . 13
       |
303 | 192, 302 | subcld 10011 |
. . . . . . . . . . . 12
     
         |
304 | 83 | recnd 9694 |
. . . . . . . . . . . 12
               |
305 | 191, 303,
304 | subsub23d 37537 |
. . . . . . . . . . 11
         
       
                                                
          |
306 | 124, 305 | mpbird 240 |
. . . . . . . . . 10
                                       |
307 | 306 | eqcomd 2467 |
. . . . . . . . 9
                    
       
          |
308 | 307 | oveq1d 6329 |
. . . . . . . 8
                                         
       
            
        
       |
309 | 191, 303 | subcld 10011 |
. . . . . . . . . 10
                           |
310 | 309, 192,
191 | addsub12d 10034 |
. . . . . . . . 9
         
       
            
        
                                      |