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

Theorem fourierdlem42 38124
 Description: The set of points in a moved partition are finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 29-Sep-2020.)
Hypotheses
Ref Expression
fourierdlem42.b
fourierdlem42.c
fourierdlem42.bc
fourierdlem42.t
fourierdlem42.a
fourierdlem42.af
fourierdlem42.ba
fourierdlem42.ca
fourierdlem42.d
fourierdlem42.i
fourierdlem42.r
fourierdlem42.e inf
fourierdlem42.x
fourierdlem42.y
fourierdlem42.j
fourierdlem42.k t
fourierdlem42.h
fourierdlem42.15
Assertion
Ref Expression
fourierdlem42
Distinct variable groups:   ,,,,,   ,   ,   ,   ,,,,   ,,,   ,   ,,   ,,,   ,   ,,,,,   ,   ,   ,,,   ,,
Allowed substitution hints:   (,)   (,,)   (,,,)   (,,,)   (,,,)   (,,,)   ()   (,)   (,,,)   (,,)   (,)   (,,,)   (,,,)

Proof of Theorem fourierdlem42
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fourierdlem42.x . . . . 5
2 fourierdlem42.y . . . . 5
3 fourierdlem42.j . . . . . 6
4 fourierdlem42.k . . . . . 6 t
53, 4icccmp 21921 . . . . 5
61, 2, 5syl2anc 673 . . . 4
8 fourierdlem42.h . . . . . 6
9 ssrab2 3500 . . . . . . 7
109a1i 11 . . . . . 6
118, 10syl5eqss 3462 . . . . 5
12 retop 21860 . . . . . . . 8
133, 12eqeltri 2545 . . . . . . 7
141, 2iccssred 37698 . . . . . . 7
15 uniretop 21861 . . . . . . . . 9
163unieqi 4199 . . . . . . . . 9
1715, 16eqtr4i 2496 . . . . . . . 8
1817restuni 20255 . . . . . . 7 t
1913, 14, 18sylancr 676 . . . . . 6 t
204unieqi 4199 . . . . . . 7 t
2120eqcomi 2480 . . . . . 6 t
2219, 21syl6eq 2521 . . . . 5
2311, 22sseqtrd 3454 . . . 4
25 simpr 468 . . 3
26 eqid 2471 . . . 4
2726bwth 20502 . . 3
287, 24, 25, 27syl3anc 1292 . 2
2911, 14sstrd 3428 . . . . . . . . . 10
3029ad2antrr 740 . . . . . . . . 9
31 ne0i 3728 . . . . . . . . . 10
3231adantl 473 . . . . . . . . 9
33 fourierdlem42.e . . . . . . . . . . 11 inf
34 fourierdlem42.r . . . . . . . . . . . . 13
35 absf 13477 . . . . . . . . . . . . . . . . . 18
36 ffn 5739 . . . . . . . . . . . . . . . . . 18
3735, 36ax-mp 5 . . . . . . . . . . . . . . . . 17
38 subf 9897 . . . . . . . . . . . . . . . . . 18
39 ffn 5739 . . . . . . . . . . . . . . . . . 18
4038, 39ax-mp 5 . . . . . . . . . . . . . . . . 17
41 frn 5747 . . . . . . . . . . . . . . . . . 18
4238, 41ax-mp 5 . . . . . . . . . . . . . . . . 17
43 fnco 5694 . . . . . . . . . . . . . . . . 17
4437, 40, 42, 43mp3an 1390 . . . . . . . . . . . . . . . 16
45 fourierdlem42.d . . . . . . . . . . . . . . . . 17
4645fneq1i 5680 . . . . . . . . . . . . . . . 16
4744, 46mpbir 214 . . . . . . . . . . . . . . 15
48 fourierdlem42.i . . . . . . . . . . . . . . . 16
49 fourierdlem42.a . . . . . . . . . . . . . . . . . . 19
50 fourierdlem42.b . . . . . . . . . . . . . . . . . . . . 21
51 fourierdlem42.c . . . . . . . . . . . . . . . . . . . . 21
5250, 51iccssred 37698 . . . . . . . . . . . . . . . . . . . 20
53 ax-resscn 9614 . . . . . . . . . . . . . . . . . . . 20
5452, 53syl6ss 3430 . . . . . . . . . . . . . . . . . . 19
5549, 54sstrd 3428 . . . . . . . . . . . . . . . . . 18
56 xpss12 4945 . . . . . . . . . . . . . . . . . 18
5755, 55, 56syl2anc 673 . . . . . . . . . . . . . . . . 17
5857ssdifssd 3560 . . . . . . . . . . . . . . . 16
5948, 58syl5eqss 3462 . . . . . . . . . . . . . . 15
60 fnssres 5699 . . . . . . . . . . . . . . 15
6147, 59, 60sylancr 676 . . . . . . . . . . . . . 14
62 fvres 5893 . . . . . . . . . . . . . . . . . . 19
6362adantl 473 . . . . . . . . . . . . . . . . . 18
6445fveq1i 5880 . . . . . . . . . . . . . . . . . . 19
6564a1i 11 . . . . . . . . . . . . . . . . . 18
66 ffun 5742 . . . . . . . . . . . . . . . . . . . 20
6738, 66ax-mp 5 . . . . . . . . . . . . . . . . . . 19
6859sselda 3418 . . . . . . . . . . . . . . . . . . . 20
6938fdmi 5746 . . . . . . . . . . . . . . . . . . . 20
7068, 69syl6eleqr 2560 . . . . . . . . . . . . . . . . . . 19
71 fvco 5956 . . . . . . . . . . . . . . . . . . 19
7267, 70, 71sylancr 676 . . . . . . . . . . . . . . . . . 18
7363, 65, 723eqtrd 2509 . . . . . . . . . . . . . . . . 17
7438a1i 11 . . . . . . . . . . . . . . . . . . 19
7574, 68ffvelrnd 6038 . . . . . . . . . . . . . . . . . 18
7675abscld 13575 . . . . . . . . . . . . . . . . 17
7773, 76eqeltrd 2549 . . . . . . . . . . . . . . . 16
78 elxp2 4857 . . . . . . . . . . . . . . . . . . . 20
7968, 78sylib 201 . . . . . . . . . . . . . . . . . . 19
80 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . 23
81803ad2ant3 1053 . . . . . . . . . . . . . . . . . . . . . 22
82 df-ov 6311 . . . . . . . . . . . . . . . . . . . . . . 23
83 simp1l 1054 . . . . . . . . . . . . . . . . . . . . . . . 24
84 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
85 simpl 464 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
8684, 85eqeltrrd 2550 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8786adantll 728 . . . . . . . . . . . . . . . . . . . . . . . . 25
88873adant2 1049 . . . . . . . . . . . . . . . . . . . . . . . 24
8955adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26
9048eleq2i 2541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
91 eldif 3400 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
9290, 91sylbb 202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
9392simpld 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
94 opelxp 4869 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
9593, 94sylib 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
9695adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
9796simpld 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26
9889, 97sseldd 3419 . . . . . . . . . . . . . . . . . . . . . . . . 25
9996simprd 470 . . . . . . . . . . . . . . . . . . . . . . . . . 26
10089, 99sseldd 3419 . . . . . . . . . . . . . . . . . . . . . . . . 25
10192simprd 470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
102 df-br 4396 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
103101, 102sylnibr 312 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
104 vex 3034 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
105104ideq 4992 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
106103, 105sylnib 311 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
107106neqned 2650 . . . . . . . . . . . . . . . . . . . . . . . . . 26
108107adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . 25
10998, 100, 108subne0d 10014 . . . . . . . . . . . . . . . . . . . . . . . 24
11083, 88, 109syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . 23
11182, 110syl5eqner 2718 . . . . . . . . . . . . . . . . . . . . . 22
11281, 111eqnetrd 2710 . . . . . . . . . . . . . . . . . . . . 21
1131123exp 1230 . . . . . . . . . . . . . . . . . . . 20
114113rexlimdvv 2877 . . . . . . . . . . . . . . . . . . 19
11579, 114mpd 15 . . . . . . . . . . . . . . . . . 18
116 absgt0 13464 . . . . . . . . . . . . . . . . . . 19
11775, 116syl 17 . . . . . . . . . . . . . . . . . 18
118115, 117mpbid 215 . . . . . . . . . . . . . . . . 17
11973eqcomd 2477 . . . . . . . . . . . . . . . . 17
120118, 119breqtrd 4420 . . . . . . . . . . . . . . . 16
12177, 120elrpd 11361 . . . . . . . . . . . . . . 15
122121ralrimiva 2809 . . . . . . . . . . . . . 14
123 fnfvrnss 6066 . . . . . . . . . . . . . 14
12461, 122, 123syl2anc 673 . . . . . . . . . . . . 13
12534, 124syl5eqss 3462 . . . . . . . . . . . 12
126 ltso 9732 . . . . . . . . . . . . . 14
127126a1i 11 . . . . . . . . . . . . 13
128 fourierdlem42.af . . . . . . . . . . . . . . . . . . 19
129 xpfi 7860 . . . . . . . . . . . . . . . . . . 19
130128, 128, 129syl2anc 673 . . . . . . . . . . . . . . . . . 18
131 diffi 7821 . . . . . . . . . . . . . . . . . 18
132130, 131syl 17 . . . . . . . . . . . . . . . . 17
13348, 132syl5eqel 2553 . . . . . . . . . . . . . . . 16
134 fnfi 7867 . . . . . . . . . . . . . . . 16
13561, 133, 134syl2anc 673 . . . . . . . . . . . . . . 15
136 rnfi 7875 . . . . . . . . . . . . . . 15
137135, 136syl 17 . . . . . . . . . . . . . 14
13834, 137syl5eqel 2553 . . . . . . . . . . . . 13
13934a1i 11 . . . . . . . . . . . . . 14
14045a1i 11 . . . . . . . . . . . . . . . . . . 19
141140reseq1d 5110 . . . . . . . . . . . . . . . . . 18
142141fveq1d 5881 . . . . . . . . . . . . . . . . 17
143 fourierdlem42.ba . . . . . . . . . . . . . . . . . . . . 21
144 fourierdlem42.ca . . . . . . . . . . . . . . . . . . . . 21
145 opelxp 4869 . . . . . . . . . . . . . . . . . . . . 21
146143, 144, 145sylanbrc 677 . . . . . . . . . . . . . . . . . . . 20
147 fourierdlem42.bc . . . . . . . . . . . . . . . . . . . . . . . 24
14850, 147ltned 9788 . . . . . . . . . . . . . . . . . . . . . . 23
149148neneqd 2648 . . . . . . . . . . . . . . . . . . . . . 22
150 ideqg 4991 . . . . . . . . . . . . . . . . . . . . . . 23
151144, 150syl 17 . . . . . . . . . . . . . . . . . . . . . 22
152149, 151mtbird 308 . . . . . . . . . . . . . . . . . . . . 21
153 df-br 4396 . . . . . . . . . . . . . . . . . . . . 21
154152, 153sylnib 311 . . . . . . . . . . . . . . . . . . . 20
155146, 154eldifd 3401 . . . . . . . . . . . . . . . . . . 19
156155, 48syl6eleqr 2560 . . . . . . . . . . . . . . . . . 18
157 fvres 5893 . . . . . . . . . . . . . . . . . 18
158156, 157syl 17 . . . . . . . . . . . . . . . . 17
15950recnd 9687 . . . . . . . . . . . . . . . . . . . . 21
16051recnd 9687 . . . . . . . . . . . . . . . . . . . . 21
161 opelxp 4869 . . . . . . . . . . . . . . . . . . . . 21
162159, 160, 161sylanbrc 677 . . . . . . . . . . . . . . . . . . . 20
163162, 69syl6eleqr 2560 . . . . . . . . . . . . . . . . . . 19
164 fvco 5956 . . . . . . . . . . . . . . . . . . 19
16567, 163, 164sylancr 676 . . . . . . . . . . . . . . . . . 18
166 df-ov 6311 . . . . . . . . . . . . . . . . . . . . 21
167166eqcomi 2480 . . . . . . . . . . . . . . . . . . . 20
168167a1i 11 . . . . . . . . . . . . . . . . . . 19
169168fveq2d 5883 . . . . . . . . . . . . . . . . . 18
170165, 169eqtrd 2505 . . . . . . . . . . . . . . . . 17
171142, 158, 1703eqtrrd 2510 . . . . . . . . . . . . . . . 16
172 fnfvelrn 6034 . . . . . . . . . . . . . . . . 17
17361, 156, 172syl2anc 673 . . . . . . . . . . . . . . . 16
174171, 173eqeltrd 2549 . . . . . . . . . . . . . . 15
175 ne0i 3728 . . . . . . . . . . . . . . 15
176174, 175syl 17 . . . . . . . . . . . . . 14
177139, 176eqnetrd 2710 . . . . . . . . . . . . 13
178 resss 5134 . . . . . . . . . . . . . . . . 17
179 rnss 5069 . . . . . . . . . . . . . . . . 17
180178, 179ax-mp 5 . . . . . . . . . . . . . . . 16
18145rneqi 5067 . . . . . . . . . . . . . . . . 17
182 rncoss 5101 . . . . . . . . . . . . . . . . . 18
183 frn 5747 . . . . . . . . . . . . . . . . . . 19
18435, 183ax-mp 5 . . . . . . . . . . . . . . . . . 18
185182, 184sstri 3427 . . . . . . . . . . . . . . . . 17
186181, 185eqsstri 3448 . . . . . . . . . . . . . . . 16
187180, 186sstri 3427 . . . . . . . . . . . . . . 15
18834, 187eqsstri 3448 . . . . . . . . . . . . . 14
189188a1i 11 . . . . . . . . . . . . 13
190 fiinfcl 8035 . . . . . . . . . . . . 13 inf
191127, 138, 177, 189, 190syl13anc 1294 . . . . . . . . . . . 12 inf
192125, 191sseldd 3419 . . . . . . . . . . 11 inf
19333, 192syl5eqel 2553 . . . . . . . . . 10
194193ad2antrr 740 . . . . . . . . 9
1953, 30, 32, 194lptre2pt 37817 . . . . . . . 8
196 simpll 768 . . . . . . . . . . . . . 14
19729sselda 3418 . . . . . . . . . . . . . . . . 17
198197adantrr 731 . . . . . . . . . . . . . . . 16
199198adantr 472 . . . . . . . . . . . . . . 15
20029sselda 3418 . . . . . . . . . . . . . . . . 17
201200adantrl 730 . . . . . . . . . . . . . . . 16
202201adantr 472 . . . . . . . . . . . . . . 15
203 simpr 468 . . . . . . . . . . . . . . 15
204199, 202, 2033jca 1210 . . . . . . . . . . . . . 14
2058eleq2i 2541 . . . . . . . . . . . . . . . . . . 19
206 oveq1 6315 . . . . . . . . . . . . . . . . . . . . . . 23
207206eleq1d 2533 . . . . . . . . . . . . . . . . . . . . . 22
208207rexbidv 2892 . . . . . . . . . . . . . . . . . . . . 21
209 oveq1 6315 . . . . . . . . . . . . . . . . . . . . . . . 24
210209oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . . 23
211210eleq1d 2533 . . . . . . . . . . . . . . . . . . . . . 22
212211cbvrexv 3006 . . . . . . . . . . . . . . . . . . . . 21
213208, 212syl6bb 269 . . . . . . . . . . . . . . . . . . . 20
214213elrab 3184 . . . . . . . . . . . . . . . . . . 19
215205, 214sylbb 202 . . . . . . . . . . . . . . . . . 18
216215simprd 470 . . . . . . . . . . . . . . . . 17
217216adantr 472 . . . . . . . . . . . . . . . 16
2188eleq2i 2541 . . . . . . . . . . . . . . . . . . 19
219 oveq1 6315 . . . . . . . . . . . . . . . . . . . . . 22
220219eleq1d 2533 . . . . . . . . . . . . . . . . . . . . 21
221220rexbidv 2892 . . . . . . . . . . . . . . . . . . . 20
222221elrab 3184 . . . . . . . . . . . . . . . . . . 19
223218, 222sylbb 202 . . . . . . . . . . . . . . . . . 18
224223simprd 470 . . . . . . . . . . . . . . . . 17
225224adantl 473 . . . . . . . . . . . . . . . 16
226 reeanv 2944 . . . . . . . . . . . . . . . 16
227217, 225, 226sylanbrc 677 . . . . . . . . . . . . . . 15
228227ad2antlr 741 . . . . . . . . . . . . . 14
229 simplll 776 . . . . . . . . . . . . . . . 16
230 simpl1 1033 . . . . . . . . . . . . . . . . . . 19
231 simpl2 1034 . . . . . . . . . . . . . . . . . . 19
232 simpr 468 . . . . . . . . . . . . . . . . . . 19
233230, 231, 2323jca 1210 . . . . . . . . . . . . . . . . . 18
234233adantll 728 . . . . . . . . . . . . . . . . 17
235234adantlr 729 . . . . . . . . . . . . . . . 16
236 simplr 770 . . . . . . . . . . . . . . . 16
237 eleq1 2537 . . . . . . . . . . . . . . . . . . . . 21
238 breq2 4399 . . . . . . . . . . . . . . . . . . . . 21
239237, 2383anbi23d 1368 . . . . . . . . . . . . . . . . . . . 20
240239anbi2d 718 . . . . . . . . . . . . . . . . . . 19
241 oveq1 6315 . . . . . . . . . . . . . . . . . . . . . 22
242241eleq1d 2533 . . . . . . . . . . . . . . . . . . . . 21
243242anbi2d 718 . . . . . . . . . . . . . . . . . . . 20
2442432rexbidv 2897 . . . . . . . . . . . . . . . . . . 19
245240, 244anbi12d 725 . . . . . . . . . . . . . . . . . 18
246 oveq2 6316 . . . . . . . . . . . . . . . . . . . 20
247246fveq2d 5883 . . . . . . . . . . . . . . . . . . 19
248247breq2d 4407 . . . . . . . . . . . . . . . . . 18
249245, 248imbi12d 327 . . . . . . . . . . . . . . . . 17
250 eleq1 2537 . . . . . . . . . . . . . . . . . . . . . 22
251 breq1 4398 . . . . . . . . . . . . . . . . . . . . . 22
252250, 2513anbi13d 1367 . . . . . . . . . . . . . . . . . . . . 21
253252anbi2d 718 . . . . . . . . . . . . . . . . . . . 20
254 oveq1 6315 . . . . . . . . . . . . . . . . . . . . . . 23
255254eleq1d 2533 . . . . . . . . . . . . . . . . . . . . . 22
256255anbi1d 719 . . . . . . . . . . . . . . . . . . . . 21
2572562rexbidv 2897 . . . . . . . . . . . . . . . . . . . 20
258253, 257anbi12d 725 . . . . . . . . . . . . . . . . . . 19
259 oveq1 6315 . . . . . . . . . . . . . . . . . . . . 21
260259fveq2d 5883 . . . . . . . . . . . . . . . . . . . 20
261260breq2d 4407 . . . . . . . . . . . . . . . . . . 19
262258, 261imbi12d 327 . . . . . . . . . . . . . . . . . 18
263 fourierdlem42.15 . . . . . . . . . . . . . . . . . . 19
264263simprbi 471 . . . . . . . . . . . . . . . . . . . 20
265263biimpi 199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
266265simpld 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
267266simpld 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
268267, 50syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
269268adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
270267, 51syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
271270adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
272267, 49syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
273272sselda 3418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
274273adantrl 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
275272sselda 3418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
276275adantrr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
277269, 271, 274, 276iccsuble 37716 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
278 fourierdlem42.t . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
279277, 278syl6breqr 4436 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
2802793adant2 1049 . . . . . . . . . . . . . . . . . . . . . . . . . 26
281280adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25
282 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
283 zre 10965 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
284283adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
285284ad2antlr 741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
286 zre 10965 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
287286adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
288287ad2antlr 741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
289285, 288ltnled 9799 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
290282, 289mpbird 240 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
29151, 50resubcld 10068 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
292278, 291syl5eqel 2553 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
293267, 292syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
294293ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
295287adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
296284adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
297295, 296resubcld 10068 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
298293adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
299297, 298remulcld 9689 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
300299adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
301266simprd 470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
302301simp2d 1043 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
303302adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
304286adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
305293adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
306304, 305remulcld 9689 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
307306adantrl 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
308303, 307readdcld 9688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
309301simp1d 1042 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
310309adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
311283adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
312293adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
313311, 312remulcld 9689 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
314313adantrr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
315310, 314readdcld 9688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
316308, 315resubcld 10068 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
317316adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
318293recnd 9687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
319318mulid2d 9679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
320319eqcomd 2477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
321320ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
322 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
323 zltlem1 11013 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
324323ad2antlr 741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
325322, 324mpbid 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
326284ad2antlr 741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
327 peano2rem 9961 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
328295, 327syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
329328adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
330 1re 9660 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
331 resubcl 9958 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
332330, 326, 331sylancr 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
333 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
334326, 329, 332, 333leadd1dd 10248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
335 zcn 10966 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
336335adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
337 1cnd 9677 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
338336, 337pncan3d 10008 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
339338ad2antlr 741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
340 zcn 10966 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
341340adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
342341, 337, 336npncand 10029 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
343342ad2antlr 741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
344334, 339, 3433brtr3d 4425 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
345325, 344syldan 478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
346330a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
347297adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
34850, 51posdifd 10221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
349147, 348mpbid 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
350349, 278syl6breqr 4436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
351292, 350elrpd 11361 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
352267, 351syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
353352ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
354346, 347, 353lemul1d 11404 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
355345, 354mpbid 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
356321, 355eqbrtrd 4416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
357302, 309resubcld 10068 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
358301simp3d 1044 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
359309, 302posdifd 10221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
360358, 359mpbid 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
361357, 360elrpd 11361 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
362361adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
363299, 362ltaddrp2d 11395 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
364302recnd 9687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
365364adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
366306recnd 9687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
367366adantrl 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
368309recnd 9687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
369368adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
370313recnd 9687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
371370adantrr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
372365, 367, 369, 371addsub4d 10052 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
373340ad2antll 743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
374335ad2antrl 742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
375318adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
376373, 374, 375subdird 10096 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
377376eqcomd 2477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
378377oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
379372, 378eqtr2d 2506 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
380363, 379breqtrd 4420 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
381380adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
382294, 300, 317, 356, 381lelttrd 9810 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
383294, 317ltnled 9799 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
384382, 383mpbid 215 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
385290, 384syldan 478 . . . . . . . . . . . . . . . . . . . . . . . . . 26
3863853adantl3 1188 . . . . . . . . . . . . . . . . . . . . . . . . 25
387281, 386condan 811 . . . . . . . . . . . . . . . . . . . . . . . 24
388188, 191sseldi 3416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 inf
38933, 388syl5eqel 2553 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
390267, 389syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
3913903ad2ant1 1051 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
392391ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
3932933ad2ant1 1051 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
394393ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
395284, 287resubcld 10068 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
396395adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
397396, 298remulcld 9689 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
3983973adant3 1050 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
399398ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
400 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
401143, 144jca 541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
402400, 401, 1473jca 1210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
403 eleq1 2537 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
404403anbi2d 718 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
405 breq2 4399 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
406404, 4053anbi23d 1368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
407 oveq1 6315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
408407breq2d 4407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
409406, 408imbi12d 327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
410 simp2l 1056 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
411 eleq1 2537 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
412411anbi1d 719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
413 breq1 4398 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
414412, 4133anbi23d 1368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
415 oveq2 6316 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
416415breq2d 4407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
417414, 416imbi12d 327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
418188a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
419 0re 9661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
42034eleq2i 2541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
421420biimpi 199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
422421adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
42361adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
424 fvelrnb 5926 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
425423, 424syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
426422, 425mpbid 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
427121rpge0d 11368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
4284273adant3 1050 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
429 simp3 1032 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
430428, 429breqtrd 4420 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
4314303exp 1230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
432431adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
433432rexlimdv 2870 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
434426, 433mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
435434ralrimiva 2809 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
436 breq1 4398 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
437436ralbidv 2829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
438437rspcev 3136 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
439419, 435, 438sylancr 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
4404393ad2ant1 1051 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
441 pm3.22 456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
442 opelxp 4869 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
443441, 442sylibr 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
4444433ad2ant2 1052 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
44549, 52sstrd 3428 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
446445sselda 3418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
447446adantrr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
4484473adant3 1050 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
449 simp3 1032 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
450448, 449gtned 9787 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
451450neneqd 2648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
452 df-br 4396 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
453 vex 3034 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
454453ideq 4992 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
455452, 454bitr3i 259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
456451, 455sylnibr 312 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
457444, 456eldifd 3401 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
458457, 48syl6eleqr 2560 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
459448, 449ltned 9788 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
4601413ad2ant1 1051 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
461460fveq1d 5881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
4624433ad2ant2 1052 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
463 necom 2696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
464463biimpi 199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
465464neneqd 2648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
4664653ad2ant3 1053 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
467466, 455sylnibr 312 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
468462, 467eldifd 3401 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
469468, 48syl6eleqr 2560 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
470 fvres 5893 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
471469, 470syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
472 simp1 1030 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
473472, 469jca 541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
474 eleq1 2537 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
475474anbi2d 718 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
476 eleq1 2537 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
477475, 476imbi12d 327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
478477, 70vtoclg 3093 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
479469, 473, 478sylc 61 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
480 fvco 5956 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
48167, 479, 480sylancr 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
482 df-ov 6311 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
483482eqcomi 2480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
484483fveq2i 5882 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
485481, 484syl6eq 2521 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
486461, 471, 4853eqtrd 2509 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
487459, 486syld3an3 1337 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
488445sselda 3418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
489488adantrl 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
4904893adant3 1050 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
491448, 490, 449ltled 9800 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
492448, 490, 491abssubge0d 13570 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
493487, 492eqtrd 2505 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
494 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
495494eqeq1d 2473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
496495rspcev 3136 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
497458, 493, 496syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
498489, 447resubcld 10068 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
499 elex 3040 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
500498, 499syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
5015003adant3 1050 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
502 simp1 1030 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
503 eleq1 2537 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
504 eqeq2 2482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
505504rexbidv 2892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
506503, 505bibi12d 328 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
507506imbi2d 323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
50861, 424syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
509507, 508vtoclg 3093 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
510501, 502, 509sylc 61 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
511497, 510mpbird 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
512511, 34syl6eleqr 2560 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
513 infrelb 10618 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 inf
514418, 440, 512, 513syl3anc 1292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 inf
51533, 514syl5eqbr 4429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
516417, 515vtoclg 3093 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
517410, 516mpcom 36 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
518409, 517vtoclg 3093 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
519144, 402, 518sylc 61 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
520519, 278syl6breqr 4436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
521267, 520syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
5225213ad2ant1 1051 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
523522ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
524364adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
525524, 366pncan2d 10007 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
526525oveq1d 6323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
527340adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
528318adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
529419a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
530529, 350gtned 9787 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
531267, 530syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
532531adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
533527, 528, 532divcan4d 10411 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
534526, 533eqtr2d 2506 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
535534adantrl 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
536535adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
537 oveq1 6315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
538537oveq1d 6323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
539538adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35