Step | Hyp | Ref
| Expression |
1 | | fourierdlem32.l |
. . . 4
  lim    |
2 | 1 | adantr 472 |
. . 3
 
  lim    |
3 | | fourierdlem32.y |
. . . . 5
          |
4 | | iftrue 3878 |
. . . . 5
  
         |
5 | 3, 4 | syl5req 2518 |
. . . 4
   |
6 | 5 | adantl 473 |
. . 3
 
   |
7 | | oveq2 6316 |
. . . . 5
        lim         lim    |
8 | 7 | adantl 473 |
. . . 4
 
        lim         lim    |
9 | | fourierdlem32.f |
. . . . . . 7
           |
10 | | cncff 22003 |
. . . . . . 7
        
          |
11 | 9, 10 | syl 17 |
. . . . . 6
           |
12 | 11 | adantr 472 |
. . . . 5
 
           |
13 | | fourierdlem32.ss |
. . . . . 6
    
      |
14 | 13 | adantr 472 |
. . . . 5
 
           |
15 | | ioosscn 37687 |
. . . . . 6
     |
16 | 15 | a1i 11 |
. . . . 5
 
       |
17 | | eqid 2471 |
. . . . 5
  ℂfld   ℂfld |
18 | | eqid 2471 |
. . . . 5
   ℂfld ↾t             ℂfld
↾t           |
19 | | fourierdlem32.c |
. . . . . . . . 9
   |
20 | 19 | leidd 10201 |
. . . . . . . . 9

  |
21 | | fourierdlem32.cltd |
. . . . . . . . 9
   |
22 | | fourierdlem32.d |
. . . . . . . . . . 11
   |
23 | 22 | rexrd 9708 |
. . . . . . . . . 10
   |
24 | | elico2 11723 |
. . . . . . . . . 10
 
      
    |
25 | 19, 23, 24 | syl2anc 673 |
. . . . . . . . 9
      
    |
26 | 19, 20, 21, 25 | mpbir3and 1213 |
. . . . . . . 8
       |
27 | 26 | adantr 472 |
. . . . . . 7
 
       |
28 | | fourierdlem32.j |
. . . . . . . . 9
   ℂfld
↾t       |
29 | 17 | cnfldtop 21882 |
. . . . . . . . . 10
  ℂfld  |
30 | | ovex 6336 |
. . . . . . . . . . 11
     |
31 | 30 | a1i 11 |
. . . . . . . . . 10
 
       |
32 | | resttop 20253 |
. . . . . . . . . 10
    ℂfld
        ℂfld
↾t        |
33 | 29, 31, 32 | sylancr 676 |
. . . . . . . . 9
 
    ℂfld
↾t        |
34 | 28, 33 | syl5eqel 2553 |
. . . . . . . 8
 
   |
35 | | mnfxr 11437 |
. . . . . . . . . . . . . . . 16
 |
36 | 35 | a1i 11 |
. . . . . . . . . . . . . . 15
 
    
  |
37 | 23 | adantr 472 |
. . . . . . . . . . . . . . 15
 
    
  |
38 | | simpr 468 |
. . . . . . . . . . . . . . . . 17
 
    
      |
39 | | fourierdlem32.a |
. . . . . . . . . . . . . . . . . . 19
   |
40 | 39 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
 
    
  |
41 | | elico2 11723 |
. . . . . . . . . . . . . . . . . 18
 
      
    |
42 | 40, 37, 41 | syl2anc 673 |
. . . . . . . . . . . . . . . . 17
 
    
          |
43 | 38, 42 | mpbid 215 |
. . . . . . . . . . . . . . . 16
 
    
    |
44 | 43 | simp1d 1042 |
. . . . . . . . . . . . . . 15
 
    
  |
45 | 44 | mnfltd 11449 |
. . . . . . . . . . . . . . 15
 
    
  |
46 | 43 | simp3d 1044 |
. . . . . . . . . . . . . . 15
 
    
  |
47 | 36, 37, 44, 45, 46 | eliood 37691 |
. . . . . . . . . . . . . 14
 
    
     |
48 | 43 | simp2d 1043 |
. . . . . . . . . . . . . . 15
 
    
  |
49 | 22 | adantr 472 |
. . . . . . . . . . . . . . . 16
 
    
  |
50 | | fourierdlem32.b |
. . . . . . . . . . . . . . . . 17
   |
51 | 50 | adantr 472 |
. . . . . . . . . . . . . . . 16
 
    
  |
52 | 39, 50, 19, 22, 21, 13 | fourierdlem10 38091 |
. . . . . . . . . . . . . . . . . 18
 
   |
53 | 52 | simprd 470 |
. . . . . . . . . . . . . . . . 17

  |
54 | 53 | adantr 472 |
. . . . . . . . . . . . . . . 16
 
    
  |
55 | 44, 49, 51, 46, 54 | ltletrd 9812 |
. . . . . . . . . . . . . . 15
 
    
  |
56 | 50 | rexrd 9708 |
. . . . . . . . . . . . . . . . 17
   |
57 | 56 | adantr 472 |
. . . . . . . . . . . . . . . 16
 
    
  |
58 | | elico2 11723 |
. . . . . . . . . . . . . . . 16
 
      
    |
59 | 40, 57, 58 | syl2anc 673 |
. . . . . . . . . . . . . . 15
 
    
          |
60 | 44, 48, 55, 59 | mpbir3and 1213 |
. . . . . . . . . . . . . 14
 
    
      |
61 | 47, 60 | elind 3609 |
. . . . . . . . . . . . 13
 
    
           |
62 | | elinel1 3610 |
. . . . . . . . . . . . . . . 16
               |
63 | | elioore 11691 |
. . . . . . . . . . . . . . . 16
      |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . . 15
            |
65 | 64 | adantl 473 |
. . . . . . . . . . . . . 14
 
         
  |
66 | | elinel2 3611 |
. . . . . . . . . . . . . . . . 17
                |
67 | 66 | adantl 473 |
. . . . . . . . . . . . . . . 16
 
         
      |
68 | 39 | adantr 472 |
. . . . . . . . . . . . . . . . 17
 
         
  |
69 | 56 | adantr 472 |
. . . . . . . . . . . . . . . . 17
 
         
  |
70 | 68, 69, 58 | syl2anc 673 |
. . . . . . . . . . . . . . . 16
 
         
          |
71 | 67, 70 | mpbid 215 |
. . . . . . . . . . . . . . 15
 
         
    |
72 | 71 | simp2d 1043 |
. . . . . . . . . . . . . 14
 
         
  |
73 | 62 | adantl 473 |
. . . . . . . . . . . . . . . 16
 
         
     |
74 | 23 | adantr 472 |
. . . . . . . . . . . . . . . . 17
 
         
  |
75 | | elioo2 11702 |
. . . . . . . . . . . . . . . . 17
     
     |
76 | 35, 74, 75 | sylancr 676 |
. . . . . . . . . . . . . . . 16
 
         

        |
77 | 73, 76 | mpbid 215 |
. . . . . . . . . . . . . . 15
 
         
    |
78 | 77 | simp3d 1044 |
. . . . . . . . . . . . . 14
 
         
  |
79 | 68, 74, 41 | syl2anc 673 |
. . . . . . . . . . . . . 14
 
         
          |
80 | 65, 72, 78, 79 | mpbir3and 1213 |
. . . . . . . . . . . . 13
 
         
      |
81 | 61, 80 | impbida 850 |
. . . . . . . . . . . 12
                  |
82 | 81 | eqrdv 2469 |
. . . . . . . . . . 11
                |
83 | | retop 21860 |
. . . . . . . . . . . . 13
     |
84 | 83 | a1i 11 |
. . . . . . . . . . . 12
       |
85 | 30 | a1i 11 |
. . . . . . . . . . . 12
       |
86 | | iooretop 21864 |
. . . . . . . . . . . . 13
        |
87 | 86 | a1i 11 |
. . . . . . . . . . . 12
          |
88 | | elrestr 15405 |
. . . . . . . . . . . 12
         
       
              ↾t        |
89 | 84, 85, 87, 88 | syl3anc 1292 |
. . . . . . . . . . 11
              
↾t        |
90 | 82, 89 | eqeltrd 2549 |
. . . . . . . . . 10
          ↾t        |
91 | 90 | adantr 472 |
. . . . . . . . 9
 
          ↾t        |
92 | | simpr 468 |
. . . . . . . . . 10
 
   |
93 | 92 | oveq1d 6323 |
. . . . . . . . 9
 
           |
94 | 28 | a1i 11 |
. . . . . . . . . . 11
    ℂfld ↾t        |
95 | 29 | a1i 11 |
. . . . . . . . . . . 12
   ℂfld
  |
96 | | icossre 11740 |
. . . . . . . . . . . . 13
 
    
  |
97 | 39, 56, 96 | syl2anc 673 |
. . . . . . . . . . . 12
    
  |
98 | | reex 9648 |
. . . . . . . . . . . . 13
 |
99 | 98 | a1i 11 |
. . . . . . . . . . . 12
   |
100 | | restabs 20258 |
. . . . . . . . . . . 12
    ℂfld
   
     ℂfld
↾t 
↾t         ℂfld
↾t        |
101 | 95, 97, 99, 100 | syl3anc 1292 |
. . . . . . . . . . 11
     ℂfld ↾t  ↾t         ℂfld ↾t        |
102 | 17 | tgioo2 21899 |
. . . . . . . . . . . . . 14
       ℂfld
↾t   |
103 | 102 | eqcomi 2480 |
. . . . . . . . . . . . 13
   ℂfld ↾t       |
104 | 103 | oveq1i 6318 |
. . . . . . . . . . . 12
    ℂfld
↾t 
↾t           ↾t       |
105 | 104 | a1i 11 |
. . . . . . . . . . 11
     ℂfld ↾t  ↾t           ↾t        |
106 | 94, 101, 105 | 3eqtr2d 2511 |
. . . . . . . . . 10
      ↾t        |
107 | 106 | adantr 472 |
. . . . . . . . 9
 
     
↾t        |
108 | 91, 93, 107 | 3eltr4d 2564 |
. . . . . . . 8
 
       |
109 | | isopn3i 20175 |
. . . . . . . 8
                         |
110 | 34, 108, 109 | syl2anc 673 |
. . . . . . 7
 
                   |
111 | 27, 110 | eleqtrrd 2552 |
. . . . . 6
 
               |
112 | | id 22 |
. . . . . . . 8
   |
113 | 112 | eqcomd 2477 |
. . . . . . 7
   |
114 | 113 | adantl 473 |
. . . . . 6
 
   |
115 | | uncom 3569 |
. . . . . . . . . . . 12
                 |
116 | 39 | rexrd 9708 |
. . . . . . . . . . . . 13
   |
117 | | fourierdlem32.altb |
. . . . . . . . . . . . 13
   |
118 | | snunioo 11784 |
. . . . . . . . . . . . 13
                 |
119 | 116, 56, 117, 118 | syl3anc 1292 |
. . . . . . . . . . . 12
               |
120 | 115, 119 | syl5eq 2517 |
. . . . . . . . . . 11
               |
121 | 120 | adantr 472 |
. . . . . . . . . 10
 
               |
122 | 121 | oveq2d 6324 |
. . . . . . . . 9
 
    ℂfld
↾t             ℂfld ↾t        |
123 | 122, 28 | syl6eqr 2523 |
. . . . . . . 8
 
    ℂfld
↾t            |
124 | 123 | fveq2d 5883 |
. . . . . . 7
 
       ℂfld ↾t                 |
125 | | uncom 3569 |
. . . . . . . . 9
                 |
126 | | sneq 3969 |
. . . . . . . . . . 11
  
    |
127 | 126 | eqcomd 2477 |
. . . . . . . . . 10
  
    |
128 | 127 | uneq1d 3578 |
. . . . . . . . 9
           
       |
129 | 125, 128 | syl5eq 2517 |
. . . . . . . 8
                   |
130 | 19 | rexrd 9708 |
. . . . . . . . 9
   |
131 | | snunioo 11784 |
. . . . . . . . 9
                 |
132 | 130, 23, 21, 131 | syl3anc 1292 |
. . . . . . . 8
               |
133 | 129, 132 | sylan9eqr 2527 |
. . . . . . 7
 
               |
134 | 124, 133 | fveq12d 5885 |
. . . . . 6
 
        ℂfld
↾t                                    |
135 | 111, 114,
134 | 3eltr4d 2564 |
. . . . 5
 
        ℂfld
↾t                        |
136 | 12, 14, 16, 17, 18, 135 | limcres 22920 |
. . . 4
 
        lim   lim    |
137 | 8, 136 | eqtr2d 2506 |
. . 3
 
  lim         lim    |
138 | 2, 6, 137 | 3eltr3d 2563 |
. 2
 
        lim    |
139 | | limcresi 22919 |
. . 3
 lim         lim   |
140 | | iffalse 3881 |
. . . . . 6
                |
141 | 3, 140 | syl5eq 2517 |
. . . . 5

      |
142 | 141 | adantl 473 |
. . . 4
 
       |
143 | | ssid 3437 |
. . . . . . . . . . . . 13
 |
144 | 143 | a1i 11 |
. . . . . . . . . . . 12

  |
145 | | eqid 2471 |
. . . . . . . . . . . . 13
   ℂfld ↾t         ℂfld
↾t       |
146 | | unicntop 37433 |
. . . . . . . . . . . . . . . 16
   ℂfld |
147 | 146 | restid 15410 |
. . . . . . . . . . . . . . 15
   ℂfld    ℂfld
↾t    ℂfld  |
148 | 29, 147 | ax-mp 5 |
. . . . . . . . . . . . . 14
   ℂfld ↾t    ℂfld |
149 | 148 | eqcomi 2480 |
. . . . . . . . . . . . 13
  ℂfld    ℂfld ↾t   |
150 | 17, 145, 149 | cncfcn 22019 |
. . . . . . . . . . . 12
     
             ℂfld
↾t        ℂfld   |
151 | 15, 144, 150 | sylancr 676 |
. . . . . . . . . . 11
             ℂfld ↾t        ℂfld   |
152 | 9, 151 | eleqtrd 2551 |
. . . . . . . . . 10
     ℂfld
↾t        ℂfld   |
153 | 17 | cnfldtopon 21881 |
. . . . . . . . . . . 12
  ℂfld TopOn   |
154 | | resttopon 20254 |
. . . . . . . . . . . 12
    ℂfld
TopOn      
   ℂfld ↾t      TopOn        |
155 | 153, 15, 154 | mp2an 686 |
. . . . . . . . . . 11
   ℂfld ↾t      TopOn       |
156 | | cncnp 20373 |
. . . . . . . . . . 11
     ℂfld
↾t      TopOn        ℂfld
TopOn        ℂfld
↾t        ℂfld
                    ℂfld
↾t        ℂfld        |
157 | 155, 153,
156 | mp2an 686 |
. . . . . . . . . 10
     ℂfld ↾t        ℂfld
                    ℂfld
↾t        ℂfld       |
158 | 152, 157 | sylib 201 |
. . . . . . . . 9
                     ℂfld ↾t        ℂfld       |
159 | 158 | simprd 470 |
. . . . . . . 8
            ℂfld
↾t        ℂfld      |
160 | 159 | adantr 472 |
. . . . . . 7
 
            ℂfld ↾t        ℂfld      |
161 | 116 | adantr 472 |
. . . . . . . 8
 
   |
162 | 56 | adantr 472 |
. . . . . . . 8
 
   |
163 | 19 | adantr 472 |
. . . . . . . 8
 
   |
164 | 39 | adantr 472 |
. . . . . . . . 9
 
   |
165 | 52 | simpld 466 |
. . . . . . . . . 10

  |
166 | 165 | adantr 472 |
. . . . . . . . 9
 
   |
167 | 112 | eqcoms 2479 |
. . . . . . . . . . . 12
   |
168 | 167 | necon3bi 2669 |
. . . . . . . . . . 11
   |
169 | 168 | adantl 473 |
. . . . . . . . . 10
 
   |
170 | 169 | necomd 2698 |
. . . . . . . . 9
 
   |
171 | 164, 163,
166, 170 | leneltd 9806 |
. . . . . . . 8
 
   |
172 | 19, 22, 50, 21, 53 | ltletrd 9812 |
. . . . . . . . 9
   |
173 | 172 | adantr 472 |
. . . . . . . 8
 
   |
174 | 161, 162,
163, 171, 173 | eliood 37691 |
. . . . . . 7
 
       |
175 | | fveq2 5879 |
. . . . . . . . 9
      ℂfld ↾t        ℂfld         ℂfld
↾t        ℂfld      |
176 | 175 | eleq2d 2534 |
. . . . . . . 8
 
     ℂfld
↾t        ℂfld   
     ℂfld ↾t        ℂfld       |
177 | 176 | rspccva 3135 |
. . . . . . 7
             ℂfld
↾t        ℂfld   
    
     ℂfld ↾t        ℂfld      |
178 | 160, 174,
177 | syl2anc 673 |
. . . . . 6
 
      ℂfld ↾t        ℂfld      |
179 | 17, 145 | cnplimc 22921 |
. . . . . . 7
     
     
     ℂfld
↾t        ℂfld                  lim      |
180 | 15, 174, 179 | sylancr 676 |
. . . . . 6
 
 
     ℂfld
↾t        ℂfld                  lim      |
181 | 178, 180 | mpbid 215 |
. . . . 5
 
               lim     |
182 | 181 | simprd 470 |
. . . 4
 
      lim    |
183 | 142, 182 | eqeltrd 2549 |
. . 3
 
  lim    |
184 | 139, 183 | sseldi 3416 |
. 2
 
        lim    |
185 | 138, 184 | pm2.61dan 808 |
1
  
     lim    |