Proof of Theorem fourierdlem114
Step | Hyp | Ref
| Expression |
1 | | fourierdlem114.f |
. 2
       |
2 | | fourierdlem114.t |
. 2
   |
3 | | fourierdlem114.per |
. 2
 

            |
4 | | fourierdlem114.x |
. 2
   |
5 | | fourierdlem114.l |
. 2
  
    lim    |
6 | | fourierdlem114.r |
. 2
  
    lim    |
7 | | fourierdlem114.p |
. 2
 
                  
 ..^                |
8 | | fourierdlem114.m |
. . 3
       |
9 | | 2z 10997 |
. . . . . 6
 |
10 | 9 | a1i 11 |
. . . . 5
   |
11 | | fourierdlem114.h |
. . . . . . . 8
              ![[,] [,]](_icc.gif)     |
12 | | tpfi 7872 |
. . . . . . . . . 10
  
       |
13 | 12 | a1i 11 |
. . . . . . . . 9
    
       |
14 | | pire 23461 |
. . . . . . . . . . . . . . 15
 |
15 | 14 | renegcli 9960 |
. . . . . . . . . . . . . 14
  |
16 | 15 | rexri 9718 |
. . . . . . . . . . . . 13
  |
17 | 14 | rexri 9718 |
. . . . . . . . . . . . 13
 |
18 | | negpilt0 37527 |
. . . . . . . . . . . . . . 15
  |
19 | | pipos 23463 |
. . . . . . . . . . . . . . 15
 |
20 | | 0re 9668 |
. . . . . . . . . . . . . . . 16
 |
21 | 15, 20, 14 | lttri 9785 |
. . . . . . . . . . . . . . 15
  
    |
22 | 18, 19, 21 | mp2an 683 |
. . . . . . . . . . . . . 14
  |
23 | 15, 14, 22 | ltleii 9782 |
. . . . . . . . . . . . 13
  |
24 | | prunioo 11789 |
. . . . . . . . . . . . 13
          
        ![[,] [,]](_icc.gif)    |
25 | 16, 17, 23, 24 | mp3an 1373 |
. . . . . . . . . . . 12
     
        ![[,] [,]](_icc.gif)   |
26 | 25 | difeq1i 3558 |
. . . . . . . . . . 11
      
  
 
     ![[,] [,]](_icc.gif)    |
27 | | difundir 3707 |
. . . . . . . . . . 11
      
  
 
            
    |
28 | 26, 27 | eqtr3i 2485 |
. . . . . . . . . 10
    ![[,] [,]](_icc.gif)              
    |
29 | | fourierdlem114.dmdv |
. . . . . . . . . . 11
          |
30 | | prfi 7871 |
. . . . . . . . . . . 12
  
  |
31 | | diffi 7828 |
. . . . . . . . . . . 12
    
        |
32 | 30, 31 | mp1i 13 |
. . . . . . . . . . 11
         |
33 | | unfi 7863 |
. . . . . . . . . . 11
                                 |
34 | 29, 32, 33 | syl2anc 671 |
. . . . . . . . . 10
                  |
35 | 28, 34 | syl5eqel 2543 |
. . . . . . . . 9
     ![[,] [,]](_icc.gif)     |
36 | | unfi 7863 |
. . . . . . . . 9
     
         ![[,] [,]](_icc.gif)       
          ![[,] [,]](_icc.gif)      |
37 | 13, 35, 36 | syl2anc 671 |
. . . . . . . 8
               ![[,] [,]](_icc.gif)      |
38 | 11, 37 | syl5eqel 2543 |
. . . . . . 7
   |
39 | | hashcl 12569 |
. . . . . . 7
       |
40 | 38, 39 | syl 17 |
. . . . . 6
       |
41 | 40 | nn0zd 11066 |
. . . . 5
       |
42 | 15, 22 | ltneii 9772 |
. . . . . . 7
  |
43 | | hashprg 12603 |
. . . . . . . 8
                 |
44 | 15, 14, 43 | mp2an 683 |
. . . . . . 7
 
          |
45 | 42, 44 | mpbi 213 |
. . . . . 6
         |
46 | 12 | elexi 3066 |
. . . . . . . . . 10
  
       |
47 | | ovex 6342 |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif)   |
48 | | difexg 4564 |
. . . . . . . . . . 11
    ![[,] [,]](_icc.gif) 
    ![[,] [,]](_icc.gif) 
   |
49 | 47, 48 | ax-mp 5 |
. . . . . . . . . 10
    ![[,] [,]](_icc.gif)    |
50 | 46, 49 | unex 6615 |
. . . . . . . . 9
              ![[,] [,]](_icc.gif)     |
51 | 11, 50 | eqeltri 2535 |
. . . . . . . 8
 |
52 | | negex 9898 |
. . . . . . . . . . 11
  |
53 | 52 | tpid1 4097 |
. . . . . . . . . 10
    
      |
54 | 14 | elexi 3066 |
. . . . . . . . . . 11
 |
55 | 54 | tpid2 4098 |
. . . . . . . . . 10
          |
56 | | prssi 4140 |
. . . . . . . . . 10
               
            
        |
57 | 53, 55, 56 | mp2an 683 |
. . . . . . . . 9
  
           |
58 | | ssun1 3608 |
. . . . . . . . . 10
  
                    ![[,] [,]](_icc.gif)     |
59 | 58, 11 | sseqtr4i 3476 |
. . . . . . . . 9
  
       |
60 | 57, 59 | sstri 3452 |
. . . . . . . 8
  
  |
61 | | hashss 12617 |
. . . . . . . 8
            
 
      |
62 | 51, 60, 61 | mp2an 683 |
. . . . . . 7
             |
63 | 62 | a1i 11 |
. . . . . 6
        
      |
64 | 45, 63 | syl5eqbrr 4450 |
. . . . 5

      |
65 | | eluz2 11193 |
. . . . 5
                     |
66 | 10, 41, 64, 65 | syl3anbrc 1198 |
. . . 4
           |
67 | | uz2m1nn 11261 |
. . . 4
                 |
68 | 66, 67 | syl 17 |
. . 3
         |
69 | 8, 68 | syl5eqel 2543 |
. 2
   |
70 | 15 | a1i 11 |
. . . . . . . . . . 11
    |
71 | 14 | a1i 11 |
. . . . . . . . . . 11
   |
72 | | negpitopissre 23537 |
. . . . . . . . . . . 12
   ![(,] (,]](_ioc.gif)   |
73 | 22 | a1i 11 |
. . . . . . . . . . . . . 14
    |
74 | | picn 23462 |
. . . . . . . . . . . . . . . 16
 |
75 | 74 | 2timesi 10758 |
. . . . . . . . . . . . . . 15
     |
76 | 74, 74 | subnegi 9978 |
. . . . . . . . . . . . . . 15
      |
77 | 75, 2, 76 | 3eqtr4i 2493 |
. . . . . . . . . . . . . 14
    |
78 | | fourierdlem114.e |
. . . . . . . . . . . . . 14
 
             |
79 | 70, 71, 73, 77, 78 | fourierdlem4 38010 |
. . . . . . . . . . . . 13
        ![(,] (,]](_ioc.gif)    |
80 | 79, 4 | ffvelrnd 6045 |
. . . . . . . . . . . 12
        ![(,] (,]](_ioc.gif)    |
81 | 72, 80 | sseldi 3441 |
. . . . . . . . . . 11
       |
82 | 70, 71, 81 | 3jca 1194 |
. . . . . . . . . 10
          |
83 | | fvex 5897 |
. . . . . . . . . . 11
     |
84 | 52, 54, 83 | tpss 4149 |
. . . . . . . . . 10
       
           |
85 | 82, 84 | sylib 201 |
. . . . . . . . 9
    
       |
86 | | iccssre 11744 |
. . . . . . . . . . 11
       ![[,] [,]](_icc.gif)    |
87 | 15, 14, 86 | mp2an 683 |
. . . . . . . . . 10
   ![[,] [,]](_icc.gif)   |
88 | | ssdifss 3575 |
. . . . . . . . . 10
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)     |
89 | 87, 88 | mp1i 13 |
. . . . . . . . 9
     ![[,] [,]](_icc.gif)  
  |
90 | 85, 89 | unssd 3621 |
. . . . . . . 8
               ![[,] [,]](_icc.gif)      |
91 | 11, 90 | syl5eqss 3487 |
. . . . . . 7

  |
92 | | fourierdlem114.q |
. . . . . . 7
            |
93 | 38, 91, 92, 8 | fourierdlem36 38043 |
. . . . . 6

         |
94 | | isof1o 6240 |
. . . . . 6
                  |
95 | | f1of 5836 |
. . . . . 6
        
          |
96 | 93, 94, 95 | 3syl 18 |
. . . . 5
           |
97 | 96, 91 | fssd 5760 |
. . . 4
           |
98 | | reex 9655 |
. . . . 5
 |
99 | | ovex 6342 |
. . . . 5
     |
100 | 98, 99 | elmap 7525 |
. . . 4
      
          |
101 | 97, 100 | sylibr 217 |
. . 3
         |
102 | | fveq2 5887 |
. . . . . . . . . . 11
           |
103 | 102 | adantl 472 |
. . . . . . . . . 10
                   |
104 | 97 | ffvelrnda 6044 |
. . . . . . . . . . . 12
 
           |
105 | 104 | leidd 10207 |
. . . . . . . . . . 11
 
               |
106 | 105 | adantr 471 |
. . . . . . . . . 10
            
      |
107 | 103, 106 | eqbrtrd 4436 |
. . . . . . . . 9
            
      |
108 | | elfzelz 11828 |
. . . . . . . . . . . . 13
       |
109 | 108 | zred 11068 |
. . . . . . . . . . . 12
       |
110 | 109 | ad2antlr 738 |
. . . . . . . . . . 11
       
   |
111 | | elfzle1 11830 |
. . . . . . . . . . . 12
       |
112 | 111 | ad2antlr 738 |
. . . . . . . . . . 11
       

  |
113 | | neqne 2642 |
. . . . . . . . . . . . 13
   |
114 | 113 | necomd 2690 |
. . . . . . . . . . . 12
   |
115 | 114 | adantl 472 |
. . . . . . . . . . 11
       
   |
116 | 110, 112,
115 | ne0gt0d 9797 |
. . . . . . . . . 10
       
   |
117 | | nnssnn0 10900 |
. . . . . . . . . . . . . . . . 17
 |
118 | | nn0uz 11221 |
. . . . . . . . . . . . . . . . 17
     |
119 | 117, 118 | sseqtri 3475 |
. . . . . . . . . . . . . . . 16
     |
120 | 119, 69 | sseldi 3441 |
. . . . . . . . . . . . . . 15
       |
121 | | eluzfz1 11834 |
. . . . . . . . . . . . . . 15
    
      |
122 | 120, 121 | syl 17 |
. . . . . . . . . . . . . 14
       |
123 | 96, 122 | ffvelrnd 6045 |
. . . . . . . . . . . . 13
       |
124 | 91, 123 | sseldd 3444 |
. . . . . . . . . . . 12
       |
125 | 124 | ad2antrr 737 |
. . . . . . . . . . 11
               |
126 | 104 | adantr 471 |
. . . . . . . . . . 11
               |
127 | | simpr 467 |
. . . . . . . . . . . 12
           |
128 | 93 | ad2antrr 737 |
. . . . . . . . . . . . 13
                  |
129 | 122 | anim1i 576 |
. . . . . . . . . . . . . 14
 
         
       |
130 | 129 | adantr 471 |
. . . . . . . . . . . . 13
             
       |
131 | | isorel 6241 |
. . . . . . . . . . . . 13
 
           
                  |
132 | 128, 130,
131 | syl2anc 671 |
. . . . . . . . . . . 12
         
           |
133 | 127, 132 | mpbid 215 |
. . . . . . . . . . 11
                   |
134 | 125, 126,
133 | ltled 9808 |
. . . . . . . . . 10
                   |
135 | 116, 134 | syldan 477 |
. . . . . . . . 9
       
    
      |
136 | 107, 135 | pm2.61dan 805 |
. . . . . . . 8
 
               |
137 | 136 | adantr 471 |
. . . . . . 7
                 
      |
138 | | simpr 467 |
. . . . . . 7
                     |
139 | 137, 138 | breqtrd 4440 |
. . . . . 6
                 
   |
140 | 70 | rexrd 9715 |
. . . . . . . 8
    |
141 | 71 | rexrd 9715 |
. . . . . . . 8
   |
142 | | lbicc2 11776 |
. . . . . . . . . . . . . 14
         ![[,] [,]](_icc.gif)    |
143 | 16, 17, 23, 142 | mp3an 1373 |
. . . . . . . . . . . . 13
    ![[,] [,]](_icc.gif)   |
144 | 143 | a1i 11 |
. . . . . . . . . . . 12
     ![[,] [,]](_icc.gif)    |
145 | | ubicc2 11777 |
. . . . . . . . . . . . . 14
        ![[,] [,]](_icc.gif)    |
146 | 16, 17, 23, 145 | mp3an 1373 |
. . . . . . . . . . . . 13
   ![[,] [,]](_icc.gif)   |
147 | 146 | a1i 11 |
. . . . . . . . . . . 12
    ![[,] [,]](_icc.gif)    |
148 | | iocssicc 11750 |
. . . . . . . . . . . . 13
   ![(,] (,]](_ioc.gif)     ![[,] [,]](_icc.gif)   |
149 | 148, 80 | sseldi 3441 |
. . . . . . . . . . . 12
        ![[,] [,]](_icc.gif)    |
150 | | tpssi 4150 |
. . . . . . . . . . . 12
      ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)     
         ![[,] [,]](_icc.gif)    |
151 | 144, 147,
149, 150 | syl3anc 1276 |
. . . . . . . . . . 11
    
        ![[,] [,]](_icc.gif)    |
152 | | difssd 3572 |
. . . . . . . . . . 11
     ![[,] [,]](_icc.gif)  
   ![[,] [,]](_icc.gif)    |
153 | 151, 152 | unssd 3621 |
. . . . . . . . . 10
               ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)    |
154 | 11, 153 | syl5eqss 3487 |
. . . . . . . . 9

   ![[,] [,]](_icc.gif)    |
155 | 154, 123 | sseldd 3444 |
. . . . . . . 8
        ![[,] [,]](_icc.gif)    |
156 | | iccgelb 11719 |
. . . . . . . 8
          ![[,] [,]](_icc.gif)          |
157 | 140, 141,
155, 156 | syl3anc 1276 |
. . . . . . 7
        |
158 | 157 | ad2antrr 737 |
. . . . . 6
              
      |
159 | 124 | ad2antrr 737 |
. . . . . . 7
                    |
160 | 15 | a1i 11 |
. . . . . . 7
                 |
161 | 159, 160 | letri3d 9802 |
. . . . . 6
                          
        |
162 | 139, 158,
161 | mpbir2and 938 |
. . . . 5
                     |
163 | 59, 53 | sselii 3440 |
. . . . . . 7
  |
164 | | f1ofo 5843 |
. . . . . . . . 9
        
          |
165 | 94, 164 | syl 17 |
. . . . . . . 8
                  |
166 | | forn 5818 |
. . . . . . . 8
           |
167 | 93, 165, 166 | 3syl 18 |
. . . . . . 7
   |
168 | 163, 167 | syl5eleqr 2546 |
. . . . . 6
    |
169 | | ffn 5750 |
. . . . . . 7
        
      |
170 | | fvelrnb 5934 |
. . . . . . 7
                     |
171 | 96, 169, 170 | 3syl 18 |
. . . . . 6
                 |
172 | 168, 171 | mpbid 215 |
. . . . 5
              |
173 | 162, 172 | r19.29a 2943 |
. . . 4
        |
174 | 59, 55 | sselii 3440 |
. . . . . . 7
 |
175 | 174, 167 | syl5eleqr 2546 |
. . . . . 6
   |
176 | | fvelrnb 5934 |
. . . . . . 7
                   |
177 | 96, 169, 176 | 3syl 18 |
. . . . . 6
  
            |
178 | 175, 177 | mpbid 215 |
. . . . 5
             |
179 | 96, 154 | fssd 5760 |
. . . . . . . . . 10
            ![[,] [,]](_icc.gif)    |
180 | | eluzfz2 11835 |
. . . . . . . . . . 11
    
      |
181 | 120, 180 | syl 17 |
. . . . . . . . . 10
       |
182 | 179, 181 | ffvelrnd 6045 |
. . . . . . . . 9
        ![[,] [,]](_icc.gif)    |
183 | | iccleub 11718 |
. . . . . . . . 9
          ![[,] [,]](_icc.gif)         |
184 | 140, 141,
182, 183 | syl3anc 1276 |
. . . . . . . 8
    
  |
185 | 184 | 3ad2ant1 1035 |
. . . . . . 7
 
   
    
      |
186 | | id 22 |
. . . . . . . . . 10
           |
187 | 186 | eqcomd 2467 |
. . . . . . . . 9
           |
188 | 187 | 3ad2ant3 1037 |
. . . . . . . 8
 
   
    
      |
189 | 105 | adantr 471 |
. . . . . . . . . . 11
                   |
190 | | fveq2 5887 |
. . . . . . . . . . . 12
           |
191 | 190 | adantl 472 |
. . . . . . . . . . 11
                   |
192 | 189, 191 | breqtrd 4440 |
. . . . . . . . . 10
                   |
193 | 109 | ad2antlr 738 |
. . . . . . . . . . . 12
       
   |
194 | | elfzel2 11826 |
. . . . . . . . . . . . . 14
       |
195 | 194 | zred 11068 |
. . . . . . . . . . . . 13
       |
196 | 195 | ad2antlr 738 |
. . . . . . . . . . . 12
       
   |
197 | | elfzle2 11831 |
. . . . . . . . . . . . 13
       |
198 | 197 | ad2antlr 738 |
. . . . . . . . . . . 12
       

  |
199 | | neqne 2642 |
. . . . . . . . . . . . . 14
   |
200 | 199 | necomd 2690 |
. . . . . . . . . . . . 13
   |
201 | 200 | adantl 472 |
. . . . . . . . . . . 12
       
   |
202 | 193, 196,
198, 201 | leneltd 9814 |
. . . . . . . . . . 11
       
   |
203 | 104 | adantr 471 |
. . . . . . . . . . . 12
               |
204 | 87, 182 | sseldi 3441 |
. . . . . . . . . . . . 13
       |
205 | 204 | ad2antrr 737 |
. . . . . . . . . . . 12
               |
206 | | simpr 467 |
. . . . . . . . . . . . 13
           |
207 | 93 | ad2antrr 737 |
. . . . . . . . . . . . . 14
                  |
208 | | simpr 467 |
. . . . . . . . . . . . . . . 16
 
           |
209 | 181 | adantr 471 |
. . . . . . . . . . . . . . . 16
 
           |
210 | 208, 209 | jca 539 |
. . . . . . . . . . . . . . 15
 
         
       |
211 | 210 | adantr 471 |
. . . . . . . . . . . . . 14
             
       |
212 | | isorel 6241 |
. . . . . . . . . . . . . 14
 
           
                  |
213 | 207, 211,
212 | syl2anc 671 |
. . . . . . . . . . . . 13
         
           |
214 | 206, 213 | mpbid 215 |
. . . . . . . . . . . 12
                   |
215 | 203, 205,
214 | ltled 9808 |
. . . . . . . . . . 11
                   |
216 | 202, 215 | syldan 477 |
. . . . . . . . . 10
       
    
      |
217 | 192, 216 | pm2.61dan 805 |
. . . . . . . . 9
 
               |
218 | 217 | 3adant3 1034 |
. . . . . . . 8
 
   
    
          |
219 | 188, 218 | eqbrtrd 4436 |
. . . . . . 7
 
   
    
      |
220 | 204 | 3ad2ant1 1035 |
. . . . . . . 8
 
   
    
      |
221 | 14 | a1i 11 |
. . . . . . . 8
 
   
    
  |
222 | 220, 221 | letri3d 9802 |
. . . . . . 7
 
   
    
    
             |
223 | 185, 219,
222 | mpbir2and 938 |
. . . . . 6
 
   
    
      |
224 | 223 | rexlimdv3a 2892 |
. . . . 5
                   |
225 | 178, 224 | mpd 15 |
. . . 4
       |
226 | | elfzoelz 11950 |
. . . . . . . . 9
  ..^
  |
227 | 226 | zred 11068 |
. . . . . . . 8
  ..^
  |
228 | 227 | ltp1d 10564 |
. . . . . . 7
  ..^
    |
229 | 228 | adantl 472 |
. . . . . 6
 
 ..^      |
230 | | elfzofz 11965 |
. . . . . . . 8
  ..^
      |
231 | | fzofzp1 12038 |
. . . . . . . 8
  ..^
        |
232 | 230, 231 | jca 539 |
. . . . . . 7
  ..^
    
         |
233 | | isorel 6241 |
. . . . . . 7
 
           
              
         |
234 | 93, 232, 233 | syl2an 484 |
. . . . . 6
 
 ..^                  |
235 | 229, 234 | mpbid 215 |
. . . . 5
 
 ..^              |
236 | 235 | ralrimiva 2813 |
. . . 4
   ..^              |
237 | 173, 225,
236 | jca31 541 |
. . 3
             
 ..^               |
238 | 7 | fourierdlem2 38008 |
. . . 4
 
   
                   
 ..^                 |
239 | 69, 238 | syl 17 |
. . 3
                         
 ..^                 |
240 | 101, 237,
239 | mpbir2and 938 |
. 2
       |
241 | | fourierdlem114.g |
. . . . 5
          |
242 | 241 | reseq1i 5119 |
. . . 4
                         
                |
243 | 16 | a1i 11 |
. . . . . 6
 
 ..^     |
244 | 17 | a1i 11 |
. . . . . 6
 
 ..^    |
245 | 179 | adantr 471 |
. . . . . 6
 
 ..^             ![[,] [,]](_icc.gif)    |
246 | | simpr 467 |
. . . . . 6
 
 ..^   ..^   |
247 | 243, 244,
245, 246 | fourierdlem27 38033 |
. . . . 5
 
 ..^                       |
248 | 247 | resabs1d 5152 |
. . . 4
 
 ..^                                               |
249 | 242, 248 | syl5req 2508 |
. . 3
 
 ..^                    
                 |
250 | | fourierdlem114.gcn |
. . . 4
       |
251 | 250, 7, 69, 240, 11, 167 | fourierdlem38 38045 |
. . 3
 
 ..^                                      |
252 | 249, 251 | eqeltrd 2539 |
. 2
 
 ..^                                        |
253 | 249 | oveq1d 6329 |
. . 3
 
 ..^                     lim       
               lim        |
254 | 250 | adantr 471 |
. . . . 5
 
 ..^        |
255 | | fourierdlem114.rlim |
. . . . . 6
 
           
  lim
   |
256 | 255 | adantlr 726 |
. . . . 5
    ..^             
  lim
   |
257 | | fourierdlem114.llim |
. . . . . 6
 
    ![(,] (,]](_ioc.gif)          lim    |
258 | 257 | adantlr 726 |
. . . . 5
    ..^      ![(,] (,]](_ioc.gif)          lim    |
259 | 93 | adantr 471 |
. . . . 5
 
 ..^           |
260 | 259, 94, 95 | 3syl 18 |
. . . . 5
 
 ..^            |
261 | 81 | adantr 471 |
. . . . 5
 
 ..^        |
262 | 259, 165,
166 | 3syl 18 |
. . . . 5
 
 ..^ 
  |
263 | 254, 256,
258, 259, 260, 246, 235, 247, 261, 11, 262 | fourierdlem46 38053 |
. . . 4
 
 ..^    
               lim                       lim           |
264 | 263 | simpld 465 |
. . 3
 
 ..^                   lim        |
265 | 253, 264 | eqnetrd 2702 |
. 2
 
 ..^                     lim        |
266 | 249 | oveq1d 6329 |
. . 3
 
 ..^                     lim         
               lim          |
267 | 263 | simprd 469 |
. . 3
 
 ..^                   lim          |
268 | 266, 267 | eqnetrd 2702 |
. 2
 
 ..^                     lim          |
269 | | fourierdlem114.a |
. 2
                         |
270 | | fourierdlem114.b |
. 2
                         |
271 | | fourierdlem114.s |
. 2
                             |
272 | 83 | tpid3 4100 |
. . . . 5
              |
273 | | elun1 3612 |
. . . . 5
                      
         ![[,] [,]](_icc.gif)      |
274 | 272, 273 | mp1i 13 |
. . . 4
                   ![[,] [,]](_icc.gif)      |
275 | 274, 11 | syl6eleqr 2550 |
. . 3
       |
276 | 275, 167 | eleqtrrd 2542 |
. 2
       |
277 | 1, 2, 3, 4, 5, 6, 7, 69, 240, 252, 265, 268, 269, 270, 271, 78, 276 | fourierdlem113 38120 |
1
                                                          |