Step | Hyp | Ref
| Expression |
1 | | fourierdlem79.q |
. . . . . . . 8
       |
2 | | fourierdlem79.m |
. . . . . . . . 9
   |
3 | | fourierdlem79.p |
. . . . . . . . . 10
 
                 
 ..^                |
4 | 3 | fourierdlem2 38083 |
. . . . . . . . 9
 
   
                  
 ..^                 |
5 | 2, 4 | syl 17 |
. . . . . . . 8
                        
 ..^                 |
6 | 1, 5 | mpbid 215 |
. . . . . . 7
                   
 ..^                |
7 | 6 | simpld 466 |
. . . . . 6
         |
8 | | elmapi 7511 |
. . . . . 6
                 |
9 | 7, 8 | syl 17 |
. . . . 5
           |
10 | 9 | adantr 472 |
. . . 4
 
 ..^            |
11 | | fourierdlem79.t |
. . . . . . . . 9
   |
12 | | fourierdlem79.e |
. . . . . . . . 9
 
             |
13 | | fourierdlem79.l |
. . . . . . . . 9
   ![(,] (,]](_ioc.gif)         |
14 | | fourierdlem79.i |
. . . . . . . . 9
     ..^                  |
15 | 3, 2, 1, 11, 12, 13, 14 | fourierdlem37 38119 |
. . . . . . . 8
       ..^ 
    ..^                  ..^                  |
16 | 15 | simpld 466 |
. . . . . . 7
      ..^   |
17 | | fzossfz 11965 |
. . . . . . . 8
 ..^      |
18 | 17 | a1i 11 |
. . . . . . 7
  ..^       |
19 | 16, 18 | fssd 5750 |
. . . . . 6
           |
20 | 19 | adantr 472 |
. . . . 5
 
 ..^            |
21 | | fourierdlem79.c |
. . . . . . . . . . . . 13
   |
22 | | fourierdlem79.d |
. . . . . . . . . . . . 13
   |
23 | | fourierdlem79.cltd |
. . . . . . . . . . . . 13
   |
24 | | fourierdlem79.o |
. . . . . . . . . . . . 13
 
                 
 ..^                |
25 | | fourierdlem79.h |
. . . . . . . . . . . . 13
   
   ![[,] [,]](_icc.gif)          |
26 | | fourierdlem79.n |
. . . . . . . . . . . . 13
       |
27 | | fourierdlem79.s |
. . . . . . . . . . . . 13
            |
28 | 11, 3, 2, 1, 21, 22, 23, 24, 25, 26, 27 | fourierdlem54 38136 |
. . . . . . . . . . . 12
                  |
29 | 28 | simpld 466 |
. . . . . . . . . . 11
         |
30 | 29 | simprd 470 |
. . . . . . . . . 10
       |
31 | 30 | adantr 472 |
. . . . . . . . 9
 
 ..^        |
32 | 29 | simpld 466 |
. . . . . . . . . . 11
   |
33 | 32 | adantr 472 |
. . . . . . . . . 10
 
 ..^    |
34 | 24 | fourierdlem2 38083 |
. . . . . . . . . 10
 
   
                  
 ..^                 |
35 | 33, 34 | syl 17 |
. . . . . . . . 9
 
 ..^                         
 ..^                 |
36 | 31, 35 | mpbid 215 |
. . . . . . . 8
 
 ..^                    
 ..^                |
37 | 36 | simpld 466 |
. . . . . . 7
 
 ..^          |
38 | | elmapi 7511 |
. . . . . . 7
                 |
39 | 37, 38 | syl 17 |
. . . . . 6
 
 ..^            |
40 | | elfzofz 11962 |
. . . . . . 7
  ..^
      |
41 | 40 | adantl 473 |
. . . . . 6
 
 ..^        |
42 | 39, 41 | ffvelrnd 6038 |
. . . . 5
 
 ..^        |
43 | 20, 42 | ffvelrnd 6038 |
. . . 4
 
 ..^                |
44 | 10, 43 | ffvelrnd 6038 |
. . 3
 
 ..^                |
45 | 44 | rexrd 9708 |
. 2
 
 ..^                |
46 | 16 | adantr 472 |
. . . . . 6
 
 ..^       ..^   |
47 | 46, 42 | ffvelrnd 6038 |
. . . . 5
 
 ..^           ..^   |
48 | | fzofzp1 12037 |
. . . . 5
          ..^
                |
49 | 47, 48 | syl 17 |
. . . 4
 
 ..^                  |
50 | 10, 49 | ffvelrnd 6038 |
. . 3
 
 ..^                  |
51 | 50 | rexrd 9708 |
. 2
 
 ..^                  |
52 | 14 | a1i 11 |
. . . . 5
 
 ..^       ..^                   |
53 | | fveq2 5879 |
. . . . . . . . . 10
                   |
54 | 53 | fveq2d 5883 |
. . . . . . . . 9
                           |
55 | 54 | breq2d 4407 |
. . . . . . . 8
         
       
                   |
56 | 55 | rabbidv 3022 |
. . . . . . 7
       ..^                ..^                    |
57 | 56 | supeq1d 7978 |
. . . . . 6
         ..^    
          
    ..^                      |
58 | 57 | adantl 473 |
. . . . 5
    ..^           ..^    
          
    ..^                      |
59 | | ltso 9732 |
. . . . . . 7
 |
60 | 59 | supex 7995 |
. . . . . 6
    ..^    
              
 |
61 | 60 | a1i 11 |
. . . . 5
 
 ..^      ..^                      |
62 | 52, 58, 42, 61 | fvmptd 5969 |
. . . 4
 
 ..^              ..^    
              
  |
63 | 62 | fveq2d 5883 |
. . 3
 
 ..^                     ..^    
              
   |
64 | | simpl 464 |
. . . . . . 7
 
 ..^    |
65 | 64, 42 | jca 541 |
. . . . . 6
 
 ..^          |
66 | | eleq1 2537 |
. . . . . . . . 9
     
       |
67 | 66 | anbi2d 718 |
. . . . . . . 8
      

         |
68 | 57, 56 | eleq12d 2543 |
. . . . . . . 8
          ..^                  ..^                  ..^                      ..^                     |
69 | 67, 68 | imbi12d 327 |
. . . . . . 7
       
     ..^                  ..^              
           ..^                      ..^                      |
70 | 15 | simprd 470 |
. . . . . . . 8
      ..^                  ..^                 |
71 | 70 | imp 436 |
. . . . . . 7
 

    ..^    
          
  ..^    
           |
72 | 69, 71 | vtoclg 3093 |
. . . . . 6
      
         ..^    
              
  ..^    
                |
73 | 42, 65, 72 | sylc 61 |
. . . . 5
 
 ..^      ..^                      ..^                    |
74 | | nfrab1 2957 |
. . . . . . 7
    ..^    
              |
75 | | nfcv 2612 |
. . . . . . 7
   |
76 | | nfcv 2612 |
. . . . . . 7
  |
77 | 74, 75, 76 | nfsup 7983 |
. . . . . 6
      ..^                     |
78 | | nfcv 2612 |
. . . . . 6
   ..^  |
79 | | nfcv 2612 |
. . . . . . . 8
   |
80 | 79, 77 | nffv 5886 |
. . . . . . 7
         ..^    
              
  |
81 | | nfcv 2612 |
. . . . . . 7
  |
82 | | nfcv 2612 |
. . . . . . 7
               |
83 | 80, 81, 82 | nfbr 4440 |
. . . . . 6
         ..^    
              
              |
84 | | fveq2 5879 |
. . . . . . 7
     ..^                               ..^                       |
85 | 84 | breq1d 4405 |
. . . . . 6
     ..^                        
           
       ..^                                    |
86 | 77, 78, 83, 85 | elrabf 3182 |
. . . . 5
     ..^                      ..^                       ..^                     ..^        ..^    
              
                |
87 | 73, 86 | sylib 201 |
. . . 4
 
 ..^       ..^    
              
 ..^        ..^                    
               |
88 | 87 | simprd 470 |
. . 3
 
 ..^         ..^                    
              |
89 | 63, 88 | eqbrtrd 4416 |
. 2
 
 ..^                            |
90 | 2 | ad2antrr 740 |
. . . . 5
    ..^             |
91 | 1 | ad2antrr 740 |
. . . . 5
    ..^                 |
92 | 21 | ad2antrr 740 |
. . . . 5
    ..^             |
93 | 22 | ad2antrr 740 |
. . . . 5
    ..^             |
94 | 23 | ad2antrr 740 |
. . . . 5
    ..^             |
95 | | 0le1 10158 |
. . . . . . . 8
 |
96 | 95 | a1i 11 |
. . . . . . 7

  |
97 | 2 | nnge1d 10674 |
. . . . . . 7

  |
98 | | 1zzd 10992 |
. . . . . . . 8
   |
99 | | 0zd 10973 |
. . . . . . . 8
   |
100 | 2 | nnzd 11062 |
. . . . . . . 8
   |
101 | | elfz 11816 |
. . . . . . . 8
 
     
     |
102 | 98, 99, 100, 101 | syl3anc 1292 |
. . . . . . 7
      
    |
103 | 96, 97, 102 | mpbir2and 936 |
. . . . . 6
       |
104 | 103 | ad2antrr 740 |
. . . . 5
    ..^                 |
105 | | simplr 770 |
. . . . 5
    ..^            ..^   |
106 | | fourierdlem79.z |
. . . . . . . 8
                                                    |
107 | | fzofzp1 12037 |
. . . . . . . . . . . . . 14
  ..^
        |
108 | 107 | adantl 473 |
. . . . . . . . . . . . 13
 
 ..^          |
109 | 39, 108 | ffvelrnd 6038 |
. . . . . . . . . . . 12
 
 ..^          |
110 | 109, 42 | resubcld 10068 |
. . . . . . . . . . 11
 
 ..^                |
111 | 110 | rehalfcld 10882 |
. . . . . . . . . 10
 
 ..^                  |
112 | 9, 103 | ffvelrnd 6038 |
. . . . . . . . . . . . 13
       |
113 | 3, 2, 1 | fourierdlem11 38092 |
. . . . . . . . . . . . . 14
     |
114 | 113 | simp1d 1042 |
. . . . . . . . . . . . 13
   |
115 | 112, 114 | resubcld 10068 |
. . . . . . . . . . . 12
         |
116 | 115 | rehalfcld 10882 |
. . . . . . . . . . 11
           |
117 | 116 | adantr 472 |
. . . . . . . . . 10
 
 ..^            |
118 | 111, 117 | ifcld 3915 |
. . . . . . . . 9
 
 ..^                                                 |
119 | 42, 118 | readdcld 9688 |
. . . . . . . 8
 
 ..^                                                       |
120 | 106, 119 | syl5eqel 2553 |
. . . . . . 7
 
 ..^    |
121 | | 2re 10701 |
. . . . . . . . . . . . . 14
 |
122 | 121 | a1i 11 |
. . . . . . . . . . . . 13
 
 ..^    |
123 | | elfzoelz 11947 |
. . . . . . . . . . . . . . . . . 18
  ..^
  |
124 | 123 | zred 11063 |
. . . . . . . . . . . . . . . . 17
  ..^
  |
125 | 124 | ltp1d 10559 |
. . . . . . . . . . . . . . . 16
  ..^
    |
126 | 125 | adantl 473 |
. . . . . . . . . . . . . . 15
 
 ..^      |
127 | 28 | simprd 470 |
. . . . . . . . . . . . . . . . 17

         |
128 | 127 | adantr 472 |
. . . . . . . . . . . . . . . 16
 
 ..^           |
129 | | isorel 6235 |
. . . . . . . . . . . . . . . 16
 
           
              
         |
130 | 128, 41, 108, 129 | syl12anc 1290 |
. . . . . . . . . . . . . . 15
 
 ..^                  |
131 | 126, 130 | mpbid 215 |
. . . . . . . . . . . . . 14
 
 ..^              |
132 | 42, 109 | posdifd 10221 |
. . . . . . . . . . . . . 14
 
 ..^                            |
133 | 131, 132 | mpbid 215 |
. . . . . . . . . . . . 13
 
 ..^                |
134 | | 2pos 10723 |
. . . . . . . . . . . . . 14
 |
135 | 134 | a1i 11 |
. . . . . . . . . . . . 13
 
 ..^    |
136 | 110, 122,
133, 135 | divgt0d 10564 |
. . . . . . . . . . . 12
 
 ..^                  |
137 | 111, 136 | elrpd 11361 |
. . . . . . . . . . 11
 
 ..^                  |
138 | 121 | a1i 11 |
. . . . . . . . . . . . . 14
   |
139 | 2 | nngt0d 10675 |
. . . . . . . . . . . . . . . . . 18
   |
140 | | fzolb 11953 |
. . . . . . . . . . . . . . . . . 18
  ..^     |
141 | 99, 100, 139, 140 | syl3anbrc 1214 |
. . . . . . . . . . . . . . . . 17
  ..^   |
142 | | 0re 9661 |
. . . . . . . . . . . . . . . . . 18
 |
143 | | eleq1 2537 |
. . . . . . . . . . . . . . . . . . . . 21
   ..^
 ..^    |
144 | 143 | anbi2d 718 |
. . . . . . . . . . . . . . . . . . . 20
  
 ..^  
 ..^     |
145 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . 21
           |
146 | | oveq1 6315 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
147 | 146 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . . 21
               |
148 | 145, 147 | breq12d 4408 |
. . . . . . . . . . . . . . . . . . . 20
     
     
             |
149 | 144, 148 | imbi12d 327 |
. . . . . . . . . . . . . . . . . . 19
   
 ..^     
      
   ..^                |
150 | 6 | simprd 470 |
. . . . . . . . . . . . . . . . . . . . 21
            
 ..^               |
151 | 150 | simprd 470 |
. . . . . . . . . . . . . . . . . . . 20
   ..^              |
152 | 151 | r19.21bi 2776 |
. . . . . . . . . . . . . . . . . . 19
 
 ..^              |
153 | 149, 152 | vtoclg 3093 |
. . . . . . . . . . . . . . . . . 18
  
 ..^ 
             |
154 | 142, 153 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
 
 ..^              |
155 | 141, 154 | mpdan 681 |
. . . . . . . . . . . . . . . 16
    
        |
156 | 150 | simpld 466 |
. . . . . . . . . . . . . . . . 17
             |
157 | 156 | simpld 466 |
. . . . . . . . . . . . . . . 16
       |
158 | | 0p1e1 10743 |
. . . . . . . . . . . . . . . . . 18
   |
159 | 158 | fveq2i 5882 |
. . . . . . . . . . . . . . . . 17
           |
160 | 159 | a1i 11 |
. . . . . . . . . . . . . . . 16
             |
161 | 155, 157,
160 | 3brtr3d 4425 |
. . . . . . . . . . . . . . 15
       |
162 | 114, 112 | posdifd 10221 |
. . . . . . . . . . . . . . 15
               |
163 | 161, 162 | mpbid 215 |
. . . . . . . . . . . . . 14
         |
164 | 134 | a1i 11 |
. . . . . . . . . . . . . 14
   |
165 | 115, 138,
163, 164 | divgt0d 10564 |
. . . . . . . . . . . . 13
           |
166 | 116, 165 | elrpd 11361 |
. . . . . . . . . . . 12
           |
167 | 166 | adantr 472 |
. . . . . . . . . . 11
 
 ..^            |
168 | 137, 167 | ifcld 3915 |
. . . . . . . . . 10
 
 ..^                                                 |
169 | 42, 168 | ltaddrpd 11394 |
. . . . . . . . 9
 
 ..^                        
                                  |
170 | 42, 119, 169 | ltled 9800 |
. . . . . . . 8
 
 ..^                        
                                  |
171 | 170, 106 | syl6breqr 4436 |
. . . . . . 7
 
 ..^        |
172 | 42, 111 | readdcld 9688 |
. . . . . . . . 9
 
 ..^                        |
173 | | iftrue 3878 |
. . . . . . . . . . . . 13
                                                                                |
174 | 173 | adantl 473 |
. . . . . . . . . . . 12
    ..^                                                                                  |
175 | 111 | leidd 10201 |
. . . . . . . . . . . . 13
 
 ..^                                |
176 | 175 | adantr 472 |
. . . . . . . . . . . 12
    ..^                                                   |
177 | 174, 176 | eqbrtrd 4416 |
. . . . . . . . . . 11
    ..^                                                                                  |
178 | | iffalse 3881 |
. . . . . . . . . . . . 13
            
                                                             |
179 | 178 | adantl 473 |
. . . . . . . . . . . 12
    ..^                                                                            |
180 | 115 | ad2antrr 740 |
. . . . . . . . . . . . 13
    ..^                             |
181 | 110 | adantr 472 |
. . . . . . . . . . . . 13
    ..^                                   |
182 | | 2rp 11330 |
. . . . . . . . . . . . . 14
 |
183 | 182 | a1i 11 |
. . . . . . . . . . . . 13
    ..^                       |
184 | | simpr 468 |
. . . . . . . . . . . . . 14
    ..^                                
        |
185 | 180, 181,
184 | nltled 9802 |
. . . . . . . . . . . . 13
    ..^                          
              |
186 | 180, 181,
183, 185 | lediv1dd 11419 |
. . . . . . . . . . . 12
    ..^                            
                |
187 | 179, 186 | eqbrtrd 4416 |
. . . . . . . . . . 11
    ..^                                                                                  |
188 | 177, 187 | pm2.61dan 808 |
. . . . . . . . . 10
 
 ..^                                                               |
189 | 118, 111,
42, 188 | leadd2dd 10249 |
. . . . . . . . 9
 
 ..^                                                                           |
190 | 42 | recnd 9687 |
. . . . . . . . . . . . . . . 16
 
 ..^        |
191 | 109 | recnd 9687 |
. . . . . . . . . . . . . . . 16
 
 ..^          |
192 | 190, 191 | addcomd 9853 |
. . . . . . . . . . . . . . 15
 
 ..^                            |
193 | 192 | oveq1d 6323 |
. . . . . . . . . . . . . 14
 
 ..^                                |
194 | 193 | oveq1d 6323 |
. . . . . . . . . . . . 13
 
 ..^                                                                |
195 | | halfaddsub 10869 |
. . . . . . . . . . . . . . 15
                                                                                       |
196 | 191, 190,
195 | syl2anc 673 |
. . . . . . . . . . . . . 14
 
 ..^                                                                            |
197 | 196 | simprd 470 |
. . . . . . . . . . . . 13
 
 ..^                                      |
198 | 194, 197 | eqtrd 2505 |
. . . . . . . . . . . 12
 
 ..^                                      |
199 | 190, 191 | addcld 9680 |
. . . . . . . . . . . . . 14
 
 ..^                |
200 | 199 | halfcld 10880 |
. . . . . . . . . . . . 13
 
 ..^                  |
201 | 111 | recnd 9687 |
. . . . . . . . . . . . 13
 
 ..^                  |
202 | 200, 201,
190 | subsub23d 37589 |
. . . . . . . . . . . 12
 
 ..^                                                                          |
203 | 198, 202 | mpbid 215 |
. . . . . . . . . . 11
 
 ..^                                      |
204 | 200, 190,
201 | subaddd 10023 |
. . . . . . . . . . 11
 
 ..^                                                                          |
205 | 203, 204 | mpbid 215 |
. . . . . . . . . 10
 
 ..^                                      |
206 | | avglt2 10874 |
. . . . . . . . . . . 12
                                     
         |
207 | 42, 109, 206 | syl2anc 673 |
. . . . . . . . . . 11
 
 ..^                                    |
208 | 131, 207 | mpbid 215 |
. . . . . . . . . 10
 
 ..^                        |
209 | 205, 208 | eqbrtrd 4416 |
. . . . . . . . 9
 
 ..^                              |
210 | 119, 172,
109, 189, 209 | lelttrd 9810 |
. . . . . . . 8
 
 ..^                                                             |
211 | 106, 210 | syl5eqbr 4429 |
. . . . . . 7
 
 ..^          |
212 | 109 | rexrd 9708 |
. . . . . . . 8
 
 ..^          |
213 | | elico2 11723 |
. . . . . . . 8
             
             
               |
214 | 42, 212, 213 | syl2anc 673 |
. . . . . . 7
 
 ..^                                |
215 | 120, 171,
211, 214 | mpbir3and 1213 |
. . . . . 6
 
 ..^                  |
216 | 215 | adantr 472 |
. . . . 5
    ..^                           |
217 | 114 | ad2antrr 740 |
. . . . . . . 8
    ..^             |
218 | 113 | simp2d 1043 |
. . . . . . . . 9
   |
219 | 218 | ad2antrr 740 |
. . . . . . . 8
    ..^             |
220 | 113 | simp3d 1044 |
. . . . . . . . 9
   |
221 | 220 | ad2antrr 740 |
. . . . . . . 8
    ..^             |
222 | 42 | adantr 472 |
. . . . . . . 8
    ..^                 |
223 | | simpr 468 |
. . . . . . . 8
    ..^                     |
224 | 169, 106 | syl6breqr 4436 |
. . . . . . . . . 10
 
 ..^        |
225 | 218, 114 | resubcld 10068 |
. . . . . . . . . . . . . 14
     |
226 | 11, 225 | syl5eqel 2553 |
. . . . . . . . . . . . 13
   |
227 | 226 | adantr 472 |
. . . . . . . . . . . 12
 
 ..^    |
228 | 111 | adantr 472 |
. . . . . . . . . . . . . . . 16
    ..^                                     |
229 | 116 | ad2antrr 740 |
. . . . . . . . . . . . . . . 16
    ..^                               |
230 | 110 | adantr 472 |
. . . . . . . . . . . . . . . . 17
    ..^                                   |
231 | 115 | ad2antrr 740 |
. . . . . . . . . . . . . . . . 17
    ..^                             |
232 | 182 | a1i 11 |
. . . . . . . . . . . . . . . . 17
    ..^                       |
233 | | simpr 468 |
. . . . . . . . . . . . . . . . 17
    ..^                                         |
234 | 230, 231,
232, 233 | ltdiv1dd 11418 |
. . . . . . . . . . . . . . . 16
    ..^                                             |
235 | 228, 229,
234 | ltled 9800 |
. . . . . . . . . . . . . . 15
    ..^                                             |
236 | 174, 235 | eqbrtrd 4416 |
. . . . . . . . . . . . . 14
    ..^                                                                            |
237 | 178 | adantl 473 |
. . . . . . . . . . . . . . . 16
 
                                                                          |
238 | 116 | leidd 10201 |
. . . . . . . . . . . . . . . . 17
        
          |
239 | 238 | adantr 472 |
. . . . . . . . . . . . . . . 16
 
                          
          |
240 | 237, 239 | eqbrtrd 4416 |
. . . . . . . . . . . . . . 15
 
                                                                          |
241 | 240 | adantlr 729 |
. . . . . . . . . . . . . 14
    ..^                                                                            |
242 | 236, 241 | pm2.61dan 808 |
. . . . . . . . . . . . 13
 
 ..^                                                         |
243 | 225 | rehalfcld 10882 |
. . . . . . . . . . . . . . . 16
       |
244 | 182 | a1i 11 |
. . . . . . . . . . . . . . . . 17
   |
245 | 114 | rexrd 9708 |
. . . . . . . . . . . . . . . . . . 19
   |
246 | 218 | rexrd 9708 |
. . . . . . . . . . . . . . . . . . 19
   |
247 | 3, 2, 1 | fourierdlem15 38096 |
. . . . . . . . . . . . . . . . . . . 20
           ![[,] [,]](_icc.gif)    |
248 | 247, 103 | ffvelrnd 6038 |
. . . . . . . . . . . . . . . . . . 19
       ![[,] [,]](_icc.gif)    |
249 | | iccleub 11715 |
. . . . . . . . . . . . . . . . . . 19
        ![[,] [,]](_icc.gif)         |
250 | 245, 246,
248, 249 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . 18
    
  |
251 | 112, 218,
114, 250 | lesub1dd 10250 |
. . . . . . . . . . . . . . . . 17
      
    |
252 | 115, 225,
244, 251 | lediv1dd 11419 |
. . . . . . . . . . . . . . . 16
        
 
    |
253 | 11 | eqcomi 2480 |
. . . . . . . . . . . . . . . . . 18
   |
254 | 253 | oveq1i 6318 |
. . . . . . . . . . . . . . . . 17
       |
255 | 114, 218 | posdifd 10221 |
. . . . . . . . . . . . . . . . . . . . 21
       |
256 | 220, 255 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . 20
     |
257 | 256, 11 | syl6breqr 4436 |
. . . . . . . . . . . . . . . . . . 19
   |
258 | 226, 257 | elrpd 11361 |
. . . . . . . . . . . . . . . . . 18
   |
259 | | rphalflt 11352 |
. . . . . . . . . . . . . . . . . 18

    |
260 | 258, 259 | syl 17 |
. . . . . . . . . . . . . . . . 17
  
  |
261 | 254, 260 | syl5eqbr 4429 |
. . . . . . . . . . . . . . . 16
    
  |
262 | 116, 243,
226, 252, 261 | lelttrd 9810 |
. . . . . . . . . . . . . . 15
        
  |
263 | 116, 226,
262 | ltled 9800 |
. . . . . . . . . . . . . 14
        
  |
264 | 263 | adantr 472 |
. . . . . . . . . . . . 13
 
 ..^            |
265 | 118, 117,
227, 242, 264 | letrd 9809 |
. . . . . . . . . . . 12
 
 ..^                                                 |
266 | 118, 227,
42, 265 | leadd2dd 10249 |
. . . . . . . . . . 11
 
 ..^                                                             |
267 | 106, 266 | syl5eqbr 4429 |
. . . . . . . . . 10
 
 ..^          |
268 | 42 | rexrd 9708 |
. . . . . . . . . . 11
 
 ..^        |
269 | 42, 227 | readdcld 9688 |
. . . . . . . . . . 11
 
 ..^          |
270 | | elioc2 11722 |
. . . . . . . . . . 11
                    ![(,] (,]](_ioc.gif)            
          |
271 | 268, 269,
270 | syl2anc 673 |
. . . . . . . . . 10
 
 ..^         ![(,] (,]](_ioc.gif)            
          |
272 | 120, 224,
267, 271 | mpbir3and 1213 |
. . . . . . . . 9
 
 ..^        ![(,] (,]](_ioc.gif)          |
273 | 272 | adantr 472 |
. . . . . . . 8
    ..^                 ![(,] (,]](_ioc.gif)          |
274 | 217, 219,
221, 11, 12, 222, 223, 273 | fourierdlem26 38107 |
. . . . . . 7
    ..^                
        |
275 | 106 | a1i 11 |
. . . . . . . . . 10
 
 ..^                    
                                  |
276 | 275 | oveq1d 6323 |
. . . . . . . . 9
 
 ..^                           
                                       |
277 | 276 | oveq2d 6324 |
. . . . . . . 8
 
 ..^   
                          
                                        |
278 | 277 | adantr 472 |
. . . . . . 7
    ..^           
                                                                    |
279 | 118 | recnd 9687 |
. . . . . . . . . 10
 
 ..^                                                 |
280 | 190, 279 | pncan2d 10007 |
. . . . . . . . 9
 
 ..^                                                                                                          |
281 | 280 | oveq2d 6324 |
. . . . . . . 8
 
 ..^                                                                           
                                  |
282 | 281 | adantr 472 |
. . . . . . 7
    ..^           
                   
                                                                                       |
283 | 274, 278,
282 | 3eqtrd 2509 |
. . . . . 6
    ..^                                                                |
284 | 173 | oveq2d 6324 |
. . . . . . . . . 10
                   
             
                                                  |
285 | 284 | adantl 473 |
. . . . . . . . 9
    ..^                     
             
                                                  |
286 | 114 | adantr 472 |
. . . . . . . . . . . 12
 
 ..^    |
287 | 286, 111 | readdcld 9688 |
. . . . . . . . . . 11
 
 ..^                    |
288 | 287 | adantr 472 |
. . . . . . . . . 10
    ..^                     
                 |
289 | 286, 117 | readdcld 9688 |
. . . . . . . . . . 11
 
 ..^              |
290 | 289 | adantr 472 |
. . . . . . . . . 10
    ..^                     
           |
291 | 112 | ad2antrr 740 |
. . . . . . . . . 10
    ..^                           |
292 | 114 | ad2antrr 740 |
. . . . . . . . . . 11
    ..^                       |
293 | 228, 229,
292, 234 | ltadd2dd 9811 |
. . . . . . . . . 10
    ..^                     
                           |
294 | 112 | recnd 9687 |
. . . . . . . . . . . . . . . 16
       |
295 | 114 | recnd 9687 |
. . . . . . . . . . . . . . . 16
   |
296 | | halfaddsub 10869 |
. . . . . . . . . . . . . . . 16
     
                                             |
297 | 294, 295,
296 | syl2anc 673 |
. . . . . . . . . . . . . . 15
                                             |
298 | 297 | simprd 470 |
. . . . . . . . . . . . . 14
                     |
299 | 298 | oveq1d 6323 |
. . . . . . . . . . . . 13
                                         |
300 | 112, 114 | readdcld 9688 |
. . . . . . . . . . . . . . . 16
         |
301 | 300 | rehalfcld 10882 |
. . . . . . . . . . . . . . 15
           |
302 | 301 | recnd 9687 |
. . . . . . . . . . . . . 14
           |
303 | 116 | recnd 9687 |
. . . . . . . . . . . . . 14
           |
304 | 302, 303 | npcand 10009 |
. . . . . . . . . . . . 13
                                       |
305 | 299, 304 | eqtr3d 2507 |
. . . . . . . . . . . 12
                     |
306 | 112, 112 | readdcld 9688 |
. . . . . . . . . . . . . 14
             |
307 | 114, 112,
112, 161 | ltadd2dd 9811 |
. . . . . . . . . . . . . 14
      
            |
308 | 300, 306,
244, 307 | ltdiv1dd 11418 |
. . . . . . . . . . . . 13
        
              |
309 | 294 | 2timesd 10878 |
. . . . . . . . . . . . . . . 16
                   |
310 | 309 | eqcomd 2477 |
. . . . . . . . . . . . . . 15
                   |
311 | 310 | oveq1d 6323 |
. . . . . . . . . . . . . 14
                       |
312 | | 2cnd 10704 |
. . . . . . . . . . . . . . 15
   |
313 | | 2ne0 10724 |
. . . . . . . . . . . . . . . 16
 |
314 | 313 | a1i 11 |
. . . . . . . . . . . . . . 15
   |
315 | 294, 312,
314 | divcan3d 10410 |
. . . . . . . . . . . . . 14
               |
316 | 311, 315 | eqtrd 2505 |
. . . . . . . . . . . . 13
                   |
317 | 308, 316 | breqtrd 4420 |
. . . . . . . . . . . 12
        
      |
318 | 305, 317 | eqbrtrd 4416 |
. . . . . . . . . . 11
                 |
319 | 318 | ad2antrr 740 |
. . . . . . . . . 10
    ..^                     
               |
320 | 288, 290,
291, 293, 319 | lttrd 9813 |
. . . . . . . . 9
    ..^                     
                     |
321 | 285, 320 | eqbrtrd 4416 |
. . . . . . . 8
    ..^                     
             
                                      |
322 | 178 | oveq2d 6324 |
. . . . . . . . . 10
            
      
             
                                            |
323 | 322 | adantl 473 |
. . . . . . . . 9
    ..^                                                                                |
324 | 318 | ad2antrr 740 |
. . . . . . . . 9
    ..^                                     |
325 | 323, 324 | eqbrtrd 4416 |
. . . . . . . 8
    ..^                                                                          |
326 | 321, 325 | pm2.61dan 808 |
. . . . . . 7
 
 ..^                                                       |
327 | 326 | adantr 472 |
. . . . . 6
    ..^           
             
                                      |
328 | 283, 327 | eqbrtrd 4416 |
. . . . 5
    ..^                     |
329 | | eqid 2471 |
. . . . 5
                         |
330 | 11, 3, 90, 91, 92, 93, 94, 24, 25, 26, 27, 12, 104, 105, 216, 328, 329 | fourierdlem63 38145 |
. . . 4
    ..^                           |
331 | 14 | a1i 11 |
. . . . . . . . 9
    ..^                ..^                   |
332 | 57 | adantl 473 |
. . . . . . . . 9
   
 ..^          
         ..^                    ..^                      |
333 | 60 | a1i 11 |
. . . . . . . . 9
    ..^               ..^    
              
  |
334 | 331, 332,
222, 333 | fvmptd 5969 |
. . . . . . . 8
    ..^                       ..^                      |
335 | | fveq2 5879 |
. . . . . . . . . . . . 13
                           |
336 | 13 | a1i 11 |
. . . . . . . . . . . . . 14
    ![(,] (,]](_ioc.gif)     
    |
337 | | iftrue 3878 |
. . . . . . . . . . . . . . 15
        |
338 | 337 | adantl 473 |
. . . . . . . . . . . . . 14
 
        |
339 | | ubioc1 11713 |
. . . . . . . . . . . . . . 15
     ![(,] (,]](_ioc.gif)    |
340 | 245, 246,
220, 339 | syl3anc 1292 |
. . . . . . . . . . . . . 14
   ![(,] (,]](_ioc.gif)    |
341 | 336, 338,
340, 114 | fvmptd 5969 |
. . . . . . . . . . . . 13
      |