Step | Hyp | Ref
| Expression |
1 | | fourierdlem113.f |
. 2
       |
2 | | oveq1 6297 |
. . . . . . 7
 
         |
3 | 2 | eqeq1d 2453 |
. . . . . 6
      
      |
4 | | oveq2 6298 |
. . . . . . . 8
               |
5 | 4 | fveq2d 5869 |
. . . . . . 7
                       |
6 | | oveq1 6297 |
. . . . . . . . 9
       |
7 | 6 | fveq2d 5869 |
. . . . . . . 8
               |
8 | 7 | oveq2d 6306 |
. . . . . . 7
   
                   |
9 | 5, 8 | oveq12d 6308 |
. . . . . 6
                                               |
10 | 3, 9 | ifbieq2d 3906 |
. . . . 5
                                                                     
           |
11 | 10 | cbvmptv 4495 |
. . . 4
                                                                                   |
12 | | oveq2 6298 |
. . . . . . . 8
       |
13 | 12 | oveq1d 6305 |
. . . . . . 7
           |
14 | 13 | oveq1d 6305 |
. . . . . 6
                   |
15 | | oveq1 6297 |
. . . . . . . . 9
           |
16 | 15 | oveq1d 6305 |
. . . . . . . 8
               |
17 | 16 | fveq2d 5869 |
. . . . . . 7
                       |
18 | 17 | oveq1d 6305 |
. . . . . 6
                                               |
19 | 14, 18 | ifeq12d 3901 |
. . . . 5
                                                                     
           |
20 | 19 | mpteq2dv 4490 |
. . . 4
                                                                                     |
21 | 11, 20 | syl5eq 2497 |
. . 3
                                                                                     |
22 | 21 | cbvmptv 4495 |
. 2
                                                                                       |
23 | | fourierdlem113.p |
. 2
 
                  
 ..^                |
24 | | fourierdlem113.m |
. 2
   |
25 | | fourierdlem113.q |
. 2
       |
26 | | oveq1 6297 |
. . . . . . . 8
           |
27 | 26 | eleq1d 2513 |
. . . . . . 7
             |
28 | 27 | rexbidv 2901 |
. . . . . 6
  

           |
29 | 28 | cbvrabv 3044 |
. . . . 5
      ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)    
      |
30 | 29 | uneq2i 3585 |
. . . 4
               ![[,] [,]](_icc.gif)                          ![[,] [,]](_icc.gif)    
       |
31 | 30 | fveq2i 5868 |
. . 3
                  ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)    
        |
32 | 31 | oveq1i 6300 |
. 2
                   ![[,] [,]](_icc.gif)                                ![[,] [,]](_icc.gif)    
         |
33 | | oveq1 6297 |
. . . . . . . . . . . 12
       |
34 | 33 | oveq2d 6306 |
. . . . . . . . . . 11
           |
35 | 34 | eleq1d 2513 |
. . . . . . . . . 10
             |
36 | 35 | cbvrexv 3020 |
. . . . . . . . 9
     
       |
37 | 36 | a1i 11 |
. . . . . . . 8
      ![[,] [,]](_icc.gif)     
            |
38 | 37 | rabbiia 3033 |
. . . . . . 7
      ![[,] [,]](_icc.gif)    
           ![[,] [,]](_icc.gif)           |
39 | 38 | uneq2i 3585 |
. . . . . 6
               ![[,] [,]](_icc.gif)    
                     ![[,] [,]](_icc.gif)    
       |
40 | | isoeq5 6214 |
. . . . . 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 6306 |
. . . . . . . . . . . . . 14
           |
44 | 43 | eleq1d 2513 |
. . . . . . . . . . . . 13
             |
45 | 44 | cbvrexv 3020 |
. . . . . . . . . . . 12
     
       |
46 | 45 | a1i 11 |
. . . . . . . . . . 11
      ![[,] [,]](_icc.gif)     

           |
47 | 46 | rabbiia 3033 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)           |
48 | 47 | uneq2i 3585 |
. . . . . . . . 9
               ![[,] [,]](_icc.gif)                          ![[,] [,]](_icc.gif)            |
49 | 48 | fveq2i 5868 |
. . . . . . . 8
                  ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)             |
50 | 49 | oveq1i 6300 |
. . . . . . 7
                   ![[,] [,]](_icc.gif)                                ![[,] [,]](_icc.gif)              |
51 | 50 | oveq2i 6301 |
. . . . . 6
                      ![[,] [,]](_icc.gif)                                    ![[,] [,]](_icc.gif)               |
52 | | isoeq4 6213 |
. . . . . 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 6210 |
. . . 4
 
                       ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)           
                       ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)               |
56 | 42, 54, 55 | 3bitrd 283 |
. . 3
 
                       ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)           
                       ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)               |
57 | 56 | cbviotav 5552 |
. 2
                          ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)               
                       ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)              |
58 | | fourierdlem113.x |
. 2
   |
59 | | pire 23413 |
. . . . 5
 |
60 | 59 | renegcli 9935 |
. . . 4
  |
61 | 60 | a1i 11 |
. . 3
    |
62 | 59 | a1i 11 |
. . 3
   |
63 | | negpilt0 37490 |
. . . 4
  |
64 | 63 | a1i 11 |
. . 3
    |
65 | | pipos 23415 |
. . . 4
 |
66 | 65 | a1i 11 |
. . 3
   |
67 | | picn 23414 |
. . . . 5
 |
68 | 67 | 2timesi 10730 |
. . . 4
     |
69 | | fourierdlem113.t |
. . . 4
   |
70 | 67, 67 | subnegi 9953 |
. . . 4
      |
71 | 68, 69, 70 | 3eqtr4i 2483 |
. . 3
    |
72 | 23 | fourierdlem2 37971 |
. . . . . . . 8
 
   
                   
 ..^                 |
73 | 24, 72 | syl 17 |
. . . . . . 7
                         
 ..^                 |
74 | 25, 73 | mpbid 214 |
. . . . . 6
                    
 ..^                |
75 | 74 | simpld 461 |
. . . . 5
         |
76 | | elmapi 7493 |
. . . . 5
                 |
77 | 75, 76 | syl 17 |
. . . 4
           |
78 | | fzfid 12186 |
. . . 4
       |
79 | | rnffi 37440 |
. . . 4
              
  |
80 | 77, 78, 79 | syl2anc 667 |
. . 3
   |
81 | 23, 24, 25 | fourierdlem15 37984 |
. . . 4
            ![[,] [,]](_icc.gif)    |
82 | | frn 5735 |
. . . 4
            ![[,] [,]](_icc.gif) 
   ![[,] [,]](_icc.gif)    |
83 | 81, 82 | syl 17 |
. . 3
    ![[,] [,]](_icc.gif)    |
84 | 74 | simprd 465 |
. . . . 5
             
 ..^               |
85 | 84 | simplrd 763 |
. . . 4
       |
86 | | ffun 5731 |
. . . . . 6
            ![[,] [,]](_icc.gif)    |
87 | 81, 86 | syl 17 |
. . . . 5
   |
88 | 24 | nnnn0d 10925 |
. . . . . . . 8
   |
89 | | nn0uz 11193 |
. . . . . . . 8
     |
90 | 88, 89 | syl6eleq 2539 |
. . . . . . 7
       |
91 | | eluzfz2 11807 |
. . . . . . 7
    
      |
92 | 90, 91 | syl 17 |
. . . . . 6
       |
93 | | fdm 5733 |
. . . . . . . 8
            ![[,] [,]](_icc.gif)        |
94 | 81, 93 | syl 17 |
. . . . . . 7
       |
95 | 94 | eqcomd 2457 |
. . . . . 6
       |
96 | 92, 95 | eleqtrd 2531 |
. . . . 5
   |
97 | | fvelrn 6015 |
. . . . 5
         |
98 | 87, 96, 97 | syl2anc 667 |
. . . 4
       |
99 | 85, 98 | eqeltrrd 2530 |
. . 3
   |
100 | | fourierdlem113.e |
. . 3
 
             |
101 | | fourierdlem113.exq |
. . 3
       |
102 | | eqid 2451 |
. . 3
               ![[,] [,]](_icc.gif)                          ![[,] [,]](_icc.gif)            |
103 | | isoeq1 6210 |
. . . . 5
 
                       ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)           
                       ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)               |
104 | 30, 48, 39 | 3eqtr4ri 2484 |
. . . . . 6
               ![[,] [,]](_icc.gif)    
                     ![[,] [,]](_icc.gif)            |
105 | | isoeq5 6214 |
. . . . . 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 265 |
. . . 4
 
                       ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)           
                       ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)               |
108 | 107 | cbviotav 5552 |
. . 3
                          ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)               
                       ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)              |
109 | | eqid 2451 |
. . 3
      ![(,] (,]](_ioc.gif)                ![(,] (,]](_ioc.gif)           |
110 | 61, 62, 64, 66, 71, 80, 83, 99, 100, 58, 101, 102, 108, 109 | fourierdlem51 38021 |
. 2
                           ![[,] [,]](_icc.gif)                              ![[,] [,]](_icc.gif)               |
111 | | fourierdlem113.per |
. 2
 

            |
112 | | ax-resscn 9596 |
. . . 4
 |
113 | 112 | a1i 11 |
. . 3
 
 ..^    |
114 | | ioossre 11696 |
. . . . . . 7
               |
115 | 114 | a1i 11 |
. . . . . 6
              
  |
116 | 1, 115 | fssresd 5750 |
. . . . 5
                                     |
117 | 112 | a1i 11 |
. . . . 5

  |
118 | 116, 117 | fssd 5738 |
. . . 4
                                     |
119 | 118 | adantr 467 |
. . 3
 
 ..^                                      |
120 | 114 | a1i 11 |
. . 3
 
 ..^                  |
121 | 1, 117 | fssd 5738 |
. . . . . . 7
       |
122 | 121 | adantr 467 |
. . . . . 6
 
 ..^        |
123 | | ssid 3451 |
. . . . . . 7
 |
124 | 123 | a1i 11 |
. . . . . 6
 
 ..^    |
125 | | eqid 2451 |
. . . . . . 7
  ℂfld   ℂfld |
126 | 125 | tgioo2 21821 |
. . . . . . 7
       ℂfld
↾t   |
127 | 125, 126 | dvres 22866 |
. . . . . 6
                                                    
                      |
128 | 113, 122,
124, 120, 127 | syl22anc 1269 |
. . . . 5
 
 ..^   
                         
                      |
129 | 128 | dmeqd 5037 |
. . . 4
 
 ..^ 
                           
                      |
130 | | ioontr 37611 |
. . . . . . 7
                                         |
131 | 130 | reseq2i 5102 |
. . . . . 6
         
                                       |
132 | 131 | dmeqi 5036 |
. . . . 5
                                                 |
133 | 132 | a1i 11 |
. . . 4
 
 ..^ 
         
                                        |
134 | | fourierdlem113.dvcn |
. . . . 5
 
 ..^                                        |
135 | | cncff 21925 |
. . . . 5
                                                                           |
136 | | fdm 5733 |
. . . . 5
                                                                       |
137 | 134, 135,
136 | 3syl 18 |
. . . 4
 
 ..^ 
                                  |
138 | 129, 133,
137 | 3eqtrd 2489 |
. . 3
 
 ..^ 
                                  |
139 | | dvcn 22875 |
. . 3
                                                                                                                         |
140 | 113, 119,
120, 138, 139 | syl31anc 1271 |
. 2
 
 ..^                                      |
141 | 120, 113 | sstrd 3442 |
. . 3
 
 ..^                  |
142 | 77 | adantr 467 |
. . . . . 6
 
 ..^            |
143 | | fzofzp1 12008 |
. . . . . . 7
  ..^
        |
144 | 143 | adantl 468 |
. . . . . 6
 
 ..^          |
145 | 142, 144 | ffvelrnd 6023 |
. . . . 5
 
 ..^          |
146 | 145 | rexrd 9690 |
. . . 4
 
 ..^          |
147 | | elfzofz 11935 |
. . . . . 6
  ..^
      |
148 | 147 | adantl 468 |
. . . . 5
 
 ..^        |
149 | 142, 148 | ffvelrnd 6023 |
. . . 4
 
 ..^        |
150 | 74 | simprrd 767 |
. . . . 5
   ..^              |
151 | 150 | r19.21bi 2757 |
. . . 4
 
 ..^              |
152 | 125, 146,
149, 151 | lptioo1cn 37727 |
. . 3
 
 ..^            ℂfld                    |
153 | 116 | adantr 467 |
. . . 4
 
 ..^                                      |
154 | 123 | a1i 11 |
. . . . . . . 8

  |
155 | 117, 121,
154 | dvbss 22856 |
. . . . . . 7
     |
156 | | dvfre 22905 |
. . . . . . . 8
                 |
157 | 1, 154, 156 | syl2anc 667 |
. . . . . . 7
           |
158 | | 0re 9643 |
. . . . . . . . . 10
 |
159 | 60, 158, 59 | lttri 9760 |
. . . . . . . . 9
  
    |
160 | 63, 65, 159 | mp2an 678 |
. . . . . . . 8
  |
161 | 160 | a1i 11 |
. . . . . . 7
    |
162 | 84 | simplld 761 |
. . . . . . 7
        |
163 | 134, 135 | syl 17 |
. . . . . . . 8
 
 ..^                                        |
164 | | fourierdlem113.dvlb |
. . . . . . . 8
 
 ..^                     lim        |
165 | 163, 141,
152, 164, 125 | ellimciota 37694 |
. . . . . . 7
 
 ..^    
                   lim                          lim        |
166 | 149 | rexrd 9690 |
. . . . . . . . 9
 
 ..^        |
167 | 125, 166,
145, 151 | lptioo2cn 37726 |
. . . . . . . 8
 
 ..^              ℂfld                    |
168 | | fourierdlem113.dvub |
. . . . . . . 8
 
 ..^                     lim          |
169 | 163, 141,
167, 168, 125 | ellimciota 37694 |
. . . . . . 7
 
 ..^    
                   lim                            lim          |
170 | 121 | adantr 467 |
. . . . . . . . . 10
 

      |
171 | | zre 10941 |
. . . . . . . . . . . 12
   |
172 | 171 | adantl 468 |
. . . . . . . . . . 11
 

  |
173 | | 2re 10679 |
. . . . . . . . . . . . . . 15
 |
174 | 173, 59 | remulcli 9657 |
. . . . . . . . . . . . . 14
   |
175 | 174 | a1i 11 |
. . . . . . . . . . . . 13
  
  |
176 | 69, 175 | syl5eqel 2533 |
. . . . . . . . . . . 12
   |
177 | 176 | adantr 467 |
. . . . . . . . . . 11
 

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

    |
179 | 170 | adantr 467 |
. . . . . . . . . . 11
           |
180 | 177 | adantr 467 |
. . . . . . . . . . 11
       |
181 | | simplr 762 |
. . . . . . . . . . 11
       |
182 | | simpr 463 |
. . . . . . . . . . 11
       |
183 | 111 | adant423 37367 |
. . . . . . . . . . 11
   

     
        |
184 | 179, 180,
181, 182, 183 | fperiodmul 37522 |
. . . . . . . . . 10
                   |
185 | | eqid 2451 |
. . . . . . . . . 10
     |
186 | 170, 178,
184, 185 | fperdvper 37790 |
. . . . . . . . 9
            

                   |
187 | 186 | an32s 813 |
. . . . . . . 8
     
      

                   |
188 | 187 | simpld 461 |
. . . . . . 7
     
         |
189 | 187 | simprd 465 |
. . . . . . 7
     
                   |
190 | | fveq2 5865 |
. . . . . . . . 9
           |
191 | | oveq1 6297 |
. . . . . . . . . 10
       |
192 | 191 | fveq2d 5869 |
. . . . . . . . 9
               |
193 | 190, 192 | oveq12d 6308 |
. . . . . . . 8
                               |
194 | 193 | cbvmptv 4495 |
. . . . . . 7
  ..^                  ..^                 |
195 | | eqid 2451 |
. . . . . . 7
                             |
196 | 155, 157,
61, 62, 161, 71, 24, 77, 162, 85, 134, 165, 169, 188, 189, 194, 195 | fourierdlem71 38041 |
. . . . . 6
                  |
197 | 196 | adantr 467 |
. . . . 5
 
 ..^                   |
198 | | nfv 1761 |
. . . . . . . . 9
    ..^   |
199 | | nfra1 2769 |
. . . . . . . . 9
   
           
 |
200 | 198, 199 | nfan 2011 |
. . . . . . . 8
   
 ..^                  |
201 | 128, 131 | syl6eq 2501 |
. . . . . . . . . . . . . 14
 
 ..^   
                                    |
202 | 201 | fveq1d 5867 |
. . . . . . . . . . . . 13
 
 ..^                                                |
203 | | fvres 5879 |
. . . . . . . . . . . . 13
                                             |
204 | 202, 203 | sylan9eq 2505 |
. . . . . . . . . . . 12
    ..^                                               |
205 | 204 | fveq2d 5869 |
. . . . . . . . . . 11
    ..^                                                       |
206 | 205 | adantlr 721 |
. . . . . . . . . 10
   
 ..^                
                                                     |
207 | | simplr 762 |
. . . . . . . . . . 11
   
 ..^                
               

           
  |
208 | | ssdmres 5126 |
. . . . . . . . . . . . . 14
              
 
                                  |
209 | 137, 208 | sylibr 216 |
. . . . . . . . . . . . 13
 
 ..^                
   |
210 | 209 | ad2antrr 732 |
. . . . . . . . . . . 12
   
 ..^                
                            
    |
211 | | simpr 463 |
. . . . . . . . . . . 12
   
 ..^                
                               |
212 | 210, 211 | sseldd 3433 |
. . . . . . . . . . 11
   
 ..^                
                   |
213 | | rspa 2755 |
. . . . . . . . . . 11
   
           
            
  |
214 | 207, 212,
213 | syl2anc 667 |
. . . . . . . . . 10
   
 ..^                
                        
  |
215 | 206, 214 | eqbrtrd 4423 |
. . . . . . . . 9
   
 ..^                
                                           |
216 | 215 | ex 436 |
. . . . . . . 8
    ..^                
              
     
                   
   |
217 | 200, 216 | ralrimi 2788 |
. . . . . . 7
    ..^                
                                            |
218 | 217 | ex 436 |
. . . . . 6
 
 ..^                                                              |
219 | 218 | reximdv 2861 |
. . . . 5
 
 ..^                                                                |
220 | 197, 219 | mpd 15 |
. . . 4
 
 ..^                                               |
221 | 149, 145,
153, 138, 220 | ioodvbdlimc1 37807 |
. . 3
 
 ..^                   lim        |
222 | 119, 141,
152, 221, 125 | ellimciota 37694 |
. 2
 
 ..^      
               lim                        lim        |
223 | 149, 145,
153, 138, 220 | ioodvbdlimc2 37810 |
. . 3
 
 ..^                   lim          |
224 | 119, 141,
167, 223, 125 | ellimciota 37694 |
. 2
 
 ..^      
               lim                          lim          |
225 | | frel 5732 |
. . . . . . 7
             |
226 | 157, 225 | syl 17 |
. . . . . 6
     |
227 | | resindm 5149 |
. . . . . 6
  
       
            |
228 | 226, 227 | syl 17 |
. . . . 5
       
             |
229 | | inss2 3653 |
. . . . . . 7
   
      |
230 | 229 | a1i 11 |
. . . . . 6
     
  
   |
231 | 157, 230 | fssresd 5750 |
. . . . 5
       
          
      |
232 | 228, 231 | feq1dd 37430 |
. . . 4
              
      |
233 | 232, 117 | fssd 5738 |
. . 3
              
      |
234 | | ioosscn 37591 |
. . . . 5
    |
235 | | ssinss1 3660 |
. . . . 5
   
   
     |
236 | 234, 235 | ax-mp 5 |
. . . 4
   
    |
237 | 236 | a1i 11 |
. . 3
     
    |
238 | | 3simpb 1006 |
. . . . . . . 8
 
 

    |
239 | | simp2 1009 |
. . . . . . . 8
 
 

    |
240 | 170 | adantr 467 |
. . . . . . . . . 10
           |
241 | 177 | adantr 467 |
. . . . . . . . . 10
       |
242 | | simplr 762 |
. . . . . . . . . 10
       |
243 | | simpr 463 |
. . . . . . . . . 10
       |
244 | | eleq1 2517 |
. . . . . . . . . . . . . 14
 
   |
245 | 244 | anbi2d 710 |
. . . . . . . . . . . . 13
  

     |
246 | | oveq1 6297 |
. . . . . . . . . . . . . . 15
       |
247 | 246 | fveq2d 5869 |
. . . . . . . . . . . . . 14
               |
248 | | fveq2 5865 |
. . . . . . . . . . . . . 14
           |
249 | 247, 248 | eqeq12d 2466 |
. . . . . . . . . . . . 13
           
             |
250 | 245, 249 | imbi12d 322 |
. . . . . . . . . . . 12
   
             
               |
251 | 250, 111 | chvarv 2107 |
. . . . . . . . . . 11
 

            |
252 | 251 | adant423 37367 |
. . . . . . . . . 10
   

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

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

                          |
256 | 255 | simpld 461 |
. . . . . 6
 
 

        |
257 | | oveq2 6298 |
. . . . . . . . . 10
 
     |
258 | 257 | oveq1d 6305 |
. . . . . . . . 9
           |
259 | 258 | fveq2d 5869 |
. . . . . . . 8
                   |
260 | 259 | oveq1d 6305 |
. . . . . . 7
                       |
261 | 260 | cbvmptv 4495 |
. . . . . 6
                         |
262 | | eqid 2451 |
. . . . . 6
                                         |
263 | 61, 62, 161, 71, 256, 58, 261, 262, 23, 24, 25, 209 | fourierdlem41 38011 |
. . . . 5
   
    
  
           |
264 | 263 | simpld 461 |
. . . 4
      
     |
265 | 125 | cnfldtop 21804 |
. . . . . . . . 9
  ℂfld  |
266 | 265 | a1i 11 |
. . . . . . . 8
 
    
    ℂfld   |
267 | 236 | a1i 11 |
. . . . . . . 8
 
    
     
     |
268 | | mnfxr 11414 |
. . . . . . . . . . . 12
 |
269 | 268 | a1i 11 |
. . . . . . . . . . 11
   |
270 | | rexr 9686 |
. . . . . . . . . . . 12
   |
271 | | mnflt 11425 |
. . . . . . . . . . . 12
   |
272 | 269, 270,
271 | xrltled 37484 |
. . . . . . . . . . 11
   |
273 | | iooss1 11671 |
. . . . . . . . . . 11
           |
274 | 269, 272,
273 | syl2anc 667 |
. . . . . . . . . 10
          |
275 | 274 | 3ad2ant2 1030 |
. . . . . . . . 9
 
    
           |
276 | | simp3 1010 |
. . . . . . . . 9
 
    
     
    |
277 | 275, 276 | ssind 3656 |
. . . . . . . 8
 
    
          
    |
278 | | unicntop 37371 |
. . . . . . . . 9
   ℂfld |
279 | 278 | lpss3 20160 |
. . . . . . . 8
    ℂfld
    
     
              ℂfld       
      ℂfld      
      |
280 | 266, 267,
277, 279 | syl3anc 1268 |
. . . . . . 7
 
    
        ℂfld       
      ℂfld      
      |
281 | 280 | 3adant3l 1264 |
. . . . . 6
 

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

    
     |
283 | 58 | 3ad2ant1 1029 |
. . . . . . 7
 

    
  
  |
284 | | simp3l 1036 |
. . . . . . 7
 

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

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

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

                  |
290 | | oveq2 6298 |
. . . . . . . 8
 
     |
291 | 290 | oveq1d 6305 |
. . . . . . 7
           |
292 | 291 | fveq2d 5869 |
. . . . . 6
                   |
293 | 292 | oveq1d 6305 |
. . . . 5
                       |
294 | 293 | cbvmptv 4495 |
. . . 4
                         |
295 | | id 22 |
. . . . . 6
   |
296 | | fveq2 5865 |
. . . . . 6
          |