Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem51 Structured version   Visualization version   Unicode version

Theorem fourierdlem51 38133
 Description: is in the periodic partition, when the considered interval is centered at . (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem51.a
fourierdlem51.b
fourierdlem51.alt0
fourierdlem51.bgt0
fourierdlem51.t
fourierdlem51.cfi
fourierdlem51.css
fourierdlem51.bc
fourierdlem51.e
fourierdlem51.x
fourierdlem51.exc
fourierdlem51.d
fourierdlem51.f
fourierdlem51.h
Assertion
Ref Expression
fourierdlem51
Distinct variable groups:   ,,,   ,,,   ,,,   ,   ,,   ,   ,   ,,,   ,,,   ,   ,,
Allowed substitution hints:   ()   ()   ()   ()   (,,)   ()   (,)   (,,)   (,,)   ()

Proof of Theorem fourierdlem51
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fourierdlem51.a . . . . . . 7
2 fourierdlem51.x . . . . . . 7
31, 2readdcld 9688 . . . . . 6
4 fourierdlem51.b . . . . . . 7
54, 2readdcld 9688 . . . . . 6
6 0red 9662 . . . . . . . . 9
7 fourierdlem51.alt0 . . . . . . . . 9
81, 6, 2, 7ltadd1dd 10245 . . . . . . . 8
92recnd 9687 . . . . . . . . 9
109addid2d 9852 . . . . . . . 8
118, 10breqtrd 4420 . . . . . . 7
123, 2, 11ltled 9800 . . . . . 6
13 fourierdlem51.bgt0 . . . . . . . . 9
146, 4, 2, 13ltadd1dd 10245 . . . . . . . 8
1510, 14eqbrtrrd 4418 . . . . . . 7
162, 5, 15ltled 9800 . . . . . 6
173, 5, 2, 12, 16eliccd 37697 . . . . 5
184, 2resubcld 10068 . . . . . . . 8
19 fourierdlem51.t . . . . . . . . 9
204, 1resubcld 10068 . . . . . . . . 9
2119, 20syl5eqel 2553 . . . . . . . 8
221, 6, 4, 7, 13lttrd 9813 . . . . . . . . . . 11
231, 4posdifd 10221 . . . . . . . . . . 11
2422, 23mpbid 215 . . . . . . . . . 10
2519eqcomi 2480 . . . . . . . . . . 11
2625a1i 11 . . . . . . . . . 10
2724, 26breqtrd 4420 . . . . . . . . 9
2827gt0ne0d 10199 . . . . . . . 8
2918, 21, 28redivcld 10457 . . . . . . 7
3029flcld 12067 . . . . . 6
31 fourierdlem51.e . . . . . . . . 9
3231a1i 11 . . . . . . . 8
33 id 22 . . . . . . . . . 10
34 oveq2 6316 . . . . . . . . . . . . 13
3534oveq1d 6323 . . . . . . . . . . . 12
3635fveq2d 5883 . . . . . . . . . . 11
3736oveq1d 6323 . . . . . . . . . 10
3833, 37oveq12d 6326 . . . . . . . . 9
3938adantl 473 . . . . . . . 8
4030zred 11063 . . . . . . . . . 10
4140, 21remulcld 9689 . . . . . . . . 9
422, 41readdcld 9688 . . . . . . . 8
4332, 39, 2, 42fvmptd 5969 . . . . . . 7
44 fourierdlem51.exc . . . . . . 7
4543, 44eqeltrrd 2550 . . . . . 6
46 oveq1 6315 . . . . . . . . 9
4746oveq2d 6324 . . . . . . . 8
4847eleq1d 2533 . . . . . . 7
4948rspcev 3136 . . . . . 6
5030, 45, 49syl2anc 673 . . . . 5
51 oveq1 6315 . . . . . . . 8
5251eleq1d 2533 . . . . . . 7
5352rexbidv 2892 . . . . . 6
5453elrab 3184 . . . . 5
5517, 50, 54sylanbrc 677 . . . 4
56 elun2 3593 . . . 4
5755, 56syl 17 . . 3
58 fourierdlem51.d . . 3
5957, 58syl6eleqr 2560 . 2
60 prfi 7864 . . . . . 6
61 snfi 7668 . . . . . . . 8
62 fourierdlem51.cfi . . . . . . . . 9
63 fvres 5893 . . . . . . . . . . . . . 14
6463adantl 473 . . . . . . . . . . . . 13
65 oveq1 6315 . . . . . . . . . . . . . . . . . . 19
6665eleq1d 2533 . . . . . . . . . . . . . . . . . 18
6766rexbidv 2892 . . . . . . . . . . . . . . . . 17
6867elrab 3184 . . . . . . . . . . . . . . . 16
6968simprbi 471 . . . . . . . . . . . . . . 15
7069adantl 473 . . . . . . . . . . . . . 14
71 nfv 1769 . . . . . . . . . . . . . . . 16
72 nfre1 2846 . . . . . . . . . . . . . . . . . 18
73 nfcv 2612 . . . . . . . . . . . . . . . . . 18
7472, 73nfrab 2958 . . . . . . . . . . . . . . . . 17
7574nfcri 2606 . . . . . . . . . . . . . . . 16
7671, 75nfan 2031 . . . . . . . . . . . . . . 15
77 nfv 1769 . . . . . . . . . . . . . . 15
78 simpl 464 . . . . . . . . . . . . . . . 16
793rexrd 9708 . . . . . . . . . . . . . . . . . . 19
80 iocssre 11739 . . . . . . . . . . . . . . . . . . 19
8179, 5, 80syl2anc 673 . . . . . . . . . . . . . . . . . 18
8281adantr 472 . . . . . . . . . . . . . . . . 17
83 elrabi 3181 . . . . . . . . . . . . . . . . . 18
8483adantl 473 . . . . . . . . . . . . . . . . 17
8582, 84sseldd 3419 . . . . . . . . . . . . . . . 16
86 simpr 468 . . . . . . . . . . . . . . . . . . . . . . 23
874adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
8887, 86resubcld 10068 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
8921adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
9028adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
9188, 89, 90redivcld 10457 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
9291flcld 12067 . . . . . . . . . . . . . . . . . . . . . . . . . 26
9392zred 11063 . . . . . . . . . . . . . . . . . . . . . . . . 25
9493, 89remulcld 9689 . . . . . . . . . . . . . . . . . . . . . . . 24
9586, 94readdcld 9688 . . . . . . . . . . . . . . . . . . . . . . 23
9631fvmpt2 5972 . . . . . . . . . . . . . . . . . . . . . . 23
9786, 95, 96syl2anc 673 . . . . . . . . . . . . . . . . . . . . . 22
9897ad2antrr 740 . . . . . . . . . . . . . . . . . . . . 21
99 simpl 464 . . . . . . . . . . . . . . . . . . . . . . . . 25
10092ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . . 25
101 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
1021rexrd 9708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
1034rexrd 9708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
1041, 4, 22ltled 9800 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
105 lbicc2 11774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
106102, 103, 104, 105syl3anc 1292 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
107106adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
108101, 107eqeltrd 2549 . . . . . . . . . . . . . . . . . . . . . . . . . 26
109108adant423 37430 . . . . . . . . . . . . . . . . . . . . . . . . 25
11099, 100, 109jca31 543 . . . . . . . . . . . . . . . . . . . . . . . 24
111 iocssicc 11747 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
1121, 4, 22, 19, 31fourierdlem4 38085 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
113112ffvelrnda 6037 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
114111, 113sseldi 3416 . . . . . . . . . . . . . . . . . . . . . . . . . 26
11597, 114eqeltrrd 2550 . . . . . . . . . . . . . . . . . . . . . . . . 25
116115ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . 24
117102adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
11887rexrd 9708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
119 iocgtlb 37695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
120117, 118, 113, 119syl3anc 1292 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
121120ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
122 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
123122eqcomd 2477 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
124123adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
125121, 124, 983brtr3d 4425 . . . . . . . . . . . . . . . . . . . . . . . . . 26
126 zre 10965 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
127126adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
12821adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
129127, 128remulcld 9689 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
130129adantlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
131130adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
13294ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
133 simpllr 777 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
134131, 132, 133ltadd2d 9808 . . . . . . . . . . . . . . . . . . . . . . . . . 26
135125, 134mpbird 240 . . . . . . . . . . . . . . . . . . . . . . . . 25
136126ad2antlr 741 . . . . . . . . . . . . . . . . . . . . . . . . . 26
13793ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . . . 26
13821, 27elrpd 11361 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
139138ad3antrrr 744 . . . . . . . . . . . . . . . . . . . . . . . . . 26
140136, 137, 139ltmul1d 11402 . . . . . . . . . . . . . . . . . . . . . . . . 25
141135, 140mpbird 240 . . . . . . . . . . . . . . . . . . . . . . . 24
142 fvex 5889 . . . . . . . . . . . . . . . . . . . . . . . . 25
143 eleq1 2537 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
144143anbi2d 718 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
145144anbi1d 719 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
146 oveq1 6315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
147146oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
148147eleq1d 2533 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
149145, 148anbi12d 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
150 breq2 4399 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
151149, 150anbi12d 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26
152 eqeq1 2475 . . . . . . . . . . . . . . . . . . . . . . . . . 26
153151, 152imbi12d 327 . . . . . . . . . . . . . . . . . . . . . . . . 25
154 eleq1 2537 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
155154anbi2d 718 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
156155anbi1d 719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
157 oveq1 6315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
158157oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
159158eleq1d 2533 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
160156, 159anbi12d 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
161160anbi1d 719 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
162 breq1 4398 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
163161, 162anbi12d 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
164 oveq1 6315 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
165164eqeq2d 2481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
166163, 165imbi12d 327 . . . . . . . . . . . . . . . . . . . . . . . . . 26
167 simp-6l 788 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
168167, 1syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
169167, 4syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
170167, 22syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
171 simp-6r 789 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
172 simp-5r 787 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
173 simp-4r 785 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
174 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
175 simpllr 777 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
176 simplr 770 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
177168, 169, 170, 19, 171, 172, 173, 174, 175, 176fourierdlem6 38087 . . . . . . . . . . . . . . . . . . . . . . . . . 26
178166, 177chvarv 2120 . . . . . . . . . . . . . . . . . . . . . . . . 25
179142, 153, 178vtocl 3086 . . . . . . . . . . . . . . . . . . . . . . . 24
180110, 116, 141, 179syl21anc 1291 . . . . . . . . . . . . . . . . . . . . . . 23
181180oveq1d 6323 . . . . . . . . . . . . . . . . . . . . . 22
182181oveq2d 6324 . . . . . . . . . . . . . . . . . . . . 21
183127recnd 9687 . . . . . . . . . . . . . . . . . . . . . . . . . 26
18421recnd 9687 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
185184adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26
186183, 185adddirp1d 37598 . . . . . . . . . . . . . . . . . . . . . . . . 25
187186oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . . . 24
188187adantlr 729 . . . . . . . . . . . . . . . . . . . . . . 23
189188adantr 472 . . . . . . . . . . . . . . . . . . . . . 22
19086recnd 9687 . . . . . . . . . . . . . . . . . . . . . . . . . 26
191190adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25
192130recnd 9687 . . . . . . . . . . . . . . . . . . . . . . . . 25
193184ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . . 25
194191, 192, 193addassd 9683 . . . . . . . . . . . . . . . . . . . . . . . 24
195194eqcomd 2477 . . . . . . . . . . . . . . . . . . . . . . 23
196195adantr 472 . . . . . . . . . . . . . . . . . . . . . 22
197 oveq1 6315 . . . . . . . . . . . . . . . . . . . . . . . 24
198197adantl 473 . . . . . . . . . . . . . . . . . . . . . . 23
1994recnd 9687 . . . . . . . . . . . . . . . . . . . . . . . . . 26
2001recnd 9687 . . . . . . . . . . . . . . . . . . . . . . . . . 26
201199, 200, 184subaddd 10023 . . . . . . . . . . . . . . . . . . . . . . . . 25
20226, 201mpbid 215 . . . . . . . . . . . . . . . . . . . . . . . 24
203202ad3antrrr 744 . . . . . . . . . . . . . . . . . . . . . . 23
204198, 203eqtrd 2505 . . . . . . . . . . . . . . . . . . . . . 22
205189, 196, 2043eqtrd 2509 . . . . . . . . . . . . . . . . . . . . 21
20698, 182, 2053eqtrd 2509 . . . . . . . . . . . . . . . . . . . 20
207 fourierdlem51.bc . . . . . . . . . . . . . . . . . . . . 21
208207ad3antrrr 744 . . . . . . . . . . . . . . . . . . . 20
209206, 208eqeltrd 2549 . . . . . . . . . . . . . . . . . . 19
2102093adantl3 1188 . . . . . . . . . . . . . . . . . 18
211 simpl1 1033 . . . . . . . . . . . . . . . . . . . 20
212 simpl2 1034 . . . . . . . . . . . . . . . . . . . 20
213 fourierdlem51.css . . . . . . . . . . . . . . . . . . . . . . . . 25
214213sselda 3418 . . . . . . . . . . . . . . . . . . . . . . . 24
215214adantlr 729 . . . . . . . . . . . . . . . . . . . . . . 23
2162153adant2 1049 . . . . . . . . . . . . . . . . . . . . . 22
217216adantr 472 . . . . . . . . . . . . . . . . . . . . 21
218 neqne 2651 . . . . . . . . . . . . . . . . . . . . . 22
219218adantl 473 . . . . . . . . . . . . . . . . . . . . 21
2201adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23
221211, 220syl 17 . . . . . . . . . . . . . . . . . . . . . 22
222211, 87syl 17 . . . . . . . . . . . . . . . . . . . . . 22
223 simplr 770 . . . . . . . . . . . . . . . . . . . . . . . . 25
224223, 130readdcld 9688 . . . . . . . . . . . . . . . . . . . . . . . 24
225224rexrd 9708 . . . . . . . . . . . . . . . . . . . . . . 23
226211, 212, 225syl2anc 673 . . . . . . . . . . . . . . . . . . . . . 22
227221, 222, 226eliccelioc 37718 . . . . . . . . . . . . . . . . . . . . 21
228217, 219, 227mpbir2and 936 . . . . . . . . . . . . . . . . . . . 20
22997ad2antrr 740 . . . . . . . . . . . . . . . . . . . . 21
2301ad3antrrr 744 . . . . . . . . . . . . . . . . . . . . . . . 24
2314ad3antrrr 744 . . . . . . . . . . . . . . . . . . . . . . . 24
23222ad3antrrr 744 . . . . . . . . . . . . . . . . . . . . . . . 24
233 simpllr 777 . . . . . . . . . . . . . . . . . . . . . . . 24
23492ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . 24
235 simplr 770 . . . . . . . . . . . . . . . . . . . . . . . 24
23697, 113eqeltrrd 2550 . . . . . . . . . . . . . . . . . . . . . . . . 25
237236ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . 24
238 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . 24
239230, 231, 232, 19, 233, 234, 235, 237, 238fourierdlem35 38117 . . . . . . . . . . . . . . . . . . . . . . 23
240239oveq1d 6323 . . . . . . . . . . . . . . . . . . . . . 22
241240oveq2d 6324 . . . . . . . . . . . . . . . . . . . . 21
242229, 241eqtrd 2505 . . . . . . . . . . . . . . . . . . . 20
243211, 212, 228, 242syl21anc 1291 . . . . . . . . . . . . . . . . . . 19
244 simpl3 1035 . . . . . . . . . . . . . . . . . . 19
245243, 244eqeltrd 2549 . . . . . . . . . . . . . . . . . 18
246210, 245pm2.61dan 808 . . . . . . . . . . . . . . . . 17
2472463exp 1230 . . . . . . . . . . . . . . . 16
24878, 85, 247syl2anc 673 . . . . . . . . . . . . . . 15
24976, 77, 248rexlimd 2866 . . . . . . . . . . . . . 14
25070, 249mpd 15 . . . . . . . . . . . . 13
25164, 250eqeltrd 2549 . . . . . . . . . . . 12
252 eqid 2471 . . . . . . . . . . . 12
253251, 252fmptd 6061 . . . . . . . . . . 11
254 iocssre 11739 . . . . . . . . . . . . . . . 16
255102, 4, 254syl2anc 673 . . . . . . . . . . . . . . 15
256112, 255fssd 5750 . . . . . . . . . . . . . 14
257 ssrab2 3500 . . . . . . . . . . . . . . 15
258257, 81syl5ss 3429 . . . . . . . . . . . . . 14
259256, 258fssresd 5762 . . . . . . . . . . . . 13
260259feqmptd 5932 . . . . . . . . . . . 12
261260feq1d 5724 . . . . . . . . . . 11
262253, 261mpbird 240 . . . . . . . . . 10
263 simplll 776 . . . . . . . . . . . . . . 15
264 id 22 . . . . . . . . . . . . . . . . 17
265 fourierdlem51.h . . . . . . . . . . . . . . . . 17
266264, 265syl6eleqr 2560 . . . . . . . . . . . . . . . 16
267266ad3antlr 745 . . . . . . . . . . . . . . 15
268263, 267jca 541 . . . . . . . . . . . . . 14
269 id 22 . . . . . . . . . . . . . . . 16
270269, 265syl6eleqr 2560 . . . . . . . . . . . . . . 15
271270ad2antlr 741 . . . . . . . . . . . . . 14
272 fvres 5893 . . . . . . . . . . . . . . . . 17
273272eqcomd 2477 . . . . . . . . . . . . . . . 16
274273ad2antlr 741 . . . . . . . . . . . . . . 15
275 id 22 . . . . . . . . . . . . . . . . 17
276275eqcomd 2477 . . . . . . . . . . . . . . . 16
277276adantl 473 . . . . . . . . . . . . . . 15
278 fvres 5893 . . . . . . . . . . . . . . . 16
279278ad3antlr 745 . . . . . . . . . . . . . . 15
280274, 277, 2793eqtrd 2509 . . . . . . . . . . . . . 14
2811ad3antrrr 744 . . . . . . . . . . . . . . . 16
2824ad3antrrr 744 . . . . . . . . . . . . . . . 16
28322ad3antrrr 744 . . . . . . . . . . . . . . . 16
2842ad3antrrr 744 . . . . . . . . . . . . . . . 16
285 simpllr 777 . . . . . . . . . . . . . . . 16
286 simplr 770 . . . . . . . . . . . . . . . 16
287 simpr 468 . . . . . . . . . . . . . . . 16
288281, 282, 283, 284, 265, 19, 31, 285, 286, 287fourierdlem19 38100 . . . . . . . . . . . . . . 15
289287eqcomd 2477 . . . . . . . . . . . . . . . 16
290281, 282, 283, 284, 265, 19, 31, 286, 285, 289fourierdlem19 38100 . . . . . . . . . . . . . . 15
291265, 258syl5eqss 3462 . . . . . . . . . . . . . . . . . 18
292291sselda 3418 . . . . . . . . . . . . . . . . 17
293292ad2antrr 740 . . . . . . . . . . . . . . . 16
294291adantr 472 . . . . . . . . . . . . . . . . . 18
295294sselda 3418 . . . . . . . . . . . . . . . . 17
296295adantr 472 . . . . . . . . . . . . . . . 16
297293, 296lttri3d 9792 . . . . . . . . . . . . . . 15
298288, 290, 297mpbir2and 936 . . . . . . . . . . . . . 14
299268, 271, 280, 298syl21anc 1291 . . . . . . . . . . . . 13
300299ex 441 . . . . . . . . . . . 12
301300ralrimiva 2809 . . . . . . . . . . 11
302301ralrimiva 2809 . . . . . . . . . 10
303 dff13 6177 . . . . . . . . . 10
304262, 302, 303sylanbrc 677 . . . . . . . . 9
305 f1fi 7879 . . . . . . . . 9
30662, 304, 305syl2anc 673 . . . . . . . 8
307 unfi 7856 . . . . . . . 8
30861, 306, 307sylancr 676 . . . . . . 7
309 simpl 464 . . . . . . . . . 10
310 elrabi 3181 . . . . . . . . . . 11
311310adantl 473 . . . . . . . . . 10
31267elrab 3184 . . . . . . . . . . . 12
313312simprbi 471 . . . . . . . . . . 11
314313adantl 473 . . . . . . . . . 10
315 elsn 3973 . . . . . . . . . . . . 13
316 elun1 3592 . . . . . . . . . . . . 13
317315, 316sylbir 218 . . . . . . . . . . . 12
318317adantl 473 . . . . . . . . . . 11
31979ad2antrr 740 . . . . . . . . . . . . . . 15
3205rexrd 9708 . . . . . . . . . . . . . . . 16
321320ad2antrr 740 . . . . . . . . . . . . . . 15
3223, 5iccssred 37698 . . . . . . . . . . . . . . . . . 18
323322sselda 3418 . . . . . . . . . . . . . . . . 17
324323rexrd 9708 . . . . . . . . . . . . . . . 16
325324adantr 472 . . . . . . . . . . . . . . 15