Step | Hyp | Ref
| Expression |
1 | | fourierdlem92.a |
. . . 4
   |
2 | 1 | adantr 471 |
. . 3
 

  |
3 | | fourierdlem92.b |
. . . 4
   |
4 | 3 | adantr 471 |
. . 3
 

  |
5 | | fourierdlem92.p |
. . 3
 
                 
 ..^                |
6 | | fourierdlem92.m |
. . . 4
   |
7 | 6 | adantr 471 |
. . 3
 

  |
8 | | fourierdlem92.t |
. . . . 5
   |
9 | 8 | adantr 471 |
. . . 4
 

  |
10 | | simpr 467 |
. . . 4
 

  |
11 | 9, 10 | elrpd 11328 |
. . 3
 

  |
12 | | fourierdlem92.q |
. . . 4
       |
13 | 12 | adantr 471 |
. . 3
 

      |
14 | | fourierdlem92.fper |
. . . 4
 
  ![[,] [,]](_icc.gif)  
            |
15 | 14 | adantlr 726 |
. . 3
      ![[,] [,]](_icc.gif)               |
16 | | fveq2 5848 |
. . . . 5
           |
17 | 16 | oveq1d 6291 |
. . . 4
               |
18 | 17 | cbvmptv 4467 |
. . 3
                         |
19 | | fourierdlem92.f |
. . . 4
       |
20 | 19 | adantr 471 |
. . 3
 

      |
21 | | fourierdlem92.cncf |
. . . 4
 
 ..^                                      |
22 | 21 | adantlr 726 |
. . 3
     ..^ 
                                    |
23 | | fourierdlem92.r |
. . . 4
 
 ..^                   lim        |
24 | 23 | adantlr 726 |
. . 3
     ..^ 
                 lim        |
25 | | fourierdlem92.l |
. . . 4
 
 ..^                   lim          |
26 | 25 | adantlr 726 |
. . 3
     ..^ 
                 lim          |
27 | | eqeq1 2456 |
. . . . 5
     
       |
28 | | eqeq1 2456 |
. . . . . 6
       
         |
29 | | fveq2 5848 |
. . . . . 6
           |
30 | 28, 29 | ifbieq2d 3874 |
. . . . 5
                                 |
31 | 27, 30 | ifbieq2d 3874 |
. . . 4
                                  
                |
32 | 31 | cbvmptv 4467 |
. . 3
       ![[,] [,]](_icc.gif)                                        ![[,] [,]](_icc.gif)                 
                |
33 | | eqid 2452 |
. . 3
                   ![[,] [,]](_icc.gif)                            ![[,] [,]](_icc.gif)                                                          ![[,] [,]](_icc.gif)                            ![[,] [,]](_icc.gif)                                   
    |
34 | 2, 4, 5, 7, 11, 13, 15, 18, 20, 22, 24, 26, 32, 33 | fourierdlem81 38108 |
. 2
 

     ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)          |
35 | | simpr 467 |
. . . . . . . 8
 
   |
36 | 35 | oveq2d 6292 |
. . . . . . 7
 
 
     |
37 | 1 | recnd 9656 |
. . . . . . . . 9
   |
38 | 37 | adantr 471 |
. . . . . . . 8
 
   |
39 | 38 | addid1d 9820 |
. . . . . . 7
 
 
   |
40 | 36, 39 | eqtrd 2486 |
. . . . . 6
 
 
   |
41 | 35 | oveq2d 6292 |
. . . . . . 7
 
 
     |
42 | 3 | recnd 9656 |
. . . . . . . . 9
   |
43 | 42 | adantr 471 |
. . . . . . . 8
 
   |
44 | 43 | addid1d 9820 |
. . . . . . 7
 
 
   |
45 | 41, 44 | eqtrd 2486 |
. . . . . 6
 
 
   |
46 | 40, 45 | oveq12d 6294 |
. . . . 5
 
     ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)    |
47 | 46 | itgeq1d 37875 |
. . . 4
 
      ![[,] [,]](_icc.gif) 
           ![[,] [,]](_icc.gif)          |
48 | 47 | adantlr 726 |
. . 3
   
      ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)          |
49 | | simpll 765 |
. . . 4
   

  |
50 | | simpr 467 |
. . . . . . 7
   

  |
51 | | simplr 767 |
. . . . . . 7
   

  |
52 | | ioran 497 |
. . . . . . 7
       |
53 | 50, 51, 52 | sylanbrc 675 |
. . . . . 6
   


   |
54 | 49, 8 | syl 17 |
. . . . . . 7
   

  |
55 | | 0red 9631 |
. . . . . . 7
   

  |
56 | 54, 55 | lttrid 9760 |
. . . . . 6
   


     |
57 | 53, 56 | mpbird 240 |
. . . . 5
   

  |
58 | 54 | lt0neg1d 10172 |
. . . . 5
   

     |
59 | 57, 58 | mpbid 215 |
. . . 4
   

   |
60 | 1, 8 | readdcld 9657 |
. . . . . . . . . . . 12
     |
61 | 60 | recnd 9656 |
. . . . . . . . . . 11
     |
62 | 8 | recnd 9656 |
. . . . . . . . . . 11
   |
63 | 61, 62 | negsubd 9979 |
. . . . . . . . . 10
            |
64 | 37, 62 | pncand 9974 |
. . . . . . . . . 10
       |
65 | 63, 64 | eqtrd 2486 |
. . . . . . . . 9
        |
66 | 3, 8 | readdcld 9657 |
. . . . . . . . . . . 12
     |
67 | 66 | recnd 9656 |
. . . . . . . . . . 11
     |
68 | 67, 62 | negsubd 9979 |
. . . . . . . . . 10
            |
69 | 42, 62 | pncand 9974 |
. . . . . . . . . 10
       |
70 | 68, 69 | eqtrd 2486 |
. . . . . . . . 9
        |
71 | 65, 70 | oveq12d 6294 |
. . . . . . . 8
        ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)    |
72 | 71 | eqcomd 2458 |
. . . . . . 7
   ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)         |
73 | 72 | itgeq1d 37875 |
. . . . . 6
    ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)               |
74 | 73 | adantr 471 |
. . . . 5
 
     ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)               |
75 | 1 | adantr 471 |
. . . . . . 7
 
    |
76 | 8 | adantr 471 |
. . . . . . 7
 
    |
77 | 75, 76 | readdcld 9657 |
. . . . . 6
 
  
   |
78 | 3 | adantr 471 |
. . . . . . 7
 
    |
79 | 78, 76 | readdcld 9657 |
. . . . . 6
 
  
   |
80 | | eqid 2452 |
. . . . . 6
                         ..^                                        ..^                |
81 | 6 | adantr 471 |
. . . . . 6
 
    |
82 | 76 | renegcld 10035 |
. . . . . . 7
 
     |
83 | | simpr 467 |
. . . . . . 7
 
     |
84 | 82, 83 | elrpd 11328 |
. . . . . 6
 
     |
85 | 5 | fourierdlem2 38028 |
. . . . . . . . . . . . . . . . . 18
 
   
                  
 ..^                 |
86 | 6, 85 | syl 17 |
. . . . . . . . . . . . . . . . 17
                        
 ..^                 |
87 | 12, 86 | mpbid 215 |
. . . . . . . . . . . . . . . 16
                   
 ..^                |
88 | 87 | simpld 465 |
. . . . . . . . . . . . . . 15
         |
89 | | elmapi 7480 |
. . . . . . . . . . . . . . 15
                 |
90 | 88, 89 | syl 17 |
. . . . . . . . . . . . . 14
           |
91 | 90 | ffvelrnda 6006 |
. . . . . . . . . . . . 13
 
           |
92 | 8 | adantr 471 |
. . . . . . . . . . . . 13
 
       |
93 | 91, 92 | readdcld 9657 |
. . . . . . . . . . . 12
 
             |
94 | | fourierdlem92.s |
. . . . . . . . . . . 12
             |
95 | 93, 94 | fmptd 6030 |
. . . . . . . . . . 11
           |
96 | | reex 9617 |
. . . . . . . . . . . . 13
 |
97 | 96 | a1i 11 |
. . . . . . . . . . . 12
   |
98 | | ovex 6304 |
. . . . . . . . . . . . 13
     |
99 | 98 | a1i 11 |
. . . . . . . . . . . 12
       |
100 | 97, 99 | elmapd 7473 |
. . . . . . . . . . 11
                   |
101 | 95, 100 | mpbird 240 |
. . . . . . . . . 10
         |
102 | 94 | a1i 11 |
. . . . . . . . . . . . 13
               |
103 | | fveq2 5848 |
. . . . . . . . . . . . . . 15
           |
104 | 103 | oveq1d 6291 |
. . . . . . . . . . . . . 14
               |
105 | 104 | adantl 472 |
. . . . . . . . . . . . 13
 
               |
106 | | 0zd 10939 |
. . . . . . . . . . . . . . . 16
   |
107 | 6 | nnzd 11029 |
. . . . . . . . . . . . . . . 16
   |
108 | 106, 107,
106 | 3jca 1189 |
. . . . . . . . . . . . . . 15
 
   |
109 | | 0le0 10688 |
. . . . . . . . . . . . . . . 16
 |
110 | 109 | a1i 11 |
. . . . . . . . . . . . . . 15

  |
111 | | nnnn0 10866 |
. . . . . . . . . . . . . . . . 17
   |
112 | 111 | nn0ge0d 10918 |
. . . . . . . . . . . . . . . 16
   |
113 | 6, 112 | syl 17 |
. . . . . . . . . . . . . . 15

  |
114 | 108, 110,
113 | jca32 542 |
. . . . . . . . . . . . . 14
    
    |
115 | | elfz2 11782 |
. . . . . . . . . . . . . 14
    
 
 
    |
116 | 114, 115 | sylibr 217 |
. . . . . . . . . . . . 13
       |
117 | 90, 116 | ffvelrnd 6007 |
. . . . . . . . . . . . . 14
       |
118 | 117, 8 | readdcld 9657 |
. . . . . . . . . . . . 13
         |
119 | 102, 105,
116, 118 | fvmptd 5938 |
. . . . . . . . . . . 12
             |
120 | | simprll 777 |
. . . . . . . . . . . . . 14
                   
 ..^                    |
121 | 87, 120 | syl 17 |
. . . . . . . . . . . . 13
       |
122 | 121 | oveq1d 6291 |
. . . . . . . . . . . 12
           |
123 | 119, 122 | eqtrd 2486 |
. . . . . . . . . . 11
         |
124 | | fveq2 5848 |
. . . . . . . . . . . . . . 15
           |
125 | 124 | oveq1d 6291 |
. . . . . . . . . . . . . 14
               |
126 | 125 | adantl 472 |
. . . . . . . . . . . . 13
 
               |
127 | 6 | nnnn0d 10915 |
. . . . . . . . . . . . . . 15
   |
128 | | nn0uz 11183 |
. . . . . . . . . . . . . . 15
     |
129 | 127, 128 | syl6eleq 2540 |
. . . . . . . . . . . . . 14
       |
130 | | eluzfz2 11798 |
. . . . . . . . . . . . . 14
    
      |
131 | 129, 130 | syl 17 |
. . . . . . . . . . . . 13
       |
132 | 90, 131 | ffvelrnd 6007 |
. . . . . . . . . . . . . 14
       |
133 | 132, 8 | readdcld 9657 |
. . . . . . . . . . . . 13
         |
134 | 102, 126,
131, 133 | fvmptd 5938 |
. . . . . . . . . . . 12
             |
135 | | simprlr 778 |
. . . . . . . . . . . . . 14
                   
 ..^                    |
136 | 87, 135 | syl 17 |
. . . . . . . . . . . . 13
       |
137 | 136 | oveq1d 6291 |
. . . . . . . . . . . 12
           |
138 | 134, 137 | eqtrd 2486 |
. . . . . . . . . . 11
         |
139 | 123, 138 | jca 539 |
. . . . . . . . . 10
                 |
140 | 90 | adantr 471 |
. . . . . . . . . . . . . 14
 
 ..^            |
141 | | elfzofz 11928 |
. . . . . . . . . . . . . . 15
  ..^
      |
142 | 141 | adantl 472 |
. . . . . . . . . . . . . 14
 
 ..^        |
143 | 140, 142 | ffvelrnd 6007 |
. . . . . . . . . . . . 13
 
 ..^        |
144 | | fzofzp1 12001 |
. . . . . . . . . . . . . . 15
  ..^
        |
145 | 144 | adantl 472 |
. . . . . . . . . . . . . 14
 
 ..^          |
146 | 140, 145 | ffvelrnd 6007 |
. . . . . . . . . . . . 13
 
 ..^          |
147 | 8 | adantr 471 |
. . . . . . . . . . . . 13
 
 ..^    |
148 | 87 | simprrd 772 |
. . . . . . . . . . . . . 14
   ..^              |
149 | 148 | r19.21bi 2757 |
. . . . . . . . . . . . 13
 
 ..^              |
150 | 143, 146,
147, 149 | ltadd1dd 10213 |
. . . . . . . . . . . 12
 
 ..^                  |
151 | 143, 147 | readdcld 9657 |
. . . . . . . . . . . . 13
 
 ..^          |
152 | 94 | fvmpt2 5941 |
. . . . . . . . . . . . 13
                         |
153 | 142, 151,
152 | syl2anc 671 |
. . . . . . . . . . . 12
 
 ..^              |
154 | 94, 18 | eqtr4i 2477 |
. . . . . . . . . . . . . 14
             |
155 | 154 | a1i 11 |
. . . . . . . . . . . . 13
 
 ..^                |
156 | | fveq2 5848 |
. . . . . . . . . . . . . . 15
               |
157 | 156 | oveq1d 6291 |
. . . . . . . . . . . . . 14
                   |
158 | 157 | adantl 472 |
. . . . . . . . . . . . 13
    ..^                     |
159 | 146, 147 | readdcld 9657 |
. . . . . . . . . . . . 13
 
 ..^            |
160 | 155, 158,
145, 159 | fvmptd 5938 |
. . . . . . . . . . . 12
 
 ..^                  |
161 | 150, 153,
160 | 3brtr4d 4405 |
. . . . . . . . . . 11
 
 ..^              |
162 | 161 | ralrimiva 2790 |
. . . . . . . . . 10
   ..^              |
163 | 101, 139,
162 | jca32 542 |
. . . . . . . . 9
                         ..^                |
164 | | fourierdlem92.h |
. . . . . . . . . . 11
 
             
         ..^     
          |
165 | 164 | fourierdlem2 38028 |
. . . . . . . . . 10
 
   
                        ..^                 |
166 | 6, 165 | syl 17 |
. . . . . . . . 9
                              ..^                 |
167 | 163, 166 | mpbird 240 |
. . . . . . . 8
       |
168 | 164 | fveq1i 5849 |
. . . . . . . 8
                              ..^                   |
169 | 167, 168 | syl6eleq 2540 |
. . . . . . 7
                 
         ..^     
              |
170 | 169 | adantr 471 |
. . . . . 6
 
                            ..^                    |
171 | 60 | adantr 471 |
. . . . . . . . . . . 12
 
    ![[,] [,]](_icc.gif) 
   
   |
172 | 66 | adantr 471 |
. . . . . . . . . . . 12
 
    ![[,] [,]](_icc.gif) 
   
   |
173 | | simpr 467 |
. . . . . . . . . . . 12
 
    ![[,] [,]](_icc.gif) 
       ![[,] [,]](_icc.gif) 
    |
174 | | eliccre 37644 |
. . . . . . . . . . . 12
    

 
  ![[,] [,]](_icc.gif)    
  |
175 | 171, 172,
173, 174 | syl3anc 1271 |
. . . . . . . . . . 11
 
    ![[,] [,]](_icc.gif) 
     |
176 | 175 | recnd 9656 |
. . . . . . . . . 10
 
    ![[,] [,]](_icc.gif) 
     |
177 | 62 | negcld 9960 |
. . . . . . . . . . 11
    |
178 | 177 | adantr 471 |
. . . . . . . . . 10
 
    ![[,] [,]](_icc.gif) 
      |
179 | 176, 178 | addcld 9649 |
. . . . . . . . 9
 
    ![[,] [,]](_icc.gif) 
        |
180 | | simpl 463 |
. . . . . . . . . 10
 
    ![[,] [,]](_icc.gif) 
     |
181 | 1 | adantr 471 |
. . . . . . . . . . 11
 
    ![[,] [,]](_icc.gif) 
     |
182 | 3 | adantr 471 |
. . . . . . . . . . 11
 
    ![[,] [,]](_icc.gif) 
     |
183 | 8 | renegcld 10035 |
. . . . . . . . . . . . 13
    |
184 | 183 | adantr 471 |
. . . . . . . . . . . 12
 
    ![[,] [,]](_icc.gif) 
      |
185 | 175, 184 | readdcld 9657 |
. . . . . . . . . . 11
 
    ![[,] [,]](_icc.gif) 
        |
186 | 63, 64 | eqtr2d 2487 |
. . . . . . . . . . . . 13
        |
187 | 186 | adantr 471 |
. . . . . . . . . . . 12
 
    ![[,] [,]](_icc.gif) 
          |
188 | 171 | rexrd 9677 |
. . . . . . . . . . . . . 14
 
    ![[,] [,]](_icc.gif) 
   
   |
189 | 172 | rexrd 9677 |
. . . . . . . . . . . . . 14
 
    ![[,] [,]](_icc.gif) 
   
   |
190 | | iccgelb 11681 |
. . . . . . . . . . . . . 14
    
     ![[,] [,]](_icc.gif) 
   
   |
191 | 188, 189,
173, 190 | syl3anc 1271 |
. . . . . . . . . . . . 13
 
    ![[,] [,]](_icc.gif) 
   
   |
192 | 171, 175,
184, 191 | leadd1dd 10216 |
. . . . . . . . . . . 12
 
    ![[,] [,]](_icc.gif) 
       
     |
193 | 187, 192 | eqbrtrd 4395 |
. . . . . . . . . . 11
 
    ![[,] [,]](_icc.gif) 
        |
194 | | iccleub 11680 |
. . . . . . . . . . . . . 14
    
     ![[,] [,]](_icc.gif) 
       |
195 | 188, 189,
173, 194 | syl3anc 1271 |
. . . . . . . . . . . . 13
 
    ![[,] [,]](_icc.gif) 
       |
196 | 175, 172,
184, 195 | leadd1dd 10216 |
. . . . . . . . . . . 12
 
    ![[,] [,]](_icc.gif) 
     
 
     |
197 | 172 | recnd 9656 |
. . . . . . . . . . . . . 14
 
    ![[,] [,]](_icc.gif) 
   
   |
198 | 62 | adantr 471 |
. . . . . . . . . . . . . 14
 
    ![[,] [,]](_icc.gif) 
     |
199 | 197, 198 | negsubd 9979 |
. . . . . . . . . . . . 13
 
    ![[,] [,]](_icc.gif) 
              |
200 | 69 | adantr 471 |
. . . . . . . . . . . . 13
 
    ![[,] [,]](_icc.gif) 
         |
201 | 199, 200 | eqtrd 2486 |
. . . . . . . . . . . 12
 
    ![[,] [,]](_icc.gif) 
          |
202 | 196, 201 | breqtrd 4399 |
. . . . . . . . . . 11
 
    ![[,] [,]](_icc.gif) 
     
  |
203 | 181, 182,
185, 193, 202 | eliccd 37642 |
. . . . . . . . . 10
 
    ![[,] [,]](_icc.gif) 
        ![[,] [,]](_icc.gif)    |
204 | 180, 203 | jca 539 |
. . . . . . . . 9
 
    ![[,] [,]](_icc.gif) 
         ![[,] [,]](_icc.gif)     |
205 | | eleq1 2518 |
. . . . . . . . . . . 12
       ![[,] [,]](_icc.gif) 
     ![[,] [,]](_icc.gif)     |
206 | 205 | anbi2d 715 |
. . . . . . . . . . 11
     
  ![[,] [,]](_icc.gif)  
      ![[,] [,]](_icc.gif)      |
207 | | oveq1 6283 |
. . . . . . . . . . . . 13
             |
208 | 207 | fveq2d 5852 |
. . . . . . . . . . . 12
                     |
209 | | fveq2 5848 |
. . . . . . . . . . . 12
           
     |
210 | 208, 209 | eqeq12d 2467 |
. . . . . . . . . . 11
              
                   |
211 | 206, 210 | imbi12d 326 |
. . . . . . . . . 10
      
  ![[,] [,]](_icc.gif)                
    ![[,] [,]](_icc.gif)                       |
212 | | eleq1 2518 |
. . . . . . . . . . . . 13
    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     |
213 | 212 | anbi2d 715 |
. . . . . . . . . . . 12
  
  ![[,] [,]](_icc.gif)  
   ![[,] [,]](_icc.gif)      |
214 | | oveq1 6283 |
. . . . . . . . . . . . . 14
       |
215 | 214 | fveq2d 5852 |
. . . . . . . . . . . . 13
               |
216 | | fveq2 5848 |
. . . . . . . . . . . . 13
           |
217 | 215, 216 | eqeq12d 2467 |
. . . . . . . . . . . 12
           
             |
218 | 213, 217 | imbi12d 326 |
. . . . . . . . . . 11
   
  ![[,] [,]](_icc.gif)               
  ![[,] [,]](_icc.gif)                 |
219 | 218, 14 | chvarv 2108 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)  
            |
220 | 211, 219 | vtoclg 3075 |
. . . . . . . . 9
           ![[,] [,]](_icc.gif)                      |
221 | 179, 204,
220 | sylc 62 |
. . . . . . . 8
 
    ![[,] [,]](_icc.gif) 
                     |
222 | 176, 198 | negsubd 9979 |
. . . . . . . . . . 11
 
    ![[,] [,]](_icc.gif) 
          |
223 | 222 | oveq1d 6291 |
. . . . . . . . . 10
 
    ![[,] [,]](_icc.gif) 
              |
224 | 176, 198 | npcand 9977 |
. . . . . . . . . 10
 
    ![[,] [,]](_icc.gif) 
         |
225 | 223, 224 | eqtrd 2486 |
. . . . . . . . 9
 
    ![[,] [,]](_icc.gif) 
          |
226 | 225 | fveq2d 5852 |
. . . . . . . 8
 
    ![[,] [,]](_icc.gif) 
                  |
227 | 221, 226 | eqtr3d 2488 |
. . . . . . 7
 
    ![[,] [,]](_icc.gif) 
                |
228 | 227 | adantlr 726 |
. . . . . 6
    
 
  ![[,] [,]](_icc.gif)                  |
229 | | fveq2 5848 |
. . . . . . . 8
           |
230 | 229 | oveq1d 6291 |
. . . . . . 7
                 |
231 | 230 | cbvmptv 4467 |
. . . . . 6
                           |
232 | 19 | adantr 471 |
. . . . . 6
 
        |
233 | 19 | adantr 471 |
. . . . . . . . . 10
 
 ..^        |
234 | | ioossre 11686 |
. . . . . . . . . . 11
               |
235 | 234 | a1i 11 |
. . . . . . . . . 10
 
 ..^                  |
236 | 233, 235 | feqresmpt 5902 |
. . . . . . . . 9
 
 ..^                                        |
237 | 153, 160 | oveq12d 6294 |
. . . . . . . . . . 11
 
 ..^                                    |
238 | 143, 146,
147 | iooshift 37664 |
. . . . . . . . . . 11
 
 ..^                     
                    |
239 | 237, 238 | eqtrd 2486 |
. . . . . . . . . 10
 
 ..^                 
                    |
240 | 239 | mpteq1d 4456 |
. . . . . . . . 9
 
 ..^                        
                         |
241 | | simpll 765 |
. . . . . . . . . . . . 13
    ..^                      
  |
242 | | simplr 767 |
. . . . . . . . . . . . 13
    ..^                      
 ..^   |
243 | 238 | eleq2d 2515 |
. . . . . . . . . . . . . 14
 
 ..^                    
                       |
244 | 243 | biimpar 492 |
. . . . . . . . . . . . 13
    ..^                      
                    |
245 | 143 | rexrd 9677 |
. . . . . . . . . . . . . . 15
 
 ..^        |
246 | 245 | 3adant3 1029 |
. . . . . . . . . . . . . 14
 
 ..^
                         |
247 | 146 | rexrd 9677 |
. . . . . . . . . . . . . . 15
 
 ..^          |
248 | 247 | 3adant3 1029 |
. . . . . . . . . . . . . 14
 
 ..^
                           |
249 | | elioore 11656 |
. . . . . . . . . . . . . . . . 17
                     |
250 | 249 | adantl 472 |
. . . . . . . . . . . . . . . 16
 
                     |
251 | 8 | adantr 471 |
. . . . . . . . . . . . . . . 16
 
                     |
252 | 250, 251 | resubcld 10036 |
. . . . . . . . . . . . . . 15
 
                       |
253 | 252 | 3adant2 1028 |
. . . . . . . . . . . . . 14
 
 ..^
                       |
254 | 143 | recnd 9656 |
. . . . . . . . . . . . . . . . . 18
 
 ..^        |
255 | 62 | adantr 471 |
. . . . . . . . . . . . . . . . . 18
 
 ..^    |
256 | 254, 255 | pncand 9974 |
. . . . . . . . . . . . . . . . 17
 
 ..^                |
257 | 256 | eqcomd 2458 |
. . . . . . . . . . . . . . . 16
 
 ..^                |
258 | 257 | 3adant3 1029 |
. . . . . . . . . . . . . . 15
 
 ..^
                                 |
259 | 151 | 3adant3 1029 |
. . . . . . . . . . . . . . . 16
 
 ..^
                           |
260 | 250 | 3adant2 1028 |
. . . . . . . . . . . . . . . 16
 
 ..^
                     |
261 | 8 | 3ad2ant1 1030 |
. . . . . . . . . . . . . . . 16
 
 ..^
                     |
262 | 151 | rexrd 9677 |
. . . . . . . . . . . . . . . . . 18
 
 ..^          |
263 | 262 | 3adant3 1029 |
. . . . . . . . . . . . . . . . 17
 
 ..^
                           |
264 | 159 | rexrd 9677 |
. . . . . . . . . . . . . . . . . 18
 
 ..^            |
265 | 264 | 3adant3 1029 |
. . . . . . . . . . . . . . . . 17
 
 ..^
                             |
266 | | simp3 1011 |
. . . . . . . . . . . . . . . . 17
 
 ..^
                                       |
267 | | ioogtlb 37633 |
. . . . . . . . . . . . . . . . 17
               
                           |
268 | 263, 265,
266, 267 | syl3anc 1271 |
. . . . . . . . . . . . . . . 16
 
 ..^
                           |
269 | 259, 260,
261, 268 | ltsub1dd 10214 |
. . . . . . . . . . . . . . 15
 
 ..^
                               |
270 | 258, 269 | eqbrtrd 4395 |
. . . . . . . . . . . . . 14
 
 ..^
                           |
271 | 159 | 3adant3 1029 |
. . . . . . . . . . . . . . . 16
 
 ..^
                             |
272 | | iooltub 37651 |
. . . . . . . . . . . . . . . . 17
               
                             |
273 | 263, 265,
266, 272 | syl3anc 1271 |
. . . . . . . . . . . . . . . 16
 
 ..^
                             |
274 | 260, 271,
261, 273 | ltsub1dd 10214 |
. . . . . . . . . . . . . . 15
 
 ..^
                                 |
275 | 146 | recnd 9656 |
. . . . . . . . . . . . . . . . 17
 
 ..^          |
276 | 275, 255 | pncand 9974 |
. . . . . . . . . . . . . . . 16
 
 ..^                    |
277 | 276 | 3adant3 1029 |
. . . . . . . . . . . . . . 15
 
 ..^
                                     |
278 | 274, 277 | breqtrd 4399 |
. . . . . . . . . . . . . 14
 
 ..^
                             |
279 | 246, 248,
253, 270, 278 | eliood 37636 |
. . . . . . . . . . . . 13
 
 ..^
                                     |
280 | 241, 242,
244, 279 | syl3anc 1271 |
. . . . . . . . . . . 12
    ..^                      
                  |
281 | | fvres 5862 |
. . . . . . . . . . . 12
                                          
    |
282 | 280, 281 | syl 17 |
. . . . . . . . . . 11
    ..^                      
                   
          |
283 | 241, 244,
252 | syl2anc 671 |
. . . . . . . . . . . 12
    ..^                      
    |
284 | 1 | 3ad2ant1 1030 |
. . . . . . . . . . . . . . 15
 
 ..^
                     |
285 | 3 | 3ad2ant1 1030 |
. . . . . . . . . . . . . . 15
 
 ..^
                     |
286 | 64 | eqcomd 2458 |
. . . . . . . . . . . . . . . . . 18
       |
287 | 286 | 3ad2ant1 1030 |
. . . . . . . . . . . . . . . . 17
 
 ..^
                         |
288 | 60 | 3ad2ant1 1030 |
. . . . . . . . . . . . . . . . . 18
 
 ..^
                       |
289 | 1 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . 21
 
 ..^    |
290 | 1 | rexrd 9677 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
291 | 290 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . 22
 
 ..^    |
292 | 3 | rexrd 9677 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
293 | 292 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . 22
 
 ..^    |
294 | 5, 6, 12 | fourierdlem15 38041 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           ![[,] [,]](_icc.gif)    |
295 | 294 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
 ..^            ![[,] [,]](_icc.gif)    |
296 | 295, 142 | ffvelrnd 6007 |
. . . . . . . . . . . . . . . . . . . . . 22
 
 ..^        ![[,] [,]](_icc.gif)    |
297 | | iccgelb 11681 |
. . . . . . . . . . . . . . . . . . . . . 22
        ![[,] [,]](_icc.gif)         |
298 | 291, 293,
296, 297 | syl3anc 1271 |
. . . . . . . . . . . . . . . . . . . . 21
 
 ..^        |
299 | 289, 143,
147, 298 | leadd1dd 10216 |
. . . . . . . . . . . . . . . . . . . 20
 
 ..^            |
300 | 299 | 3adant3 1029 |
. . . . . . . . . . . . . . . . . . 19
 
 ..^
                             |
301 | 288, 259,
260, 300, 268 | lelttrd 9780 |
. . . . . . . . . . . . . . . . . 18
 
 ..^
                       |
302 | 288, 260,
261, 301 | ltsub1dd 10214 |
. . . . . . . . . . . . . . . . 17
 
 ..^
                           |
303 | 287, 302 | eqbrtrd 4395 |
. . . . . . . . . . . . . . . 16
 
 ..^
                       |
304 | 284, 253,
303 | ltled 9770 |
. . . . . . . . . . . . . . 15
 
 ..^
                       |
305 | 146 | 3adant3 1029 |
. . . . . . . . . . . . . . . . 17
 
 ..^
                           |
306 | 295, 145 | ffvelrnd 6007 |
. . . . . . . . . . . . . . . . . . 19
 
 ..^          ![[,] [,]](_icc.gif)    |
307 | | iccleub 11680 |
. . . . . . . . . . . . . . . . . . 19
          ![[,] [,]](_icc.gif)           |
308 | 291, 293,
306, 307 | syl3anc 1271 |
. . . . . . . . . . . . . . . . . 18
 
 ..^          |
309 | 308 | 3adant3 1029 |
. . . . . . . . . . . . . . . . 17
 
 ..^
                           |
310 | 253, 305,
285, 278, 309 | ltletrd 9782 |
. . . . . . . . . . . . . . . 16
 
 ..^
                       |
311 | 253, 285,
310 | ltled 9770 |
. . . . . . . . . . . . . . 15
 
 ..^
                       |
312 | 284, 285,
253, 304, 311 | eliccd 37642 |
. . . . . . . . . . . . . 14
 
 ..^
                       ![[,] [,]](_icc.gif)    |
313 | 241, 242,
244, 312 | syl3anc 1271 |
. . . . . . . . . . . . 13
    ..^                      
    ![[,] [,]](_icc.gif)    |
314 | 241, 313 | jca 539 |
. . . . . . . . . . . 12
    ..^                      
     ![[,] [,]](_icc.gif)     |
315 | | eleq1 2518 |
. . . . . . . . . . . . . . 15
      ![[,] [,]](_icc.gif) 
    ![[,] [,]](_icc.gif)     |
316 | 315 | anbi2d 715 |
. . . . . . . . . . . . . 14
    
  ![[,] [,]](_icc.gif)  
     ![[,] [,]](_icc.gif)      |
317 | | oveq1 6283 |
. . . . . . . . . . . . . . . 16
           |
318 | 317 | fveq2d 5852 |
. . . . . . . . . . . . . . 15
                   |
319 | | fveq2 5848 |
. . . . . . . . . . . . . . 15
          
    |
320 | 318, 319 | eqeq12d 2467 |
. . . . . . . . . . . . . 14
             
                 |
321 | 316, 320 | imbi12d 326 |
. . . . . . . . . . . . 13
     
  ![[,] [,]](_icc.gif)                
   ![[,] [,]](_icc.gif)                     |
322 | 321, 219 | vtoclg 3075 |
. . . . . . . . . . . 12
    
    ![[,] [,]](_icc.gif)                    |
323 | 283, 314,
322 | sylc 62 |
. . . . . . . . . . 11
    ..^                      
                |
324 | 244, 249 | syl 17 |
. . . . . . . . . . . 12
    ..^                      
  |
325 | | recn 9616 |
. . . . . . . . . . . . . . 15
   |
326 | 325 | adantl 472 |
. . . . . . . . . . . . . 14
 

  |
327 | 62 | adantr 471 |
. . . . . . . . . . . . . 14
 

  |
328 | 326, 327 | npcand 9977 |
. . . . . . . . . . . . 13
 

      |
329 | 328 | fveq2d 5852 |
. . . . . . . . . . . 12
 

              |
330 | 241, 324,
329 | syl2anc 671 |
. . . . . . . . . . 11
    ..^                      
              |
331 | 282, 323,
330 | 3eqtr2rd 2493 |
. . . . . . . . . 10
    ..^                      
                            |
332 | 331 | mpteq2dva 4461 |
. . . . . . . . 9
 
 ..^                                                                          |
333 | 236, 240,
332 | 3eqtrd 2490 |
. . . . . . . 8
 
 ..^                                                                |
334 | | ioosscn 37632 |
. . . . . . . . . . 11
               |
335 | 334 | a1i 11 |
. . . . . . . . . 10
 
 ..^                  |
336 | | eqeq1 2456 |
. . . . . . . . . . . . 13
   
     |
337 | 336 | rexbidv 2873 |
. . . . . . . . . . . 12
  
                
                     |
338 | | oveq1 6283 |
. . . . . . . . . . . . . 14
       |
339 | 338 | eqeq2d 2462 |
. . . . . . . . . . . . 13
   
     |
340 | 339 | cbvrexv 2988 |
. . . . . . . . . . . 12
                  
                    |
341 | 337, 340 | syl6bb 269 |
. . . . . . . . . . 11
  
                
                     |
342 | 341 | cbvrabv 3012 |
. . . . . . . . . 10
                                         |
343 | | eqid 2452 |
. . . . . . . . . 10
                                                                                         |
344 | 335, 255,
342, 21, 343 | cncfshift 37793 |
. . . . . . . . 9
 
 ..^                                                                        |
345 | 239 | eqcomd 2458 |
. . . . . . . . . 10
 
 ..^                                      |
346 | 345 | oveq1d 6291 |
. . . . . . . . 9
 
 ..^                                              |
347 | 344, 346 | eleqtrd 2532 |
. . . . . . . 8
 
 ..^                                                                  |
348 | 333, 347 | eqeltrd 2530 |
. . . . . . 7
 
 ..^                                      |
349 | 348 | adantlr 726 |
. . . . . 6
    
 ..^                                      |
350 | | ffdm 5726 |
. . . . . . . . . . . 12
             |
351 | 19, 350 | syl 17 |
. . . . . . . . . . 11
         |
352 | 351 | simpld 465 |
. . . . . . . . . 10
       |
353 | 352 | adantr 471 |
. . . . . . . . 9
 
 ..^        |
354 | | ioossre 11686 |
. . . . . . . . . 10
               |
355 | | fdm 5716 |
. . . . . . . . . . 11
       |
356 | 233, 355 | syl 17 |
. . . . . . . . . 10
 
 ..^ 
  |
357 | 354, 356 | syl5sseqr 3449 |
. . . . . . . . 9
 
 ..^                  |
358 | 342 | eqcomi 2461 |
. . . . . . . . 9
                                         |
359 | 235, 345,
356 | 3sstr4d 3443 |
. . . . . . . . . 10
 
 ..^                     
  |
360 | 342, 359 | syl5eqssr 3445 |
. . . . . . . . 9
 
 ..^                     
  |
361 | | simpll 765 |
. . . . . . . . . 10
    ..^                   |
362 | 361, 290 | syl 17 |
. . . . . . . . . . 11
    ..^                   |
363 | 361, 292 | syl 17 |
. . . . . . . . . . 11
    ..^                   |
364 | 361, 294 | syl 17 |
. . . . . . . . . . 11
    ..^                           ![[,] [,]](_icc.gif)    |
365 | | simplr 767 |
. . . . . . . . . . 11
    ..^                  ..^   |
366 | | ioossicc 11710 |
. . . . . . . . . . . . 13
                    ![[,] [,]](_icc.gif)         |
367 | 366 | sseli 3396 |
. . . . . . . . . . . 12
                     ![[,] [,]](_icc.gif)          |
368 | 367 | adantl 472 |
. . . . . . . . . . 11
    ..^                       ![[,] [,]](_icc.gif)          |
369 | 362, 363,
364, 365, 368 | fourierdlem1 38027 |
. . . . . . . . . 10
    ..^                   ![[,] [,]](_icc.gif)    |
370 | | eleq1 2518 |
. . . . . . . . . . . . 13
    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)     |
371 | 370 | anbi2d 715 |
. . . . . . . . . . . 12
  
  ![[,] [,]](_icc.gif)  
   ![[,] [,]](_icc.gif)      |
372 | | oveq1 6283 |
. . . . . . . . . . . . . 14
       |
373 | 372 | fveq2d 5852 |
. . . . . . . . . . . . 13
               |
374 | | fveq2 5848 |
. . . . . . . . . . . . 13
           |
375 | 373, 374 | eqeq12d 2467 |
. . . . . . . . . . . 12
           
             |
376 | 371, 375 | imbi12d 326 |
. . . . . . . . . . 11
   
  ![[,] [,]](_icc.gif)               
  ![[,] [,]](_icc.gif)                 |
377 | 376, 14 | chvarv 2108 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)  
            |
378 | 361, 369,
377 | syl2anc 671 |
. . . . . . . . 9
    ..^                             |
379 | 353, 335,
357, 255, 358, 360, 378, 23 | limcperiod 37750 |
. . . . . . . 8
 
 ..^                         lim          |
380 | 358, 345 | syl5eq 2498 |
. . . . . . . . . 10
 
 ..^                                      |
381 | 380 | reseq2d 5083 |
. . . . . . . . 9
 
 ..^   
                                      |
382 | 153 | eqcomd 2458 |
. . . . . . . . 9
 
 ..^              |
383 | 381, 382 | oveq12d 6294 |
. . . . . . . 8
 
 ..^                         lim                         lim        |
384 | 379, 383 | eleqtrd 2532 |
. . . . . . 7
 
 ..^                   lim        |
385 | 384 | adantlr 726 |
. . . . . 6
    
 ..^ 
                 lim        |
386 | 353, 335,
357, 255, 358, 360, 378, 25 | limcperiod 37750 |
. . . . . . . 8
 
 ..^                         lim            |
387 | 160 | eqcomd 2458 |
. . . . . . . . 9
 
 ..^                  |
388 | 381, 387 | oveq12d 6294 |
. . . . . . . 8
 
 ..^                         lim                           lim          |
389 | 386, 388 | eleqtrd 2532 |
. . . . . . 7
 
 ..^                   lim          |
390 | 389 | adantlr 726 |
. . . . . 6
    
 ..^ 
                 lim          |
391 | | eqeq1 2456 |
. . . . . . . 8
     
       |
392 | | eqeq1 2456 |
. . . . . . . . 9
       
         |
393 | 392, 29 | ifbieq2d 3874 |
. . . . . . . 8
                                 |
394 | 391, 393 | ifbieq2d 3874 |
. . . . . . 7
                                  
                |
395 | 394 | cbvmptv 4467 |
. . . . . 6
       ![[,] [,]](_icc.gif)                                        ![[,] [,]](_icc.gif)                 
                |
396 | | eqid 2452 |
. . . . . 6
                    ![[,] [,]](_icc.gif)                             ![[,] [,]](_icc.gif)                                   
                        ![[,] [,]](_icc.gif)                             ![[,] [,]](_icc.gif)                                         |
397 | 77, 79, 80, 81, 84, 170, 228, 231, 232, 349, 385, 390, 395, 396 | fourierdlem81 38108 |
. . . . 5
 
          ![[,] [,]](_icc.gif)                  ![[,] [,]](_icc.gif) 
          |
398 | 74, 397 | eqtr2d 2487 |
. . . 4
 
       ![[,] [,]](_icc.gif) 
           ![[,] [,]](_icc.gif)          |
399 | 49, 59, 398 | syl2anc 671 |
. . 3
   

     ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)          |
400 | 48, 399 | pm2.61dan 805 |
. 2
 
      ![[,] [,]](_icc.gif) 
           ![[,] [,]](_icc.gif)          |
401 | 34, 400 | pm2.61dan 805 |
1
      ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)          |