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

Theorem fourierdlem42 31820
 Description: The set of points in a moved partition are finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
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
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 21307 . . . . 5
61, 2, 5syl2anc 661 . . . 4
76adantr 465 . . 3
8 fourierdlem42.h . . . . . 6
9 ssrab2 3570 . . . . . . 7
109a1i 11 . . . . . 6
118, 10syl5eqss 3533 . . . . 5
12 retop 21245 . . . . . . . 8
133, 12eqeltri 2527 . . . . . . 7
141, 2iccssred 31475 . . . . . . 7
15 uniretop 21246 . . . . . . . . 9
163unieqi 4243 . . . . . . . . 9
1715, 16eqtr4i 2475 . . . . . . . 8
1817restuni 19640 . . . . . . 7 t
1913, 14, 18sylancr 663 . . . . . 6 t
204unieqi 4243 . . . . . . 7 t
2120eqcomi 2456 . . . . . 6 t
2219, 21syl6eq 2500 . . . . 5
2311, 22sseqtrd 3525 . . . 4
2423adantr 465 . . 3
25 simpr 461 . . 3
26 eqid 2443 . . . 4
2726bwth 19887 . . 3
287, 24, 25, 27syl3anc 1229 . 2
2911, 14sstrd 3499 . . . . . . . . . 10
3029ad2antrr 725 . . . . . . . . 9
31 ne0i 3776 . . . . . . . . . 10
3231adantl 466 . . . . . . . . 9
33 fourierdlem42.e . . . . . . . . . . 11
34 fourierdlem42.r . . . . . . . . . . . . 13
35 absf 13151 . . . . . . . . . . . . . . . . . 18
36 ffn 5721 . . . . . . . . . . . . . . . . . 18
3735, 36ax-mp 5 . . . . . . . . . . . . . . . . 17
38 subf 9827 . . . . . . . . . . . . . . . . . 18
39 ffn 5721 . . . . . . . . . . . . . . . . . 18
4038, 39ax-mp 5 . . . . . . . . . . . . . . . . 17
41 frn 5727 . . . . . . . . . . . . . . . . . 18
4238, 41ax-mp 5 . . . . . . . . . . . . . . . . 17
43 fnco 5679 . . . . . . . . . . . . . . . . 17
4437, 40, 42, 43mp3an 1325 . . . . . . . . . . . . . . . 16
45 fourierdlem42.d . . . . . . . . . . . . . . . . 17
4645fneq1i 5665 . . . . . . . . . . . . . . . 16
4744, 46mpbir 209 . . . . . . . . . . . . . . 15
48 fourierdlem42.i . . . . . . . . . . . . . . . 16
49 fourierdlem42.a . . . . . . . . . . . . . . . . . . 19
50 fourierdlem42.b . . . . . . . . . . . . . . . . . . . . 21
51 fourierdlem42.c . . . . . . . . . . . . . . . . . . . . 21
5250, 51iccssred 31475 . . . . . . . . . . . . . . . . . . . 20
53 ax-resscn 9552 . . . . . . . . . . . . . . . . . . . 20
5452, 53syl6ss 3501 . . . . . . . . . . . . . . . . . . 19
5549, 54sstrd 3499 . . . . . . . . . . . . . . . . . 18
56 xpss12 5098 . . . . . . . . . . . . . . . . . 18
5755, 55, 56syl2anc 661 . . . . . . . . . . . . . . . . 17
5857ssdifssd 3627 . . . . . . . . . . . . . . . 16
5948, 58syl5eqss 3533 . . . . . . . . . . . . . . 15
60 fnssres 5684 . . . . . . . . . . . . . . 15
6147, 59, 60sylancr 663 . . . . . . . . . . . . . 14
62 fvres 5870 . . . . . . . . . . . . . . . . . . 19
6362adantl 466 . . . . . . . . . . . . . . . . . 18
6445fveq1i 5857 . . . . . . . . . . . . . . . . . . 19
6564a1i 11 . . . . . . . . . . . . . . . . . 18
66 ffun 5723 . . . . . . . . . . . . . . . . . . . 20
6738, 66ax-mp 5 . . . . . . . . . . . . . . . . . . 19
6859sselda 3489 . . . . . . . . . . . . . . . . . . . 20
6938fdmi 5726 . . . . . . . . . . . . . . . . . . . 20
7068, 69syl6eleqr 2542 . . . . . . . . . . . . . . . . . . 19
71 fvco 5934 . . . . . . . . . . . . . . . . . . 19
7267, 70, 71sylancr 663 . . . . . . . . . . . . . . . . . 18
7363, 65, 723eqtrd 2488 . . . . . . . . . . . . . . . . 17
7438a1i 11 . . . . . . . . . . . . . . . . . . 19
7574, 68ffvelrnd 6017 . . . . . . . . . . . . . . . . . 18
7675abscld 13248 . . . . . . . . . . . . . . . . 17
7773, 76eqeltrd 2531 . . . . . . . . . . . . . . . 16
78 elxp2 5007 . . . . . . . . . . . . . . . . . . . 20
7968, 78sylib 196 . . . . . . . . . . . . . . . . . . 19
80 fveq2 5856 . . . . . . . . . . . . . . . . . . . . . . 23
81803ad2ant3 1020 . . . . . . . . . . . . . . . . . . . . . 22
82 df-ov 6284 . . . . . . . . . . . . . . . . . . . . . . 23
83 simp1l 1021 . . . . . . . . . . . . . . . . . . . . . . . 24
84 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
85 simpl 457 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
8684, 85eqeltrrd 2532 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8786adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . 25
88873adant2 1016 . . . . . . . . . . . . . . . . . . . . . . . 24
8955adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . 26
9048eleq2i 2521 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
91 eldif 3471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
9290, 91sylbb 197 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
9392simpld 459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
94 opelxp 5019 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
9593, 94sylib 196 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
9695adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
9796simpld 459 . . . . . . . . . . . . . . . . . . . . . . . . . 26
9889, 97sseldd 3490 . . . . . . . . . . . . . . . . . . . . . . . . 25
9996simprd 463 . . . . . . . . . . . . . . . . . . . . . . . . . 26
10089, 99sseldd 3490 . . . . . . . . . . . . . . . . . . . . . . . . 25
10192simprd 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
102 df-br 4438 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
103101, 102sylnibr 305 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
104 vex 3098 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
105104ideq 5145 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
106103, 105sylnib 304 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
107106neqned 2646 . . . . . . . . . . . . . . . . . . . . . . . . . 26
108107adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . 25
10998, 100, 108subne0d 9945 . . . . . . . . . . . . . . . . . . . . . . . 24
11083, 88, 109syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . 23
11182, 110syl5eqner 2744 . . . . . . . . . . . . . . . . . . . . . 22
11281, 111eqnetrd 2736 . . . . . . . . . . . . . . . . . . . . 21
1131123exp 1196 . . . . . . . . . . . . . . . . . . . 20
114113rexlimdvv 2941 . . . . . . . . . . . . . . . . . . 19
11579, 114mpd 15 . . . . . . . . . . . . . . . . . 18
116 absgt0 13138 . . . . . . . . . . . . . . . . . . 19
11775, 116syl 16 . . . . . . . . . . . . . . . . . 18
118115, 117mpbid 210 . . . . . . . . . . . . . . . . 17
11973eqcomd 2451 . . . . . . . . . . . . . . . . 17
120118, 119breqtrd 4461 . . . . . . . . . . . . . . . 16
12177, 120elrpd 11264 . . . . . . . . . . . . . . 15
122121ralrimiva 2857 . . . . . . . . . . . . . 14
123 fnfvrnss 6044 . . . . . . . . . . . . . 14
12461, 122, 123syl2anc 661 . . . . . . . . . . . . 13
12534, 124syl5eqss 3533 . . . . . . . . . . . 12
126 ltso 9668 . . . . . . . . . . . . . . 15
127126a1i 11 . . . . . . . . . . . . . 14
128 cnvso 5536 . . . . . . . . . . . . . 14
129127, 128sylib 196 . . . . . . . . . . . . 13
130 fourierdlem42.af . . . . . . . . . . . . . . . . . . 19
131 xpfi 7793 . . . . . . . . . . . . . . . . . . 19
132130, 130, 131syl2anc 661 . . . . . . . . . . . . . . . . . 18
133 diffi 7753 . . . . . . . . . . . . . . . . . 18
134132, 133syl 16 . . . . . . . . . . . . . . . . 17
13548, 134syl5eqel 2535 . . . . . . . . . . . . . . . 16
136 fnfi 7800 . . . . . . . . . . . . . . . 16
13761, 135, 136syl2anc 661 . . . . . . . . . . . . . . 15
138 rnfi 7807 . . . . . . . . . . . . . . 15
139137, 138syl 16 . . . . . . . . . . . . . 14
14034, 139syl5eqel 2535 . . . . . . . . . . . . 13
14134a1i 11 . . . . . . . . . . . . . 14
14245a1i 11 . . . . . . . . . . . . . . . . . . 19
143142reseq1d 5262 . . . . . . . . . . . . . . . . . 18
144143fveq1d 5858 . . . . . . . . . . . . . . . . 17
145 fourierdlem42.ba . . . . . . . . . . . . . . . . . . . . 21
146 fourierdlem42.ca . . . . . . . . . . . . . . . . . . . . 21
147 opelxp 5019 . . . . . . . . . . . . . . . . . . . . 21
148145, 146, 147sylanbrc 664 . . . . . . . . . . . . . . . . . . . 20
149 fourierdlem42.bc . . . . . . . . . . . . . . . . . . . . . . . 24
15050, 149ltned 9724 . . . . . . . . . . . . . . . . . . . . . . 23
151150neneqd 2645 . . . . . . . . . . . . . . . . . . . . . 22
152 ideqg 5144 . . . . . . . . . . . . . . . . . . . . . . 23
153146, 152syl 16 . . . . . . . . . . . . . . . . . . . . . 22
154151, 153mtbird 301 . . . . . . . . . . . . . . . . . . . . 21
155 df-br 4438 . . . . . . . . . . . . . . . . . . . . 21
156154, 155sylnib 304 . . . . . . . . . . . . . . . . . . . 20
157148, 156eldifd 3472 . . . . . . . . . . . . . . . . . . 19
158157, 48syl6eleqr 2542 . . . . . . . . . . . . . . . . . 18
159 fvres 5870 . . . . . . . . . . . . . . . . . 18
160158, 159syl 16 . . . . . . . . . . . . . . . . 17
16150recnd 9625 . . . . . . . . . . . . . . . . . . . . 21
16251recnd 9625 . . . . . . . . . . . . . . . . . . . . 21
163 opelxp 5019 . . . . . . . . . . . . . . . . . . . . 21
164161, 162, 163sylanbrc 664 . . . . . . . . . . . . . . . . . . . 20
165164, 69syl6eleqr 2542 . . . . . . . . . . . . . . . . . . 19
166 fvco 5934 . . . . . . . . . . . . . . . . . . 19
16767, 165, 166sylancr 663 . . . . . . . . . . . . . . . . . 18
168 df-ov 6284 . . . . . . . . . . . . . . . . . . . . 21
169168eqcomi 2456 . . . . . . . . . . . . . . . . . . . 20
170169a1i 11 . . . . . . . . . . . . . . . . . . 19
171170fveq2d 5860 . . . . . . . . . . . . . . . . . 18
172167, 171eqtrd 2484 . . . . . . . . . . . . . . . . 17
173144, 160, 1723eqtrrd 2489 . . . . . . . . . . . . . . . 16
174 fnfvelrn 6013 . . . . . . . . . . . . . . . . 17
17561, 158, 174syl2anc 661 . . . . . . . . . . . . . . . 16
176173, 175eqeltrd 2531 . . . . . . . . . . . . . . 15
177 ne0i 3776 . . . . . . . . . . . . . . 15
178176, 177syl 16 . . . . . . . . . . . . . 14
179141, 178eqnetrd 2736 . . . . . . . . . . . . 13
180 resss 5287 . . . . . . . . . . . . . . . . 17
181 rnss 5221 . . . . . . . . . . . . . . . . 17
182180, 181ax-mp 5 . . . . . . . . . . . . . . . 16
18345rneqi 5219 . . . . . . . . . . . . . . . . 17
184 rncoss 5253 . . . . . . . . . . . . . . . . . 18
185 frn 5727 . . . . . . . . . . . . . . . . . . 19
18635, 185ax-mp 5 . . . . . . . . . . . . . . . . . 18
187184, 186sstri 3498 . . . . . . . . . . . . . . . . 17
188183, 187eqsstri 3519 . . . . . . . . . . . . . . . 16
189182, 188sstri 3498 . . . . . . . . . . . . . . 15
19034, 189eqsstri 3519 . . . . . . . . . . . . . 14
191190a1i 11 . . . . . . . . . . . . 13
192 fisupcl 7930 . . . . . . . . . . . . 13
193129, 140, 179, 191, 192syl13anc 1231 . . . . . . . . . . . 12
194125, 193sseldd 3490 . . . . . . . . . . 11
19533, 194syl5eqel 2535 . . . . . . . . . 10
196195ad2antrr 725 . . . . . . . . 9
1973, 30, 32, 196lptre2pt 31554 . . . . . . . 8
198 simpll 753 . . . . . . . . . . . . . 14
19929sselda 3489 . . . . . . . . . . . . . . . . 17
200199adantrr 716 . . . . . . . . . . . . . . . 16
201200adantr 465 . . . . . . . . . . . . . . 15
20229sselda 3489 . . . . . . . . . . . . . . . . 17
203202adantrl 715 . . . . . . . . . . . . . . . 16
204203adantr 465 . . . . . . . . . . . . . . 15
205 simpr 461 . . . . . . . . . . . . . . 15
206201, 204, 2053jca 1177 . . . . . . . . . . . . . 14
2078eleq2i 2521 . . . . . . . . . . . . . . . . . . 19
208 oveq1 6288 . . . . . . . . . . . . . . . . . . . . . . 23
209208eleq1d 2512 . . . . . . . . . . . . . . . . . . . . . 22
210209rexbidv 2954 . . . . . . . . . . . . . . . . . . . . 21
211 oveq1 6288 . . . . . . . . . . . . . . . . . . . . . . . 24
212211oveq2d 6297 . . . . . . . . . . . . . . . . . . . . . . 23
213212eleq1d 2512 . . . . . . . . . . . . . . . . . . . . . 22
214213cbvrexv 3071 . . . . . . . . . . . . . . . . . . . . 21
215210, 214syl6bb 261 . . . . . . . . . . . . . . . . . . . 20
216215elrab 3243 . . . . . . . . . . . . . . . . . . 19
217207, 216sylbb 197 . . . . . . . . . . . . . . . . . 18
218217simprd 463 . . . . . . . . . . . . . . . . 17
219218adantr 465 . . . . . . . . . . . . . . . 16
2208eleq2i 2521 . . . . . . . . . . . . . . . . . . 19
221 oveq1 6288 . . . . . . . . . . . . . . . . . . . . . 22
222221eleq1d 2512 . . . . . . . . . . . . . . . . . . . . 21
223222rexbidv 2954 . . . . . . . . . . . . . . . . . . . 20
224223elrab 3243 . . . . . . . . . . . . . . . . . . 19
225220, 224sylbb 197 . . . . . . . . . . . . . . . . . 18
226225simprd 463 . . . . . . . . . . . . . . . . 17
227226adantl 466 . . . . . . . . . . . . . . . 16
228 reeanv 3011 . . . . . . . . . . . . . . . 16
229219, 227, 228sylanbrc 664 . . . . . . . . . . . . . . 15
230229ad2antlr 726 . . . . . . . . . . . . . 14
231 simplll 759 . . . . . . . . . . . . . . . 16
232 simpl1 1000 . . . . . . . . . . . . . . . . . . 19
233 simpl2 1001 . . . . . . . . . . . . . . . . . . 19
234 simpr 461 . . . . . . . . . . . . . . . . . . 19
235232, 233, 2343jca 1177 . . . . . . . . . . . . . . . . . 18
236235adantll 713 . . . . . . . . . . . . . . . . 17
237236adantlr 714 . . . . . . . . . . . . . . . 16
238 simplr 755 . . . . . . . . . . . . . . . 16
239 eleq1 2515 . . . . . . . . . . . . . . . . . . . . 21
240 breq2 4441 . . . . . . . . . . . . . . . . . . . . 21
241239, 2403anbi23d 1303 . . . . . . . . . . . . . . . . . . . 20
242241anbi2d 703 . . . . . . . . . . . . . . . . . . 19
243 oveq1 6288 . . . . . . . . . . . . . . . . . . . . . 22
244243eleq1d 2512 . . . . . . . . . . . . . . . . . . . . 21
245244anbi2d 703 . . . . . . . . . . . . . . . . . . . 20
2462452rexbidv 2961 . . . . . . . . . . . . . . . . . . 19
247242, 246anbi12d 710 . . . . . . . . . . . . . . . . . 18
248 oveq2 6289 . . . . . . . . . . . . . . . . . . . 20
249248fveq2d 5860 . . . . . . . . . . . . . . . . . . 19
250249breq2d 4449 . . . . . . . . . . . . . . . . . 18
251247, 250imbi12d 320 . . . . . . . . . . . . . . . . 17
252 eleq1 2515 . . . . . . . . . . . . . . . . . . . . . 22
253 breq1 4440 . . . . . . . . . . . . . . . . . . . . . 22
254252, 2533anbi13d 1302 . . . . . . . . . . . . . . . . . . . . 21
255254anbi2d 703 . . . . . . . . . . . . . . . . . . . 20
256 oveq1 6288 . . . . . . . . . . . . . . . . . . . . . . 23
257256eleq1d 2512 . . . . . . . . . . . . . . . . . . . . . 22
258257anbi1d 704 . . . . . . . . . . . . . . . . . . . . 21
2592582rexbidv 2961 . . . . . . . . . . . . . . . . . . . 20
260255, 259anbi12d 710 . . . . . . . . . . . . . . . . . . 19
261 oveq1 6288 . . . . . . . . . . . . . . . . . . . . 21
262261fveq2d 5860 . . . . . . . . . . . . . . . . . . . 20
263262breq2d 4449 . . . . . . . . . . . . . . . . . . 19
264260, 263imbi12d 320 . . . . . . . . . . . . . . . . . 18
265 fourierdlem42.15 . . . . . . . . . . . . . . . . . . 19
266265simprbi 464 . . . . . . . . . . . . . . . . . . . 20
267265biimpi 194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
268267simpld 459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
269268simpld 459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
270269, 50syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
271270adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
272269, 51syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
273272adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
274269, 49syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
275274sselda 3489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
276275adantrl 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
277274sselda 3489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
278277adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
279271, 273, 276, 278iccsuble 31495 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
280 fourierdlem42.t . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
281279, 280syl6breqr 4477 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
2822813adant2 1016 . . . . . . . . . . . . . . . . . . . . . . . . . 26
283282adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25
284 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
285 zre 10875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
286285adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
287286ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
288 zre 10875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
289288adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
290289ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
291287, 290ltnled 9735 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
292284, 291mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
29351, 50resubcld 9994 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
294280, 293syl5eqel 2535 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
295269, 294syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
296295ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
297289adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
298286adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
299297, 298resubcld 9994 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
300295adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
301299, 300remulcld 9627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
302301adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
303268simprd 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
304303simp2d 1010 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
305304adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
306288adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
307295adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
308306, 307remulcld 9627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
309308adantrl 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
310305, 309readdcld 9626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
311303simp1d 1009 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
312311adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
313285adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
314295adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
315313, 314remulcld 9627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
316315adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
317312, 316readdcld 9626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
318310, 317resubcld 9994 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
319318adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
320295recnd 9625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
321320mulid2d 9617 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
322321eqcomd 2451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
323322ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
324 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
325 zltlem1 10923 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
326325ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
327324, 326mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
328286ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
329 peano2rem 9891 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
330297, 329syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
331330adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
332 1re 9598 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
333 resubcl 9888 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
334332, 328, 333sylancr 663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
335 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
336328, 331, 334, 335leadd1dd 10173 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
337 zcn 10876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
338337adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
339 1cnd 9615 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
340338, 339pncan3d 9939 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
341340ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
342 zcn 10876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
343342adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
344343, 339, 338npncand 9960 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
345344ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
346336, 341, 3453brtr3d 4466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
347327, 346syldan 470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
348332a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
349299adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
35050, 51posdifd 10146 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
351149, 350mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
352351, 280syl6breqr 4477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
353294, 352elrpd 11264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
354269, 353syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
355354ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
356348, 349, 355lemul1d 11305 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
357347, 356mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
358323, 357eqbrtrd 4457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
359304, 311resubcld 9994 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
360303simp3d 1011 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
361311, 304posdifd 10146 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
362360, 361mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
363359, 362elrpd 11264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
364363adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
365301, 364ltaddrp2d 11296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
366304recnd 9625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
367366adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
368308recnd 9625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
369368adantrl 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
370311recnd 9625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
371370adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
372315recnd 9625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
373372adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
374367, 369, 371, 373addsub4d 9983 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
375342ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
376337ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
377320adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
378375, 376, 377subdird 10020 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
379378eqcomd 2451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
380379oveq2d 6297 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
381374, 380eqtr2d 2485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
382365, 381breqtrd 4461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
383382adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
384296, 302, 319, 358, 383lelttrd 9743 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
385296, 319ltnled 9735 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
386384, 385mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
387292, 386syldan 470 . . . . . . . . . . . . . . . . . . . . . . . . . 26
3883873adantl3 1155 . . . . . . . . . . . . . . . . . . . . . . . . 25
389283, 388condan 794 . . . . . . . . . . . . . . . . . . . . . . . 24
390190, 193sseldi 3487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
39133, 390syl5eqel 2535 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
392269, 391syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
3933923ad2ant1 1018 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
394393ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
3952953ad2ant1 1018 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
396395ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
397286, 289resubcld 9994 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
398397adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
399398, 300remulcld 9627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
4003993adant3 1017 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
401400ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
402 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
403145, 146jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
404402, 403, 1493jca 1177 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
405 eleq1 2515 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
406405anbi2d 703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
407 breq2 4441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
408406, 4073anbi23d 1303 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
409 oveq1 6288 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
410409breq2d 4449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
411408, 410imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
412 simp2l 1023 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
413 eleq1 2515 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
414413anbi1d 704 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
415 breq1 4440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
416414, 4153anbi23d 1303 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
417 oveq2 6289 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
418417breq2d 4449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
419416, 418imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
420190a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
421 0re 9599 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
42234eleq2i 2521 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
423422biimpi 194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
424423adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
42561adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
426 fvelrnb 5905 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
427425, 426syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
428424, 427mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
429121rpge0d 11270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
4304293adant3 1017 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
431 simp3 999 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
432430, 431breqtrd 4461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
4334323exp 1196 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
434433adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
435434rexlimdv 2933 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
436428, 435mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
437436ralrimiva 2857 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
438 breq1 4440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
439438ralbidv 2882 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
440439rspcev 3196 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
441421, 437, 440sylancr 663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
4424413ad2ant1 1018 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
443 pm3.22 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
444 opelxp 5019 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
445443, 444sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
4464453ad2ant2 1019 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
44749, 52sstrd 3499 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
448447sselda 3489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
449448adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
4504493adant3 1017 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
451 simp3 999 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
452450, 451gtned 9723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
453452neneqd 2645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
454 df-br 4438 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
455 vex 3098 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
456455ideq 5145 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
457454, 456bitr3i 251 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
458453, 457sylnibr 305 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
459446, 458eldifd 3472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
460459, 48syl6eleqr 2542 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
461450, 451ltned 9724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
4621433ad2ant1 1018 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
463462fveq1d 5858 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
4644453ad2ant2 1019 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
465 necom 2712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
466465biimpi 194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
467466neneqd 2645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
4684673ad2ant3 1020 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
469468, 457sylnibr 305 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
470464, 469eldifd 3472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
471470, 48syl6eleqr 2542 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
472 fvres 5870 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
473471, 472syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
474 simp1 997 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
475474, 471jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
476 eleq1 2515 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
477476anbi2d 703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
478 eleq1 2515 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
479477, 478imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
480479, 70vtoclg 3153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
481471, 475, 480sylc 60 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
482 fvco 5934 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
48367, 481, 482sylancr 663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
484 df-ov 6284 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
485484eqcomi 2456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
486485fveq2i 5859 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
487483, 486syl6eq 2500 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
488463, 473, 4873eqtrd 2488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
489461, 488syld3an3 1274 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
490447sselda 3489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
491490adantrl 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
4924913adant3 1017 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
493450, 492, 451ltled 9736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
494450, 492, 493abssubge0d 13244 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
495489, 494eqtrd 2484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
496 fveq2 5856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
497496eqeq1d 2445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
498497rspcev 3196 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
499460, 495, 498syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
500491, 449resubcld 9994 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
501 elex 3104 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
502500, 501syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
5035023adant3 1017 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
504 simp1 997 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
505 eleq1 2515 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
506 eqeq2 2458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
507506rexbidv 2954 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
508505, 507bibi12d 321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
509508imbi2d 316 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
51061, 426syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
511509, 510vtoclg 3153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
512503, 504, 511sylc 60 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
513499, 512mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
514513, 34syl6eleqr 2542 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
515 infmrlb 10531 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
516420, 442, 514, 515syl3anc 1229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
51733, 516syl5eqbr 4470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
518419, 517vtoclg 3153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
519412, 518mpcom 36 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
520411, 519vtoclg 3153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
521146, 404, 520sylc 60 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
522521, 280syl6breqr 4477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
523269, 522syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
5245233ad2ant1 1018 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
525524ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
526366adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
527526, 368pncan2d 9938 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
528527oveq1d 6296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
529342adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
530320adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
531421a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
532531, 352gtned 9723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
533269, 532syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
534533adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
535529, 530, 534divcan4d 10333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
536528, 535eqtr2d 2485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
537536adantrl 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
538537adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
539 oveq1 6288 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
540539oveq1d 6296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36