Step | Hyp | Ref
| Expression |
1 | | fourierdlem81.q |
. . . . . . . . 9
       |
2 | | fourierdlem81.m |
. . . . . . . . . 10
   |
3 | | fourierdlem81.p |
. . . . . . . . . . 11
 
                 
 ..^                |
4 | 3 | fourierdlem2 38072 |
. . . . . . . . . 10
 
   
                  
 ..^                 |
5 | 2, 4 | syl 17 |
. . . . . . . . 9
                        
 ..^                 |
6 | 1, 5 | mpbid 215 |
. . . . . . . 8
                   
 ..^                |
7 | 6 | simprd 469 |
. . . . . . 7
            
 ..^               |
8 | 7 | simpld 465 |
. . . . . 6
             |
9 | 8 | simpld 465 |
. . . . 5
       |
10 | 9 | eqcomd 2468 |
. . . 4
       |
11 | 8 | simprd 469 |
. . . . 5
       |
12 | 11 | eqcomd 2468 |
. . . 4
       |
13 | 10, 12 | oveq12d 6338 |
. . 3
   ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)        |
14 | 13 | itgeq1d 37919 |
. 2
    ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)              |
15 | | 0zd 10983 |
. . 3
   |
16 | | nnuz 11228 |
. . . . 5
     |
17 | | 0p1e1 10754 |
. . . . . 6
   |
18 | 17 | fveq2i 5895 |
. . . . 5
           |
19 | 16, 18 | eqtr4i 2487 |
. . . 4
       |
20 | 2, 19 | syl6eleq 2550 |
. . 3
         |
21 | 6 | simpld 465 |
. . . 4
         |
22 | | reex 9661 |
. . . . . 6
 |
23 | 22 | a1i 11 |
. . . . 5
   |
24 | | ovex 6348 |
. . . . . 6
     |
25 | 24 | a1i 11 |
. . . . 5
       |
26 | 23, 25 | elmapd 7517 |
. . . 4
                   |
27 | 21, 26 | mpbid 215 |
. . 3
           |
28 | 7 | simprd 469 |
. . . 4
   ..^              |
29 | 28 | r19.21bi 2769 |
. . 3
 
 ..^              |
30 | | fourierdlem81.f |
. . . . 5
       |
31 | 30 | adantr 471 |
. . . 4
 
      ![[,] [,]](_icc.gif)             |
32 | | fourierdlem81.a |
. . . . . . 7
   |
33 | 9, 32 | eqeltrd 2540 |
. . . . . 6
       |
34 | | fourierdlem81.b |
. . . . . . 7
   |
35 | 11, 34 | eqeltrd 2540 |
. . . . . 6
       |
36 | 33, 35 | iccssred 37687 |
. . . . 5
       ![[,] [,]](_icc.gif)     
  |
37 | 36 | sselda 3444 |
. . . 4
 
      ![[,] [,]](_icc.gif)         |
38 | 31, 37 | ffvelrnd 6051 |
. . 3
 
      ![[,] [,]](_icc.gif)             |
39 | 27 | adantr 471 |
. . . . 5
 
 ..^            |
40 | | elfzofz 11972 |
. . . . . 6
  ..^
      |
41 | 40 | adantl 472 |
. . . . 5
 
 ..^        |
42 | 39, 41 | ffvelrnd 6051 |
. . . 4
 
 ..^        |
43 | | fzofzp1 12045 |
. . . . . 6
  ..^
        |
44 | 43 | adantl 472 |
. . . . 5
 
 ..^          |
45 | 39, 44 | ffvelrnd 6051 |
. . . 4
 
 ..^          |
46 | 30 | feqmptd 5945 |
. . . . . . . 8
         |
47 | 46 | reseq1d 5126 |
. . . . . . 7
                       
                 |
48 | 47 | adantr 471 |
. . . . . 6
 
 ..^                        
                 |
49 | | ioossre 11730 |
. . . . . . . 8
               |
50 | 49 | a1i 11 |
. . . . . . 7
 
 ..^                  |
51 | 50 | resmptd 5178 |
. . . . . 6
 
 ..^                                              |
52 | 48, 51 | eqtr2d 2497 |
. . . . 5
 
 ..^                                        |
53 | | fourierdlem81.cncf |
. . . . . 6
 
 ..^                                      |
54 | | fourierdlem81.l |
. . . . . 6
 
 ..^                   lim          |
55 | | fourierdlem81.r |
. . . . . 6
 
 ..^                   lim        |
56 | 42, 45, 53, 54, 55 | iblcncfioo 37941 |
. . . . 5
 
 ..^                     |
57 | 52, 56 | eqeltrd 2540 |
. . . 4
 
 ..^                         |
58 | 30 | ad2antrr 737 |
. . . . 5
    ..^        ![[,] [,]](_icc.gif)               |
59 | 42, 45 | iccssred 37687 |
. . . . . 6
 
 ..^        ![[,] [,]](_icc.gif)          |
60 | 59 | sselda 3444 |
. . . . 5
    ..^        ![[,] [,]](_icc.gif)           |
61 | 58, 60 | ffvelrnd 6051 |
. . . 4
    ..^        ![[,] [,]](_icc.gif)               |
62 | 42, 45, 57, 61 | ibliooicc 37934 |
. . 3
 
 ..^         ![[,] [,]](_icc.gif)                |
63 | 15, 20, 27, 29, 38, 62 | itgspltprt 37942 |
. 2
        ![[,] [,]](_icc.gif)              ..^         ![[,] [,]](_icc.gif)                |
64 | | fourierdlem81.s |
. . . . . . . 8
             |
65 | 64 | a1i 11 |
. . . . . . 7
               |
66 | | fveq2 5892 |
. . . . . . . . 9
           |
67 | 66 | oveq1d 6335 |
. . . . . . . 8
               |
68 | 67 | adantl 472 |
. . . . . . 7
 
               |
69 | 2 | nnnn0d 10959 |
. . . . . . . . 9
   |
70 | | nn0uz 11227 |
. . . . . . . . 9
     |
71 | 69, 70 | syl6eleq 2550 |
. . . . . . . 8
       |
72 | | eluzfz1 11841 |
. . . . . . . 8
    
      |
73 | 71, 72 | syl 17 |
. . . . . . 7
       |
74 | | fourierdlem81.t |
. . . . . . . . 9
   |
75 | 74 | rpred 11375 |
. . . . . . . 8
   |
76 | 33, 75 | readdcld 9701 |
. . . . . . 7
         |
77 | 65, 68, 73, 76 | fvmptd 5982 |
. . . . . 6
             |
78 | 9 | oveq1d 6335 |
. . . . . 6
           |
79 | 77, 78 | eqtr2d 2497 |
. . . . 5
         |
80 | | fveq2 5892 |
. . . . . . . . 9
           |
81 | 80 | oveq1d 6335 |
. . . . . . . 8
               |
82 | 81 | adantl 472 |
. . . . . . 7
 
               |
83 | | eluzfz2 11842 |
. . . . . . . 8
    
      |
84 | 71, 83 | syl 17 |
. . . . . . 7
       |
85 | 35, 75 | readdcld 9701 |
. . . . . . 7
         |
86 | 65, 82, 84, 85 | fvmptd 5982 |
. . . . . 6
             |
87 | 11 | oveq1d 6335 |
. . . . . 6
           |
88 | 86, 87 | eqtr2d 2497 |
. . . . 5
         |
89 | 79, 88 | oveq12d 6338 |
. . . 4
     ![[,] [,]](_icc.gif) 
        ![[,] [,]](_icc.gif)        |
90 | 89 | itgeq1d 37919 |
. . 3
      ![[,] [,]](_icc.gif)                 ![[,] [,]](_icc.gif)              |
91 | 27 | ffvelrnda 6050 |
. . . . . 6
 
           |
92 | 75 | adantr 471 |
. . . . . 6
 
       |
93 | 91, 92 | readdcld 9701 |
. . . . 5
 
             |
94 | 93, 64 | fmptd 6074 |
. . . 4
           |
95 | 75 | adantr 471 |
. . . . . 6
 
 ..^    |
96 | 42, 45, 95, 29 | ltadd1dd 10257 |
. . . . 5
 
 ..^                  |
97 | 40, 93 | sylan2 481 |
. . . . . 6
 
 ..^          |
98 | 64 | fvmpt2 5985 |
. . . . . 6
                         |
99 | 41, 97, 98 | syl2anc 671 |
. . . . 5
 
 ..^              |
100 | | fveq2 5892 |
. . . . . . . . . 10
           |
101 | 100 | oveq1d 6335 |
. . . . . . . . 9
               |
102 | 101 | cbvmptv 4511 |
. . . . . . . 8
                         |
103 | 64, 102 | eqtri 2484 |
. . . . . . 7
             |
104 | 103 | a1i 11 |
. . . . . 6
 
 ..^                |
105 | | fveq2 5892 |
. . . . . . . 8
               |
106 | 105 | oveq1d 6335 |
. . . . . . 7
                   |
107 | 106 | adantl 472 |
. . . . . 6
    ..^                     |
108 | 45, 95 | readdcld 9701 |
. . . . . 6
 
 ..^            |
109 | 104, 107,
44, 108 | fvmptd 5982 |
. . . . 5
 
 ..^                  |
110 | 96, 99, 109 | 3brtr4d 4449 |
. . . 4
 
 ..^              |
111 | 30 | adantr 471 |
. . . . 5
 
      ![[,] [,]](_icc.gif)             |
112 | 77, 76 | eqeltrd 2540 |
. . . . . . . 8
       |
113 | 112 | adantr 471 |
. . . . . . 7
 
      ![[,] [,]](_icc.gif)             |
114 | 86, 85 | eqeltrd 2540 |
. . . . . . . 8
       |
115 | 114 | adantr 471 |
. . . . . . 7
 
      ![[,] [,]](_icc.gif)             |
116 | 113, 115 | iccssred 37687 |
. . . . . 6
 
      ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)        |
117 | | simpr 467 |
. . . . . 6
 
      ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)        |
118 | 116, 117 | sseldd 3445 |
. . . . 5
 
      ![[,] [,]](_icc.gif)         |
119 | 111, 118 | ffvelrnd 6051 |
. . . 4
 
      ![[,] [,]](_icc.gif)             |
120 | 99, 97 | eqeltrd 2540 |
. . . . 5
 
 ..^        |
121 | 109, 108 | eqeltrd 2540 |
. . . . 5
 
 ..^          |
122 | | ioosscn 37676 |
. . . . . . . . 9
               |
123 | 122 | a1i 11 |
. . . . . . . 8
 
 ..^                  |
124 | | eqeq1 2466 |
. . . . . . . . . . 11
   
     |
125 | 124 | rexbidv 2913 |
. . . . . . . . . 10
  
                
                     |
126 | | oveq1 6327 |
. . . . . . . . . . . 12
       |
127 | 126 | eqeq2d 2472 |
. . . . . . . . . . 11
   
     |
128 | 127 | cbvrexv 3032 |
. . . . . . . . . 10
                  
                    |
129 | 125, 128 | syl6bb 269 |
. . . . . . . . 9
  
                
                     |
130 | 129 | cbvrabv 3056 |
. . . . . . . 8
                                         |
131 | | fdm 5760 |
. . . . . . . . . . . 12
       |
132 | 30, 131 | syl 17 |
. . . . . . . . . . 11
   |
133 | 132 | feq2d 5741 |
. . . . . . . . . 10
             |
134 | 30, 133 | mpbird 240 |
. . . . . . . . 9
       |
135 | 134 | adantr 471 |
. . . . . . . 8
 
 ..^        |
136 | | elioore 11700 |
. . . . . . . . . . . . . . . . . 18
                 |
137 | 136 | adantl 472 |
. . . . . . . . . . . . . . . . 17
 
                 |
138 | 75 | adantr 471 |
. . . . . . . . . . . . . . . . 17
 
                 |
139 | 137, 138 | readdcld 9701 |
. . . . . . . . . . . . . . . 16
 
                   |
140 | 139 | adantlr 726 |
. . . . . . . . . . . . . . 15
    ..^                     |
141 | 140 | 3adant3 1034 |
. . . . . . . . . . . . . 14
    ..^                       |
142 | | simp3 1016 |
. . . . . . . . . . . . . 14
    ..^                       |
143 | 132 | 3ad2ant1 1035 |
. . . . . . . . . . . . . . 15
 
                   |
144 | 143 | 3adant1r 1269 |
. . . . . . . . . . . . . 14
    ..^                     |
145 | 141, 142,
144 | 3eltr4d 2555 |
. . . . . . . . . . . . 13
    ..^                     |
146 | 145 | 3exp 1214 |
. . . . . . . . . . . 12
 
 ..^                
       |
147 | 146 | adantr 471 |
. . . . . . . . . . 11
    ..^                         |
148 | 147 | rexlimdv 2889 |
. . . . . . . . . 10
    ..^    
                
   |
149 | 148 | ralrimiva 2814 |
. . . . . . . . 9
 
 ..^                     
   |
150 | | rabss 3518 |
. . . . . . . . 9
  
                 
                       |
151 | 149, 150 | sylibr 217 |
. . . . . . . 8
 
 ..^                     
  |
152 | | simpll 765 |
. . . . . . . . 9
    ..^                   |
153 | 32 | rexrd 9721 |
. . . . . . . . . . 11
   |
154 | 153 | ad2antrr 737 |
. . . . . . . . . 10
    ..^                   |
155 | 34 | rexrd 9721 |
. . . . . . . . . . 11
   |
156 | 155 | ad2antrr 737 |
. . . . . . . . . 10
    ..^                   |
157 | 3, 2, 1 | fourierdlem15 38085 |
. . . . . . . . . . 11
           ![[,] [,]](_icc.gif)    |
158 | 157 | ad2antrr 737 |
. . . . . . . . . 10
    ..^                           ![[,] [,]](_icc.gif)    |
159 | | simplr 767 |
. . . . . . . . . 10
    ..^                  ..^   |
160 | | ioossicc 11754 |
. . . . . . . . . . . 12
                    ![[,] [,]](_icc.gif)         |
161 | 160 | sseli 3440 |
. . . . . . . . . . 11
                     ![[,] [,]](_icc.gif)          |
162 | 161 | adantl 472 |
. . . . . . . . . 10
    ..^                       ![[,] [,]](_icc.gif)          |
163 | 154, 156,
158, 159, 162 | fourierdlem1 38071 |
. . . . . . . . 9
    ..^                   ![[,] [,]](_icc.gif)    |
164 | | fourierdlem81.fper |
. . . . . . . . 9
 
  ![[,] [,]](_icc.gif)  
            |
165 | 152, 163,
164 | syl2anc 671 |
. . . . . . . 8
    ..^                             |
166 | 123, 95, 130, 135, 151, 165, 53 | cncfperiod 37842 |
. . . . . . 7
 
 ..^   
                      
                       |
167 | 125 | elrab 3208 |
. . . . . . . . . . . . 13
                                           |
168 | 167 | simprbi 470 |
. . . . . . . . . . . 12
                    
                    |
169 | | simpr 467 |
. . . . . . . . . . . . . 14
    ..^                    
                    |
170 | | nfv 1772 |
. . . . . . . . . . . . . . . 16
    ..^   |
171 | | nfre1 2860 |
. . . . . . . . . . . . . . . 16
                     |
172 | 170, 171 | nfan 2022 |
. . . . . . . . . . . . . . 15
   
 ..^                      |
173 | | nfv 1772 |
. . . . . . . . . . . . . . 15
      
        |
174 | | simp3 1016 |
. . . . . . . . . . . . . . . . . . . 20
 
                     |
175 | 139 | 3adant3 1034 |
. . . . . . . . . . . . . . . . . . . 20
 
                     |
176 | 174, 175 | eqeltrd 2540 |
. . . . . . . . . . . . . . . . . . 19
 
                   |
177 | 176 | 3adant1r 1269 |
. . . . . . . . . . . . . . . . . 18
    ..^                     |
178 | 42 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . 21
    ..^                       |
179 | 136 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . 21
    ..^                   |
180 | 75 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . . . 21
    ..^                   |
181 | | simpr 467 |
. . . . . . . . . . . . . . . . . . . . . . 23
    ..^                                 |
182 | 42 | rexrd 9721 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
 ..^        |
183 | 182 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    ..^                       |
184 | 45 | rexrd 9721 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
 ..^          |
185 | 184 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    ..^                         |
186 | | elioo2 11711 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                           
    
          |
187 | 183, 185,
186 | syl2anc 671 |
. . . . . . . . . . . . . . . . . . . . . . 23
    ..^                               
    
          |
188 | 181, 187 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . . . 22
    ..^                               |
189 | 188 | simp2d 1027 |
. . . . . . . . . . . . . . . . . . . . 21
    ..^                       |
190 | 178, 179,
180, 189 | ltadd1dd 10257 |
. . . . . . . . . . . . . . . . . . . 20
    ..^                           |
191 | 190 | 3adant3 1034 |
. . . . . . . . . . . . . . . . . . 19
    ..^                             |
192 | 99 | 3ad2ant1 1035 |
. . . . . . . . . . . . . . . . . . 19
    ..^                               |
193 | | simp3 1016 |
. . . . . . . . . . . . . . . . . . 19
    ..^                       |
194 | 191, 192,
193 | 3brtr4d 4449 |
. . . . . . . . . . . . . . . . . 18
    ..^                         |
195 | 45 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . 21
    ..^                         |
196 | 188 | simp3d 1028 |
. . . . . . . . . . . . . . . . . . . . 21
    ..^                         |
197 | 179, 195,
180, 196 | ltadd1dd 10257 |
. . . . . . . . . . . . . . . . . . . 20
    ..^                             |
198 | 197 | 3adant3 1034 |
. . . . . . . . . . . . . . . . . . 19
    ..^                               |
199 | 109 | 3ad2ant1 1035 |
. . . . . . . . . . . . . . . . . . 19
    ..^                                   |
200 | 198, 193,
199 | 3brtr4d 4449 |
. . . . . . . . . . . . . . . . . 18
    ..^                           |
201 | 177, 194,
200 | 3jca 1194 |
. . . . . . . . . . . . . . . . 17
    ..^                                 |
202 | 201 | 3exp 1214 |
. . . . . . . . . . . . . . . 16
 
 ..^                
                   |
203 | 202 | adantr 471 |
. . . . . . . . . . . . . . 15
    ..^                    
              
                   |
204 | 172, 173,
203 | rexlimd 2883 |
. . . . . . . . . . . . . 14
    ..^                    
 
                
    
          |
205 | 169, 204 | mpd 15 |
. . . . . . . . . . . . 13
    ..^                    
    
         |
206 | 120 | rexrd 9721 |
. . . . . . . . . . . . . . 15
 
 ..^        |
207 | 206 | adantr 471 |
. . . . . . . . . . . . . 14
    ..^                    
      |
208 | 121 | rexrd 9721 |
. . . . . . . . . . . . . . 15
 
 ..^          |
209 | 208 | adantr 471 |
. . . . . . . . . . . . . 14
    ..^                    
        |
210 | | elioo2 11711 |
. . . . . . . . . . . . . 14
                           
    
          |
211 | 207, 209,
210 | syl2anc 671 |
. . . . . . . . . . . . 13
    ..^                    
                   
          |
212 | 205, 211 | mpbird 240 |
. . . . . . . . . . . 12
    ..^                    
                |
213 | 168, 212 | sylan2 481 |
. . . . . . . . . . 11
    ..^                      
                |
214 | | elioore 11700 |
. . . . . . . . . . . . . 14
                 |
215 | 214 | recnd 9700 |
. . . . . . . . . . . . 13
                 |
216 | 215 | adantl 472 |
. . . . . . . . . . . 12
    ..^                   |
217 | 182 | adantr 471 |
. . . . . . . . . . . . . 14
    ..^                       |
218 | 184 | adantr 471 |
. . . . . . . . . . . . . 14
    ..^                         |
219 | 214 | adantl 472 |
. . . . . . . . . . . . . . . 16
 
                 |
220 | 75 | adantr 471 |
. . . . . . . . . . . . . . . 16
 
                 |
221 | 219, 220 | resubcld 10080 |
. . . . . . . . . . . . . . 15
 
                   |
222 | 221 | adantlr 726 |
. . . . . . . . . . . . . 14
    ..^                     |
223 | 99 | oveq1d 6335 |
. . . . . . . . . . . . . . . . 17
 
 ..^                  |
224 | 42 | recnd 9700 |
. . . . . . . . . . . . . . . . . 18
 
 ..^        |
225 | 95 | recnd 9700 |
. . . . . . . . . . . . . . . . . 18
 
 ..^    |
226 | 224, 225 | pncand 10018 |
. . . . . . . . . . . . . . . . 17
 
 ..^                |
227 | 223, 226 | eqtr2d 2497 |
. . . . . . . . . . . . . . . 16
 
 ..^              |
228 | 227 | adantr 471 |
. . . . . . . . . . . . . . 15
    ..^                             |
229 | 120 | adantr 471 |
. . . . . . . . . . . . . . . 16
    ..^                       |
230 | 214 | adantl 472 |
. . . . . . . . . . . . . . . 16
    ..^                   |
231 | 75 | ad2antrr 737 |
. . . . . . . . . . . . . . . 16
    ..^                   |
232 | | simpr 467 |
. . . . . . . . . . . . . . . . . 18
    ..^                                 |
233 | 206 | adantr 471 |
. . . . . . . . . . . . . . . . . . 19
    ..^                       |
234 | 208 | adantr 471 |
. . . . . . . . . . . . . . . . . . 19
    ..^                         |
235 | 233, 234,
210 | syl2anc 671 |
. . . . . . . . . . . . . . . . . 18
    ..^                               
    
          |
236 | 232, 235 | mpbid 215 |
. . . . . . . . . . . . . . . . 17
    ..^                               |
237 | 236 | simp2d 1027 |
. . . . . . . . . . . . . . . 16
    ..^                       |
238 | 229, 230,
231, 237 | ltsub1dd 10258 |
. . . . . . . . . . . . . . 15
    ..^                           |
239 | 228, 238 | eqbrtrd 4439 |
. . . . . . . . . . . . . 14
    ..^                         |
240 | 121 | adantr 471 |
. . . . . . . . . . . . . . . 16
    ..^                         |
241 | 236 | simp3d 1028 |
. . . . . . . . . . . . . . . 16
    ..^                         |
242 | 230, 240,
231, 241 | ltsub1dd 10258 |
. . . . . . . . . . . . . . 15
    ..^                             |
243 | 109 | oveq1d 6335 |
. . . . . . . . . . . . . . . . 17
 
 ..^                      |
244 | 45 | recnd 9700 |
. . . . . . . . . . . . . . . . . 18
 
 ..^          |
245 | 244, 225 | pncand 10018 |
. . . . . . . . . . . . . . . . 17
 
 ..^                    |
246 | 243, 245 | eqtrd 2496 |
. . . . . . . . . . . . . . . 16
 
 ..^                  |
247 | 246 | adantr 471 |
. . . . . . . . . . . . . . 15
    ..^                                 |
248 | 242, 247 | breqtrd 4443 |
. . . . . . . . . . . . . 14
    ..^                           |
249 | 217, 218,
222, 239, 248 | eliood 37680 |
. . . . . . . . . . . . 13
    ..^                                   |
250 | 219 | recnd 9700 |
. . . . . . . . . . . . . . . 16
 
                 |
251 | 220 | recnd 9700 |
. . . . . . . . . . . . . . . 16
 
                 |
252 | 250, 251 | npcand 10021 |
. . . . . . . . . . . . . . 15
 
                     |
253 | 252 | eqcomd 2468 |
. . . . . . . . . . . . . 14
 
                     |
254 | 253 | adantlr 726 |
. . . . . . . . . . . . 13
    ..^                       |
255 | | oveq1 6327 |
. . . . . . . . . . . . . . 15
           |
256 | 255 | eqeq2d 2472 |
. . . . . . . . . . . . . 14
     
       |
257 | 256 | rspcev 3162 |
. . . . . . . . . . . . 13
                 
                         |
258 | 249, 254,
257 | syl2anc 671 |
. . . . . . . . . . . 12
    ..^                                     |
259 | 216, 258,
167 | sylanbrc 675 |
. . . . . . . . . . 11
    ..^                                       |
260 | 213, 259 | impbida 848 |
. . . . . . . . . 10
 
 ..^                                        |
261 | 260 | eqrdv 2460 |
. . . . . . . . 9
 
 ..^                                      |
262 | 261 | reseq2d 5127 |
. . . . . . . 8
 
 ..^   
                                      |
263 | 30 | adantr 471 |
. . . . . . . . 9
 
 ..^        |
264 | | ioossre 11730 |
. . . . . . . . . 10
               |
265 | 264 | a1i 11 |
. . . . . . . . 9
 
 ..^                  |
266 | 263, 265 | feqresmpt 5946 |
. . . . . . . 8
 
 ..^                                        |
267 | 262, 266 | eqtrd 2496 |
. . . . . . 7
 
 ..^   
                                          |
268 | 261 | oveq1d 6335 |
. . . . . . 7
 
 ..^                                              |
269 | 166, 267,
268 | 3eltr3d 2554 |
. . . . . 6
 
 ..^                                          |
270 | 49, 132 | syl5sseqr 3493 |
. . . . . . . . 9
              
  |
271 | 270 | adantr 471 |
. . . . . . . 8
 
 ..^                  |
272 | | eqid 2462 |
. . . . . . . 8
                                         |
273 | | simpll 765 |
. . . . . . . . 9
    ..^                   |
274 | 153 | ad2antrr 737 |
. . . . . . . . . 10
    ..^                   |
275 | 155 | ad2antrr 737 |
. . . . . . . . . 10
    ..^                   |
276 | 157 | ad2antrr 737 |
. . . . . . . . . 10
    ..^                           ![[,] [,]](_icc.gif)    |
277 | | simplr 767 |
. . . . . . . . . 10
    ..^                  ..^   |
278 | 160, 181 | sseldi 3442 |
. . . . . . . . . 10
    ..^                       ![[,] [,]](_icc.gif)          |
279 | 274, 275,
276, 277, 278 | fourierdlem1 38071 |
. . . . . . . . 9
    ..^                   ![[,] [,]](_icc.gif)    |
280 | | eleq1 2528 |
. . . . . . . . . . . 12
    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     |
281 | 280 | anbi2d 715 |
. . . . . . . . . . 11
  
  ![[,] [,]](_icc.gif)  
   ![[,] [,]](_icc.gif)      |
282 | | oveq1 6327 |
. . . . . . . . . . . . 13
       |
283 | 282 | fveq2d 5896 |
. . . . . . . . . . . 12
               |
284 | | fveq2 5892 |
. . . . . . . . . . . 12
           |
285 | 283, 284 | eqeq12d 2477 |
. . . . . . . . . . 11
           
             |
286 | 281, 285 | imbi12d 326 |
. . . . . . . . . 10
   
  ![[,] [,]](_icc.gif)               
  ![[,] [,]](_icc.gif)                 |
287 | 286, 164 | chvarv 2118 |
. . . . . . . . 9
 
  ![[,] [,]](_icc.gif)  
            |
288 | 273, 279,
287 | syl2anc 671 |
. . . . . . . 8
    ..^                             |
289 | 135, 123,
271, 225, 272, 151, 288, 54 | limcperiod 37794 |
. . . . . . 7
 
 ..^                         lim            |
290 | 109 | eqcomd 2468 |
. . . . . . . 8
 
 ..^                  |
291 | 267, 290 | oveq12d 6338 |
. . . . . . 7
 
 ..^                         lim                               lim          |
292 | 289, 291 | eleqtrd 2542 |
. . . . . 6
 
 ..^                       lim          |
293 | 135, 123,
271, 225, 272, 151, 288, 55 | limcperiod 37794 |
. . . . . . 7
 
 ..^                         lim          |
294 | 99 | eqcomd 2468 |
. . . . . . . 8
 
 ..^              |
295 | 267, 294 | oveq12d 6338 |
. . . . . . 7
 
 ..^                         lim                             lim        |
296 | 293, 295 | eleqtrd 2542 |
. . . . . 6
 
 ..^                       lim        |
297 | 120, 121,
269, 292, 296 | iblcncfioo 37941 |
. . . . 5
 
 ..^                         |
298 | 30 | ad2antrr 737 |
. . . . . 6
    ..^        ![[,] [,]](_icc.gif)               |
299 | 120 | adantr 471 |
. . . . . . 7
    ..^        ![[,] [,]](_icc.gif)               |
300 | 121 | adantr 471 |
. . . . . . 7
    ..^        ![[,] [,]](_icc.gif)                 |
301 | | simpr 467 |
. . . . . . 7
    ..^        ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)          |
302 | | eliccre 37688 |
. . . . . . 7
                  ![[,] [,]](_icc.gif)           |
303 | 299, 300,
301, 302 | syl3anc 1276 |
. . . . . 6
    ..^        ![[,] [,]](_icc.gif)           |
304 | 298, 303 | ffvelrnd 6051 |
. . . . 5
    ..^        ![[,] [,]](_icc.gif)               |
305 | 120, 121,
297, 304 | ibliooicc 37934 |
. . . 4
 
 ..^         ![[,] [,]](_icc.gif)                |
306 | 15, 20, 94, 110, 119, 305 | itgspltprt 37942 |
. . 3
        ![[,] [,]](_icc.gif)              ..^         ![[,] [,]](_icc.gif)                |
307 | | iftrue 3899 |
. . . . . . . . . . . 12
      
                 
                      |
308 | 307 | adantl 472 |
. . . . . . . . . . 11
    ..^        
                 
                      |
309 | | fourierdlem81.g |
. . . . . . . . . . . . . . 15
       ![[,] [,]](_icc.gif)                                  |
310 | | iftrue 3899 |
. . . . . . . . . . . . . . . . . . 19
      
                        |
311 | | iftrue 3899 |
. . . . . . . . . . . . . . . . . . 19
      
                 
                      |
312 | 310, 311 | eqtr4d 2499 |
. . . . . . . . . . . . . . . . . 18
      
                                         
                      |
313 | 312 | adantl 472 |
. . . . . . . . . . . . . . . . 17
   
 ..^ 
      ![[,] [,]](_icc.gif)        
              
                       
                                |
314 | | iffalse 3902 |
. . . . . . . . . . . . . . . . . . . . 21
              
                               |
315 | 314 | adantr 471 |
. . . . . . . . . . . . . . . . . . . 20
            
                                         |
316 | | iftrue 3899 |
. . . . . . . . . . . . . . . . . . . . 21
        
               |
317 | 316 | adantl 472 |
. . . . . . . . . . . . . . . . . . . 20
            
                 |
318 | | iffalse 3902 |
. . . . . . . . . . . . . . . . . . . . . 22
              
                                                               |
319 | 318 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . 21
            
                   
                                                     |
320 | | iftrue 3899 |
. . . . . . . . . . . . . . . . . . . . . 22
        
                               |
321 | 320 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . 21
            
           
                     |
322 | 319, 321 | eqtr2d 2497 |
. . . . . . . . . . . . . . . . . . . 20
            
         
                                |
323 | 315, 317,
322 | 3eqtrd 2500 |
. . . . . . . . . . . . . . . . . . 19
            
                                           
                      |
324 | 323 | adantll 725 |
. . . . . . . . . . . . . . . . . 18
      ..^ 
      ![[,] [,]](_icc.gif)        
    
      
                                           
                      |
325 | 314 | ad2antlr 738 |
. . . . . . . . . . . . . . . . . . 19
      ..^ 
      ![[,] [,]](_icc.gif)        
    
                
                               |
326 | | iffalse 3902 |
. . . . . . . . . . . . . . . . . . . 20
                            |
327 | 326 | adantl 472 |
. . . . . . . . . . . . . . . . . . 19
      ..^ 
      ![[,] [,]](_icc.gif)        
    
                            |
328 | 318 | ad2antlr 738 |
. . . . . . . . . . . . . . . . . . . 20
      ..^ 
      ![[,] [,]](_icc.gif)        
    
                
                                                               |
329 | | iffalse 3902 |
. . . . . . . . . . . . . . . . . . . . 21
                                       
                    |
330 | 329 | adantl 472 |
. . . . . . . . . . . . . . . . . . . 20
      ..^ 
      ![[,] [,]](_icc.gif)        
    
                                       
                    |
331 | 182 | ad3antrrr 741 |
. . . . . . . . . . . . . . . . . . . . . 22
      ..^ 
      ![[,] [,]](_icc.gif)        
    
             |
332 | 184 | ad3antrrr 741 |
. . . . . . . . . . . . . . . . . . . . . 22
      ..^ 
      ![[,] [,]](_icc.gif)        
    
               |
333 | 60 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . . . . 22
      ..^ 
      ![[,] [,]](_icc.gif)        
    
      
  |
334 | 42 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
 ..^ 
      ![[,] [,]](_icc.gif)        
    
      |
335 | 60 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
 ..^ 
      ![[,] [,]](_icc.gif)        
    
  |
336 | 182 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
 ..^ 
      ![[,] [,]](_icc.gif)        
    
      |
337 | 184 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
 ..^ 
      ![[,] [,]](_icc.gif)        
    
        |
338 | | simplr 767 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
 ..^ 
      ![[,] [,]](_icc.gif)        
    
      ![[,] [,]](_icc.gif)          |
339 | | iccgelb 11725 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
           
      ![[,] [,]](_icc.gif)               |
340 | 336, 337,
338, 339 | syl3anc 1276 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
 ..^ 
      ![[,] [,]](_icc.gif)        
    
      |
341 | | neqne 2643 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
           |
342 | 341 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
 ..^ 
      ![[,] [,]](_icc.gif)        
    
      |
343 | 334, 335,
340, 342 | leneltd 9820 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
 ..^ 
      ![[,] [,]](_icc.gif)        
    
      |
344 | 343 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . 22
      ..^ 
      ![[,] [,]](_icc.gif)        
    
          
  |
345 | 45 | ad3antrrr 741 |
. . . . . . . . . . . . . . . . . . . . . . 23
      ..^ 
      ![[,] [,]](_icc.gif)        
    
               |
346 | 182 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    ..^        ![[,] [,]](_icc.gif)               |
347 | 184 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    ..^        ![[,] [,]](_icc.gif)                 |
348 | | simpr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    ..^        ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)          |
349 | | iccleub 11724 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
           
      ![[,] [,]](_icc.gif)                 |
350 | 346, 347,
348, 349 | syl3anc 1276 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    ..^        ![[,] [,]](_icc.gif)                 |
351 | 350 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . . . . . 23
      ..^ 
      ![[,] [,]](_icc.gif)        
    
               |
352 | | neqne 2643 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
               |
353 | 352 | necomd 2691 |
. . . . . . . . . . . . . . . . . . . . . . . 24
               |
354 | 353 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . 23
      ..^ 
      ![[,] [,]](_icc.gif)        
    
               |
355 | 333, 345,
351, 354 | leneltd 9820 |
. . . . . . . . . . . . . . . . . . . . . 22
      ..^ 
      ![[,] [,]](_icc.gif)        
    
               |
356 | 331, 332,
333, 344, 355 | eliood 37680 |
. . . . . . . . . . . . . . . . . . . . 21
      ..^ 
      ![[,] [,]](_icc.gif)        
    
      
                |
357 | | fvres 5906 |
. . . . . . . . . . . . . . . . . . . . 21
                                         |
358 | 356, 357 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
      ..^ 
      ![[,] [,]](_icc.gif)        
    
                                 |
359 | 328, 330,
358 | 3eqtrrd 2501 |
. . . . . . . . . . . . . . . . . . 19
      ..^ 
      ![[,] [,]](_icc.gif)        
    
        |