Step | Hyp | Ref
| Expression |
1 | | fourierdlem54.n |
. . 3
       |
2 | | 2z 10966 |
. . . . . 6
 |
3 | 2 | a1i 11 |
. . . . 5
   |
4 | | fourierdlem54.c |
. . . . . . . . . 10
   |
5 | | prid1g 4077 |
. . . . . . . . . 10
      |
6 | | elun1 3600 |
. . . . . . . . . 10
   
   
   ![[,] [,]](_icc.gif)           |
7 | 4, 5, 6 | 3syl 18 |
. . . . . . . . 9
        ![[,] [,]](_icc.gif)           |
8 | | fourierdlem54.h |
. . . . . . . . 9
   
   ![[,] [,]](_icc.gif)          |
9 | 7, 8 | syl6eleqr 2539 |
. . . . . . . 8
   |
10 | | ne0i 3736 |
. . . . . . . 8
   |
11 | 9, 10 | syl 17 |
. . . . . . 7
   |
12 | | prfi 7843 |
. . . . . . . . . 10
    |
13 | | fourierdlem54.p |
. . . . . . . . . . . . 13
 
                 
 ..^                |
14 | | fourierdlem54.m |
. . . . . . . . . . . . 13
   |
15 | | fourierdlem54.q |
. . . . . . . . . . . . 13
       |
16 | 13, 14, 15 | fourierdlem11 37974 |
. . . . . . . . . . . 12
     |
17 | 16 | simp1d 1019 |
. . . . . . . . . . 11
   |
18 | 16 | simp2d 1020 |
. . . . . . . . . . 11
   |
19 | 16 | simp3d 1021 |
. . . . . . . . . . 11
   |
20 | | fourierdlem54.t |
. . . . . . . . . . 11
   |
21 | 13, 14, 15 | fourierdlem15 37978 |
. . . . . . . . . . . 12
           ![[,] [,]](_icc.gif)    |
22 | | frn 5733 |
. . . . . . . . . . . 12
           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)    |
23 | 21, 22 | syl 17 |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif)    |
24 | 13 | fourierdlem2 37965 |
. . . . . . . . . . . . . . . . 17
 
   
                  
 ..^                 |
25 | 14, 24 | syl 17 |
. . . . . . . . . . . . . . . 16
                        
 ..^                 |
26 | 15, 25 | mpbid 214 |
. . . . . . . . . . . . . . 15
                   
 ..^                |
27 | 26 | simpld 461 |
. . . . . . . . . . . . . 14
         |
28 | | elmapi 7490 |
. . . . . . . . . . . . . 14
                 |
29 | | ffn 5726 |
. . . . . . . . . . . . . 14
               |
30 | 27, 28, 29 | 3syl 18 |
. . . . . . . . . . . . 13
       |
31 | | fzfid 12183 |
. . . . . . . . . . . . 13
       |
32 | | fnfi 7846 |
. . . . . . . . . . . . 13
             |
33 | 30, 31, 32 | syl2anc 666 |
. . . . . . . . . . . 12
   |
34 | | rnfi 7854 |
. . . . . . . . . . . 12
   |
35 | 33, 34 | syl 17 |
. . . . . . . . . . 11
   |
36 | 26 | simprd 465 |
. . . . . . . . . . . . . 14
            
 ..^               |
37 | 36 | simpld 461 |
. . . . . . . . . . . . 13
             |
38 | 37 | simpld 461 |
. . . . . . . . . . . 12
       |
39 | 14 | nnnn0d 10922 |
. . . . . . . . . . . . . . 15
   |
40 | | nn0uz 11190 |
. . . . . . . . . . . . . . 15
     |
41 | 39, 40 | syl6eleq 2538 |
. . . . . . . . . . . . . 14
       |
42 | | eluzfz1 11803 |
. . . . . . . . . . . . . 14
    
      |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . . 13
       |
44 | | fnfvelrn 6017 |
. . . . . . . . . . . . 13
     
           |
45 | 30, 43, 44 | syl2anc 666 |
. . . . . . . . . . . 12
       |
46 | 38, 45 | eqeltrrd 2529 |
. . . . . . . . . . 11
   |
47 | 37 | simprd 465 |
. . . . . . . . . . . 12
       |
48 | | eluzfz2 11804 |
. . . . . . . . . . . . . 14
    
      |
49 | 41, 48 | syl 17 |
. . . . . . . . . . . . 13
       |
50 | | fnfvelrn 6017 |
. . . . . . . . . . . . 13
     
           |
51 | 30, 49, 50 | syl2anc 666 |
. . . . . . . . . . . 12
       |
52 | 47, 51 | eqeltrrd 2529 |
. . . . . . . . . . 11
   |
53 | | eqid 2450 |
. . . . . . . . . . 11

  |
54 | | eqid 2450 |
. . . . . . . . . . 11
     
 |
55 | | eqid 2450 |
. . . . . . . . . . 11
 
     
     |
56 | | eqid 2450 |
. . . . . . . . . . 11
inf  
      inf  
       |
57 | | fourierdlem54.d |
. . . . . . . . . . 11
   |
58 | | eqid 2450 |
. . . . . . . . . . 11
         |
59 | | eqid 2450 |
. . . . . . . . . . 11
     ↾t   ![[,] [,]](_icc.gif)       
↾t   ![[,] [,]](_icc.gif)    |
60 | | oveq1 6295 |
. . . . . . . . . . . . . 14
           |
61 | 60 | eleq1d 2512 |
. . . . . . . . . . . . 13
             |
62 | 61 | rexbidv 2900 |
. . . . . . . . . . . 12
  

           |
63 | 62 | cbvrabv 3043 |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)         |
64 | | oveq1 6295 |
. . . . . . . . . . . . . . . 16
       |
65 | 64 | oveq2d 6304 |
. . . . . . . . . . . . . . 15
           |
66 | 65 | eleq1d 2512 |
. . . . . . . . . . . . . 14
             |
67 | 66 | anbi1d 710 |
. . . . . . . . . . . . 13
                
        |
68 | | oveq1 6295 |
. . . . . . . . . . . . . . . 16
       |
69 | 68 | oveq2d 6304 |
. . . . . . . . . . . . . . 15
           |
70 | 69 | eleq1d 2512 |
. . . . . . . . . . . . . 14
             |
71 | 70 | anbi2d 709 |
. . . . . . . . . . . . 13
                
        |
72 | 67, 71 | cbvrex2v 3027 |
. . . . . . . . . . . 12
  
                        |
73 | 72 | anbi2i 699 |
. . . . . . . . . . 11
   
   
          
      
             |
74 | 17, 18, 19, 20, 23, 35, 46, 52, 53, 54, 55, 56, 4, 57, 58, 59, 63, 73 | fourierdlem42 38006 |
. . . . . . . . . 10
    ![[,] [,]](_icc.gif)          |
75 | | unfi 7835 |
. . . . . . . . . 10
    
   ![[,] [,]](_icc.gif)   
   
    
   ![[,] [,]](_icc.gif)           |
76 | 12, 74, 75 | sylancr 668 |
. . . . . . . . 9
    
   ![[,] [,]](_icc.gif)           |
77 | 8, 76 | syl5eqel 2532 |
. . . . . . . 8
   |
78 | | hashnncl 12544 |
. . . . . . . 8
     
   |
79 | 77, 78 | syl 17 |
. . . . . . 7
     
   |
80 | 11, 79 | mpbird 236 |
. . . . . 6
       |
81 | 80 | nnzd 11036 |
. . . . 5
       |
82 | | fourierdlem54.cd |
. . . . . . . . 9
   |
83 | 4, 82 | ltned 9768 |
. . . . . . . 8
   |
84 | | hashprg 12569 |
. . . . . . . . 9
 
            |
85 | 4, 57, 84 | syl2anc 666 |
. . . . . . . 8
            |
86 | 83, 85 | mpbid 214 |
. . . . . . 7
     
    |
87 | 86 | eqcomd 2456 |
. . . . . 6
          |
88 | | ssun1 3596 |
. . . . . . . . 9
          ![[,] [,]](_icc.gif)          |
89 | 88 | a1i 11 |
. . . . . . . 8
           ![[,] [,]](_icc.gif)   
       |
90 | 89, 8 | syl6sseqr 3478 |
. . . . . . 7
      |
91 | | hashssle 37509 |
. . . . . . 7
                   |
92 | 77, 90, 91 | syl2anc 666 |
. . . . . 6
     
 
      |
93 | 87, 92 | eqbrtrd 4422 |
. . . . 5

      |
94 | | eluz2 11162 |
. . . . 5
                     |
95 | 3, 81, 93, 94 | syl3anbrc 1191 |
. . . 4
           |
96 | | uz2m1nn 11230 |
. . . 4
                 |
97 | 95, 96 | syl 17 |
. . 3
         |
98 | 1, 97 | syl5eqel 2532 |
. 2
   |
99 | | prssg 4126 |
. . . . . . . . . . . . 13
 
   
      |
100 | 4, 57, 99 | syl2anc 666 |
. . . . . . . . . . . 12
   
      |
101 | 4, 57, 100 | mpbi2and 931 |
. . . . . . . . . . 11
      |
102 | | ssrab2 3513 |
. . . . . . . . . . . 12
   ![[,] [,]](_icc.gif)       
  ![[,] [,]](_icc.gif)   |
103 | 4, 57 | iccssred 37596 |
. . . . . . . . . . . 12
   ![[,] [,]](_icc.gif) 
  |
104 | 102, 103 | syl5ss 3442 |
. . . . . . . . . . 11
    ![[,] [,]](_icc.gif)       
  |
105 | 101, 104 | unssd 3609 |
. . . . . . . . . 10
    
   ![[,] [,]](_icc.gif)           |
106 | 8, 105 | syl5eqss 3475 |
. . . . . . . . 9

  |
107 | | fourierdlem54.s |
. . . . . . . . 9
            |
108 | 77, 106, 107, 1 | fourierdlem36 38000 |
. . . . . . . 8

         |
109 | | df-isom 5590 |
. . . . . . . 8
                                          |
110 | 108, 109 | sylib 200 |
. . . . . . 7
                                   |
111 | 110 | simpld 461 |
. . . . . 6
           |
112 | | f1of 5812 |
. . . . . 6
        
          |
113 | 111, 112 | syl 17 |
. . . . 5
           |
114 | 113, 106 | fssd 5736 |
. . . 4
           |
115 | | reex 9627 |
. . . . 5
 |
116 | | ovex 6316 |
. . . . . 6
     |
117 | 116 | a1i 11 |
. . . . 5
       |
118 | | elmapg 7482 |
. . . . 5
                         |
119 | 115, 117,
118 | sylancr 668 |
. . . 4
                   |
120 | 114, 119 | mpbird 236 |
. . 3
         |
121 | | df-f1o 5588 |
. . . . . . . . . . 11
                 
           |
122 | 111, 121 | sylib 200 |
. . . . . . . . . 10
                     |
123 | 122 | simprd 465 |
. . . . . . . . 9
           |
124 | | dffo3 6035 |
. . . . . . . . 9
        
          
            |
125 | 123, 124 | sylib 200 |
. . . . . . . 8
          
             |
126 | 125 | simprd 465 |
. . . . . . 7
  
           |
127 | | eqeq1 2454 |
. . . . . . . . . 10
     
       |
128 | | eqcom 2457 |
. . . . . . . . . 10
    
      |
129 | 127, 128 | syl6bb 265 |
. . . . . . . . 9
     
       |
130 | 129 | rexbidv 2900 |
. . . . . . . 8
  
        
             |
131 | 130 | rspcv 3145 |
. . . . . . 7
  

                      |
132 | 9, 126, 131 | sylc 62 |
. . . . . 6
             |
133 | | fveq2 5863 |
. . . . . . . . . . . . . 14
           |
134 | 133 | eqcomd 2456 |
. . . . . . . . . . . . 13
           |
135 | 134 | adantl 468 |
. . . . . . . . . . . 12
                   |
136 | | simplr 761 |
. . . . . . . . . . . 12
               |
137 | 135, 136 | eqtrd 2484 |
. . . . . . . . . . 11
               |
138 | 4 | ad2antrr 731 |
. . . . . . . . . . 11
        
  |
139 | 137, 138 | eqeltrd 2528 |
. . . . . . . . . 10
               |
140 | 139, 137 | eqled 9734 |
. . . . . . . . 9
            
  |
141 | 140 | 3adantl2 1164 |
. . . . . . . 8
      
            |
142 | 4 | rexrd 9687 |
. . . . . . . . . . . . . . . . 17
   |
143 | 57 | rexrd 9687 |
. . . . . . . . . . . . . . . . 17
   |
144 | 4, 57, 82 | ltled 9780 |
. . . . . . . . . . . . . . . . 17

  |
145 | | lbicc2 11745 |
. . . . . . . . . . . . . . . . 17
     ![[,] [,]](_icc.gif)    |
146 | 142, 143,
144, 145 | syl3anc 1267 |
. . . . . . . . . . . . . . . 16
   ![[,] [,]](_icc.gif)    |
147 | | ubicc2 11746 |
. . . . . . . . . . . . . . . . 17
     ![[,] [,]](_icc.gif)    |
148 | 142, 143,
144, 147 | syl3anc 1267 |
. . . . . . . . . . . . . . . 16
   ![[,] [,]](_icc.gif)    |
149 | | prssg 4126 |
. . . . . . . . . . . . . . . . 17
    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)     |
150 | 146, 148,
149 | syl2anc 666 |
. . . . . . . . . . . . . . . 16
     ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)     |
151 | 146, 148,
150 | mpbi2and 931 |
. . . . . . . . . . . . . . 15
      ![[,] [,]](_icc.gif)    |
152 | 102 | a1i 11 |
. . . . . . . . . . . . . . 15
    ![[,] [,]](_icc.gif)       
  ![[,] [,]](_icc.gif)    |
153 | 151, 152 | unssd 3609 |
. . . . . . . . . . . . . 14
    
   ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)    |
154 | 8, 153 | syl5eqss 3475 |
. . . . . . . . . . . . 13

  ![[,] [,]](_icc.gif)    |
155 | | nnm1nn0 10908 |
. . . . . . . . . . . . . . . . . 18
    
        |
156 | 80, 155 | syl 17 |
. . . . . . . . . . . . . . . . 17
         |
157 | 1, 156 | syl5eqel 2532 |
. . . . . . . . . . . . . . . 16
   |
158 | 157, 40 | syl6eleq 2538 |
. . . . . . . . . . . . . . 15
       |
159 | | eluzfz1 11803 |
. . . . . . . . . . . . . . 15
    
      |
160 | 158, 159 | syl 17 |
. . . . . . . . . . . . . 14
       |
161 | 113, 160 | ffvelrnd 6021 |
. . . . . . . . . . . . 13
       |
162 | 154, 161 | sseldd 3432 |
. . . . . . . . . . . 12
       ![[,] [,]](_icc.gif)    |
163 | 103, 162 | sseldd 3432 |
. . . . . . . . . . 11
       |
164 | 163 | adantr 467 |
. . . . . . . . . 10
 
       |
165 | 164 | 3ad2antl1 1169 |
. . . . . . . . 9
      
            |
166 | 4 | adantr 467 |
. . . . . . . . . 10
 

  |
167 | 166 | 3ad2antl1 1169 |
. . . . . . . . 9
      
     
  |
168 | | elfzelz 11797 |
. . . . . . . . . . . . . . 15
       |
169 | 168 | zred 11037 |
. . . . . . . . . . . . . 14
       |
170 | 169 | adantr 467 |
. . . . . . . . . . . . 13
     

  |
171 | | elfzle1 11799 |
. . . . . . . . . . . . . 14
       |
172 | 171 | adantr 467 |
. . . . . . . . . . . . 13
     

  |
173 | | neqne 37368 |
. . . . . . . . . . . . . 14
   |
174 | 173 | adantl 468 |
. . . . . . . . . . . . 13
     

  |
175 | 170, 172,
174 | ne0gt0d 9769 |
. . . . . . . . . . . 12
     

  |
176 | 175 | 3ad2antl2 1170 |
. . . . . . . . . . 11
      
     
  |
177 | | simpl1 1010 |
. . . . . . . . . . . 12
      
        |
178 | | simpl2 1011 |
. . . . . . . . . . . 12
      
            |
179 | 110 | simprd 465 |
. . . . . . . . . . . . . 14
                         |
180 | | breq1 4404 |
. . . . . . . . . . . . . . . . 17
 
   |
181 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . 18
           |
182 | 181 | breq1d 4411 |
. . . . . . . . . . . . . . . . 17
     
   
           |
183 | 180, 182 | bibi12d 323 |
. . . . . . . . . . . . . . . 16
           

            |
184 | 183 | ralbidv 2826 |
. . . . . . . . . . . . . . 15
  
     
                            |
185 | 184 | rspcv 3145 |
. . . . . . . . . . . . . 14
      
     
     
        
                   |
186 | 160, 179,
185 | sylc 62 |
. . . . . . . . . . . . 13
                   |
187 | 186 | r19.21bi 2756 |
. . . . . . . . . . . 12
 
     
           |
188 | 177, 178,
187 | syl2anc 666 |
. . . . . . . . . . 11
      
                  |
189 | 176, 188 | mpbid 214 |
. . . . . . . . . 10
      
         
      |
190 | | simpl3 1012 |
. . . . . . . . . 10
      
            |
191 | 189, 190 | breqtrd 4426 |
. . . . . . . . 9
      
         
  |
192 | 165, 167,
191 | ltled 9780 |
. . . . . . . 8
      
         
  |
193 | 141, 192 | pm2.61dan 799 |
. . . . . . 7
 
   
    
      |
194 | 193 | rexlimdv3a 2880 |
. . . . . 6
                   |
195 | 132, 194 | mpd 15 |
. . . . 5
    
  |
196 | | elicc2 11696 |
. . . . . . . 8
 
        ![[,] [,]](_icc.gif)      
            |
197 | 4, 57, 196 | syl2anc 666 |
. . . . . . 7
        ![[,] [,]](_icc.gif)      
            |
198 | 162, 197 | mpbid 214 |
. . . . . 6
     
           |
199 | 198 | simp2d 1020 |
. . . . 5

      |
200 | 163, 4 | letri3d 9774 |
. . . . 5
          
        |
201 | 195, 199,
200 | mpbir2and 932 |
. . . 4
       |
202 | | eluzfz2 11804 |
. . . . . . . . . 10
    
      |
203 | 158, 202 | syl 17 |
. . . . . . . . 9
       |
204 | 113, 203 | ffvelrnd 6021 |
. . . . . . . 8
       |
205 | 154, 204 | sseldd 3432 |
. . . . . . 7
       ![[,] [,]](_icc.gif)    |
206 | | elicc2 11696 |
. . . . . . . 8
 
        ![[,] [,]](_icc.gif)      
            |
207 | 4, 57, 206 | syl2anc 666 |
. . . . . . 7
        ![[,] [,]](_icc.gif)      
            |
208 | 205, 207 | mpbid 214 |
. . . . . 6
     
           |
209 | 208 | simp3d 1021 |
. . . . 5
    
  |
210 | | prid2g 4078 |
. . . . . . . . 9
      |
211 | | elun1 3600 |
. . . . . . . . 9
   
   
   ![[,] [,]](_icc.gif)           |
212 | 57, 210, 211 | 3syl 18 |
. . . . . . . 8
        ![[,] [,]](_icc.gif)           |
213 | 212, 8 | syl6eleqr 2539 |
. . . . . . 7
   |
214 | | eqeq1 2454 |
. . . . . . . . . 10
     
       |
215 | | eqcom 2457 |
. . . . . . . . . 10
    
      |
216 | 214, 215 | syl6bb 265 |
. . . . . . . . 9
     
       |
217 | 216 | rexbidv 2900 |
. . . . . . . 8
  
        
             |
218 | 217 | rspcv 3145 |
. . . . . . 7
  

                      |
219 | 213, 126,
218 | sylc 62 |
. . . . . 6
             |
220 | 215 | biimpri 210 |
. . . . . . . . 9
           |
221 | 220 | 3ad2ant3 1030 |
. . . . . . . 8
 
   
    
      |
222 | 114 | ffvelrnda 6020 |
. . . . . . . . . 10
 
           |
223 | 103, 205 | sseldd 3432 |
. . . . . . . . . . 11
       |
224 | 223 | adantr 467 |
. . . . . . . . . 10
 
           |
225 | 169 | adantl 468 |
. . . . . . . . . . . 12
 
       |
226 | | elfzel2 11795 |
. . . . . . . . . . . . . 14
       |
227 | 226 | zred 11037 |
. . . . . . . . . . . . 13
       |
228 | 227 | adantl 468 |
. . . . . . . . . . . 12
 
       |
229 | | elfzle2 11800 |
. . . . . . . . . . . . 13
       |
230 | 229 | adantl 468 |
. . . . . . . . . . . 12
 
       |
231 | 225, 228,
230 | lensymd 9783 |
. . . . . . . . . . 11
 
       |
232 | | breq1 4404 |
. . . . . . . . . . . . . . . 16
 
   |
233 | | fveq2 5863 |
. . . . . . . . . . . . . . . . 17
           |
234 | 233 | breq1d 4411 |
. . . . . . . . . . . . . . . 16
     
   
           |
235 | 232, 234 | bibi12d 323 |
. . . . . . . . . . . . . . 15
           
             |
236 | 235 | ralbidv 2826 |
. . . . . . . . . . . . . 14
  
     
                            |
237 | 236 | rspcv 3145 |
. . . . . . . . . . . . 13
      
     
     
        
                   |
238 | 203, 179,
237 | sylc 62 |
. . . . . . . . . . . 12
                   |
239 | 238 | r19.21bi 2756 |
. . . . . . . . . . 11
 
     
           |
240 | 231, 239 | mtbid 302 |
. . . . . . . . . 10
 
               |
241 | 222, 224,
240 | nltled 9782 |
. . . . . . . . 9
 
               |
242 | 241 | 3adant3 1027 |
. . . . . . . 8
 
   
    
          |
243 | 221, 242 | eqbrtrd 4422 |
. . . . . . 7
 
   
    
      |
244 | 243 | rexlimdv3a 2880 |
. . . . . 6
                   |
245 | 219, 244 | mpd 15 |
. . . . 5

      |
246 | 223, 57 | letri3d 9774 |
. . . . 5
          
        |
247 | 209, 245,
246 | mpbir2and 932 |
. . . 4
       |
248 | | elfzoelz 11917 |
. . . . . . . . 9
  ..^
  |
249 | 248 | zred 11037 |
. . . . . . . 8
  ..^
  |
250 | 249 | ltp1d 10534 |
. . . . . . 7
  ..^
    |
251 | 250 | adantl 468 |
. . . . . 6
 
 ..^      |
252 | 179 | adantr 467 |
. . . . . . 7
 
 ..^                          |
253 | | elfzofz 11932 |
. . . . . . . . 9
  ..^
      |
254 | 253 | adantl 468 |
. . . . . . . 8
 
 ..^        |
255 | | fzofzp1 12005 |
. . . . . . . . 9
  ..^
        |
256 | 255 | adantl 468 |
. . . . . . . 8
 
 ..^          |
257 | | breq1 4404 |
. . . . . . . . . 10
 
   |
258 | | fveq2 5863 |
. . . . . . . . . . 11
           |
259 | 258 | breq1d 4411 |
. . . . . . . . . 10
     
   
           |
260 | 257, 259 | bibi12d 323 |
. . . . . . . . 9
           
             |
261 | | breq2 4405 |
. . . . . . . . . 10
   
     |
262 | | fveq2 5863 |
. . . . . . . . . . 11
               |
263 | 262 | breq2d 4413 |
. . . . . . . . . 10
       
   
             |
264 | 261, 263 | bibi12d 323 |
. . . . . . . . 9
             
                 |
265 | 260, 264 | rspc2v 3158 |
. . . . . . . 8
                                   
                 |
266 | 254, 256,
265 | syl2anc 666 |
. . . . . . 7
 
 ..^                        
                 |
267 | 252, 266 | mpd 15 |
. . . . . 6
 
 ..^                  |
268 | 251, 267 | mpbid 214 |
. . . . 5
 
 ..^              |
269 | 268 | ralrimiva 2801 |
. . . 4
   ..^              |
270 | 201, 247,
269 | jca31 537 |
. . 3
            
 ..^               |
271 | | fourierdlem54.o |
. . . . 5
 
                 
 ..^                |
272 | 271 | fourierdlem2 37965 |
. . . 4
 
   
                  
 ..^                 |
273 | 98, 272 | syl 17 |
. . 3
                        
 ..^                 |
274 | 120, 270,
273 | mpbir2and 932 |
. 2
       |
275 | 98, 274, 108 | jca31 537 |
1
                  |