Step | Hyp | Ref
| Expression |
1 | | fourierdlem33.5 |
. . . 4
  lim    |
2 | 1 | adantr 467 |
. . 3
 
  lim    |
3 | | fourierdlem33.y |
. . . . 5
          |
4 | | iftrue 3889 |
. . . . 5
  
         |
5 | 3, 4 | syl5req 2500 |
. . . 4
   |
6 | 5 | adantl 468 |
. . 3
 
   |
7 | | oveq2 6303 |
. . . . 5
        lim         lim    |
8 | 7 | adantl 468 |
. . . 4
 
        lim         lim    |
9 | | fourierdlem33.4 |
. . . . . . 7
           |
10 | | cncff 21937 |
. . . . . . 7
        
          |
11 | 9, 10 | syl 17 |
. . . . . 6
           |
12 | 11 | adantr 467 |
. . . . 5
 
           |
13 | | fourierdlem33.ss |
. . . . . 6
    
      |
14 | 13 | adantr 467 |
. . . . 5
 
           |
15 | | ioosscn 37601 |
. . . . . 6
     |
16 | 15 | a1i 11 |
. . . . 5
 
       |
17 | | eqid 2453 |
. . . . 5
  ℂfld   ℂfld |
18 | | fourierdlem33.10 |
. . . . 5
   ℂfld
↾t           |
19 | | fourierdlem33.7 |
. . . . . . . . 9
   |
20 | | fourierdlem33.8 |
. . . . . . . . 9
   |
21 | 19 | leidd 10187 |
. . . . . . . . 9

  |
22 | | fourierdlem33.6 |
. . . . . . . . . . 11
   |
23 | 22 | rexrd 9695 |
. . . . . . . . . 10
   |
24 | | elioc2 11704 |
. . . . . . . . . 10
   
  ![(,] (,]](_ioc.gif) 

    |
25 | 23, 19, 24 | syl2anc 667 |
. . . . . . . . 9
    ![(,] (,]](_ioc.gif)       |
26 | 19, 20, 21, 25 | mpbir3and 1192 |
. . . . . . . 8
   ![(,] (,]](_ioc.gif)    |
27 | 26 | adantr 467 |
. . . . . . 7
 
   ![(,] (,]](_ioc.gif)    |
28 | | eqcom 2460 |
. . . . . . . . 9

  |
29 | 28 | biimpi 198 |
. . . . . . . 8
   |
30 | 29 | adantl 468 |
. . . . . . 7
 
   |
31 | 17 | cnfldtop 21816 |
. . . . . . . . . . 11
  ℂfld  |
32 | | fourierdlem33.1 |
. . . . . . . . . . . . . 14
   |
33 | 32 | rexrd 9695 |
. . . . . . . . . . . . 13
   |
34 | | fourierdlem33.2 |
. . . . . . . . . . . . . 14
   |
35 | 34 | rexrd 9695 |
. . . . . . . . . . . . 13
   |
36 | | fourierdlem33.3 |
. . . . . . . . . . . . 13
   |
37 | | snunioo2 37616 |
. . . . . . . . . . . . 13
             ![(,] (,]](_ioc.gif)    |
38 | 33, 35, 36, 37 | syl3anc 1269 |
. . . . . . . . . . . 12
           ![(,] (,]](_ioc.gif)    |
39 | | ovex 6323 |
. . . . . . . . . . . . 13
  ![(,] (,]](_ioc.gif)   |
40 | 39 | a1i 11 |
. . . . . . . . . . . 12
   ![(,] (,]](_ioc.gif)    |
41 | 38, 40 | eqeltrd 2531 |
. . . . . . . . . . 11
           |
42 | | resttop 20188 |
. . . . . . . . . . 11
    ℂfld
            ℂfld ↾t            |
43 | 31, 41, 42 | sylancr 670 |
. . . . . . . . . 10
    ℂfld
↾t            |
44 | 18, 43 | syl5eqel 2535 |
. . . . . . . . 9
   |
45 | 44 | adantr 467 |
. . . . . . . 8
 
   |
46 | | oveq2 6303 |
. . . . . . . . . . 11
   ![(,] (,]](_ioc.gif)    ![(,] (,]](_ioc.gif)    |
47 | 46 | adantl 468 |
. . . . . . . . . 10
 
   ![(,] (,]](_ioc.gif)    ![(,] (,]](_ioc.gif)    |
48 | 23 | adantr 467 |
. . . . . . . . . . . . . . . 16
 
  ![(,] (,]](_ioc.gif)  
  |
49 | | pnfxr 11419 |
. . . . . . . . . . . . . . . . 17
 |
50 | 49 | a1i 11 |
. . . . . . . . . . . . . . . 16
 
  ![(,] (,]](_ioc.gif)  
  |
51 | | simpr 463 |
. . . . . . . . . . . . . . . . . 18
 
  ![(,] (,]](_ioc.gif)  
  ![(,] (,]](_ioc.gif)    |
52 | 34 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
 
  ![(,] (,]](_ioc.gif)  
  |
53 | | elioc2 11704 |
. . . . . . . . . . . . . . . . . . 19
      ![(,] (,]](_ioc.gif) 

    |
54 | 48, 52, 53 | syl2anc 667 |
. . . . . . . . . . . . . . . . . 18
 
  ![(,] (,]](_ioc.gif)  
   ![(,] (,]](_ioc.gif)  
    |
55 | 51, 54 | mpbid 214 |
. . . . . . . . . . . . . . . . 17
 
  ![(,] (,]](_ioc.gif)  

   |
56 | 55 | simp1d 1021 |
. . . . . . . . . . . . . . . 16
 
  ![(,] (,]](_ioc.gif)  
  |
57 | 55 | simp2d 1022 |
. . . . . . . . . . . . . . . 16
 
  ![(,] (,]](_ioc.gif)  
  |
58 | 56 | ltpnfd 11430 |
. . . . . . . . . . . . . . . 16
 
  ![(,] (,]](_ioc.gif)  
  |
59 | 48, 50, 56, 57, 58 | eliood 37605 |
. . . . . . . . . . . . . . 15
 
  ![(,] (,]](_ioc.gif)  
     |
60 | 32 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
  ![(,] (,]](_ioc.gif)  
  |
61 | 22 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
  ![(,] (,]](_ioc.gif)  
  |
62 | 32, 34, 22, 19, 20, 13 | fourierdlem10 37989 |
. . . . . . . . . . . . . . . . . . 19
 
   |
63 | 62 | simpld 461 |
. . . . . . . . . . . . . . . . . 18

  |
64 | 63 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
  ![(,] (,]](_ioc.gif)  
  |
65 | 60, 61, 56, 64, 57 | lelttrd 9798 |
. . . . . . . . . . . . . . . 16
 
  ![(,] (,]](_ioc.gif)  
  |
66 | 55 | simp3d 1023 |
. . . . . . . . . . . . . . . 16
 
  ![(,] (,]](_ioc.gif)  
  |
67 | 33 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
  ![(,] (,]](_ioc.gif)  
  |
68 | | elioc2 11704 |
. . . . . . . . . . . . . . . . 17
      ![(,] (,]](_ioc.gif) 

    |
69 | 67, 52, 68 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
 
  ![(,] (,]](_ioc.gif)  
   ![(,] (,]](_ioc.gif)  
    |
70 | 56, 65, 66, 69 | mpbir3and 1192 |
. . . . . . . . . . . . . . 15
 
  ![(,] (,]](_ioc.gif)  
  ![(,] (,]](_ioc.gif)    |
71 | 59, 70 | elind 3620 |
. . . . . . . . . . . . . 14
 
  ![(,] (,]](_ioc.gif)  
      ![(,] (,]](_ioc.gif)     |
72 | | elinel1 3621 |
. . . . . . . . . . . . . . . . 17
       ![(,] (,]](_ioc.gif)        |
73 | | elioore 11673 |
. . . . . . . . . . . . . . . . 17
   
  |
74 | 72, 73 | syl 17 |
. . . . . . . . . . . . . . . 16
       ![(,] (,]](_ioc.gif)     |
75 | 74 | adantl 468 |
. . . . . . . . . . . . . . 15
 
      ![(,] (,]](_ioc.gif)   
  |
76 | 23 | adantr 467 |
. . . . . . . . . . . . . . . 16
 
      ![(,] (,]](_ioc.gif)   
  |
77 | 49 | a1i 11 |
. . . . . . . . . . . . . . . 16
 
      ![(,] (,]](_ioc.gif)   
  |
78 | 72 | adantl 468 |
. . . . . . . . . . . . . . . 16
 
      ![(,] (,]](_ioc.gif)   
     |
79 | | ioogtlb 37602 |
. . . . . . . . . . . . . . . 16
        |
80 | 76, 77, 78, 79 | syl3anc 1269 |
. . . . . . . . . . . . . . 15
 
      ![(,] (,]](_ioc.gif)   
  |
81 | | elinel2 3622 |
. . . . . . . . . . . . . . . . . 18
       ![(,] (,]](_ioc.gif)     ![(,] (,]](_ioc.gif)    |
82 | 81 | adantl 468 |
. . . . . . . . . . . . . . . . 17
 
      ![(,] (,]](_ioc.gif)   
  ![(,] (,]](_ioc.gif)    |
83 | 33 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
 
      ![(,] (,]](_ioc.gif)   
  |
84 | 34 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
 
      ![(,] (,]](_ioc.gif)   
  |
85 | 83, 84, 68 | syl2anc 667 |
. . . . . . . . . . . . . . . . 17
 
      ![(,] (,]](_ioc.gif)   
   ![(,] (,]](_ioc.gif)  
    |
86 | 82, 85 | mpbid 214 |
. . . . . . . . . . . . . . . 16
 
      ![(,] (,]](_ioc.gif)   

   |
87 | 86 | simp3d 1023 |
. . . . . . . . . . . . . . 15
 
      ![(,] (,]](_ioc.gif)   
  |
88 | 76, 84, 53 | syl2anc 667 |
. . . . . . . . . . . . . . 15
 
      ![(,] (,]](_ioc.gif)   
   ![(,] (,]](_ioc.gif)  
    |
89 | 75, 80, 87, 88 | mpbir3and 1192 |
. . . . . . . . . . . . . 14
 
      ![(,] (,]](_ioc.gif)   
  ![(,] (,]](_ioc.gif)    |
90 | 71, 89 | impbida 844 |
. . . . . . . . . . . . 13
    ![(,] (,]](_ioc.gif)        ![(,] (,]](_ioc.gif)      |
91 | 90 | eqrdv 2451 |
. . . . . . . . . . . 12
   ![(,] (,]](_ioc.gif)        ![(,] (,]](_ioc.gif)     |
92 | | retop 21794 |
. . . . . . . . . . . . . 14
     |
93 | 92 | a1i 11 |
. . . . . . . . . . . . 13
       |
94 | | iooretop 21798 |
. . . . . . . . . . . . . 14
        |
95 | 94 | a1i 11 |
. . . . . . . . . . . . 13
   
      |
96 | | elrestr 15339 |
. . . . . . . . . . . . 13
        ![(,] (,]](_ioc.gif) 
       
      ![(,] (,]](_ioc.gif)        ↾t   ![(,] (,]](_ioc.gif)     |
97 | 93, 40, 95, 96 | syl3anc 1269 |
. . . . . . . . . . . 12
       ![(,] (,]](_ioc.gif)       
↾t   ![(,] (,]](_ioc.gif)     |
98 | 91, 97 | eqeltrd 2531 |
. . . . . . . . . . 11
   ![(,] (,]](_ioc.gif)       ↾t   ![(,] (,]](_ioc.gif)     |
99 | 98 | adantr 467 |
. . . . . . . . . 10
 
   ![(,] (,]](_ioc.gif)       ↾t   ![(,] (,]](_ioc.gif)     |
100 | 47, 99 | eqeltrd 2531 |
. . . . . . . . 9
 
   ![(,] (,]](_ioc.gif)       ↾t   ![(,] (,]](_ioc.gif)     |
101 | 18 | a1i 11 |
. . . . . . . . . . 11
    ℂfld ↾t            |
102 | 38 | oveq2d 6311 |
. . . . . . . . . . 11
    ℂfld
↾t             ℂfld ↾t   ![(,] (,]](_ioc.gif)     |
103 | 17 | tgioo2 21833 |
. . . . . . . . . . . . . 14
       ℂfld
↾t   |
104 | 103 | eqcomi 2462 |
. . . . . . . . . . . . 13
   ℂfld ↾t       |
105 | 104 | oveq1i 6305 |
. . . . . . . . . . . 12
    ℂfld
↾t 
↾t   ![(,] (,]](_ioc.gif)        ↾t   ![(,] (,]](_ioc.gif)    |
106 | 31 | a1i 11 |
. . . . . . . . . . . . 13
   ℂfld
  |
107 | | iocssre 11721 |
. . . . . . . . . . . . . 14
     ![(,] (,]](_ioc.gif)    |
108 | 33, 34, 107 | syl2anc 667 |
. . . . . . . . . . . . 13
   ![(,] (,]](_ioc.gif) 
  |
109 | | reex 9635 |
. . . . . . . . . . . . . 14
 |
110 | 109 | a1i 11 |
. . . . . . . . . . . . 13
   |
111 | | restabs 20193 |
. . . . . . . . . . . . 13
    ℂfld
  ![(,] (,]](_ioc.gif) 
     ℂfld
↾t 
↾t   ![(,] (,]](_ioc.gif)      ℂfld
↾t   ![(,] (,]](_ioc.gif)     |
112 | 106, 108,
110, 111 | syl3anc 1269 |
. . . . . . . . . . . 12
     ℂfld ↾t  ↾t   ![(,] (,]](_ioc.gif)      ℂfld ↾t   ![(,] (,]](_ioc.gif)     |
113 | 105, 112 | syl5reqr 2502 |
. . . . . . . . . . 11
    ℂfld
↾t   ![(,] (,]](_ioc.gif)        ↾t   ![(,] (,]](_ioc.gif)     |
114 | 101, 102,
113 | 3eqtrrd 2492 |
. . . . . . . . . 10
      ↾t   ![(,] (,]](_ioc.gif)     |
115 | 114 | adantr 467 |
. . . . . . . . 9
 
      ↾t   ![(,] (,]](_ioc.gif)     |
116 | 100, 115 | eleqtrd 2533 |
. . . . . . . 8
 
   ![(,] (,]](_ioc.gif)    |
117 | | isopn3i 20110 |
. . . . . . . 8
    ![(,] (,]](_ioc.gif)            ![(,] (,]](_ioc.gif)     ![(,] (,]](_ioc.gif)    |
118 | 45, 116, 117 | syl2anc 667 |
. . . . . . 7
 
          ![(,] (,]](_ioc.gif)     ![(,] (,]](_ioc.gif)    |
119 | 27, 30, 118 | 3eltr4d 2546 |
. . . . . 6
 
          ![(,] (,]](_ioc.gif)     |
120 | | sneq 3980 |
. . . . . . . . . . 11
  
    |
121 | 120 | eqcomd 2459 |
. . . . . . . . . 10
  
    |
122 | 121 | uneq2d 3590 |
. . . . . . . . 9
                   |
123 | 122 | adantl 468 |
. . . . . . . 8
 
                   |
124 | 19 | rexrd 9695 |
. . . . . . . . . 10
   |
125 | | snunioo2 37616 |
. . . . . . . . . 10
             ![(,] (,]](_ioc.gif)    |
126 | 23, 124, 20, 125 | syl3anc 1269 |
. . . . . . . . 9
           ![(,] (,]](_ioc.gif)    |
127 | 126 | adantr 467 |
. . . . . . . 8
 
           ![(,] (,]](_ioc.gif)    |
128 | 123, 127 | eqtr2d 2488 |
. . . . . . 7
 
   ![(,] (,]](_ioc.gif)            |
129 | 128 | fveq2d 5874 |
. . . . . 6
 
          ![(,] (,]](_ioc.gif)                     |
130 | 119, 129 | eleqtrd 2533 |
. . . . 5
 
                   |
131 | 12, 14, 16, 17, 18, 130 | limcres 22853 |
. . . 4
 
        lim   lim    |
132 | 8, 131 | eqtr2d 2488 |
. . 3
 
  lim         lim    |
133 | 2, 6, 132 | 3eltr3d 2545 |
. 2
 
        lim    |
134 | | limcresi 22852 |
. . 3
 lim         lim   |
135 | | iffalse 3892 |
. . . . . 6
                |
136 | 3, 135 | syl5eq 2499 |
. . . . 5

      |
137 | 136 | adantl 468 |
. . . 4
 
       |
138 | | ssid 3453 |
. . . . . . . . . . . . 13
 |
139 | 138 | a1i 11 |
. . . . . . . . . . . 12

  |
140 | | eqid 2453 |
. . . . . . . . . . . . 13
   ℂfld ↾t         ℂfld
↾t       |
141 | | unicntop 37381 |
. . . . . . . . . . . . . . . 16
   ℂfld |
142 | 141 | restid 15344 |
. . . . . . . . . . . . . . 15
   ℂfld    ℂfld
↾t    ℂfld  |
143 | 31, 142 | ax-mp 5 |
. . . . . . . . . . . . . 14
   ℂfld ↾t    ℂfld |
144 | 143 | eqcomi 2462 |
. . . . . . . . . . . . 13
  ℂfld    ℂfld ↾t   |
145 | 17, 140, 144 | cncfcn 21953 |
. . . . . . . . . . . 12
     
             ℂfld
↾t        ℂfld   |
146 | 15, 139, 145 | sylancr 670 |
. . . . . . . . . . 11
             ℂfld ↾t        ℂfld   |
147 | 9, 146 | eleqtrd 2533 |
. . . . . . . . . 10
     ℂfld
↾t        ℂfld   |
148 | 17 | cnfldtopon 21815 |
. . . . . . . . . . . 12
  ℂfld TopOn   |
149 | 15 | a1i 11 |
. . . . . . . . . . . 12
    
  |
150 | | resttopon 20189 |
. . . . . . . . . . . 12
    ℂfld
TopOn      
   ℂfld ↾t      TopOn        |
151 | 148, 149,
150 | sylancr 670 |
. . . . . . . . . . 11
    ℂfld
↾t      TopOn        |
152 | 148 | a1i 11 |
. . . . . . . . . . 11
   ℂfld
TopOn    |
153 | | cncnp 20308 |
. . . . . . . . . . 11
     ℂfld
↾t      TopOn        ℂfld
TopOn        ℂfld
↾t        ℂfld
                    ℂfld
↾t        ℂfld        |
154 | 151, 152,
153 | syl2anc 667 |
. . . . . . . . . 10
      ℂfld
↾t        ℂfld
                    ℂfld
↾t        ℂfld        |
155 | 147, 154 | mpbid 214 |
. . . . . . . . 9
                     ℂfld ↾t        ℂfld       |
156 | 155 | simprd 465 |
. . . . . . . 8
            ℂfld
↾t        ℂfld      |
157 | 156 | adantr 467 |
. . . . . . 7
 
            ℂfld ↾t        ℂfld      |
158 | 33 | adantr 467 |
. . . . . . . 8
 
   |
159 | 35 | adantr 467 |
. . . . . . . 8
 
   |
160 | 19 | adantr 467 |
. . . . . . . 8
 
   |
161 | 32, 22, 19, 63, 20 | lelttrd 9798 |
. . . . . . . . 9
   |
162 | 161 | adantr 467 |
. . . . . . . 8
 
   |
163 | 34 | adantr 467 |
. . . . . . . . 9
 
   |
164 | 62 | simprd 465 |
. . . . . . . . . 10

  |
165 | 164 | adantr 467 |
. . . . . . . . 9
 
   |
166 | | neqne 37384 |
. . . . . . . . . . 11
   |
167 | 166 | necomd 2681 |
. . . . . . . . . 10
   |
168 | 167 | adantl 468 |
. . . . . . . . 9
 
   |
169 | 160, 163,
165, 168 | leneltd 9794 |
. . . . . . . 8
 
   |
170 | 158, 159,
160, 162, 169 | eliood 37605 |
. . . . . . 7
 
       |
171 | | fveq2 5870 |
. . . . . . . . 9
      ℂfld ↾t        ℂfld         ℂfld
↾t        ℂfld      |
172 | 171 | eleq2d 2516 |
. . . . . . . 8
 
     ℂfld
↾t        ℂfld   
     ℂfld ↾t        ℂfld       |
173 | 172 | rspccva 3151 |
. . . . . . 7
             ℂfld
↾t        ℂfld   
    
     ℂfld ↾t        ℂfld      |
174 | 157, 170,
173 | syl2anc 667 |
. . . . . 6
 
      ℂfld ↾t        ℂfld      |
175 | 17, 140 | cnplimc 22854 |
. . . . . . 7
     
     
     ℂfld
↾t        ℂfld                  lim      |
176 | 15, 170, 175 | sylancr 670 |
. . . . . 6
 
 
     ℂfld
↾t        ℂfld                  lim      |
177 | 174, 176 | mpbid 214 |
. . . . 5
 
               lim     |
178 | 177 | simprd 465 |
. . . 4
 
      lim    |
179 | 137, 178 | eqeltrd 2531 |
. . 3
 
  lim    |
180 | 134, 179 | sseldi 3432 |
. 2
 
        lim    |
181 | 133, 180 | pm2.61dan 801 |
1
  
     lim    |