Step | Hyp | Ref
| Expression |
1 | | simpr 467 |
. . . . 5
 
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)    |
2 | | fourierdlem101.f |
. . . . . . 7
      ![[,] [,]](_icc.gif)      |
3 | 2 | ffvelrnda 6006 |
. . . . . 6
 
   ![[,] [,]](_icc.gif)         |
4 | | fourierdlem101.n |
. . . . . . . . 9
   |
5 | 4 | adantr 471 |
. . . . . . . 8
 
   ![[,] [,]](_icc.gif)     |
6 | | pire 23425 |
. . . . . . . . . . . 12
 |
7 | 6 | renegcli 9922 |
. . . . . . . . . . 11
  |
8 | | eliccre 37644 |
. . . . . . . . . . 11
  
   ![[,] [,]](_icc.gif)     |
9 | 7, 6, 8 | mp3an12 1358 |
. . . . . . . . . 10
    ![[,] [,]](_icc.gif)    |
10 | 9 | adantl 472 |
. . . . . . . . 9
 
   ![[,] [,]](_icc.gif)     |
11 | | fourierdlem101.x |
. . . . . . . . . 10
   |
12 | 11 | adantr 471 |
. . . . . . . . 9
 
   ![[,] [,]](_icc.gif)     |
13 | 10, 12 | resubcld 10036 |
. . . . . . . 8
 
   ![[,] [,]](_icc.gif)       |
14 | | fourierdlem101.d |
. . . . . . . . 9
                                            |
15 | 14 | dirkerre 38014 |
. . . . . . . 8
                 |
16 | 5, 13, 15 | syl2anc 671 |
. . . . . . 7
 
   ![[,] [,]](_icc.gif)               |
17 | 16 | recnd 9656 |
. . . . . 6
 
   ![[,] [,]](_icc.gif)               |
18 | 3, 17 | mulcld 9650 |
. . . . 5
 
   ![[,] [,]](_icc.gif)                     |
19 | | fourierdlem101.g |
. . . . . 6
    ![[,] [,]](_icc.gif)                    |
20 | 19 | fvmpt2 5941 |
. . . . 5
     ![[,] [,]](_icc.gif)                                         |
21 | 1, 18, 20 | syl2anc 671 |
. . . 4
 
   ![[,] [,]](_icc.gif)                         |
22 | 21 | eqcomd 2458 |
. . 3
 
   ![[,] [,]](_icc.gif)                         |
23 | 22 | itgeq2dv 22751 |
. 2
     ![[,] [,]](_icc.gif)                        ![[,] [,]](_icc.gif)          |
24 | | fourierdlem101.p |
. . 3
 
                  
 ..^                |
25 | | fveq2 5848 |
. . . . 5
           |
26 | 25 | oveq1d 6291 |
. . . 4
               |
27 | 26 | cbvmptv 4467 |
. . 3
                         |
28 | | fourierdlem101.6 |
. . 3
   |
29 | | fourierdlem101.q |
. . 3
       |
30 | 18, 19 | fmptd 6030 |
. . 3
      ![[,] [,]](_icc.gif)      |
31 | 19 | reseq1i 5079 |
. . . . 5
                     ![[,] [,]](_icc.gif)                                   |
32 | | ioossicc 11710 |
. . . . . . 7
                    ![[,] [,]](_icc.gif)         |
33 | 7 | a1i 11 |
. . . . . . . . . 10
    |
34 | 33 | rexrd 9677 |
. . . . . . . . 9
    |
35 | 34 | adantr 471 |
. . . . . . . 8
 
 ..^     |
36 | 6 | a1i 11 |
. . . . . . . . . 10
   |
37 | 36 | rexrd 9677 |
. . . . . . . . 9
   |
38 | 37 | adantr 471 |
. . . . . . . 8
 
 ..^    |
39 | 24, 28, 29 | fourierdlem15 38041 |
. . . . . . . . 9
            ![[,] [,]](_icc.gif)    |
40 | 39 | adantr 471 |
. . . . . . . 8
 
 ..^             ![[,] [,]](_icc.gif)    |
41 | | simpr 467 |
. . . . . . . 8
 
 ..^   ..^   |
42 | 35, 38, 40, 41 | fourierdlem8 38034 |
. . . . . . 7
 
 ..^        ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)    |
43 | 32, 42 | syl5ss 3411 |
. . . . . 6
 
 ..^                   ![[,] [,]](_icc.gif)    |
44 | 43 | resmptd 5134 |
. . . . 5
 
 ..^       ![[,] [,]](_icc.gif)                                                                    |
45 | 31, 44 | syl5eq 2498 |
. . . 4
 
 ..^                                                    |
46 | 2 | adantr 471 |
. . . . . . 7
 
 ..^       ![[,] [,]](_icc.gif)      |
47 | 46, 43 | feqresmpt 5902 |
. . . . . 6
 
 ..^                                        |
48 | | fourierdlem101.fcn |
. . . . . 6
 
 ..^                                      |
49 | 47, 48 | eqeltrrd 2531 |
. . . . 5
 
 ..^                                          |
50 | | eqidd 2453 |
. . . . . . . . . 10
    ..^                                       |
51 | | simpr 467 |
. . . . . . . . . . . 12
   
 ..^ 
              
                      
                        |
52 | | eqidd 2453 |
. . . . . . . . . . . . . 14
    ..^                                                       |
53 | | oveq1 6283 |
. . . . . . . . . . . . . . 15
       |
54 | 53 | adantl 472 |
. . . . . . . . . . . . . 14
   
 ..^ 
              
       |
55 | | simpr 467 |
. . . . . . . . . . . . . 14
    ..^                                 |
56 | | elioore 11656 |
. . . . . . . . . . . . . . . . 17
                 |
57 | 56 | adantl 472 |
. . . . . . . . . . . . . . . 16
 
                 |
58 | 11 | adantr 471 |
. . . . . . . . . . . . . . . 16
 
                 |
59 | 57, 58 | resubcld 10036 |
. . . . . . . . . . . . . . 15
 
                   |
60 | 59 | adantlr 726 |
. . . . . . . . . . . . . 14
    ..^                     |
61 | 52, 54, 55, 60 | fvmptd 5938 |
. . . . . . . . . . . . 13
    ..^                                           |
62 | 61 | adantr 471 |
. . . . . . . . . . . 12
   
 ..^ 
              
                      
                          |
63 | 51, 62 | eqtrd 2486 |
. . . . . . . . . . 11
   
 ..^ 
              
                      
    |
64 | 63 | fveq2d 5852 |
. . . . . . . . . 10
   
 ..^ 
              
                      
                    |
65 | | elioore 11656 |
. . . . . . . . . . . . . . 15
                 |
66 | 65 | adantl 472 |
. . . . . . . . . . . . . 14
 
                 |
67 | 11 | adantr 471 |
. . . . . . . . . . . . . 14
 
                 |
68 | 66, 67 | resubcld 10036 |
. . . . . . . . . . . . 13
 
                   |
69 | 68 | adantlr 726 |
. . . . . . . . . . . 12
    ..^                     |
70 | | eqid 2452 |
. . . . . . . . . . . 12
                                     |
71 | 69, 70 | fmptd 6030 |
. . . . . . . . . . 11
 
 ..^                                        |
72 | 71 | ffvelrnda 6006 |
. . . . . . . . . 10
    ..^                                         |
73 | 4 | ad2antrr 737 |
. . . . . . . . . . 11
    ..^                   |
74 | 14 | dirkerre 38014 |
. . . . . . . . . . 11
                 |
75 | 73, 60, 74 | syl2anc 671 |
. . . . . . . . . 10
    ..^                             |
76 | 50, 64, 72, 75 | fvmptd 5938 |
. . . . . . . . 9
    ..^                                                                 |
77 | 76 | eqcomd 2458 |
. . . . . . . 8
    ..^                                                                 |
78 | 77 | mpteq2dva 4461 |
. . . . . . 7
 
 ..^                                                                                  |
79 | 53 | fveq2d 5852 |
. . . . . . . . 9
                       |
80 | 79 | cbvmptv 4467 |
. . . . . . . 8
                                                     |
81 | 80 | a1i 11 |
. . . . . . 7
 
 ..^                                                        |
82 | 14 | dirkerre 38014 |
. . . . . . . . . . 11
 
           |
83 | 4, 82 | sylan 478 |
. . . . . . . . . 10
 

          |
84 | | eqid 2452 |
. . . . . . . . . 10
                     |
85 | 83, 84 | fmptd 6030 |
. . . . . . . . 9
                 |
86 | 85 | adantr 471 |
. . . . . . . 8
 
 ..^                  |
87 | | fcompt 6044 |
. . . . . . . 8
                                                                                                                                         |
88 | 86, 71, 87 | syl2anc 671 |
. . . . . . 7
 
 ..^                                                                                      |
89 | 78, 81, 88 | 3eqtr4d 2496 |
. . . . . 6
 
 ..^                                                            |
90 | | eqid 2452 |
. . . . . . . 8
         |
91 | | simpr 467 |
. . . . . . . . . . . . 13
 

  |
92 | 11 | recnd 9656 |
. . . . . . . . . . . . . 14
   |
93 | 92 | adantr 471 |
. . . . . . . . . . . . 13
 

  |
94 | 91, 93 | negsubd 9979 |
. . . . . . . . . . . 12
 

       |
95 | 94 | eqcomd 2458 |
. . . . . . . . . . 11
 

       |
96 | 95 | mpteq2dva 4461 |
. . . . . . . . . 10
            |
97 | 92 | negcld 9960 |
. . . . . . . . . . 11
    |
98 | | eqid 2452 |
. . . . . . . . . . . 12
           |
99 | 98 | addccncf 21959 |
. . . . . . . . . . 11
 
           |
100 | 97, 99 | syl 17 |
. . . . . . . . . 10
            |
101 | 96, 100 | eqeltrd 2530 |
. . . . . . . . 9
           |
102 | 101 | adantr 471 |
. . . . . . . 8
 
 ..^            |
103 | | ioossre 11686 |
. . . . . . . . . 10
               |
104 | | ax-resscn 9583 |
. . . . . . . . . 10
 |
105 | 103, 104 | sstri 3409 |
. . . . . . . . 9
               |
106 | 105 | a1i 11 |
. . . . . . . 8
 
 ..^                  |
107 | 104 | a1i 11 |
. . . . . . . 8
 
 ..^    |
108 | 90, 102, 106, 107, 69 | cncfmptssg 37789 |
. . . . . . 7
 
 ..^                                        |
109 | 83 | recnd 9656 |
. . . . . . . . . 10
 

          |
110 | 109, 84 | fmptd 6030 |
. . . . . . . . 9
                 |
111 | | ssid 3419 |
. . . . . . . . . 10
 |
112 | 14 | dirkerf 38016 |
. . . . . . . . . . . . 13
           |
113 | 4, 112 | syl 17 |
. . . . . . . . . . . 12
           |
114 | 113 | feqmptd 5901 |
. . . . . . . . . . 11
                 |
115 | 14 | dirkercncf 38026 |
. . . . . . . . . . . 12
           |
116 | 4, 115 | syl 17 |
. . . . . . . . . . 11
           |
117 | 114, 116 | eqeltrrd 2531 |
. . . . . . . . . 10
                 |
118 | | cncffvrn 21941 |
. . . . . . . . . 10
 
                                               |
119 | 111, 117,
118 | sylancr 674 |
. . . . . . . . 9
                                 |
120 | 110, 119 | mpbird 240 |
. . . . . . . 8
                 |
121 | 120 | adantr 471 |
. . . . . . 7
 
 ..^                  |
122 | 108, 121 | cncfco 21950 |
. . . . . 6
 
 ..^                                                    |
123 | 89, 122 | eqeltrd 2530 |
. . . . 5
 
 ..^                                                |
124 | 49, 123 | mulcncf 22409 |
. . . 4
 
 ..^                                                      |
125 | 45, 124 | eqeltrd 2530 |
. . 3
 
 ..^                                      |
126 | | cncff 21936 |
. . . . . . . 8
 
                                                                     |
127 | 48, 126 | syl 17 |
. . . . . . 7
 
 ..^                                      |
128 | 113 | adantr 471 |
. . . . . . . . . . 11
 
                         |
129 | | elioore 11656 |
. . . . . . . . . . . . 13
                 |
130 | 129 | adantl 472 |
. . . . . . . . . . . 12
 
                 |
131 | 11 | adantr 471 |
. . . . . . . . . . . 12
 
                 |
132 | 130, 131 | resubcld 10036 |
. . . . . . . . . . 11
 
                   |
133 | 128, 132 | ffvelrnd 6007 |
. . . . . . . . . 10
 
                           |
134 | 133 | recnd 9656 |
. . . . . . . . 9
 
                           |
135 | | eqid 2452 |
. . . . . . . . 9
                                                     |
136 | 134, 135 | fmptd 6030 |
. . . . . . . 8
                                               |
137 | 136 | adantr 471 |
. . . . . . 7
 
 ..^                                                |
138 | | eqid 2452 |
. . . . . . 7
                                                                                                                                         |
139 | | fourierdlem101.r |
. . . . . . 7
 
 ..^                   lim        |
140 | | oveq1 6283 |
. . . . . . . . . . . . . 14
               |
141 | 140 | fveq2d 5852 |
. . . . . . . . . . . . 13
                               |
142 | 141 | eqcomd 2458 |
. . . . . . . . . . . 12
                               |
143 | 142 | adantl 472 |
. . . . . . . . . . 11
   
 ..^ 
                                                      |
144 | | eqidd 2453 |
. . . . . . . . . . . 12
   
 ..^ 
                      
                                                           |
145 | | oveq1 6283 |
. . . . . . . . . . . . . 14
       |
146 | 145 | fveq2d 5852 |
. . . . . . . . . . . . 13
                       |
147 | 146 | adantl 472 |
. . . . . . . . . . . 12
      ..^ 
                      
    
                       |
148 | | elsn 3950 |
. . . . . . . . . . . . . . 15
             |
149 | 148 | notbii 302 |
. . . . . . . . . . . . . 14
      
      |
150 | | elunnel2 37357 |
. . . . . . . . . . . . . 14
                                               |
151 | 149, 150 | sylan2br 483 |
. . . . . . . . . . . . 13
                                             |
152 | 151 | adantll 725 |
. . . . . . . . . . . 12
   
 ..^ 
                      
                     |
153 | 113 | ad2antrr 737 |
. . . . . . . . . . . . . 14
    ..^                                   |
154 | | simpr 467 |
. . . . . . . . . . . . . . . . . 18
    ..^             |
155 | 9 | ssriv 3404 |
. . . . . . . . . . . . . . . . . . . 20
   ![[,] [,]](_icc.gif)   |
156 | | fzossfz 11931 |
. . . . . . . . . . . . . . . . . . . . . 22
 ..^      |
157 | 156, 41 | sseldi 3398 |
. . . . . . . . . . . . . . . . . . . . 21
 
 ..^        |
158 | 40, 157 | ffvelrnd 6007 |
. . . . . . . . . . . . . . . . . . . 20
 
 ..^         ![[,] [,]](_icc.gif)    |
159 | 155, 158 | sseldi 3398 |
. . . . . . . . . . . . . . . . . . 19
 
 ..^        |
160 | 159 | adantr 471 |
. . . . . . . . . . . . . . . . . 18
    ..^             |
161 | 154, 160 | eqeltrd 2530 |
. . . . . . . . . . . . . . . . 17
    ..^         |
162 | 161 | adantlr 726 |
. . . . . . . . . . . . . . . 16
   
 ..^ 
                              |
163 | 152, 65 | syl 17 |
. . . . . . . . . . . . . . . 16
   
 ..^ 
                      
       |
164 | 162, 163 | pm2.61dan 805 |
. . . . . . . . . . . . . . 15
    ..^                           |
165 | 11 | ad2antrr 737 |
. . . . . . . . . . . . . . 15
    ..^                           |
166 | 164, 165 | resubcld 10036 |
. . . . . . . . . . . . . 14
    ..^                             |
167 | 153, 166 | ffvelrnd 6007 |
. . . . . . . . . . . . 13
    ..^                                     |
168 | 167 | adantr 471 |
. . . . . . . . . . . 12
   
 ..^ 
                      
                 |
169 | 144, 147,
152, 168 | fvmptd 5938 |
. . . . . . . . . . 11
   
 ..^ 
                      
                                               |
170 | 143, 169 | ifeqda 3882 |
. . . . . . . . . 10
    ..^                                                                                          |
171 | 170 | mpteq2dva 4461 |
. . . . . . . . 9
 
 ..^                                                                                                                   |
172 | 113 | adantr 471 |
. . . . . . . . . . . . . . 15
 
 ..^            |
173 | | simpr 467 |
. . . . . . . . . . . . . . . . . . . 20
 
                                               |
174 | | elun 3542 |
. . . . . . . . . . . . . . . . . . . 20
                                               |
175 | 173, 174 | sylib 201 |
. . . . . . . . . . . . . . . . . . 19
 
                                               |
176 | 175 | adantlr 726 |
. . . . . . . . . . . . . . . . . 18
    ..^                                                 |
177 | | elsni 3961 |
. . . . . . . . . . . . . . . . . . . . . . 23
             |
178 | 177 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . 22
    ..^               |
179 | 159 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . 22
    ..^               |
180 | 178, 179 | eqeltrd 2530 |
. . . . . . . . . . . . . . . . . . . . 21
    ..^           |
181 | 180 | ex 440 |
. . . . . . . . . . . . . . . . . . . 20
 
 ..^            |
182 | 181 | adantr 471 |
. . . . . . . . . . . . . . . . . . 19
    ..^                                   |
183 | | pm3.44 518 |
. . . . . . . . . . . . . . . . . . 19
                                                     |
184 | 129, 182,
183 | sylancr 674 |
. . . . . . . . . . . . . . . . . 18
    ..^                                                   |
185 | 176, 184 | mpd 15 |
. . . . . . . . . . . . . . . . 17
    ..^                           |
186 | 11 | ad2antrr 737 |
. . . . . . . . . . . . . . . . 17
    ..^                           |
187 | 185, 186 | resubcld 10036 |
. . . . . . . . . . . . . . . 16
    ..^                             |
188 | | eqid 2452 |
. . . . . . . . . . . . . . . 16
                                                     |
189 | 187, 188 | fmptd 6030 |
. . . . . . . . . . . . . . 15
 
 ..^                                                        |
190 | | fcompt 6044 |
. . . . . . . . . . . . . . 15
                                                                                                                                                               |
191 | 172, 189,
190 | syl2anc 671 |
. . . . . . . . . . . . . 14
 
 ..^                                                                                                  |
192 | | eqidd 2453 |
. . . . . . . . . . . . . . . . 17
    ..^                                                                               |
193 | 145 | adantl 472 |
. . . . . . . . . . . . . . . . 17
   
 ..^ 
                              |
194 | | simpr 467 |
. . . . . . . . . . . . . . . . 17
    ..^                                                 |
195 | 192, 193,
194, 166 | fvmptd 5938 |
. . . . . . . . . . . . . . . 16
    ..^                                                           |
196 | 195 | fveq2d 5852 |
. . . . . . . . . . . . . . 15
    ..^                                                                           |
197 | 196 | mpteq2dva 4461 |
. . . . . . . . . . . . . 14
 
 ..^                                                                                                    |
198 | 191, 197 | eqtr2d 2487 |
. . . . . . . . . . . . 13
 
 ..^                                                                      |
199 | | eqid 2452 |
. . . . . . . . . . . . . . . 16
         |
200 | | simpr 467 |
. . . . . . . . . . . . . . . . . . . . 21
 

  |
201 | 92 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . 21
 

  |
202 | 200, 201 | negsubd 9979 |
. . . . . . . . . . . . . . . . . . . 20
 

       |
203 | 202 | eqcomd 2458 |
. . . . . . . . . . . . . . . . . . 19
 

       |
204 | 203 | mpteq2dva 4461 |
. . . . . . . . . . . . . . . . . 18
            |
205 | | eqid 2452 |
. . . . . . . . . . . . . . . . . . . 20
           |
206 | 205 | addccncf 21959 |
. . . . . . . . . . . . . . . . . . 19
 
           |
207 | 97, 206 | syl 17 |
. . . . . . . . . . . . . . . . . 18
            |
208 | 204, 207 | eqeltrd 2530 |
. . . . . . . . . . . . . . . . 17
           |
209 | 208 | adantr 471 |
. . . . . . . . . . . . . . . 16
 
 ..^            |
210 | 159 | recnd 9656 |
. . . . . . . . . . . . . . . . . 18
 
 ..^        |
211 | 210 | snssd 4086 |
. . . . . . . . . . . . . . . . 17
 
 ..^          |
212 | 106, 211 | unssd 3578 |
. . . . . . . . . . . . . . . 16
 
 ..^                          |
213 | 199, 209,
212, 107, 187 | cncfmptssg 37789 |
. . . . . . . . . . . . . . 15
 
 ..^                                                        |
214 | 114, 120 | eqeltrd 2530 |
. . . . . . . . . . . . . . . 16
           |
215 | 214 | adantr 471 |
. . . . . . . . . . . . . . 15
 
 ..^            |
216 | 213, 215 | cncfco 21950 |
. . . . . . . . . . . . . 14
 
 ..^                                                              |
217 | | eqid 2452 |
. . . . . . . . . . . . . . . 16
  ℂfld   ℂfld |
218 | | eqid 2452 |
. . . . . . . . . . . . . . . 16
   ℂfld ↾t                           ℂfld ↾t                         |
219 | 217 | cnfldtop 21815 |
. . . . . . . . . . . . . . . . . 18
  ℂfld  |
220 | | unicntop 37367 |
. . . . . . . . . . . . . . . . . . 19
   ℂfld |
221 | 220 | restid 15343 |
. . . . . . . . . . . . . . . . . 18
   ℂfld    ℂfld
↾t    ℂfld  |
222 | 219, 221 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
   ℂfld ↾t    ℂfld |
223 | 222 | eqcomi 2461 |
. . . . . . . . . . . . . . . 16
  ℂfld    ℂfld ↾t   |
224 | 217, 218,
223 | cncfcn 21952 |
. . . . . . . . . . . . . . 15
                                                       ℂfld
↾t                          ℂfld   |
225 | 212, 111,
224 | sylancl 673 |
. . . . . . . . . . . . . 14
 
 ..^                                ℂfld
↾t                          ℂfld   |
226 | 216, 225 | eleqtrd 2532 |
. . . . . . . . . . . . 13
 
 ..^                                      ℂfld
↾t                          ℂfld   |
227 | 198, 226 | eqeltrd 2530 |
. . . . . . . . . . . 12
 
 ..^                                        ℂfld ↾t                          ℂfld   |
228 | 217 | cnfldtopon 21814 |
. . . . . . . . . . . . . 14
  ℂfld TopOn   |
229 | | resttopon 20188 |
. . . . . . . . . . . . . 14
    ℂfld
TopOn                            ℂfld ↾t                        TopOn                          |
230 | 228, 212,
229 | sylancr 674 |
. . . . . . . . . . . . 13
 
 ..^     ℂfld ↾t                        TopOn                          |
231 | | cncnp 20307 |
. . . . . . . . . . . . 13
     ℂfld
↾t                        TopOn                          ℂfld
TopOn                                          ℂfld ↾t                          ℂfld
                                                                                                                            ℂfld ↾t                          ℂfld        |
232 | 230, 228,
231 | sylancl 673 |
. . . . . . . . . . . 12
 
 ..^                                         ℂfld
↾t                          ℂfld                                                                                                                             ℂfld
↾t                          ℂfld        |
233 | 227, 232 | mpbid 215 |
. . . . . . . . . . 11
 
 ..^                                                                                                                              ℂfld
↾t                          ℂfld       |
234 | 233 | simprd 469 |
. . . . . . . . . 10
 
 ..^                                                                 ℂfld ↾t                          ℂfld      |
235 | | eqidd 2453 |
. . . . . . . . . . . . 13
 
 ..^            |
236 | | elsncg 3959 |
. . . . . . . . . . . . . 14
                           |
237 | 159, 236 | syl 17 |
. . . . . . . . . . . . 13
 
 ..^            
           |
238 | 235, 237 | mpbird 240 |
. . . . . . . . . . . 12
 
 ..^              |
239 | 238 | olcd 399 |
. . . . . . . . . . 11
 
 ..^                                  |
240 | | elun 3542 |
. . . . . . . . . . 11
                                                           |
241 | 239, 240 | sylibr 217 |
. . . . . . . . . 10
 
 ..^                              |
242 | | fveq2 5848 |
. . . . . . . . . . . 12
          ℂfld ↾t                          ℂfld         ℂfld
↾t                          ℂfld          |
243 | 242 | eleq2d 2515 |
. . . . . . . . . . 11
                                             ℂfld
↾t                          ℂfld                                           ℂfld ↾t                          ℂfld           |
244 | 243 | rspccva 3117 |
. . . . . . . . . 10
                                                                 ℂfld ↾t                          ℂfld   
                                                                  ℂfld
↾t                          ℂfld          |
245 | 234, 241,
244 | syl2anc 671 |
. . . . . . . . 9
 
 ..^                                         ℂfld
↾t                          ℂfld          |
246 | 171, 245 | eqeltrd 2530 |
. . . . . . . 8
 
 ..^                                                                                    ℂfld ↾t                          ℂfld          |
247 | | eqid 2452 |
. . . . . . . . 9
                                                                                                                                                           |
248 | 218, 217,
247, 137, 106, 210 | ellimc 22840 |
. . . . . . . 8
 
 ..^                                            lim                                                                                        ℂfld ↾t                          ℂfld           |
249 | 246, 248 | mpbird 240 |
. . . . . . 7
 
 ..^                                           lim        |
250 | 127, 137,
138, 139, 249 | mullimcf 37745 |
. . . . . 6
 
 ..^                                                                                       lim        |
251 | | fvres 5862 |
. . . . . . . . . 10
                                         |
252 | 251 | adantl 472 |
. . . . . . . . 9
    ..^                                           |
253 | 252 | oveq1d 6291 |
. . . . . . . 8
    ..^                                                                                                           |
254 | 253 | mpteq2dva 4461 |
. . . . . . 7
 
 ..^                   
                                                                                                        |
255 | 254 | oveq1d 6291 |
. . . . . 6
 
 ..^                                                                       lim                                                           lim        |
256 | 250, 255 | eleqtrd 2532 |
. . . . 5
 
 ..^                                                                       lim        |
257 | | eqidd 2453 |
. . . . . . . . 9
    ..^                                                                       |
258 | | simpr 467 |
. . . . . . . . . . 11
   
 ..^ 
              
   |
259 | 258 | oveq1d 6291 |
. . . . . . . . . 10
   
 ..^ 
              
       |
260 | 259 | fveq2d 5852 |
. . . . . . . . 9
   
 ..^ 
              
                       |
261 | | simpr 467 |
. . . . . . . . 9
    ..^                                 |
262 | 113 | ad2antrr 737 |
. . . . . . . . . 10
    ..^                           |
263 | 262, 69 | ffvelrnd 6007 |
. . . . . . . . 9
    ..^                             |
264 | 257, 260,
261, 263 | fvmptd 5938 |
. . . . . . . 8
    ..^                                                           |
265 | 264 | oveq2d 6292 |
. . . . . . 7
    ..^                                                                       |
266 | 265 | mpteq2dva 4461 |
. . . . . 6
 
 ..^                                                                                        |
267 | 266 | oveq1d 6291 |
. . . . 5
 
 ..^                                                       lim                                       lim        |
268 | 256, 267 | eleqtrd 2532 |
. . . 4
 
 ..^                                                   lim        |
269 | 45 | eqcomd 2458 |
. . . . 5
 
 ..^                                                    |
270 | 269 | oveq1d 6291 |
. . . 4
 
 ..^                                   lim                       lim        |
271 | 268, 270 | eleqtrd 2532 |
. . 3
 
 ..^                                   lim        |
272 | | fourierdlem101.l |
. . . . 5
 
 ..^                   lim          |
273 | | iftrue 3855 |
. . . . . . . . . . 11
                                                                                  |
274 | | oveq1 6283 |
. . . . . . . . . . . . 13
                   |
275 | 274 | eqcomd 2458 |
. . . . . . . . . . . 12
                   |
276 | 275 | fveq2d 5852 |
. . . . . . . . . . 11
                                   |
277 | 273< |