Step | Hyp | Ref
| Expression |
1 | | fourierdlem80.o |
. . . . . . . . 9
|
2 | | oveq2 6658 |
. . . . . . . . . . . . 13
|
3 | 2 | fveq2d 6195 |
. . . . . . . . . . . 12
|
4 | 3 | oveq1d 6665 |
. . . . . . . . . . 11
|
5 | | oveq1 6657 |
. . . . . . . . . . . . 13
|
6 | 5 | fveq2d 6195 |
. . . . . . . . . . . 12
|
7 | 6 | oveq2d 6666 |
. . . . . . . . . . 11
|
8 | 4, 7 | oveq12d 6668 |
. . . . . . . . . 10
|
9 | 8 | cbvmptv 4750 |
. . . . . . . . 9
|
10 | 1, 9 | eqtr2i 2645 |
. . . . . . . 8
|
11 | 10 | oveq2i 6661 |
. . . . . . 7
|
12 | 11 | dmeqi 5325 |
. . . . . 6
|
13 | 12 | ineq2i 3811 |
. . . . 5
|
14 | 13 | sneqi 4188 |
. . . 4
|
15 | 14 | uneq1i 3763 |
. . 3
..^ ..^ |
16 | | snfi 8038 |
. . . . 5
|
17 | | fzofi 12773 |
. . . . . 6
..^ |
18 | | eqid 2622 |
. . . . . . 7
..^ ..^ |
19 | 18 | rnmptfi 39351 |
. . . . . 6
..^
..^ |
20 | 17, 19 | ax-mp 5 |
. . . . 5
..^ |
21 | | unfi 8227 |
. . . . 5
..^
..^ |
22 | 16, 20, 21 | mp2an 708 |
. . . 4
..^ |
23 | 22 | a1i 11 |
. . 3
..^ |
24 | 15, 23 | syl5eqel 2705 |
. 2
..^ |
25 | | id 22 |
. . . 4
..^
..^ |
26 | 15 | unieqi 4445 |
. . . 4
..^ ..^ |
27 | 25, 26 | syl6eleq 2711 |
. . 3
..^
..^ |
28 | | simpl 473 |
. . . . 5
..^ |
29 | | uniun 4456 |
. . . . . . . . 9
..^
..^ |
30 | 29 | eleq2i 2693 |
. . . . . . . 8
..^
..^ |
31 | | elun 3753 |
. . . . . . . 8
..^
..^ |
32 | 30, 31 | sylbb 209 |
. . . . . . 7
..^
..^ |
33 | 32 | adantl 482 |
. . . . . 6
..^
..^ |
34 | | fourierdlem80.sf |
. . . . . . . . . . . . 13
|
35 | | ovex 6678 |
. . . . . . . . . . . . . 14
|
36 | 35 | a1i 11 |
. . . . . . . . . . . . 13
|
37 | | fex 6490 |
. . . . . . . . . . . . 13
|
38 | 34, 36, 37 | syl2anc 693 |
. . . . . . . . . . . 12
|
39 | | rnexg 7098 |
. . . . . . . . . . . 12
|
40 | 38, 39 | syl 17 |
. . . . . . . . . . 11
|
41 | | inex1g 4801 |
. . . . . . . . . . 11
|
42 | 40, 41 | syl 17 |
. . . . . . . . . 10
|
43 | | unisng 4452 |
. . . . . . . . . 10
|
44 | 42, 43 | syl 17 |
. . . . . . . . 9
|
45 | 44 | eleq2d 2687 |
. . . . . . . 8
|
46 | 45 | adantr 481 |
. . . . . . 7
..^
|
47 | 46 | orbi1d 739 |
. . . . . 6
..^ ..^
..^ |
48 | 33, 47 | mpbid 222 |
. . . . 5
..^
..^ |
49 | | dvf 23671 |
. . . . . . . . 9
|
50 | 49 | a1i 11 |
. . . . . . . 8
|
51 | | elinel2 3800 |
. . . . . . . 8
|
52 | 50, 51 | ffvelrnd 6360 |
. . . . . . 7
|
53 | 52 | adantl 482 |
. . . . . 6
|
54 | | ovex 6678 |
. . . . . . . . . . . 12
|
55 | 54 | dfiun3 5380 |
. . . . . . . . . . 11
..^ ..^ |
56 | 55 | eleq2i 2693 |
. . . . . . . . . 10
..^ ..^ |
57 | 56 | biimpri 218 |
. . . . . . . . 9
..^
..^ |
58 | 57 | adantl 482 |
. . . . . . . 8
..^ ..^ |
59 | | eliun 4524 |
. . . . . . . 8
..^ ..^ |
60 | 58, 59 | sylib 208 |
. . . . . . 7
..^
..^ |
61 | | nfv 1843 |
. . . . . . . . 9
|
62 | | nfmpt1 4747 |
. . . . . . . . . . . 12
..^ |
63 | 62 | nfrn 5368 |
. . . . . . . . . . 11
..^ |
64 | 63 | nfuni 4442 |
. . . . . . . . . 10
..^ |
65 | 64 | nfcri 2758 |
. . . . . . . . 9
..^ |
66 | 61, 65 | nfan 1828 |
. . . . . . . 8
..^ |
67 | | nfv 1843 |
. . . . . . . 8
|
68 | 49 | a1i 11 |
. . . . . . . . . . 11
..^
|
69 | 1 | reseq1i 5392 |
. . . . . . . . . . . . . . . . . . . 20
|
70 | | ioossicc 12259 |
. . . . . . . . . . . . . . . . . . . . . 22
|
71 | | fourierdlem80.sjss |
. . . . . . . . . . . . . . . . . . . . . 22
..^ |
72 | 70, 71 | syl5ss 3614 |
. . . . . . . . . . . . . . . . . . . . 21
..^ |
73 | 72 | resmptd 5452 |
. . . . . . . . . . . . . . . . . . . 20
..^
|
74 | 69, 73 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . . 19
..^
|
75 | | fourierdlem80.y |
. . . . . . . . . . . . . . . . . . 19
|
76 | 74, 75 | syl6reqr 2675 |
. . . . . . . . . . . . . . . . . 18
..^
|
77 | 76 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
..^ |
78 | | ax-resscn 9993 |
. . . . . . . . . . . . . . . . . . . . 21
|
79 | 78 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
|
80 | | fourierdlem80.f |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
81 | 80 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
82 | | fourierdlem80.xre |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
83 | 82 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
84 | | fourierdlem80.a |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
85 | | fourierdlem80.b |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
86 | 84, 85 | iccssred 39727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
87 | 86 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
88 | 83, 87 | readdcld 10069 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
89 | 81, 88 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
90 | 89 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
91 | | fourierdlem80.c |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
92 | 91 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
93 | 92 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
94 | 90, 93 | subcld 10392 |
. . . . . . . . . . . . . . . . . . . . . 22
|
95 | | 2cnd 11093 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
96 | 86, 79 | sstrd 3613 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
97 | 96 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
98 | 97 | halfcld 11277 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
99 | 98 | sincld 14860 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
100 | 95, 99 | mulcld 10060 |
. . . . . . . . . . . . . . . . . . . . . 22
|
101 | | 2ne0 11113 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
102 | 101 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
103 | | fourierdlem80.ab |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
104 | 103 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
105 | | eqcom 2629 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
106 | 105 | biimpi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
107 | 106 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
108 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
109 | 107, 108 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
110 | 109 | adantll 750 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
111 | | fourierdlem80.n0 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
112 | 111 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
113 | 110, 112 | pm2.65da 600 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
114 | 113 | neqned 2801 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
115 | | fourierdlem44 40368 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
116 | 104, 114,
115 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
117 | 95, 99, 102, 116 | mulne0d 10679 |
. . . . . . . . . . . . . . . . . . . . . 22
|
118 | 94, 100, 117 | divcld 10801 |
. . . . . . . . . . . . . . . . . . . . 21
|
119 | 118, 1 | fmptd 6385 |
. . . . . . . . . . . . . . . . . . . 20
|
120 | | ioossre 12235 |
. . . . . . . . . . . . . . . . . . . . 21
|
121 | 120 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
|
122 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . 21
ℂfld ℂfld |
123 | 122 | tgioo2 22606 |
. . . . . . . . . . . . . . . . . . . . 21
ℂfld
↾t |
124 | 122, 123 | dvres 23675 |
. . . . . . . . . . . . . . . . . . . 20
|
125 | 79, 119, 86, 121, 124 | syl22anc 1327 |
. . . . . . . . . . . . . . . . . . 19
|
126 | | ioontr 39736 |
. . . . . . . . . . . . . . . . . . . 20
|
127 | 126 | reseq2i 5393 |
. . . . . . . . . . . . . . . . . . 19
|
128 | 125, 127 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . 18
|
129 | 128 | adantr 481 |
. . . . . . . . . . . . . . . . 17
..^
|
130 | 77, 129 | eqtr2d 2657 |
. . . . . . . . . . . . . . . 16
..^ |
131 | 130 | dmeqd 5326 |
. . . . . . . . . . . . . . 15
..^
|
132 | 80 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
..^ |
133 | 82 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
..^ |
134 | 86 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
..^ |
135 | 34 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
..^ |
136 | | elfzofz 12485 |
. . . . . . . . . . . . . . . . . . . . . 22
..^
|
137 | 136 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
..^ |
138 | 135, 137 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . . 20
..^ |
139 | 134, 138 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . 19
..^ |
140 | | fzofzp1 12565 |
. . . . . . . . . . . . . . . . . . . . . 22
..^
|
141 | 140 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
..^ |
142 | 135, 141 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . . 20
..^ |
143 | 134, 142 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . 19
..^ |
144 | | fdv |
. . . . . . . . . . . . . . . . . . . . 21
..^
|
145 | | fourierdlem80.i |
. . . . . . . . . . . . . . . . . . . . . 22
|
146 | 145 | feq2i 6037 |
. . . . . . . . . . . . . . . . . . . . 21
|
147 | 144, 146 | sylib 208 |
. . . . . . . . . . . . . . . . . . . 20
..^
|
148 | 145 | reseq2i 5393 |
. . . . . . . . . . . . . . . . . . . . . 22
|
149 | 148 | oveq2i 6661 |
. . . . . . . . . . . . . . . . . . . . 21
|
150 | 149 | feq1i 6036 |
. . . . . . . . . . . . . . . . . . . 20
|
151 | 147, 150 | sylib 208 |
. . . . . . . . . . . . . . . . . . 19
..^
|
152 | 103 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
..^ |
153 | 72, 152 | sstrd 3613 |
. . . . . . . . . . . . . . . . . . 19
..^ |
154 | 111 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
..^
|
155 | 72, 154 | ssneldd 3606 |
. . . . . . . . . . . . . . . . . . 19
..^
|
156 | 91 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
..^ |
157 | 132, 133,
139, 143, 151, 153, 155, 156, 75 | fourierdlem57 40380 |
. . . . . . . . . . . . . . . . . 18
..^
|
158 | 157 | simpli 474 |
. . . . . . . . . . . . . . . . 17
..^ |
159 | 158 | simpld 475 |
. . . . . . . . . . . . . . . 16
..^ |
160 | | fdm 6051 |
. . . . . . . . . . . . . . . 16
|
161 | 159, 160 | syl 17 |
. . . . . . . . . . . . . . 15
..^
|
162 | 131, 161 | eqtr2d 2657 |
. . . . . . . . . . . . . 14
..^ |
163 | | resss 5422 |
. . . . . . . . . . . . . . 15
|
164 | | dmss 5323 |
. . . . . . . . . . . . . . 15
|
165 | 163, 164 | mp1i 13 |
. . . . . . . . . . . . . 14
..^
|
166 | 162, 165 | eqsstrd 3639 |
. . . . . . . . . . . . 13
..^
|
167 | 166 | 3adant3 1081 |
. . . . . . . . . . . 12
..^
|
168 | | simp3 1063 |
. . . . . . . . . . . 12
..^
|
169 | 167, 168 | sseldd 3604 |
. . . . . . . . . . 11
..^
|
170 | 68, 169 | ffvelrnd 6360 |
. . . . . . . . . 10
..^
|
171 | 170 | 3exp 1264 |
. . . . . . . . 9
..^ |
172 | 171 | adantr 481 |
. . . . . . . 8
..^ ..^ |
173 | 66, 67, 172 | rexlimd 3026 |
. . . . . . 7
..^ ..^ |
174 | 60, 173 | mpd 15 |
. . . . . 6
..^ |
175 | 53, 174 | jaodan 826 |
. . . . 5
..^
|
176 | 28, 48, 175 | syl2anc 693 |
. . . 4
..^ |
177 | 176 | abscld 14175 |
. . 3
..^ |
178 | 27, 177 | sylan2 491 |
. 2
..^ |
179 | | id 22 |
. . . 4
..^
..^ |
180 | 179, 15 | syl6eleq 2711 |
. . 3
..^
..^ |
181 | | elsni 4194 |
. . . . . 6
|
182 | | simpr 477 |
. . . . . . . 8
|
183 | | fzfid 12772 |
. . . . . . . . . . 11
|
184 | | rnffi 39356 |
. . . . . . . . . . 11
|
185 | 34, 183, 184 | syl2anc 693 |
. . . . . . . . . 10
|
186 | | infi 8184 |
. . . . . . . . . 10
|
187 | 185, 186 | syl 17 |
. . . . . . . . 9
|
188 | 187 | adantr 481 |
. . . . . . . 8
|
189 | 182, 188 | eqeltrd 2701 |
. . . . . . 7
|
190 | | nfv 1843 |
. . . . . . . . 9
|
191 | | nfcv 2764 |
. . . . . . . . . . 11
|
192 | | nfcv 2764 |
. . . . . . . . . . . . 13
|
193 | | nfcv 2764 |
. . . . . . . . . . . . 13
|
194 | | nfmpt1 4747 |
. . . . . . . . . . . . . 14
|
195 | 1, 194 | nfcxfr 2762 |
. . . . . . . . . . . . 13
|
196 | 192, 193,
195 | nfov 6676 |
. . . . . . . . . . . 12
|
197 | 196 | nfdm 5367 |
. . . . . . . . . . 11
|
198 | 191, 197 | nfin 3820 |
. . . . . . . . . 10
|
199 | 198 | nfeq2 2780 |
. . . . . . . . 9
|
200 | 190, 199 | nfan 1828 |
. . . . . . . 8
|
201 | | simpr 477 |
. . . . . . . . . . . . 13
|
202 | | simpl 473 |
. . . . . . . . . . . . 13
|
203 | 201, 202 | eleqtrd 2703 |
. . . . . . . . . . . 12
|
204 | 203, 51 | syl 17 |
. . . . . . . . . . 11
|
205 | 204 | adantll 750 |
. . . . . . . . . 10
|
206 | 49 | ffvelrni 6358 |
. . . . . . . . . . 11
|
207 | 206 | abscld 14175 |
. . . . . . . . . 10
|
208 | 205, 207 | syl 17 |
. . . . . . . . 9
|
209 | 208 | ex 450 |
. . . . . . . 8
|
210 | 200, 209 | ralrimi 2957 |
. . . . . . 7
|
211 | | fimaxre3 10970 |
. . . . . . 7
|
212 | 189, 210,
211 | syl2anc 693 |
. . . . . 6
|
213 | 181, 212 | sylan2 491 |
. . . . 5
|
214 | 213 | adantlr 751 |
. . . 4
..^
|
215 | | simpll 790 |
. . . . 5
..^
|
216 | | elunnel1 3754 |
. . . . . 6
..^
..^ |
217 | 216 | adantll 750 |
. . . . 5
..^
..^ |
218 | | vex 3203 |
. . . . . . . . 9
|
219 | 18 | elrnmpt 5372 |
. . . . . . . . 9
..^
..^ |
220 | 218, 219 | ax-mp 5 |
. . . . . . . 8
..^
..^ |
221 | 220 | biimpi 206 |
. . . . . . 7
..^
..^ |
222 | 221 | adantl 482 |
. . . . . 6
..^ ..^ |
223 | 63 | nfcri 2758 |
. . . . . . . 8
..^ |
224 | 61, 223 | nfan 1828 |
. . . . . . 7
..^ |
225 | | nfv 1843 |
. . . . . . 7
|
226 | | fourierdlem80.fbdioo |
. . . . . . . . . . . . 13
..^ |
227 | | fourierdlem80.fdvbdioo |
. . . . . . . . . . . . 13
..^ |
228 | | reeanv 3107 |
. . . . . . . . . . . . 13
|
229 | 226, 227,
228 | sylanbrc 698 |
. . . . . . . . . . . 12
..^
|
230 | | simp1 1061 |
. . . . . . . . . . . . . . . . . 18
..^
..^ |
231 | | simp2l 1087 |
. . . . . . . . . . . . . . . . . 18
..^
|
232 | | simp2r 1088 |
. . . . . . . . . . . . . . . . . 18
..^
|
233 | 230, 231,
232 | jca31 557 |
. . . . . . . . . . . . . . . . 17
..^
..^
|
234 | | simp3l 1089 |
. . . . . . . . . . . . . . . . 17
..^
|
235 | | simp3r 1090 |
. . . . . . . . . . . . . . . . 17
..^
|
236 | 233, 234,
235 | jca31 557 |
. . . . . . . . . . . . . . . 16
..^
..^
|
237 | | fourierdlem80.ch |
. . . . . . . . . . . . . . . 16
..^
|
238 | 236, 237 | sylibr 224 |
. . . . . . . . . . . . . . 15
..^
|
239 | 237 | biimpi 206 |
. . . . . . . . . . . . . . . . . . . . 21
..^
|
240 | | simp-5l 808 |
. . . . . . . . . . . . . . . . . . . . 21
..^
|
241 | 239, 240 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
242 | 241, 80 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
243 | 241, 82 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
244 | | simp-4l 806 |
. . . . . . . . . . . . . . . . . . . . 21
..^
..^ |
245 | 239, 244 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
..^ |
246 | 245, 139 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
247 | 245, 143 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
248 | | fourierdlem80.slt |
. . . . . . . . . . . . . . . . . . . 20
..^ |
249 | 245, 248 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
250 | 71, 152 | sstrd 3613 |
. . . . . . . . . . . . . . . . . . . 20
..^ |
251 | 245, 250 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
252 | 71, 154 | ssneldd 3606 |
. . . . . . . . . . . . . . . . . . . 20
..^
|
253 | 245, 252 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
254 | 245, 151 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
255 | | simp-4r 807 |
. . . . . . . . . . . . . . . . . . . 20
..^
|
256 | 239, 255 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
257 | 239 | simplrd 793 |
. . . . . . . . . . . . . . . . . . . 20
|
258 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
|
259 | 258, 145 | syl6eleqr 2712 |
. . . . . . . . . . . . . . . . . . . 20
|
260 | | rspa 2930 |
. . . . . . . . . . . . . . . . . . . 20
|
261 | 257, 259,
260 | syl2an 494 |
. . . . . . . . . . . . . . . . . . 19
|
262 | | simpllr 799 |
. . . . . . . . . . . . . . . . . . . 20
..^
|
263 | 239, 262 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
264 | 149 | fveq1i 6192 |
. . . . . . . . . . . . . . . . . . . . . 22
|
265 | 264 | fveq2i 6194 |
. . . . . . . . . . . . . . . . . . . . 21
|
266 | 239 | simprd 479 |
. . . . . . . . . . . . . . . . . . . . . 22
|
267 | 266 | r19.21bi 2932 |
. . . . . . . . . . . . . . . . . . . . 21
|
268 | 265, 267 | syl5eqbrr 4689 |
. . . . . . . . . . . . . . . . . . . 20
|
269 | 259, 268 | sylan2 491 |
. . . . . . . . . . . . . . . . . . 19
|
270 | 241, 91 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
271 | 242, 243,
246, 247, 249, 251, 253, 254, 256, 261, 263, 269, 270, 75 | fourierdlem68 40391 |
. . . . . . . . . . . . . . . . . 18
|
272 | 271 | simprd 479 |
. . . . . . . . . . . . . . . . 17
|
273 | 271 | simpld 475 |
. . . . . . . . . . . . . . . . . . 19
|
274 | 273 | raleqdv 3144 |
. . . . . . . . . . . . . . . . . 18
|
275 | 274 | rexbidv 3052 |
. . . . . . . . . . . . . . . . 17
|
276 | 272, 275 | mpbid 222 |
. . . . . . . . . . . . . . . 16
|
277 | 126 | eqcomi 2631 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
278 | 277 | reseq2i 5393 |
. . . . . . . . . . . . . . . . . . . . . 22
|
279 | 278 | fveq1i 6192 |
. . . . . . . . . . . . . . . . . . . . 21
|
280 | | fvres 6207 |
. . . . . . . . . . . . . . . . . . . . . 22
|
281 | 280 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
|
282 | 245, 72 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
283 | 282 | resmptd 5452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
284 | 69, 283 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
285 | 284, 75 | syl6reqr 2675 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
286 | 285 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
287 | 286 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
288 | 125 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
289 | 241, 288 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
290 | 287, 289 | eqtr2d 2657 |
. . . . . . . . . . . . . . . . . . . . . 22
|
291 | 290 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
292 | 279, 281,
291 | 3eqtr3a 2680 |
. . . . . . . . . . . . . . . . . . . 20
|
293 | 292 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
|
294 | 293 | breq1d 4663 |
. . . . . . . . . . . . . . . . . 18
|
295 | 294 | ralbidva 2985 |
. . . . . . . . . . . . . . . . 17
|
296 | 295 | rexbidv 3052 |
. . . . . . . . . . . . . . . 16
|
297 | 276, 296 | mpbird 247 |
. . . . . . . . . . . . . . 15
|
298 | 238, 297 | syl 17 |
. . . . . . . . . . . . . 14
..^
|
299 | 298 | 3exp 1264 |
. . . . . . . . . . . . 13
..^
|
300 | 299 | rexlimdvv 3037 |
. . . . . . . . . . . 12
..^
|
301 | 229, 300 | mpd 15 |
. . . . . . . . . . 11
..^ |
302 | 301 | 3adant3 1081 |
. . . . . . . . . 10
..^
|
303 | | raleq 3138 |
. . . . . . . . . . . 12
|
304 | 303 | 3ad2ant3 1084 |
. . . . . . . . . . 11
..^
|
305 | 304 | rexbidv 3052 |
. . . . . . . . . 10
..^
|
306 | 302, 305 | mpbird 247 |
. . . . . . . . 9
..^
|
307 | 306 | 3exp 1264 |
. . . . . . . 8
..^ |
308 | 307 | adantr 481 |
. . . . . . 7
..^ ..^
|
309 | 224, 225,
308 | rexlimd 3026 |
. . . . . 6
..^
..^
|
310 | 222, 309 | mpd 15 |
. . . . 5
..^
|
311 | 215, 217,
310 | syl2anc 693 |
. . . 4
..^
|
312 | 214, 311 | pm2.61dan 832 |
. . 3
..^
|
313 | 180, 312 | sylan2 491 |
. 2
..^
|
314 | | pm3.22 465 |
. . . . . . . . . . . 12
|
315 | | elin 3796 |
. . . . . . . . . . . 12
|
316 | 314, 315 | sylibr 224 |
. . . . . . . . . . 11
|
317 | 316 | adantll 750 |
. . . . . . . . . 10
|
318 | 44 | eqcomd 2628 |
. . . . . . . . . . 11
|
319 | 318 | ad2antrr 762 |
. . . . . . . . . 10
|
320 | 317, 319 | eleqtrd 2703 |
. . . . . . . . 9
|
321 | 320 | orcd 407 |
. . . . . . . 8
..^ |
322 | | simpll 790 |
. . . . . . . . . . 11
|
323 | 78 | a1i 11 |
. . . . . . . . . . . . . 14
|
324 | 119 | adantr 481 |
. . . . . . . . . . . . . 14
|
325 | 84 | adantr 481 |
. . . . . . . . . . . . . . 15
|
326 | 85 | adantr 481 |
. . . . . . . . . . . . . . 15
|
327 | 325, 326 | iccssred 39727 |
. . . . . . . . . . . . . 14
|
328 | 323, 324,
327 | dvbss 23665 |
. . . . . . . . . . . . 13
|
329 | | simpr 477 |
. . . . . . . . . . . . 13
|
330 | 328, 329 | sseldd 3604 |
. . . . . . . . . . . 12
|
331 | 330 | adantr 481 |
. . . . . . . . . . 11
|
332 | | simpr 477 |
. . . . . . . . . . 11
|
333 | | fourierdlem80.relioo |
. . . . . . . . . . . . 13
..^ |
334 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
|
335 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . 18
|
336 | 335 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
|
337 | 334, 336 | oveq12d 6668 |
. . . . . . . . . . . . . . . 16
|
338 | | ovex 6678 |
. . . . . . . . . . . . . . . 16
|
339 | 337, 18, 338 | fvmpt 6282 |
. . . . . . . . . . . . . . 15
..^
..^ |
340 | 339 | eleq2d 2687 |
. . . . . . . . . . . . . 14
..^
..^ |
341 | 340 | rexbiia 3040 |
. . . . . . . . . . . . 13
..^ ..^ ..^ |
342 | 333, 341 | sylibr 224 |
. . . . . . . . . . . 12
..^ ..^ |
343 | 54, 18 | dmmpti 6023 |
. . . . . . . . . . . . 13
..^ ..^ |
344 | 343 | rexeqi 3143 |
. . . . . . . . . . . 12
..^ ..^
..^ ..^ |
345 | 342, 344 | sylibr 224 |
. . . . . . . . . . 11
..^ ..^ |
346 | 322, 331,
332, 345 | syl21anc 1325 |
. . . . . . . . . 10
..^ ..^ |
347 | | funmpt 5926 |
. . . . . . . . . . 11
..^ |
348 | | elunirn 6509 |
. . . . . . . . . . 11
..^
..^
..^ ..^ |
349 | 347, 348 | mp1i 13 |
. . . . . . . . . 10
..^
..^ ..^ |
350 | 346, 349 | mpbird 247 |
. . . . . . . . 9
..^ |
351 | 350 | olcd 408 |
. . . . . . . 8
..^ |
352 | 321, 351 | pm2.61dan 832 |
. . . . . . 7
..^ |
353 | | elun 3753 |
. . . . . . 7
..^
..^ |
354 | 352, 353 | sylibr 224 |
. . . . . 6
..^ |
355 | 354, 29 | syl6eleqr 2712 |
. . . . 5
..^ |
356 | 355 | ralrimiva 2966 |
. . . 4
..^ |
357 | | dfss3 3592 |
. . . 4
..^
..^ |
358 | 356, 357 | sylibr 224 |
. . 3
..^ |
359 | 358, 26 | syl6sseqr 3652 |
. 2
..^ |
360 | 24, 178, 313, 359 | ssfiunibd 39523 |
1
|