Step | Hyp | Ref
| Expression |
1 | | fourierdlem113.f |
. 2
       |
2 | | oveq1 6315 |
. . . . . . 7
 
         |
3 | 2 | eqeq1d 2473 |
. . . . . 6
      
      |
4 | | oveq2 6316 |
. . . . . . . 8
               |
5 | 4 | fveq2d 5883 |
. . . . . . 7
                       |
6 | | oveq1 6315 |
. . . . . . . . 9
       |
7 | 6 | fveq2d 5883 |
. . . . . . . 8
               |
8 | 7 | oveq2d 6324 |
. . . . . . 7
   
                   |
9 | 5, 8 | oveq12d 6326 |
. . . . . 6
                                               |
10 | 3, 9 | ifbieq2d 3897 |
. . . . 5
                                                                     
           |
11 | 10 | cbvmptv 4488 |
. . . 4
                                                                                   |
12 | | oveq2 6316 |
. . . . . . . 8
       |
13 | 12 | oveq1d 6323 |
. . . . . . 7
           |
14 | 13 | oveq1d 6323 |
. . . . . 6
                   |
15 | | oveq1 6315 |
. . . . . . . . 9
           |
16 | 15 | oveq1d 6323 |
. . . . . . . 8
               |
17 | 16 | fveq2d 5883 |
. . . . . . 7
                       |
18 | 17 | oveq1d 6323 |
. . . . . 6
                                               |
19 | 14, 18 | ifeq12d 3892 |
. . . . 5
                                                                     
           |
20 | 19 | mpteq2dv 4483 |
. . . 4
                                                                                     |
21 | 11, 20 | syl5eq 2517 |
. . 3
                                                                                     |
22 | 21 | cbvmptv 4488 |
. 2
                                                                                       |
23 | | fourierdlem113.p |
. 2
 
                  
 ..^                |
24 | | fourierdlem113.m |
. 2
   |
25 | | fourierdlem113.q |
. 2
       |
26 | | oveq1 6315 |
. . . . . . . 8
           |
27 | 26 | eleq1d 2533 |
. . . . . . 7
             |
28 | 27 | rexbidv 2892 |
. . . . . 6
  

           |
29 | 28 | cbvrabv 3030 |
. . . . 5
      ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)    
      |
30 | 29 | uneq2i 3576 |
. . . 4
               ![[,] [,]](_icc.gif)                          ![[,] [,]](_icc.gif)    
       |
31 | 30 | fveq2i 5882 |
. . 3
                  ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)    
        |
32 | 31 | oveq1i 6318 |
. 2
                   ![[,] [,]](_icc.gif)                                ![[,] [,]](_icc.gif)    
         |
33 | | oveq1 6315 |
. . . . . . . . . . . 12
       |
34 | 33 | oveq2d 6324 |
. . . . . . . . . . 11
           |
35 | 34 | eleq1d 2533 |
. . . . . . . . . 10
             |
36 | 35 | cbvrexv 3006 |
. . . . . . . . 9
     
       |
37 | 36 | a1i 11 |
. . . . . . . 8
      ![[,] [,]](_icc.gif)     
            |
38 | 37 | rabbiia 3019 |
. . . . . . 7
      ![[,] [,]](_icc.gif)    
           ![[,] [,]](_icc.gif)           |
39 | 38 | uneq2i 3576 |
. . . . . 6
               ![[,] [,]](_icc.gif)    
                     ![[,] [,]](_icc.gif)    
       |
40 | | isoeq5 6232 |
. . . . . 6
                ![[,] [,]](_icc.gif)    
                     ![[,] [,]](_icc.gif)    
     
                        ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)           
                       ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)               |
41 | 39, 40 | ax-mp 5 |
. . . . 5
                        ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)           
                       ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)              |
42 | 41 | a1i 11 |
. . . 4
 
                       ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)           
                       ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)               |
43 | 33 | oveq2d 6324 |
. . . . . . . . . . . . . 14
           |
44 | 43 | eleq1d 2533 |
. . . . . . . . . . . . 13
             |
45 | 44 | cbvrexv 3006 |
. . . . . . . . . . . 12
     
       |
46 | 45 | a1i 11 |
. . . . . . . . . . 11
      ![[,] [,]](_icc.gif)     

           |
47 | 46 | rabbiia 3019 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)           |
48 | 47 | uneq2i 3576 |
. . . . . . . . 9
               ![[,] [,]](_icc.gif)                          ![[,] [,]](_icc.gif)            |
49 | 48 | fveq2i 5882 |
. . . . . . . 8
                  ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)             |
50 | 49 | oveq1i 6318 |
. . . . . . 7
                   ![[,] [,]](_icc.gif)                                ![[,] [,]](_icc.gif)              |
51 | 50 | oveq2i 6319 |
. . . . . 6
                      ![[,] [,]](_icc.gif)                                    ![[,] [,]](_icc.gif)               |
52 | | isoeq4 6231 |
. . . . . 6
                       ![[,] [,]](_icc.gif)                                    ![[,] [,]](_icc.gif)                                      ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)           
                       ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)               |
53 | 51, 52 | ax-mp 5 |
. . . . 5
                        ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)           
                       ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)              |
54 | 53 | a1i 11 |
. . . 4
 
                       ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)           
                       ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)               |
55 | | isoeq1 6228 |
. . . 4
 
                       ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)           
                       ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)               |
56 | 42, 54, 55 | 3bitrd 287 |
. . 3
 
                       ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)           
                       ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)               |
57 | 56 | cbviotav 5559 |
. 2
                          ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)               
                       ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)              |
58 | | fourierdlem113.x |
. 2
   |
59 | | pire 23492 |
. . . . 5
 |
60 | 59 | renegcli 9955 |
. . . 4
  |
61 | 60 | a1i 11 |
. . 3
    |
62 | 59 | a1i 11 |
. . 3
   |
63 | | negpilt0 37580 |
. . . 4
  |
64 | 63 | a1i 11 |
. . 3
    |
65 | | pipos 23494 |
. . . 4
 |
66 | 65 | a1i 11 |
. . 3
   |
67 | | picn 23493 |
. . . . 5
 |
68 | 67 | 2timesi 10753 |
. . . 4
     |
69 | | fourierdlem113.t |
. . . 4
   |
70 | 67, 67 | subnegi 9973 |
. . . 4
      |
71 | 68, 69, 70 | 3eqtr4i 2503 |
. . 3
    |
72 | 23 | fourierdlem2 38083 |
. . . . . . . 8
 
   
                   
 ..^                 |
73 | 24, 72 | syl 17 |
. . . . . . 7
                         
 ..^                 |
74 | 25, 73 | mpbid 215 |
. . . . . 6
                    
 ..^                |
75 | 74 | simpld 466 |
. . . . 5
         |
76 | | elmapi 7511 |
. . . . 5
                 |
77 | 75, 76 | syl 17 |
. . . 4
           |
78 | | fzfid 12224 |
. . . 4
       |
79 | | rnffi 37513 |
. . . 4
              
  |
80 | 77, 78, 79 | syl2anc 673 |
. . 3
   |
81 | 23, 24, 25 | fourierdlem15 38096 |
. . . 4
            ![[,] [,]](_icc.gif)    |
82 | | frn 5747 |
. . . 4
            ![[,] [,]](_icc.gif) 
   ![[,] [,]](_icc.gif)    |
83 | 81, 82 | syl 17 |
. . 3
    ![[,] [,]](_icc.gif)    |
84 | 74 | simprd 470 |
. . . . 5
             
 ..^               |
85 | 84 | simplrd 771 |
. . . 4
       |
86 | | ffun 5742 |
. . . . . 6
            ![[,] [,]](_icc.gif)    |
87 | 81, 86 | syl 17 |
. . . . 5
   |
88 | 24 | nnnn0d 10949 |
. . . . . . . 8
   |
89 | | nn0uz 11217 |
. . . . . . . 8
     |
90 | 88, 89 | syl6eleq 2559 |
. . . . . . 7
       |
91 | | eluzfz2 11833 |
. . . . . . 7
    
      |
92 | 90, 91 | syl 17 |
. . . . . 6
       |
93 | | fdm 5745 |
. . . . . . . 8
            ![[,] [,]](_icc.gif)        |
94 | 81, 93 | syl 17 |
. . . . . . 7
       |
95 | 94 | eqcomd 2477 |
. . . . . 6
       |
96 | 92, 95 | eleqtrd 2551 |
. . . . 5
   |
97 | | fvelrn 6030 |
. . . . 5
         |
98 | 87, 96, 97 | syl2anc 673 |
. . . 4
       |
99 | 85, 98 | eqeltrrd 2550 |
. . 3
   |
100 | | fourierdlem113.e |
. . 3
 
             |
101 | | fourierdlem113.exq |
. . 3
       |
102 | | eqid 2471 |
. . 3
               ![[,] [,]](_icc.gif)                          ![[,] [,]](_icc.gif)            |
103 | | isoeq1 6228 |
. . . . 5
 
                       ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)           
                       ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)               |
104 | 30, 48, 39 | 3eqtr4ri 2504 |
. . . . . 6
               ![[,] [,]](_icc.gif)    
                     ![[,] [,]](_icc.gif)            |
105 | | isoeq5 6232 |
. . . . . 6
                ![[,] [,]](_icc.gif)    
                     ![[,] [,]](_icc.gif)           
                       ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)           
                       ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)               |
106 | 104, 105 | ax-mp 5 |
. . . . 5
                        ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)           
                       ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)              |
107 | 103, 106 | syl6bb 269 |
. . . 4
 
                       ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)           
                       ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)               |
108 | 107 | cbviotav 5559 |
. . 3
                          ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)               
                       ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)              |
109 | | eqid 2471 |
. . 3
      ![(,] (,]](_ioc.gif)                ![(,] (,]](_ioc.gif)           |
110 | 61, 62, 64, 66, 71, 80, 83, 99, 100, 58, 101, 102, 108, 109 | fourierdlem51 38133 |
. 2
                           ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)               |
111 | | fourierdlem113.per |
. 2
 

            |
112 | | ax-resscn 9614 |
. . . 4
 |
113 | 112 | a1i 11 |
. . 3
 
 ..^    |
114 | | ioossre 11721 |
. . . . . . 7
               |
115 | 114 | a1i 11 |
. . . . . 6
              
  |
116 | 1, 115 | fssresd 5762 |
. . . . 5
                                     |
117 | 112 | a1i 11 |
. . . . 5

  |
118 | 116, 117 | fssd 5750 |
. . . 4
                                     |
119 | 118 | adantr 472 |
. . 3
 
 ..^                                      |
120 | 114 | a1i 11 |
. . 3
 
 ..^                  |
121 | 1, 117 | fssd 5750 |
. . . . . . 7
       |
122 | 121 | adantr 472 |
. . . . . 6
 
 ..^        |
123 | | ssid 3437 |
. . . . . . 7
 |
124 | 123 | a1i 11 |
. . . . . 6
 
 ..^    |
125 | | eqid 2471 |
. . . . . . 7
  ℂfld   ℂfld |
126 | 125 | tgioo2 21899 |
. . . . . . 7
       ℂfld
↾t   |
127 | 125, 126 | dvres 22945 |
. . . . . 6
                                                    
                      |
128 | 113, 122,
124, 120, 127 | syl22anc 1293 |
. . . . 5
 
 ..^   
                         
                      |
129 | 128 | dmeqd 5042 |
. . . 4
 
 ..^ 
                           
                      |
130 | | ioontr 37707 |
. . . . . . 7
                                         |
131 | 130 | reseq2i 5108 |
. . . . . 6
         
                                       |
132 | 131 | dmeqi 5041 |
. . . . 5
                                                 |
133 | 132 | a1i 11 |
. . . 4
 
 ..^ 
         
                                        |
134 | | fourierdlem113.dvcn |
. . . . 5
 
 ..^                                        |
135 | | cncff 22003 |
. . . . 5
                                                                           |
136 | | fdm 5745 |
. . . . 5
                                                                       |
137 | 134, 135,
136 | 3syl 18 |
. . . 4
 
 ..^ 
                                  |
138 | 129, 133,
137 | 3eqtrd 2509 |
. . 3
 
 ..^ 
                                  |
139 | | dvcn 22954 |
. . 3
                                                                                                                         |
140 | 113, 119,
120, 138, 139 | syl31anc 1295 |
. 2
 
 ..^                                      |
141 | 120, 113 | sstrd 3428 |
. . 3
 
 ..^                  |
142 | 77 | adantr 472 |
. . . . . 6
 
 ..^            |
143 | | fzofzp1 12037 |
. . . . . . 7
  ..^
        |
144 | 143 | adantl 473 |
. . . . . 6
 
 ..^          |
145 | 142, 144 | ffvelrnd 6038 |
. . . . 5
 
 ..^          |
146 | 145 | rexrd 9708 |
. . . 4
 
 ..^          |
147 | | elfzofz 11962 |
. . . . . 6
  ..^
      |
148 | 147 | adantl 473 |
. . . . 5
 
 ..^        |
149 | 142, 148 | ffvelrnd 6038 |
. . . 4
 
 ..^        |
150 | 74 | simprrd 775 |
. . . . 5
   ..^              |
151 | 150 | r19.21bi 2776 |
. . . 4
 
 ..^              |
152 | 125, 146,
149, 151 | lptioo1cn 37824 |
. . 3
 
 ..^            ℂfld                    |
153 | 116 | adantr 472 |
. . . 4
 
 ..^                                      |
154 | 123 | a1i 11 |
. . . . . . . 8

  |
155 | 117, 121,
154 | dvbss 22935 |
. . . . . . 7
     |
156 | | dvfre 22984 |
. . . . . . . 8
                 |
157 | 1, 154, 156 | syl2anc 673 |
. . . . . . 7
           |
158 | | 0re 9661 |
. . . . . . . . . 10
 |
159 | 60, 158, 59 | lttri 9778 |
. . . . . . . . 9
  
    |
160 | 63, 65, 159 | mp2an 686 |
. . . . . . . 8
  |
161 | 160 | a1i 11 |
. . . . . . 7
    |
162 | 84 | simplld 769 |
. . . . . . 7
        |
163 | 134, 135 | syl 17 |
. . . . . . . 8
 
 ..^                                        |
164 | | fourierdlem113.dvlb |
. . . . . . . 8
 
 ..^                     lim        |
165 | 163, 141,
152, 164, 125 | ellimciota 37791 |
. . . . . . 7
 
 ..^    
                   lim                          lim        |
166 | 149 | rexrd 9708 |
. . . . . . . . 9
 
 ..^        |
167 | 125, 166,
145, 151 | lptioo2cn 37823 |
. . . . . . . 8
 
 ..^              ℂfld                    |
168 | | fourierdlem113.dvub |
. . . . . . . 8
 
 ..^                     lim          |
169 | 163, 141,
167, 168, 125 | ellimciota 37791 |
. . . . . . 7
 
 ..^    
                   lim                            lim          |
170 | 121 | adantr 472 |
. . . . . . . . . 10
 

      |
171 | | zre 10965 |
. . . . . . . . . . . 12
   |
172 | 171 | adantl 473 |
. . . . . . . . . . 11
 

  |
173 | | 2re 10701 |
. . . . . . . . . . . . . . 15
 |
174 | 173, 59 | remulcli 9675 |
. . . . . . . . . . . . . 14
   |
175 | 174 | a1i 11 |
. . . . . . . . . . . . 13
  
  |
176 | 69, 175 | syl5eqel 2553 |
. . . . . . . . . . . 12
   |
177 | 176 | adantr 472 |
. . . . . . . . . . 11
 

  |
178 | 172, 177 | remulcld 9689 |
. . . . . . . . . 10
 

    |
179 | 170 | adantr 472 |
. . . . . . . . . . 11
           |
180 | 177 | adantr 472 |
. . . . . . . . . . 11
       |
181 | | simplr 770 |
. . . . . . . . . . 11
       |
182 | | simpr 468 |
. . . . . . . . . . 11
       |
183 | 111 | adant423 37430 |
. . . . . . . . . . 11
   

     
        |
184 | 179, 180,
181, 182, 183 | fperiodmul 37610 |
. . . . . . . . . 10
                   |
185 | | eqid 2471 |
. . . . . . . . . 10
     |
186 | 170, 178,
184, 185 | fperdvper 37887 |
. . . . . . . . 9
            

                   |
187 | 186 | an32s 821 |
. . . . . . . 8
     
      

                   |
188 | 187 | simpld 466 |
. . . . . . 7
     
         |
189 | 187 | simprd 470 |
. . . . . . 7
     
                   |
190 | | fveq2 5879 |
. . . . . . . . 9
           |
191 | | oveq1 6315 |
. . . . . . . . . 10
       |
192 | 191 | fveq2d 5883 |
. . . . . . . . 9
               |
193 | 190, 192 | oveq12d 6326 |
. . . . . . . 8
                               |
194 | 193 | cbvmptv 4488 |
. . . . . . 7
  ..^                  ..^                 |
195 | | eqid 2471 |
. . . . . . 7
                             |
196 | 155, 157,
61, 62, 161, 71, 24, 77, 162, 85, 134, 165, 169, 188, 189, 194, 195 | fourierdlem71 38153 |
. . . . . 6
                  |
197 | 196 | adantr 472 |
. . . . 5
 
 ..^                   |
198 | | nfv 1769 |
. . . . . . . . 9
    ..^   |
199 | | nfra1 2785 |
. . . . . . . . 9
   
           
 |
200 | 198, 199 | nfan 2031 |
. . . . . . . 8
   
 ..^                  |
201 | 128, 131 | syl6eq 2521 |
. . . . . . . . . . . . . 14
 
 ..^   
                                    |
202 | 201 | fveq1d 5881 |
. . . . . . . . . . . . 13
 
 ..^                                                |
203 | | fvres 5893 |
. . . . . . . . . . . . 13
                                             |
204 | 202, 203 | sylan9eq 2525 |
. . . . . . . . . . . 12
    ..^                                               |
205 | 204 | fveq2d 5883 |
. . . . . . . . . . 11
    ..^                                                       |
206 | 205 | adantlr 729 |
. . . . . . . . . 10
   
 ..^                
                                                     |
207 | | simplr 770 |
. . . . . . . . . . 11
   
 ..^                
               

           
  |
208 | | ssdmres 5132 |
. . . . . . . . . . . . . 14
              
 
                                  |
209 | 137, 208 | sylibr 217 |
. . . . . . . . . . . . 13
 
 ..^                
   |
210 | 209 | ad2antrr 740 |
. . . . . . . . . . . 12
   
 ..^                
                            
    |
211 | | simpr 468 |
. . . . . . . . . . . 12
   
 ..^                
                               |
212 | 210, 211 | sseldd 3419 |
. . . . . . . . . . 11
   
 ..^                
                   |
213 | | rspa 2774 |
. . . . . . . . . . 11
   
           
            
  |
214 | 207, 212,
213 | syl2anc 673 |
. . . . . . . . . 10
   
 ..^                
                        
  |
215 | 206, 214 | eqbrtrd 4416 |
. . . . . . . . 9
   
 ..^                
                                           |
216 | 215 | ex 441 |
. . . . . . . 8
    ..^                
              
     
                   
   |
217 | 200, 216 | ralrimi 2800 |
. . . . . . 7
    ..^                
                                            |
218 | 217 | ex 441 |
. . . . . 6
 
 ..^                                                              |
219 | 218 | reximdv 2857 |
. . . . 5
 
 ..^                                                                |
220 | 197, 219 | mpd 15 |
. . . 4
 
 ..^                                               |
221 | 149, 145,
153, 138, 220 | ioodvbdlimc1 37904 |
. . 3
 
 ..^                   lim        |
222 | 119, 141,
152, 221, 125 | ellimciota 37791 |
. 2
 
 ..^      
               lim                        lim        |
223 | 149, 145,
153, 138, 220 | ioodvbdlimc2 37907 |
. . 3
 
 ..^                   lim          |
224 | 119, 141,
167, 223, 125 | ellimciota 37791 |
. 2
 
 ..^      
               lim                          lim          |
225 | | frel 5744 |
. . . . . . 7
             |
226 | 157, 225 | syl 17 |
. . . . . 6
     |
227 | | resindm 5155 |
. . . . . 6
  
       
            |
228 | 226, 227 | syl 17 |
. . . . 5
       
             |
229 | | inss2 3644 |
. . . . . . 7
   
      |
230 | 229 | a1i 11 |
. . . . . 6
     
  
   |
231 | 157, 230 | fssresd 5762 |
. . . . 5
       
          
      |
232 | 228, 231 | feq1dd 37503 |
. . . 4
              
      |
233 | 232, 117 | fssd 5750 |
. . 3
              
      |
234 | | ioosscn 37687 |
. . . . 5
    |
235 | | ssinss1 3651 |
. . . . 5
   
   
     |
236 | 234, 235 | ax-mp 5 |
. . . 4
   
    |
237 | 236 | a1i 11 |
. . 3
     
    |
238 | | 3simpb 1028 |
. . . . . . . 8
 
 

    |
239 | | simp2 1031 |
. . . . . . . 8
 
 

    |
240 | 170 | adantr 472 |
. . . . . . . . . 10
           |
241 | 177 | adantr 472 |
. . . . . . . . . 10
       |
242 | | simplr 770 |
. . . . . . . . . 10
       |
243 | | simpr 468 |
. . . . . . . . . 10
       |
244 | | eleq1 2537 |
. . . . . . . . . . . . . 14
 
   |
245 | 244 | anbi2d 718 |
. . . . . . . . . . . . 13
  

     |
246 | | oveq1 6315 |
. . . . . . . . . . . . . . 15
       |
247 | 246 | fveq2d 5883 |
. . . . . . . . . . . . . 14
               |
248 | | fveq2 5879 |
. . . . . . . . . . . . . 14
           |
249 | 247, 248 | eqeq12d 2486 |
. . . . . . . . . . . . 13
           
             |
250 | 245, 249 | imbi12d 327 |
. . . . . . . . . . . 12
   
             
               |
251 | 250, 111 | chvarv 2120 |
. . . . . . . . . . 11
 

            |
252 | 251 | adant423 37430 |
. . . . . . . . . 10
   

              |
253 | 240, 241,
242, 243, 252 | fperiodmul 37610 |
. . . . . . . . 9
                   |
254 | 170, 178,
253, 185 | fperdvper 37887 |
. . . . . . . 8
            

     
             |
255 | 238, 239,
254 | syl2anc 673 |
. . . . . . 7
 
 

                          |
256 | 255 | simpld 466 |
. . . . . 6
 
 

        |
257 | | oveq2 6316 |
. . . . . . . . . 10
 
     |
258 | 257 | oveq1d 6323 |
. . . . . . . . 9
           |
259 | 258 | fveq2d 5883 |
. . . . . . . 8
                   |
260 | 259 | oveq1d 6323 |
. . . . . . 7
                       |
261 | 260 | cbvmptv 4488 |
. . . . . 6
                         |
262 | | eqid 2471 |
. . . . . 6
                                         |
263 | 61, 62, 161, 71, 256, 58, 261, 262, 23, 24, 25, 209 | fourierdlem41 38123 |
. . . . 5
   
    
  
           |
264 | 263 | simpld 466 |
. . . 4
      
     |
265 | 125 | cnfldtop 21882 |
. . . . . . . . 9
  ℂfld  |
266 | 265 | a1i 11 |
. . . . . . . 8
 
    
    ℂfld   |
267 | 236 | a1i 11 |
. . . . . . . 8
 
    
     
     |
268 | | mnfxr 11437 |
. . . . . . . . . . . 12
 |
269 | 268 | a1i 11 |
. . . . . . . . . . 11
   |
270 | | rexr 9704 |
. . . . . . . . . . . 12
   |
271 | | mnflt 11448 |
. . . . . . . . . . . 12
   |
272 | 269, 270,
271 | xrltled 37574 |
. . . . . . . . . . 11
   |
273 | | iooss1 11696 |
. . . . . . . . . . 11
           |
274 | 269, 272,
273 | syl2anc 673 |
. . . . . . . . . 10
          |
275 | 274 | 3ad2ant2 1052 |
. . . . . . . . 9
 
    
           |
276 | | simp3 1032 |
. . . . . . . . 9
 
    
     
    |
277 | 275, 276 | ssind 3647 |
. . . . . . . 8
 
    
          
    |
278 | | unicntop 37433 |
. . . . . . . . 9
   ℂfld |
279 | 278 | lpss3 20237 |
. . . . . . . 8
    ℂfld
    
     
              ℂfld       
      ℂfld      
      |
280 | 266, 267,
277, 279 | syl3anc 1292 |
. . . . . . 7
 
    
        ℂfld       
      ℂfld      
      |
281 | 280 | 3adant3l 1288 |
. . . . . 6
 

    
         ℂfld       
      ℂfld      
      |
282 | 270 | 3ad2ant2 1052 |
. . . . . . 7
 

    
     |
283 | 58 | 3ad2ant1 1051 |
. . . . . . 7
 

    
  
  |
284 | | simp3l 1058 |
. . . . . . 7
 

    
  
  |
285 | 125, 282,
283, 284 | lptioo2cn 37823 |
. . . . . 6
 

    
  
      ℂfld          |
286 | 281, 285 | sseldd 3419 |
. . . . 5
 

    
  
      ℂfld      
      |
287 | 286 | rexlimdv3a 2873 |
. . . 4
   
    
        ℂfld      
       |
288 | 264, 287 | mpd 15 |
. . 3
       ℂfld      
      |
289 | 255 | simprd 470 |
. . . 4
 
 

                  |
290 | | oveq2 6316 |
. . . . . . . 8
 
     |
291 | 290 | oveq1d 6323 |
. . . . . . 7
           |
292 | 291 | fveq2d 5883 |
. . . . . 6
                   |
293 | 292 | oveq1d 6323 |
. . . . 5
                       |
294 | 293 | cbvmptv 4488 |
. . . 4
                         |
295 | | id 22 |
. . . . . 6
   |
296 | | fveq2 5879 |
. . . . . 6
          |