Step | Hyp | Ref
| Expression |
1 | | fourierdlem32.l |
. . . 4
lim |
2 | 1 | adantr 481 |
. . 3
lim |
3 | | fourierdlem32.y |
. . . . 5
|
4 | | iftrue 4092 |
. . . . 5
|
5 | 3, 4 | syl5req 2669 |
. . . 4
|
6 | 5 | adantl 482 |
. . 3
|
7 | | oveq2 6658 |
. . . . 5
lim lim |
8 | 7 | adantl 482 |
. . . 4
lim lim |
9 | | fourierdlem32.f |
. . . . . . 7
|
10 | | cncff 22696 |
. . . . . . 7
|
11 | 9, 10 | syl 17 |
. . . . . 6
|
12 | 11 | adantr 481 |
. . . . 5
|
13 | | fourierdlem32.ss |
. . . . . 6
|
14 | 13 | adantr 481 |
. . . . 5
|
15 | | ioosscn 39716 |
. . . . . 6
|
16 | 15 | a1i 11 |
. . . . 5
|
17 | | eqid 2622 |
. . . . 5
ℂfld ℂfld |
18 | | eqid 2622 |
. . . . 5
ℂfld ↾t ℂfld
↾t |
19 | | fourierdlem32.c |
. . . . . . . . 9
|
20 | 19 | leidd 10594 |
. . . . . . . . 9
|
21 | | fourierdlem32.cltd |
. . . . . . . . 9
|
22 | | fourierdlem32.d |
. . . . . . . . . . 11
|
23 | 22 | rexrd 10089 |
. . . . . . . . . 10
|
24 | | elico2 12237 |
. . . . . . . . . 10
|
25 | 19, 23, 24 | syl2anc 693 |
. . . . . . . . 9
|
26 | 19, 20, 21, 25 | mpbir3and 1245 |
. . . . . . . 8
|
27 | 26 | adantr 481 |
. . . . . . 7
|
28 | | fourierdlem32.j |
. . . . . . . . 9
ℂfld
↾t |
29 | 17 | cnfldtop 22587 |
. . . . . . . . . 10
ℂfld |
30 | | ovex 6678 |
. . . . . . . . . . 11
|
31 | 30 | a1i 11 |
. . . . . . . . . 10
|
32 | | resttop 20964 |
. . . . . . . . . 10
ℂfld
ℂfld
↾t |
33 | 29, 31, 32 | sylancr 695 |
. . . . . . . . 9
ℂfld
↾t |
34 | 28, 33 | syl5eqel 2705 |
. . . . . . . 8
|
35 | | mnfxr 10096 |
. . . . . . . . . . . . . . . 16
|
36 | 35 | a1i 11 |
. . . . . . . . . . . . . . 15
|
37 | 23 | adantr 481 |
. . . . . . . . . . . . . . 15
|
38 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
|
39 | | fourierdlem32.a |
. . . . . . . . . . . . . . . . . . 19
|
40 | 39 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
41 | | elico2 12237 |
. . . . . . . . . . . . . . . . . 18
|
42 | 40, 37, 41 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
43 | 38, 42 | mpbid 222 |
. . . . . . . . . . . . . . . 16
|
44 | 43 | simp1d 1073 |
. . . . . . . . . . . . . . 15
|
45 | 44 | mnfltd 11958 |
. . . . . . . . . . . . . . 15
|
46 | 43 | simp3d 1075 |
. . . . . . . . . . . . . . 15
|
47 | 36, 37, 44, 45, 46 | eliood 39720 |
. . . . . . . . . . . . . 14
|
48 | 43 | simp2d 1074 |
. . . . . . . . . . . . . . 15
|
49 | 22 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
50 | | fourierdlem32.b |
. . . . . . . . . . . . . . . . 17
|
51 | 50 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
52 | 39, 50, 19, 22, 21, 13 | fourierdlem10 40334 |
. . . . . . . . . . . . . . . . . 18
|
53 | 52 | simprd 479 |
. . . . . . . . . . . . . . . . 17
|
54 | 53 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
55 | 44, 49, 51, 46, 54 | ltletrd 10197 |
. . . . . . . . . . . . . . 15
|
56 | 50 | rexrd 10089 |
. . . . . . . . . . . . . . . . 17
|
57 | 56 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
58 | | elico2 12237 |
. . . . . . . . . . . . . . . 16
|
59 | 40, 57, 58 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
60 | 44, 48, 55, 59 | mpbir3and 1245 |
. . . . . . . . . . . . . 14
|
61 | 47, 60 | elind 3798 |
. . . . . . . . . . . . 13
|
62 | | elinel1 3799 |
. . . . . . . . . . . . . . . 16
|
63 | | elioore 12205 |
. . . . . . . . . . . . . . . 16
|
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . . 15
|
65 | 64 | adantl 482 |
. . . . . . . . . . . . . 14
|
66 | | elinel2 3800 |
. . . . . . . . . . . . . . . . 17
|
67 | 66 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
68 | 39 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
69 | 56 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
70 | 68, 69, 58 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
71 | 67, 70 | mpbid 222 |
. . . . . . . . . . . . . . 15
|
72 | 71 | simp2d 1074 |
. . . . . . . . . . . . . 14
|
73 | 62 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
74 | 23 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
75 | | elioo2 12216 |
. . . . . . . . . . . . . . . . 17
|
76 | 35, 74, 75 | sylancr 695 |
. . . . . . . . . . . . . . . 16
|
77 | 73, 76 | mpbid 222 |
. . . . . . . . . . . . . . 15
|
78 | 77 | simp3d 1075 |
. . . . . . . . . . . . . 14
|
79 | 68, 74, 41 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
80 | 65, 72, 78, 79 | mpbir3and 1245 |
. . . . . . . . . . . . 13
|
81 | 61, 80 | impbida 877 |
. . . . . . . . . . . 12
|
82 | 81 | eqrdv 2620 |
. . . . . . . . . . 11
|
83 | | retop 22565 |
. . . . . . . . . . . . 13
|
84 | 83 | a1i 11 |
. . . . . . . . . . . 12
|
85 | 30 | a1i 11 |
. . . . . . . . . . . 12
|
86 | | iooretop 22569 |
. . . . . . . . . . . . 13
|
87 | 86 | a1i 11 |
. . . . . . . . . . . 12
|
88 | | elrestr 16089 |
. . . . . . . . . . . 12
↾t |
89 | 84, 85, 87, 88 | syl3anc 1326 |
. . . . . . . . . . 11
↾t |
90 | 82, 89 | eqeltrd 2701 |
. . . . . . . . . 10
↾t |
91 | 90 | adantr 481 |
. . . . . . . . 9
↾t |
92 | | simpr 477 |
. . . . . . . . . 10
|
93 | 92 | oveq1d 6665 |
. . . . . . . . 9
|
94 | 28 | a1i 11 |
. . . . . . . . . . 11
ℂfld ↾t |
95 | 29 | a1i 11 |
. . . . . . . . . . . 12
ℂfld
|
96 | | icossre 12254 |
. . . . . . . . . . . . 13
|
97 | 39, 56, 96 | syl2anc 693 |
. . . . . . . . . . . 12
|
98 | | reex 10027 |
. . . . . . . . . . . . 13
|
99 | 98 | a1i 11 |
. . . . . . . . . . . 12
|
100 | | restabs 20969 |
. . . . . . . . . . . 12
ℂfld
ℂfld
↾t
↾t ℂfld
↾t |
101 | 95, 97, 99, 100 | syl3anc 1326 |
. . . . . . . . . . 11
ℂfld ↾t ↾t ℂfld ↾t |
102 | 17 | tgioo2 22606 |
. . . . . . . . . . . . . 14
ℂfld
↾t |
103 | 102 | eqcomi 2631 |
. . . . . . . . . . . . 13
ℂfld ↾t |
104 | 103 | oveq1i 6660 |
. . . . . . . . . . . 12
ℂfld
↾t
↾t ↾t |
105 | 104 | a1i 11 |
. . . . . . . . . . 11
ℂfld ↾t ↾t ↾t |
106 | 94, 101, 105 | 3eqtr2d 2662 |
. . . . . . . . . 10
↾t |
107 | 106 | adantr 481 |
. . . . . . . . 9
↾t |
108 | 91, 93, 107 | 3eltr4d 2716 |
. . . . . . . 8
|
109 | | isopn3i 20886 |
. . . . . . . 8
|
110 | 34, 108, 109 | syl2anc 693 |
. . . . . . 7
|
111 | 27, 110 | eleqtrrd 2704 |
. . . . . 6
|
112 | | id 22 |
. . . . . . . 8
|
113 | 112 | eqcomd 2628 |
. . . . . . 7
|
114 | 113 | adantl 482 |
. . . . . 6
|
115 | | uncom 3757 |
. . . . . . . . . . . 12
|
116 | 39 | rexrd 10089 |
. . . . . . . . . . . . 13
|
117 | | fourierdlem32.altb |
. . . . . . . . . . . . 13
|
118 | | snunioo 12298 |
. . . . . . . . . . . . 13
|
119 | 116, 56, 117, 118 | syl3anc 1326 |
. . . . . . . . . . . 12
|
120 | 115, 119 | syl5eq 2668 |
. . . . . . . . . . 11
|
121 | 120 | adantr 481 |
. . . . . . . . . 10
|
122 | 121 | oveq2d 6666 |
. . . . . . . . 9
ℂfld
↾t ℂfld ↾t |
123 | 122, 28 | syl6eqr 2674 |
. . . . . . . 8
ℂfld
↾t |
124 | 123 | fveq2d 6195 |
. . . . . . 7
ℂfld ↾t |
125 | | uncom 3757 |
. . . . . . . . 9
|
126 | | sneq 4187 |
. . . . . . . . . . 11
|
127 | 126 | eqcomd 2628 |
. . . . . . . . . 10
|
128 | 127 | uneq1d 3766 |
. . . . . . . . 9
|
129 | 125, 128 | syl5eq 2668 |
. . . . . . . 8
|
130 | 19 | rexrd 10089 |
. . . . . . . . 9
|
131 | | snunioo 12298 |
. . . . . . . . 9
|
132 | 130, 23, 21, 131 | syl3anc 1326 |
. . . . . . . 8
|
133 | 129, 132 | sylan9eqr 2678 |
. . . . . . 7
|
134 | 124, 133 | fveq12d 6197 |
. . . . . 6
ℂfld
↾t |
135 | 111, 114,
134 | 3eltr4d 2716 |
. . . . 5
ℂfld
↾t |
136 | 12, 14, 16, 17, 18, 135 | limcres 23650 |
. . . 4
lim lim |
137 | 8, 136 | eqtr2d 2657 |
. . 3
lim lim |
138 | 2, 6, 137 | 3eltr3d 2715 |
. 2
lim |
139 | | limcresi 23649 |
. . 3
lim lim |
140 | | iffalse 4095 |
. . . . . 6
|
141 | 3, 140 | syl5eq 2668 |
. . . . 5
|
142 | 141 | adantl 482 |
. . . 4
|
143 | | ssid 3624 |
. . . . . . . . . . . . 13
|
144 | 143 | a1i 11 |
. . . . . . . . . . . 12
|
145 | | eqid 2622 |
. . . . . . . . . . . . 13
ℂfld ↾t ℂfld
↾t |
146 | | unicntop 22589 |
. . . . . . . . . . . . . . . 16
ℂfld |
147 | 146 | restid 16094 |
. . . . . . . . . . . . . . 15
ℂfld ℂfld
↾t ℂfld |
148 | 29, 147 | ax-mp 5 |
. . . . . . . . . . . . . 14
ℂfld ↾t ℂfld |
149 | 148 | eqcomi 2631 |
. . . . . . . . . . . . 13
ℂfld ℂfld ↾t |
150 | 17, 145, 149 | cncfcn 22712 |
. . . . . . . . . . . 12
ℂfld
↾t ℂfld |
151 | 15, 144, 150 | sylancr 695 |
. . . . . . . . . . 11
ℂfld ↾t ℂfld |
152 | 9, 151 | eleqtrd 2703 |
. . . . . . . . . 10
ℂfld
↾t ℂfld |
153 | 17 | cnfldtopon 22586 |
. . . . . . . . . . . 12
ℂfld TopOn |
154 | | resttopon 20965 |
. . . . . . . . . . . 12
ℂfld
TopOn
ℂfld ↾t TopOn |
155 | 153, 15, 154 | mp2an 708 |
. . . . . . . . . . 11
ℂfld ↾t TopOn |
156 | | cncnp 21084 |
. . . . . . . . . . 11
ℂfld
↾t TopOn ℂfld
TopOn ℂfld
↾t ℂfld
ℂfld
↾t ℂfld |
157 | 155, 153,
156 | mp2an 708 |
. . . . . . . . . 10
ℂfld ↾t ℂfld
ℂfld
↾t ℂfld |
158 | 152, 157 | sylib 208 |
. . . . . . . . 9
ℂfld ↾t ℂfld |
159 | 158 | simprd 479 |
. . . . . . . 8
ℂfld
↾t ℂfld |
160 | 159 | adantr 481 |
. . . . . . 7
ℂfld ↾t ℂfld |
161 | 116 | adantr 481 |
. . . . . . . 8
|
162 | 56 | adantr 481 |
. . . . . . . 8
|
163 | 19 | adantr 481 |
. . . . . . . 8
|
164 | 39 | adantr 481 |
. . . . . . . . 9
|
165 | 52 | simpld 475 |
. . . . . . . . . 10
|
166 | 165 | adantr 481 |
. . . . . . . . 9
|
167 | 112 | eqcoms 2630 |
. . . . . . . . . . . 12
|
168 | 167 | necon3bi 2820 |
. . . . . . . . . . 11
|
169 | 168 | adantl 482 |
. . . . . . . . . 10
|
170 | 169 | necomd 2849 |
. . . . . . . . 9
|
171 | 164, 163,
166, 170 | leneltd 10191 |
. . . . . . . 8
|
172 | 19, 22, 50, 21, 53 | ltletrd 10197 |
. . . . . . . . 9
|
173 | 172 | adantr 481 |
. . . . . . . 8
|
174 | 161, 162,
163, 171, 173 | eliood 39720 |
. . . . . . 7
|
175 | | fveq2 6191 |
. . . . . . . . 9
ℂfld ↾t ℂfld ℂfld
↾t ℂfld |
176 | 175 | eleq2d 2687 |
. . . . . . . 8
ℂfld
↾t ℂfld
ℂfld ↾t ℂfld |
177 | 176 | rspccva 3308 |
. . . . . . 7
ℂfld
↾t ℂfld
ℂfld ↾t ℂfld |
178 | 160, 174,
177 | syl2anc 693 |
. . . . . 6
ℂfld ↾t ℂfld |
179 | 17, 145 | cnplimc 23651 |
. . . . . . 7
ℂfld
↾t ℂfld lim |
180 | 15, 174, 179 | sylancr 695 |
. . . . . 6
ℂfld
↾t ℂfld lim |
181 | 178, 180 | mpbid 222 |
. . . . 5
lim |
182 | 181 | simprd 479 |
. . . 4
lim |
183 | 142, 182 | eqeltrd 2701 |
. . 3
lim |
184 | 139, 183 | sseldi 3601 |
. 2
lim |
185 | 138, 184 | pm2.61dan 832 |
1
lim |