Mathbox for Jeff Madsen < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  heiborlem6 Unicode version

Theorem heiborlem6 26415
 Description: Lemma for heibor 26420. Since the sequence of balls connected by the function ensures that each ball nontrivially intersects with the next (since the empty set has a finite subcover, the intersection of any two successive balls in the sequence is nonempty), and each ball is half the size of the previous one, the distance between the centers is at most times the size of the larger, and so if we expand each ball by a factor of we get a nested sequence of balls. (Contributed by Jeff Madsen, 23-Jan-2014.)
Hypotheses
Ref Expression
heibor.1
heibor.3
heibor.4
heibor.5
heibor.6
heibor.7
heibor.8
heibor.9
heibor.10
heibor.11
heibor.12
Assertion
Ref Expression
heiborlem6
Distinct variable groups:   ,,,,,   ,,   ,,   ,,,,,,,,   ,,,,,,   ,,,,,   ,,,,   ,,,,,,,,   ,,,,,,   ,,,,,,,,   ,,,,,,,,   ,,,,,   ,,,,   ,
Allowed substitution hints:   (,,,,,)   (,,)   (,,)   (,,)   (,)   (,,)   (,,,,,)   (,,,)   (,)

Proof of Theorem heiborlem6
StepHypRef Expression
1 nnnn0 10184 . . . 4
2 heibor.6 . . . . . . . 8
3 cmetmet 19192 . . . . . . . 8
42, 3syl 16 . . . . . . 7
5 metxmet 18317 . . . . . . 7
64, 5syl 16 . . . . . 6
76adantr 452 . . . . 5
8 heibor.7 . . . . . . . . 9
9 inss1 3521 . . . . . . . . 9
10 fss 5558 . . . . . . . . 9
118, 9, 10sylancl 644 . . . . . . . 8
12 peano2nn0 10216 . . . . . . . 8
13 ffvelrn 5827 . . . . . . . 8
1411, 12, 13syl2an 464 . . . . . . 7
1514elpwid 3768 . . . . . 6
16 heibor.1 . . . . . . . . 9
17 heibor.3 . . . . . . . . 9
18 heibor.4 . . . . . . . . 9
19 heibor.5 . . . . . . . . 9
20 heibor.8 . . . . . . . . 9
21 heibor.9 . . . . . . . . 9
22 heibor.10 . . . . . . . . 9
23 heibor.11 . . . . . . . . 9
2416, 17, 18, 19, 2, 8, 20, 21, 22, 23heiborlem4 26413 . . . . . . . 8
2512, 24sylan2 461 . . . . . . 7
26 fvex 5701 . . . . . . . . 9
27 ovex 6065 . . . . . . . . 9
2816, 17, 18, 26, 27heiborlem2 26411 . . . . . . . 8
2928simp2bi 973 . . . . . . 7
3025, 29syl 16 . . . . . 6
3115, 30sseldd 3309 . . . . 5
3211ffvelrnda 5829 . . . . . . 7
3332elpwid 3768 . . . . . 6
3416, 17, 18, 19, 2, 8, 20, 21, 22, 23heiborlem4 26413 . . . . . . 7
35 fvex 5701 . . . . . . . . 9
36 vex 2919 . . . . . . . . 9
3716, 17, 18, 35, 36heiborlem2 26411 . . . . . . . 8
3837simp2bi 973 . . . . . . 7
3934, 38syl 16 . . . . . 6
4033, 39sseldd 3309 . . . . 5
41 3re 10027 . . . . . 6
42 2nn 10089 . . . . . . . . 9
43 nnexpcl 11349 . . . . . . . . 9
4442, 12, 43sylancr 645 . . . . . . . 8
4544nnrpd 10603 . . . . . . 7
4645adantl 453 . . . . . 6
47 rerpdivcl 10595 . . . . . 6
4841, 46, 47sylancr 645 . . . . 5
49 nnexpcl 11349 . . . . . . . . 9
5042, 49mpan 652 . . . . . . . 8
5150nnrpd 10603 . . . . . . 7
5251adantl 453 . . . . . 6
53 rerpdivcl 10595 . . . . . 6
5441, 52, 53sylancr 645 . . . . 5
55 oveq1 6047 . . . . . . . . . . . 12
56 oveq2 6048 . . . . . . . . . . . . . 14
5756oveq2d 6056 . . . . . . . . . . . . 13
5857oveq2d 6056 . . . . . . . . . . . 12
59 ovex 6065 . . . . . . . . . . . 12
6055, 58, 19, 59ovmpt2 6168 . . . . . . . . . . 11
6140, 60sylancom 649 . . . . . . . . . 10
62 df-br 4173 . . . . . . . . . . . . . . . . 17
63 fveq2 5687 . . . . . . . . . . . . . . . . . . . . . 22
64 df-ov 6043 . . . . . . . . . . . . . . . . . . . . . 22
6563, 64syl6eqr 2454 . . . . . . . . . . . . . . . . . . . . 21
6635, 36op2ndd 6317 . . . . . . . . . . . . . . . . . . . . . 22
6766oveq1d 6055 . . . . . . . . . . . . . . . . . . . . 21
6865, 67breq12d 4185 . . . . . . . . . . . . . . . . . . . 20
69 fveq2 5687 . . . . . . . . . . . . . . . . . . . . . . 23
70 df-ov 6043 . . . . . . . . . . . . . . . . . . . . . . 23
7169, 70syl6eqr 2454 . . . . . . . . . . . . . . . . . . . . . 22
7265, 67oveq12d 6058 . . . . . . . . . . . . . . . . . . . . . 22
7371, 72ineq12d 3503 . . . . . . . . . . . . . . . . . . . . 21
7473eleq1d 2470 . . . . . . . . . . . . . . . . . . . 20
7568, 74anbi12d 692 . . . . . . . . . . . . . . . . . . 19
7675rspccv 3009 . . . . . . . . . . . . . . . . . 18
7721, 76syl 16 . . . . . . . . . . . . . . . . 17
7862, 77syl5bi 209 . . . . . . . . . . . . . . . 16
7978adantr 452 . . . . . . . . . . . . . . 15
8034, 79mpd 15 . . . . . . . . . . . . . 14
8180simpld 446 . . . . . . . . . . . . 13
82 ovex 6065 . . . . . . . . . . . . . . 15
8316, 17, 18, 82, 27heiborlem2 26411 . . . . . . . . . . . . . 14
8483simp2bi 973 . . . . . . . . . . . . 13
8581, 84syl 16 . . . . . . . . . . . 12
8615, 85sseldd 3309 . . . . . . . . . . 11
8712adantl 453 . . . . . . . . . . 11
88 oveq1 6047 . . . . . . . . . . . 12
89 oveq2 6048 . . . . . . . . . . . . . 14
9089oveq2d 6056 . . . . . . . . . . . . 13
9190oveq2d 6056 . . . . . . . . . . . 12
92 ovex 6065 . . . . . . . . . . . 12
9388, 91, 19, 92ovmpt2 6168 . . . . . . . . . . 11
9486, 87, 93syl2anc 643 . . . . . . . . . 10
9561, 94ineq12d 3503 . . . . . . . . 9
9680simprd 450 . . . . . . . . . 10
97 0elpw 4329 . . . . . . . . . . . . 13
98 0fin 7295 . . . . . . . . . . . . 13
99 elin 3490 . . . . . . . . . . . . 13
10097, 98, 99mpbir2an 887 . . . . . . . . . . . 12
101 0ss 3616 . . . . . . . . . . . 12
102 unieq 3984 . . . . . . . . . . . . . 14
103102sseq2d 3336 . . . . . . . . . . . . 13
104103rspcev 3012 . . . . . . . . . . . 12
105100, 101, 104mp2an 654 . . . . . . . . . . 11
106 0ex 4299 . . . . . . . . . . . . 13
107 sseq1 3329 . . . . . . . . . . . . . . 15
108107rexbidv 2687 . . . . . . . . . . . . . 14
109108notbid 286 . . . . . . . . . . . . 13
110106, 109, 17elab2 3045 . . . . . . . . . . . 12
111110con2bii 323 . . . . . . . . . . 11
112105, 111mpbi 200 . . . . . . . . . 10
113 nelne2 2657 . . . . . . . . . 10
11496, 112, 113sylancl 644 . . . . . . . . 9
11595, 114eqnetrrd 2587 . . . . . . . 8
11651rpreccld 10614 . . . . . . . . . . . . . 14
117116adantl 453 . . . . . . . . . . . . 13
118117rpred 10604 . . . . . . . . . . . 12
11945rpreccld 10614 . . . . . . . . . . . . . 14
120119adantl 453 . . . . . . . . . . . . 13
121120rpred 10604 . . . . . . . . . . . 12
122 rexadd 10774 . . . . . . . . . . . 12
123118, 121, 122syl2anc 643 . . . . . . . . . . 11
124123breq1d 4182 . . . . . . . . . 10
125117rpxrd 10605 . . . . . . . . . . 11
126120rpxrd 10605 . . . . . . . . . . 11
127 bldisj 18381 . . . . . . . . . . . . 13
1281273exp2 1171 . . . . . . . . . . . 12
129128imp32 423 . . . . . . . . . . 11
1307, 40, 86, 125, 126, 129syl32anc 1192 . . . . . . . . . 10
131124, 130sylbird 227 . . . . . . . . 9
132131necon3ad 2603 . . . . . . . 8
133115, 132mpd 15 . . . . . . 7
134117, 120rpaddcld 10619 . . . . . . . . . 10
135134rpred 10604 . . . . . . . . 9
1364adantr 452 . . . . . . . . . 10
137 metcl 18315 . . . . . . . . . 10
138136, 40, 86, 137syl3anc 1184 . . . . . . . . 9
139135, 138letrid 9179 . . . . . . . 8
140139ord 367 . . . . . . 7
141133, 140mpd 15 . . . . . 6
142 seqp1 11293 . . . . . . . . . . . 12
143 nn0uz 10476 . . . . . . . . . . . 12
144142, 143eleq2s 2496 . . . . . . . . . . 11
14523fveq1i 5688 . . . . . . . . . . 11
14623fveq1i 5688 . . . . . . . . . . . 12
147146oveq1i 6050 . . . . . . . . . . 11
148144, 145, 1473eqtr4g 2461 . . . . . . . . . 10
149 nn0p1nn 10215 . . . . . . . . . . . . . . . 16
150 nnne0 9988 . . . . . . . . . . . . . . . . 17
151150neneqd 2583 . . . . . . . . . . . . . . . 16
152149, 151syl 16 . . . . . . . . . . . . . . 15
153 iffalse 3706 . . . . . . . . . . . . . . 15
154152, 153syl 16 . . . . . . . . . . . . . 14
155 ovex 6065 . . . . . . . . . . . . . 14
156154, 155syl6eqel 2492 . . . . . . . . . . . . 13
157 eqeq1 2410 . . . . . . . . . . . . . . 15
158 oveq1 6047 . . . . . . . . . . . . . . 15
159157, 158ifbieq2d 3719 . . . . . . . . . . . . . 14
160 eqid 2404 . . . . . . . . . . . . . 14
161159, 160fvmptg 5763 . . . . . . . . . . . . 13
16212, 156, 161syl2anc 643 . . . . . . . . . . . 12
163 nn0cn 10187 . . . . . . . . . . . . 13
164 ax-1cn 9004 . . . . . . . . . . . . 13
165 pncan 9267 . . . . . . . . . . . . 13
166163, 164, 165sylancl 644 . . . . . . . . . . . 12
167162, 154, 1663eqtrd 2440 . . . . . . . . . . 11
168167oveq2d 6056 . . . . . . . . . 10
169148, 168eqtrd 2436 . . . . . . . . 9
170169adantl 453 . . . . . . . 8
171170oveq1d 6055 . . . . . . 7
172 metsym 18333 . . . . . . . 8
173136, 86, 40, 172syl3anc 1184 . . . . . . 7
174171, 173eqtrd 2436 . . . . . 6
175 3cn 10028 . . . . . . . . . . . . 13
1761752timesi 10057 . . . . . . . . . . . 12
177176oveq1i 6050 . . . . . . . . . . 11
178 pncan 9267 . . . . . . . . . . . 12
179175, 175, 178mp2an 654 . . . . . . . . . . 11
180 df-3 10015 . . . . . . . . . . 11
181177, 179, 1803eqtri 2428 . . . . . . . . . 10
182181oveq1i 6050 . . . . . . . . 9
183 rpcn 10576 . . . . . . . . . . 11
184 rpne0 10583 . . . . . . . . . . 11
185 2cn 10026 . . . . . . . . . . . . 13
186185, 175mulcli 9051 . . . . . . . . . . . 12
187 divsubdir 9666 . . . . . . . . . . . 12
188186, 175, 187mp3an12 1269 . . . . . . . . . . 11
189183, 184, 188syl2anc 643 . . . . . . . . . 10
19045, 189syl 16 . . . . . . . . 9
191 divdir 9657 . . . . . . . . . . . 12
192185, 164, 191mp3an12 1269 . . . . . . . . . . 11
193183, 184, 192syl2anc 643 . . . . . . . . . 10
19445, 193syl 16 . . . . . . . . 9
195182, 190, 1943eqtr3a 2460 . . . . . . . 8
196 rpcn 10576 . . . . . . . . . . . 12
197 rpne0 10583 . . . . . . . . . . . 12
198 2ne0 10039 . . . . . . . . . . . . . 14
199185, 198pm3.2i 442 . . . . . . . . . . . . 13
200 divcan5 9672 . . . . . . . . . . . . 13
201175, 199, 200mp3an13 1270 . . . . . . . . . . . 12
202196, 197, 201syl2anc 643 . . . . . . . . . . 11
20351, 202syl 16 . . . . . . . . . 10
20451, 196syl 16 . . . . . . . . . . . . 13
205 mulcom 9032 . . . . . . . . . . . . 13
206185, 204, 205sylancr 645 . . . . . . . . . . . 12
207 expp1 11343 . . . . . . . . . . . . 13
208185, 207mpan 652 . . . . . . . . . . . 12
209206, 208eqtr4d 2439 . . . . . . . . . . 11
210209oveq2d 6056 . . . . . . . . . 10
211203, 210eqtr3d 2438 . . . . . . . . 9
212211oveq1d 6055 . . . . . . . 8
213 divcan5 9672 . . . . . . . . . . . . 13
214164, 199, 213mp3an13 1270 . . . . . . . . . . . 12
215196, 197, 214syl2anc 643 . . . . . . . . . . 11
21651, 215syl 16 . . . . . . . . . 10
217185mulid1i 9048 . . . . . . . . . . . 12
218217a1i 11 . . . . . . . . . . 11
219218, 209oveq12d 6058 . . . . . . . . . 10
220216, 219eqtr3d 2438 . . . . . . . . 9
221220oveq1d 6055 . . . . . . . 8
222195, 212, 2213eqtr4d 2446 . . . . . . 7
223222adantl 453 . . . . . 6
224141, 174, 2233brtr4d 4202 . . . . 5
225 blss2 18387 . . . . 5
2267, 31, 40, 48, 54, 224, 225syl33anc 1199 . . . 4
2271, 226sylan2 461 . . 3
228 peano2nn 9968 . . . . . . 7
229 fveq2 5687 . . . . . . . . 9
230 oveq2 6048 . . . . . . . . . 10
231230oveq2d 6056 . . . . . . . . 9
232229, 231opeq12d 3952 . . . . . . . 8
233 heibor.12 . . . . . . . 8
234 opex 4387 . . . . . . . 8
235232, 233, 234fvmpt 5765 . . . . . . 7
236228, 235syl 16 . . . . . 6
237236adantl 453 . . . . 5
238237fveq2d 5691 . . . 4
239 df-ov 6043 . . . 4
240238, 239syl6eqr 2454 . . 3
241 fveq2 5687 . . . . . . . 8
242 oveq2 6048 . . . . . . . . 9
243242oveq2d 6056 . . . . . . . 8
244241, 243opeq12d 3952 . . . . . . 7
245 opex 4387 . . . . . . 7
246244, 233, 245fvmpt 5765 . . . . . 6
247246fveq2d 5691 . . . . 5
248 df-ov 6043 . . . . 5
249247, 248syl6eqr 2454 . . . 4