Step | Hyp | Ref
| Expression |
1 | | fourierdlem63.e |
. . . . 5
 
             |
2 | 1 | a1i 11 |
. . . 4
                 |
3 | | id 22 |
. . . . . 6
    
     
    |
4 | | oveq2 6298 |
. . . . . . . . 9
    
  
           |
5 | 4 | oveq1d 6305 |
. . . . . . . 8
    
           
      |
6 | 5 | fveq2d 5869 |
. . . . . . 7
    
                          |
7 | 6 | oveq1d 6305 |
. . . . . 6
    
                     
        |
8 | 3, 7 | oveq12d 6308 |
. . . . 5
    
                                        |
9 | 8 | adantl 468 |
. . . 4
 
      
                
                     |
10 | | fourierdlem63.t |
. . . . . . . . . . 11
   |
11 | | fourierdlem63.p |
. . . . . . . . . . 11
 
                 
 ..^                |
12 | | fourierdlem63.m |
. . . . . . . . . . 11
   |
13 | | fourierdlem63.q |
. . . . . . . . . . 11
       |
14 | | fourierdlem63.c |
. . . . . . . . . . 11
   |
15 | | fourierdlem63.d |
. . . . . . . . . . 11
   |
16 | | fourierdlem63.cltd |
. . . . . . . . . . 11
   |
17 | | fourierdlem63.o |
. . . . . . . . . . 11
 
                 
 ..^                |
18 | | fourierdlem63.h |
. . . . . . . . . . 11
   
   ![[,] [,]](_icc.gif)          |
19 | | fourierdlem63.n |
. . . . . . . . . . 11
       |
20 | | fourierdlem63.s |
. . . . . . . . . . 11
            |
21 | 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20 | fourierdlem54 38024 |
. . . . . . . . . 10
                  |
22 | 21 | simpld 461 |
. . . . . . . . 9
         |
23 | 22 | simprd 465 |
. . . . . . . 8
       |
24 | 22 | simpld 461 |
. . . . . . . . 9
   |
25 | 17 | fourierdlem2 37971 |
. . . . . . . . 9
 
   
                  
 ..^                 |
26 | 24, 25 | syl 17 |
. . . . . . . 8
                        
 ..^                 |
27 | 23, 26 | mpbid 214 |
. . . . . . 7
                   
 ..^                |
28 | 27 | simpld 461 |
. . . . . 6
         |
29 | | elmapi 7493 |
. . . . . 6
                 |
30 | 28, 29 | syl 17 |
. . . . 5
           |
31 | | fourierdlem63.j |
. . . . . 6
  ..^   |
32 | | fzofzp1 12008 |
. . . . . 6
  ..^
        |
33 | 31, 32 | syl 17 |
. . . . 5
         |
34 | 30, 33 | ffvelrnd 6023 |
. . . 4
    
    |
35 | 11, 12, 13 | fourierdlem11 37980 |
. . . . . . . . . . 11
     |
36 | 35 | simp2d 1021 |
. . . . . . . . . 10
   |
37 | 36, 34 | resubcld 10047 |
. . . . . . . . 9
           |
38 | 35 | simp1d 1020 |
. . . . . . . . . . 11
   |
39 | 36, 38 | resubcld 10047 |
. . . . . . . . . 10
     |
40 | 10, 39 | syl5eqel 2533 |
. . . . . . . . 9
   |
41 | 35 | simp3d 1022 |
. . . . . . . . . . . 12
   |
42 | 38, 36 | posdifd 10200 |
. . . . . . . . . . . 12
       |
43 | 41, 42 | mpbid 214 |
. . . . . . . . . . 11
     |
44 | 43, 10 | syl6breqr 4443 |
. . . . . . . . . 10
   |
45 | 44 | gt0ne0d 10178 |
. . . . . . . . 9
   |
46 | 37, 40, 45 | redivcld 10435 |
. . . . . . . 8
             |
47 | 46 | flcld 12034 |
. . . . . . 7
                 |
48 | 47 | zred 11040 |
. . . . . 6
                 |
49 | 48, 40 | remulcld 9671 |
. . . . 5
                   |
50 | 34, 49 | readdcld 9670 |
. . . 4
     
                     |
51 | 2, 9, 34, 50 | fvmptd 5954 |
. . 3
                           
         |
52 | 51, 50 | eqeltrd 2529 |
. 2
             |
53 | 11 | fourierdlem2 37971 |
. . . . . . 7
 
   
                  
 ..^                 |
54 | 12, 53 | syl 17 |
. . . . . 6
                        
 ..^                 |
55 | 13, 54 | mpbid 214 |
. . . . 5
                   
 ..^                |
56 | 55 | simpld 461 |
. . . 4
         |
57 | | elmapi 7493 |
. . . 4
                 |
58 | 56, 57 | syl 17 |
. . 3
           |
59 | | fourierdlem63.k |
. . 3
       |
60 | 58, 59 | ffvelrnd 6023 |
. 2
       |
61 | 14 | adantr 467 |
. . . . . . 7
 
                 |
62 | 15 | adantr 467 |
. . . . . . 7
 
                 |
63 | 38 | rexrd 9690 |
. . . . . . . . . . . 12
   |
64 | | iocssre 11714 |
. . . . . . . . . . . 12
     ![(,] (,]](_ioc.gif)    |
65 | 63, 36, 64 | syl2anc 667 |
. . . . . . . . . . 11
   ![(,] (,]](_ioc.gif) 
  |
66 | 38, 36, 41, 10, 1 | fourierdlem4 37973 |
. . . . . . . . . . . 12
       ![(,] (,]](_ioc.gif)    |
67 | | fourierdlem63.y |
. . . . . . . . . . . . . 14
           
     |
68 | | elfzofz 11935 |
. . . . . . . . . . . . . . . . 17
  ..^
      |
69 | 31, 68 | syl 17 |
. . . . . . . . . . . . . . . 16
       |
70 | 30, 69 | ffvelrnd 6023 |
. . . . . . . . . . . . . . 15
       |
71 | 34 | rexrd 9690 |
. . . . . . . . . . . . . . 15
    
    |
72 | | elico2 11698 |
. . . . . . . . . . . . . . 15
             
          
  
               |
73 | 70, 71, 72 | syl2anc 667 |
. . . . . . . . . . . . . 14
                    
   
      |
74 | 67, 73 | mpbid 214 |
. . . . . . . . . . . . 13
     
   
     |
75 | 74 | simp1d 1020 |
. . . . . . . . . . . 12
   |
76 | 66, 75 | ffvelrnd 6023 |
. . . . . . . . . . 11
       ![(,] (,]](_ioc.gif)    |
77 | 65, 76 | sseldd 3433 |
. . . . . . . . . 10
       |
78 | 77, 75 | resubcld 10047 |
. . . . . . . . 9
         |
79 | 60, 78 | resubcld 10047 |
. . . . . . . 8
               |
80 | 79 | adantr 467 |
. . . . . . 7
 
                             |
81 | | icossicc 11721 |
. . . . . . . . . . . . . 14
          
         ![[,] [,]](_icc.gif)         |
82 | 14 | rexrd 9690 |
. . . . . . . . . . . . . . 15
   |
83 | 15 | rexrd 9690 |
. . . . . . . . . . . . . . 15
   |
84 | 17, 24, 23 | fourierdlem15 37984 |
. . . . . . . . . . . . . . 15
           ![[,] [,]](_icc.gif)    |
85 | 82, 83, 84, 31 | fourierdlem8 37977 |
. . . . . . . . . . . . . 14
       ![[,] [,]](_icc.gif)       
  ![[,] [,]](_icc.gif)    |
86 | 81, 85 | syl5ss 3443 |
. . . . . . . . . . . . 13
              
  ![[,] [,]](_icc.gif)    |
87 | 86, 67 | sseldd 3433 |
. . . . . . . . . . . 12
   ![[,] [,]](_icc.gif)    |
88 | | elicc2 11699 |
. . . . . . . . . . . . 13
 
    ![[,] [,]](_icc.gif)  
    |
89 | 14, 15, 88 | syl2anc 667 |
. . . . . . . . . . . 12
    ![[,] [,]](_icc.gif)  
    |
90 | 87, 89 | mpbid 214 |
. . . . . . . . . . 11
 
   |
91 | 90 | simp2d 1021 |
. . . . . . . . . 10

  |
92 | 60, 77 | resubcld 10047 |
. . . . . . . . . . . . 13
             |
93 | | fourierdlem63.eyltqk |
. . . . . . . . . . . . . 14
    
      |
94 | 77, 60 | posdifd 10200 |
. . . . . . . . . . . . . 14
                       |
95 | 93, 94 | mpbid 214 |
. . . . . . . . . . . . 13
             |
96 | 92, 95 | elrpd 11338 |
. . . . . . . . . . . 12
             |
97 | 75, 96 | ltaddrpd 11371 |
. . . . . . . . . . 11
               |
98 | 60 | recnd 9669 |
. . . . . . . . . . . . 13
       |
99 | 77 | recnd 9669 |
. . . . . . . . . . . . 13
       |
100 | 75 | recnd 9669 |
. . . . . . . . . . . . 13
   |
101 | 98, 99, 100 | subsub3d 10016 |
. . . . . . . . . . . 12
                           |
102 | 98, 100 | addcomd 9835 |
. . . . . . . . . . . . 13
               |
103 | 102 | oveq1d 6305 |
. . . . . . . . . . . 12
                           |
104 | 100, 98, 99 | addsubassd 10006 |
. . . . . . . . . . . 12
                           |
105 | 101, 103,
104 | 3eqtrrd 2490 |
. . . . . . . . . . 11
                           |
106 | 97, 105 | breqtrd 4427 |
. . . . . . . . . 10
               |
107 | 14, 75, 79, 91, 106 | lelttrd 9793 |
. . . . . . . . 9
               |
108 | 14, 79, 107 | ltled 9783 |
. . . . . . . 8

              |
109 | 108 | adantr 467 |
. . . . . . 7
 
                             |
110 | 34 | adantr 467 |
. . . . . . . . 9
 
                  
    |
111 | 60 | adantr 467 |
. . . . . . . . . . 11
 
                     |
112 | 52, 34 | resubcld 10047 |
. . . . . . . . . . . 12
                     |
113 | 112 | adantr 467 |
. . . . . . . . . . 11
 
                      
            |
114 | 111, 113 | resubcld 10047 |
. . . . . . . . . 10
 
                                         |
115 | 74 | simp3d 1022 |
. . . . . . . . . . . . . 14
         |
116 | 75, 34, 115 | ltled 9783 |
. . . . . . . . . . . . 13

        |
117 | 38, 36, 41, 10, 1, 75, 34, 116 | fourierdlem7 37976 |
. . . . . . . . . . . 12
                           |
118 | 112, 78, 60, 117 | lesub2dd 10230 |
. . . . . . . . . . 11
            
            
             |
119 | 118 | adantr 467 |
. . . . . . . . . 10
 
                                              
      |
120 | 98 | adantr 467 |
. . . . . . . . . . . . 13
 
                     |
121 | 52 | recnd 9669 |
. . . . . . . . . . . . . 14
             |
122 | 121 | adantr 467 |
. . . . . . . . . . . . 13
 
                           |
123 | 110 | recnd 9669 |
. . . . . . . . . . . . 13
 
                  
    |
124 | 120, 122,
123 | subsubd 10014 |
. . . . . . . . . . . 12
 
                                                   
       
     |
125 | 98, 121 | subcld 9986 |
. . . . . . . . . . . . . 14
                   |
126 | 34 | recnd 9669 |
. . . . . . . . . . . . . 14
    
    |
127 | 125, 126 | addcomd 9835 |
. . . . . . . . . . . . 13
                                                   |
128 | 127 | adantr 467 |
. . . . . . . . . . . 12
 
                                                                 |
129 | 124, 128 | eqtrd 2485 |
. . . . . . . . . . 11
 
                                                                 |
130 | | simpr 463 |
. . . . . . . . . . . . 13
 
                               |
131 | 52 | adantr 467 |
. . . . . . . . . . . . . 14
 
                           |
132 | 111, 131 | sublt0d 10238 |
. . . . . . . . . . . . 13
 
                                                 |
133 | 130, 132 | mpbird 236 |
. . . . . . . . . . . 12
 
                                 |
134 | 111, 131 | resubcld 10047 |
. . . . . . . . . . . . 13
 
                                 |
135 | | ltaddneg 37508 |
. . . . . . . . . . . . 13
                                              
                      
     |
136 | 134, 110,
135 | syl2anc 667 |
. . . . . . . . . . . 12
 
                                    
                      
     |
137 | 133, 136 | mpbid 214 |
. . . . . . . . . . 11
 
                                               |
138 | 129, 137 | eqbrtrd 4423 |
. . . . . . . . . 10
 
                                               |
139 | 80, 114, 110, 119, 138 | lelttrd 9793 |
. . . . . . . . 9
 
                                   |
140 | 84, 33 | ffvelrnd 6023 |
. . . . . . . . . . . 12
    
    ![[,] [,]](_icc.gif)    |
141 | | elicc2 11699 |
. . . . . . . . . . . . 13
 
     
    ![[,] [,]](_icc.gif)      
 
                |
142 | 14, 15, 141 | syl2anc 667 |
. . . . . . . . . . . 12
     
    ![[,] [,]](_icc.gif)      
 
                |
143 | 140, 142 | mpbid 214 |
. . . . . . . . . . 11
     
 
               |
144 | 143 | simp3d 1022 |
. . . . . . . . . 10
    
 
  |
145 | 144 | adantr 467 |
. . . . . . . . 9
 
                  
    |
146 | 80, 110, 62, 139, 145 | ltletrd 9795 |
. . . . . . . 8
 
                             |
147 | 80, 62, 146 | ltled 9783 |
. . . . . . 7
 
                             |
148 | 61, 62, 80, 109, 147 | eliccd 37601 |
. . . . . 6
 
                             ![[,] [,]](_icc.gif)    |
149 | | id 22 |
. . . . . . . . . . . . . . 15
   |
150 | | oveq2 6298 |
. . . . . . . . . . . . . . . . . 18
 
     |
151 | 150 | oveq1d 6305 |
. . . . . . . . . . . . . . . . 17
           |
152 | 151 | fveq2d 5869 |
. . . . . . . . . . . . . . . 16
                   |
153 | 152 | oveq1d 6305 |
. . . . . . . . . . . . . . 15
                       |
154 | 149, 153 | oveq12d 6308 |
. . . . . . . . . . . . . 14
                           |
155 | 154 | adantl 468 |
. . . . . . . . . . . . 13
 
                           |
156 | 36, 75 | resubcld 10047 |
. . . . . . . . . . . . . . . . . 18
     |
157 | 156, 40, 45 | redivcld 10435 |
. . . . . . . . . . . . . . . . 17
       |
158 | 157 | flcld 12034 |
. . . . . . . . . . . . . . . 16
           |
159 | 158 | zred 11040 |
. . . . . . . . . . . . . . 15
           |
160 | 159, 40 | remulcld 9671 |
. . . . . . . . . . . . . 14
             |
161 | 75, 160 | readdcld 9670 |
. . . . . . . . . . . . 13
               |
162 | 2, 155, 75, 161 | fvmptd 5954 |
. . . . . . . . . . . 12
                   |
163 | 162 | oveq1d 6305 |
. . . . . . . . . . 11
                       |
164 | 163 | oveq1d 6305 |
. . . . . . . . . 10
                           |
165 | 160 | recnd 9669 |
. . . . . . . . . . . 12
             |
166 | 100, 165 | pncan2d 9988 |
. . . . . . . . . . 11
                           |
167 | 166 | oveq1d 6305 |
. . . . . . . . . 10
                               |
168 | 159 | recnd 9669 |
. . . . . . . . . . 11
           |
169 | 40 | recnd 9669 |
. . . . . . . . . . 11
   |
170 | 168, 169,
45 | divcan4d 10389 |
. . . . . . . . . 10
                       |
171 | 164, 167,
170 | 3eqtrd 2489 |
. . . . . . . . 9
                   |
172 | 171, 158 | eqeltrd 2529 |
. . . . . . . 8
           |
173 | 78 | recnd 9669 |
. . . . . . . . . . . 12
         |
174 | 173, 169,
45 | divcan1d 10384 |
. . . . . . . . . . 11
                   |
175 | 174 | oveq2d 6306 |
. . . . . . . . . 10
                                               |
176 | 98, 173 | npcand 9990 |
. . . . . . . . . 10
                           |
177 | 175, 176 | eqtrd 2485 |
. . . . . . . . 9
                               |
178 | | ffun 5731 |
. . . . . . . . . . 11
           |
179 | 58, 178 | syl 17 |
. . . . . . . . . 10
   |
180 | | fdm 5733 |
. . . . . . . . . . . 12
               |
181 | 58, 180 | syl 17 |
. . . . . . . . . . 11
       |
182 | 59, 181 | eleqtrrd 2532 |
. . . . . . . . . 10
   |
183 | | fvelrn 6015 |
. . . . . . . . . 10
         |
184 | 179, 182,
183 | syl2anc 667 |
. . . . . . . . 9
       |
185 | 177, 184 | eqeltrd 2529 |
. . . . . . . 8
                           |
186 | | oveq1 6297 |
. . . . . . . . . . 11
                       |
187 | 186 | oveq2d 6306 |
. . . . . . . . . 10
                                                   |
188 | 187 | eleq1d 2513 |
. . . . . . . . 9
                                                     |
189 | 188 | rspcev 3150 |
. . . . . . . 8
                                  
                   |
190 | 172, 185,
189 | syl2anc 667 |
. . . . . . 7
                    |
191 | 190 | adantr 467 |
. . . . . 6
 
                                  |
192 | | oveq1 6297 |
. . . . . . . . 9
                                   |
193 | 192 | eleq1d 2513 |
. . . . . . . 8
                                     |
194 | 193 | rexbidv 2901 |
. . . . . . 7
              

                       |
195 | 194 | elrab 3196 |
. . . . . 6
                ![[,] [,]](_icc.gif)                       ![[,] [,]](_icc.gif) 
                    |
196 | 148, 191,
195 | sylanbrc 670 |
. . . . 5
 
                              ![[,] [,]](_icc.gif)   
      |
197 | | elun2 3602 |
. . . . 5
                ![[,] [,]](_icc.gif)       
               
   ![[,] [,]](_icc.gif)           |
198 | 196, 197 | syl 17 |
. . . 4
 
                              
   ![[,] [,]](_icc.gif)           |
199 | | fourierdlem63.x |
. . . 4
             |
200 | 198, 199,
18 | 3eltr4g 2546 |
. . 3
 
                 |
201 | | elfzelz 11800 |
. . . . . . . . 9
       |
202 | 201 | ad2antlr 733 |
. . . . . . . 8
            
           
      |
203 | | elfzoelz 11920 |
. . . . . . . . . . 11
  ..^
  |
204 | 31, 203 | syl 17 |
. . . . . . . . . 10
   |
205 | 204 | ad2antrr 732 |
. . . . . . . . 9
            
           
   
  |
206 | | simpr 463 |
. . . . . . . . . . 11
                           |
207 | 21 | simprd 465 |
. . . . . . . . . . . . 13

         |
208 | 207 | ad2antrr 732 |
. . . . . . . . . . . 12
                          |
209 | 69 | ad2antrr 732 |
. . . . . . . . . . . 12
                       |
210 | | simplr 762 |
. . . . . . . . . . . 12
                       |
211 | | isorel 6217 |
. . . . . . . . . . . 12
 
           
                  |
212 | 208, 209,
210, 211 | syl12anc 1266 |
. . . . . . . . . . 11
                 
           |
213 | 206, 212 | mpbird 236 |
. . . . . . . . . 10
                   |
214 | 213 | adantrr 723 |
. . . . . . . . 9
            
           
      |
215 | | simpr 463 |
. . . . . . . . . . 11
               
          
    |
216 | 207 | ad2antrr 732 |
. . . . . . . . . . . 12
               
            |
217 | | simplr 762 |
. . . . . . . . . . . 12
               
         |
218 | 33 | ad2antrr 732 |
. . . . . . . . . . . 12
               
   
       |
219 | | isorel 6217 |
. . . . . . . . . . . 12
 
           
         
    
         |
220 | 216, 217,
218, 219 | syl12anc 1266 |
. . . . . . . . . . 11
               
   
 
             |
221 | 215, 220 | mpbird 236 |
. . . . . . . . . 10
               
       |
222 | 221 | adantrl 722 |
. . . . . . . . 9
            
           
   
    |
223 | | btwnnz 11012 |
. . . . . . . . 9
    
  |
224 | 205, 214,
222, 223 | syl3anc 1268 |
. . . . . . . 8
            
           
   
  |
225 | 202, 224 | pm2.65da 580 |
. . . . . . 7
 
                 
         |
226 | 225 | adantlr 721 |
. . . . . 6
                                   
         |
227 | 70 | ad2antrr 732 |
. . . . . . . . 9
                   |
228 | 75 | ad2antrr 732 |
. . . . . . . . 9
               |
229 | 30 | ffvelrnda 6022 |
. . . . . . . . . 10
 
           |
230 | 229 | adantr 467 |
. . . . . . . . 9
                   |
231 | 74 | simp2d 1021 |
. . . . . . . . . 10
    
  |
232 | 231 | ad2antrr 732 |
. . . . . . . . 9
                   |
233 | 106, 199 | syl6breqr 4443 |
. . . . . . . . . . . 12
   |
234 | 233 | adantr 467 |
. . . . . . . . . . 11
 
    
  |
235 | | eqcom 2458 |
. . . . . . . . . . . . 13
    
      |
236 | 235 | biimpri 210 |
. . . . . . . . . . . 12
           |
237 | 236 | adantl 468 |
. . . . . . . . . . 11
 
    
      |
238 | 234, 237 | breqtrd 4427 |
. . . . . . . . . 10
 
    
      |
239 | 238 | adantlr 721 |
. . . . . . . . 9
                   |
240 | 227, 228,
230, 232, 239 | lelttrd 9793 |
. . . . . . . 8
                       |
241 | 240 | adantllr 725 |
. . . . . . 7
                                       |
242 | | simpr 463 |
. . . . . . . . 9
                             |
243 | 199, 139 | syl5eqbr 4436 |
. . . . . . . . . 10
 
                       |
244 | 243 | adantr 467 |
. . . . . . . . 9
                          
    |
245 | 242, 244 | eqbrtrd 4423 |
. . . . . . . 8
                              
    |
246 | 245 | adantlr 721 |
. . . . . . 7
                                    
    |
247 | 241, 246 | jca 535 |
. . . . . 6
                                 
           
     |
248 | 226, 247 | mtand 665 |
. . . . 5
                             |
249 | 248 | nrexdv 2843 |
. . . 4
 
              
            |
250 | | isof1o 6216 |
. . . . . . . . 9
                  |
251 | 207, 250 | syl 17 |
. . . . . . . 8
           |
252 | | f1ofo 5821 |
. . . . . . . 8
        
          |
253 | 251, 252 | syl 17 |
. . . . . . 7
           |
254 | | foelrn 6041 |
. . . . . . 7
          
            |
255 | 253, 254 | sylan 474 |
. . . . . 6
 
             |
256 | 235 | rexbii 2889 |
. . . . . 6
          
            |
257 | 255, 256 | sylib 200 |
. . . . 5
 
             |
258 | 257 | adantlr 721 |
. . . 4
                               |
259 | 249, 258 | mtand 665 |
. . 3
 
              
  |
260 | 200, 259 | pm2.65da 580 |
. 2
                 |
261 | 52, 60, 260 | nltled 9785 |
1
          
      |