Step | Hyp | Ref
| Expression |
1 | | remet.1 |
. . . 4
β’ π· = ((abs β β )
βΎ (β Γ β)) |
2 | 1 | rexmet 24177 |
. . 3
β’ π· β
(βMetββ) |
3 | | tgioo.2 |
. . . 4
β’ π½ = (MetOpenβπ·) |
4 | 3 | mopnval 23814 |
. . 3
β’ (π· β
(βMetββ) β π½ = (topGenβran (ballβπ·))) |
5 | 2, 4 | ax-mp 5 |
. 2
β’ π½ = (topGenβran
(ballβπ·)) |
6 | 1 | blssioo 24181 |
. . 3
β’ ran
(ballβπ·) β ran
(,) |
7 | | elssuni 4902 |
. . . . . . 7
β’ (π£ β ran (,) β π£ β βͺ ran (,)) |
8 | | unirnioo 13375 |
. . . . . . 7
β’ β =
βͺ ran (,) |
9 | 7, 8 | sseqtrrdi 3999 |
. . . . . 6
β’ (π£ β ran (,) β π£ β
β) |
10 | | retopbas 24147 |
. . . . . . . . . 10
β’ ran (,)
β TopBases |
11 | 10 | a1i 11 |
. . . . . . . . 9
β’ ((π£ β ran (,) β§ π₯ β π£) β ran (,) β
TopBases) |
12 | | simpl 484 |
. . . . . . . . 9
β’ ((π£ β ran (,) β§ π₯ β π£) β π£ β ran (,)) |
13 | 9 | sselda 3948 |
. . . . . . . . . 10
β’ ((π£ β ran (,) β§ π₯ β π£) β π₯ β β) |
14 | | 1re 11163 |
. . . . . . . . . . . 12
β’ 1 β
β |
15 | 1 | bl2ioo 24178 |
. . . . . . . . . . . 12
β’ ((π₯ β β β§ 1 β
β) β (π₯(ballβπ·)1) = ((π₯ β 1)(,)(π₯ + 1))) |
16 | 14, 15 | mpan2 690 |
. . . . . . . . . . 11
β’ (π₯ β β β (π₯(ballβπ·)1) = ((π₯ β 1)(,)(π₯ + 1))) |
17 | | ioof 13373 |
. . . . . . . . . . . . 13
β’
(,):(β* Γ β*)βΆπ«
β |
18 | | ffn 6672 |
. . . . . . . . . . . . 13
β’
((,):(β* Γ β*)βΆπ«
β β (,) Fn (β* Γ
β*)) |
19 | 17, 18 | ax-mp 5 |
. . . . . . . . . . . 12
β’ (,) Fn
(β* Γ β*) |
20 | | peano2rem 11476 |
. . . . . . . . . . . . 13
β’ (π₯ β β β (π₯ β 1) β
β) |
21 | 20 | rexrd 11213 |
. . . . . . . . . . . 12
β’ (π₯ β β β (π₯ β 1) β
β*) |
22 | | peano2re 11336 |
. . . . . . . . . . . . 13
β’ (π₯ β β β (π₯ + 1) β
β) |
23 | 22 | rexrd 11213 |
. . . . . . . . . . . 12
β’ (π₯ β β β (π₯ + 1) β
β*) |
24 | | fnovrn 7533 |
. . . . . . . . . . . 12
β’ (((,) Fn
(β* Γ β*) β§ (π₯ β 1) β β* β§
(π₯ + 1) β
β*) β ((π₯ β 1)(,)(π₯ + 1)) β ran (,)) |
25 | 19, 21, 23, 24 | mp3an2i 1467 |
. . . . . . . . . . 11
β’ (π₯ β β β ((π₯ β 1)(,)(π₯ + 1)) β ran
(,)) |
26 | 16, 25 | eqeltrd 2834 |
. . . . . . . . . 10
β’ (π₯ β β β (π₯(ballβπ·)1) β ran (,)) |
27 | 13, 26 | syl 17 |
. . . . . . . . 9
β’ ((π£ β ran (,) β§ π₯ β π£) β (π₯(ballβπ·)1) β ran (,)) |
28 | | simpr 486 |
. . . . . . . . . 10
β’ ((π£ β ran (,) β§ π₯ β π£) β π₯ β π£) |
29 | | 1rp 12927 |
. . . . . . . . . . . 12
β’ 1 β
β+ |
30 | | blcntr 23789 |
. . . . . . . . . . . 12
β’ ((π· β
(βMetββ) β§ π₯ β β β§ 1 β
β+) β π₯ β (π₯(ballβπ·)1)) |
31 | 2, 29, 30 | mp3an13 1453 |
. . . . . . . . . . 11
β’ (π₯ β β β π₯ β (π₯(ballβπ·)1)) |
32 | 13, 31 | syl 17 |
. . . . . . . . . 10
β’ ((π£ β ran (,) β§ π₯ β π£) β π₯ β (π₯(ballβπ·)1)) |
33 | 28, 32 | elind 4158 |
. . . . . . . . 9
β’ ((π£ β ran (,) β§ π₯ β π£) β π₯ β (π£ β© (π₯(ballβπ·)1))) |
34 | | basis2 22324 |
. . . . . . . . 9
β’ (((ran
(,) β TopBases β§ π£
β ran (,)) β§ ((π₯(ballβπ·)1) β ran (,) β§ π₯ β (π£ β© (π₯(ballβπ·)1)))) β βπ§ β ran (,)(π₯ β π§ β§ π§ β (π£ β© (π₯(ballβπ·)1)))) |
35 | 11, 12, 27, 33, 34 | syl22anc 838 |
. . . . . . . 8
β’ ((π£ β ran (,) β§ π₯ β π£) β βπ§ β ran (,)(π₯ β π§ β§ π§ β (π£ β© (π₯(ballβπ·)1)))) |
36 | | ovelrn 7534 |
. . . . . . . . . . 11
β’ ((,) Fn
(β* Γ β*) β (π§ β ran (,) β βπ β β*
βπ β
β* π§ =
(π(,)π))) |
37 | 19, 36 | ax-mp 5 |
. . . . . . . . . 10
β’ (π§ β ran (,) β
βπ β
β* βπ β β* π§ = (π(,)π)) |
38 | | eleq2 2823 |
. . . . . . . . . . . . . . 15
β’ (π§ = (π(,)π) β (π₯ β π§ β π₯ β (π(,)π))) |
39 | | sseq1 3973 |
. . . . . . . . . . . . . . 15
β’ (π§ = (π(,)π) β (π§ β (π£ β© (π₯(ballβπ·)1)) β (π(,)π) β (π£ β© (π₯(ballβπ·)1)))) |
40 | 38, 39 | anbi12d 632 |
. . . . . . . . . . . . . 14
β’ (π§ = (π(,)π) β ((π₯ β π§ β§ π§ β (π£ β© (π₯(ballβπ·)1))) β (π₯ β (π(,)π) β§ (π(,)π) β (π£ β© (π₯(ballβπ·)1))))) |
41 | | inss2 4193 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π£ β© (π₯(ballβπ·)1)) β (π₯(ballβπ·)1) |
42 | | sstr 3956 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π(,)π) β (π£ β© (π₯(ballβπ·)1)) β§ (π£ β© (π₯(ballβπ·)1)) β (π₯(ballβπ·)1)) β (π(,)π) β (π₯(ballβπ·)1)) |
43 | 41, 42 | mpan2 690 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π(,)π) β (π£ β© (π₯(ballβπ·)1)) β (π(,)π) β (π₯(ballβπ·)1)) |
44 | 43 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π₯ β (π(,)π) β§ (π(,)π) β (π£ β© (π₯(ballβπ·)1))) β (π(,)π) β (π₯(ballβπ·)1)) |
45 | | elioore 13303 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π₯ β (π(,)π) β π₯ β β) |
46 | 45 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π₯ β (π(,)π) β§ (π(,)π) β (π£ β© (π₯(ballβπ·)1))) β π₯ β β) |
47 | 46, 16 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π₯ β (π(,)π) β§ (π(,)π) β (π£ β© (π₯(ballβπ·)1))) β (π₯(ballβπ·)1) = ((π₯ β 1)(,)(π₯ + 1))) |
48 | 44, 47 | sseqtrd 3988 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π₯ β (π(,)π) β§ (π(,)π) β (π£ β© (π₯(ballβπ·)1))) β (π(,)π) β ((π₯ β 1)(,)(π₯ + 1))) |
49 | | dfss 3932 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π(,)π) β ((π₯ β 1)(,)(π₯ + 1)) β (π(,)π) = ((π(,)π) β© ((π₯ β 1)(,)(π₯ + 1)))) |
50 | 48, 49 | sylib 217 |
. . . . . . . . . . . . . . . . . 18
β’ ((π₯ β (π(,)π) β§ (π(,)π) β (π£ β© (π₯(ballβπ·)1))) β (π(,)π) = ((π(,)π) β© ((π₯ β 1)(,)(π₯ + 1)))) |
51 | | eliooxr 13331 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β (π(,)π) β (π β β* β§ π β
β*)) |
52 | 21, 23 | jca 513 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ β β β ((π₯ β 1) β
β* β§ (π₯ + 1) β
β*)) |
53 | 45, 52 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β (π(,)π) β ((π₯ β 1) β β* β§
(π₯ + 1) β
β*)) |
54 | | iooin 13307 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β β*
β§ π β
β*) β§ ((π₯ β 1) β β* β§
(π₯ + 1) β
β*)) β ((π(,)π) β© ((π₯ β 1)(,)(π₯ + 1))) = (if(π β€ (π₯ β 1), (π₯ β 1), π)(,)if(π β€ (π₯ + 1), π, (π₯ + 1)))) |
55 | 51, 53, 54 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β (π(,)π) β ((π(,)π) β© ((π₯ β 1)(,)(π₯ + 1))) = (if(π β€ (π₯ β 1), (π₯ β 1), π)(,)if(π β€ (π₯ + 1), π, (π₯ + 1)))) |
56 | 55 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π₯ β (π(,)π) β§ (π(,)π) β (π£ β© (π₯(ballβπ·)1))) β ((π(,)π) β© ((π₯ β 1)(,)(π₯ + 1))) = (if(π β€ (π₯ β 1), (π₯ β 1), π)(,)if(π β€ (π₯ + 1), π, (π₯ + 1)))) |
57 | 50, 56 | eqtrd 2773 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β (π(,)π) β§ (π(,)π) β (π£ β© (π₯(ballβπ·)1))) β (π(,)π) = (if(π β€ (π₯ β 1), (π₯ β 1), π)(,)if(π β€ (π₯ + 1), π, (π₯ + 1)))) |
58 | | mnfxr 11220 |
. . . . . . . . . . . . . . . . . . . 20
β’ -β
β β* |
59 | 58 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π₯ β (π(,)π) β§ (π(,)π) β (π£ β© (π₯(ballβπ·)1))) β -β β
β*) |
60 | 46, 21 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π₯ β (π(,)π) β§ (π(,)π) β (π£ β© (π₯(ballβπ·)1))) β (π₯ β 1) β
β*) |
61 | 51 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π₯ β (π(,)π) β§ (π(,)π) β (π£ β© (π₯(ballβπ·)1))) β (π β β* β§ π β
β*)) |
62 | 61 | simpld 496 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π₯ β (π(,)π) β§ (π(,)π) β (π£ β© (π₯(ballβπ·)1))) β π β β*) |
63 | 60, 62 | ifcld 4536 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π₯ β (π(,)π) β§ (π(,)π) β (π£ β© (π₯(ballβπ·)1))) β if(π β€ (π₯ β 1), (π₯ β 1), π) β
β*) |
64 | 61 | simprd 497 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π₯ β (π(,)π) β§ (π(,)π) β (π£ β© (π₯(ballβπ·)1))) β π β β*) |
65 | 46, 22 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π₯ β (π(,)π) β§ (π(,)π) β (π£ β© (π₯(ballβπ·)1))) β (π₯ + 1) β β) |
66 | 65 | rexrd 11213 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π₯ β (π(,)π) β§ (π(,)π) β (π£ β© (π₯(ballβπ·)1))) β (π₯ + 1) β
β*) |
67 | 64, 66 | ifcld 4536 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π₯ β (π(,)π) β§ (π(,)π) β (π£ β© (π₯(ballβπ·)1))) β if(π β€ (π₯ + 1), π, (π₯ + 1)) β
β*) |
68 | 45, 20 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π₯ β (π(,)π) β (π₯ β 1) β β) |
69 | 68 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π₯ β (π(,)π) β§ (π(,)π) β (π£ β© (π₯(ballβπ·)1))) β (π₯ β 1) β β) |
70 | 69 | mnfltd 13053 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π₯ β (π(,)π) β§ (π(,)π) β (π£ β© (π₯(ballβπ·)1))) β -β < (π₯ β 1)) |
71 | | xrmax2 13104 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β β*
β§ (π₯ β 1) β
β*) β (π₯ β 1) β€ if(π β€ (π₯ β 1), (π₯ β 1), π)) |
72 | 62, 60, 71 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π₯ β (π(,)π) β§ (π(,)π) β (π£ β© (π₯(ballβπ·)1))) β (π₯ β 1) β€ if(π β€ (π₯ β 1), (π₯ β 1), π)) |
73 | 59, 60, 63, 70, 72 | xrltletrd 13089 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π₯ β (π(,)π) β§ (π(,)π) β (π£ β© (π₯(ballβπ·)1))) β -β < if(π β€ (π₯ β 1), (π₯ β 1), π)) |
74 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π₯ β (π(,)π) β§ (π(,)π) β (π£ β© (π₯(ballβπ·)1))) β π₯ β (π(,)π)) |
75 | 74, 57 | eleqtrd 2836 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π₯ β (π(,)π) β§ (π(,)π) β (π£ β© (π₯(ballβπ·)1))) β π₯ β (if(π β€ (π₯ β 1), (π₯ β 1), π)(,)if(π β€ (π₯ + 1), π, (π₯ + 1)))) |
76 | | eliooxr 13331 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ β (if(π β€ (π₯ β 1), (π₯ β 1), π)(,)if(π β€ (π₯ + 1), π, (π₯ + 1))) β (if(π β€ (π₯ β 1), (π₯ β 1), π) β β* β§ if(π β€ (π₯ + 1), π, (π₯ + 1)) β
β*)) |
77 | | ne0i 4298 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π₯ β (if(π β€ (π₯ β 1), (π₯ β 1), π)(,)if(π β€ (π₯ + 1), π, (π₯ + 1))) β (if(π β€ (π₯ β 1), (π₯ β 1), π)(,)if(π β€ (π₯ + 1), π, (π₯ + 1))) β β
) |
78 | | ioon0 13299 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((if(π β€ (π₯ β 1), (π₯ β 1), π) β β* β§ if(π β€ (π₯ + 1), π, (π₯ + 1)) β β*) β
((if(π β€ (π₯ β 1), (π₯ β 1), π)(,)if(π β€ (π₯ + 1), π, (π₯ + 1))) β β
β if(π β€ (π₯ β 1), (π₯ β 1), π) < if(π β€ (π₯ + 1), π, (π₯ + 1)))) |
79 | 77, 78 | imbitrid 243 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((if(π β€ (π₯ β 1), (π₯ β 1), π) β β* β§ if(π β€ (π₯ + 1), π, (π₯ + 1)) β β*) β
(π₯ β (if(π β€ (π₯ β 1), (π₯ β 1), π)(,)if(π β€ (π₯ + 1), π, (π₯ + 1))) β if(π β€ (π₯ β 1), (π₯ β 1), π) < if(π β€ (π₯ + 1), π, (π₯ + 1)))) |
80 | 76, 79 | mpcom 38 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β (if(π β€ (π₯ β 1), (π₯ β 1), π)(,)if(π β€ (π₯ + 1), π, (π₯ + 1))) β if(π β€ (π₯ β 1), (π₯ β 1), π) < if(π β€ (π₯ + 1), π, (π₯ + 1))) |
81 | 75, 80 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π₯ β (π(,)π) β§ (π(,)π) β (π£ β© (π₯(ballβπ·)1))) β if(π β€ (π₯ β 1), (π₯ β 1), π) < if(π β€ (π₯ + 1), π, (π₯ + 1))) |
82 | | xrre2 13098 |
. . . . . . . . . . . . . . . . . . 19
β’
(((-β β β* β§ if(π β€ (π₯ β 1), (π₯ β 1), π) β β* β§ if(π β€ (π₯ + 1), π, (π₯ + 1)) β β*) β§
(-β < if(π β€
(π₯ β 1), (π₯ β 1), π) β§ if(π β€ (π₯ β 1), (π₯ β 1), π) < if(π β€ (π₯ + 1), π, (π₯ + 1)))) β if(π β€ (π₯ β 1), (π₯ β 1), π) β β) |
83 | 59, 63, 67, 73, 81, 82 | syl32anc 1379 |
. . . . . . . . . . . . . . . . . 18
β’ ((π₯ β (π(,)π) β§ (π(,)π) β (π£ β© (π₯(ballβπ·)1))) β if(π β€ (π₯ β 1), (π₯ β 1), π) β β) |
84 | | mnfle 13063 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (if(π β€ (π₯ β 1), (π₯ β 1), π) β β* β -β
β€ if(π β€ (π₯ β 1), (π₯ β 1), π)) |
85 | 63, 84 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π₯ β (π(,)π) β§ (π(,)π) β (π£ β© (π₯(ballβπ·)1))) β -β β€ if(π β€ (π₯ β 1), (π₯ β 1), π)) |
86 | 59, 63, 67, 85, 81 | xrlelttrd 13088 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π₯ β (π(,)π) β§ (π(,)π) β (π£ β© (π₯(ballβπ·)1))) β -β < if(π β€ (π₯ + 1), π, (π₯ + 1))) |
87 | | xrmin2 13106 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β*
β§ (π₯ + 1) β
β*) β if(π β€ (π₯ + 1), π, (π₯ + 1)) β€ (π₯ + 1)) |
88 | 64, 66, 87 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π₯ β (π(,)π) β§ (π(,)π) β (π£ β© (π₯(ballβπ·)1))) β if(π β€ (π₯ + 1), π, (π₯ + 1)) β€ (π₯ + 1)) |
89 | | xrre 13097 |
. . . . . . . . . . . . . . . . . . 19
β’
(((if(π β€ (π₯ + 1), π, (π₯ + 1)) β β* β§
(π₯ + 1) β β)
β§ (-β < if(π
β€ (π₯ + 1), π, (π₯ + 1)) β§ if(π β€ (π₯ + 1), π, (π₯ + 1)) β€ (π₯ + 1))) β if(π β€ (π₯ + 1), π, (π₯ + 1)) β β) |
90 | 67, 65, 86, 88, 89 | syl22anc 838 |
. . . . . . . . . . . . . . . . . 18
β’ ((π₯ β (π(,)π) β§ (π(,)π) β (π£ β© (π₯(ballβπ·)1))) β if(π β€ (π₯ + 1), π, (π₯ + 1)) β β) |
91 | 1 | ioo2blex 24180 |
. . . . . . . . . . . . . . . . . 18
β’
((if(π β€ (π₯ β 1), (π₯ β 1), π) β β β§ if(π β€ (π₯ + 1), π, (π₯ + 1)) β β) β (if(π β€ (π₯ β 1), (π₯ β 1), π)(,)if(π β€ (π₯ + 1), π, (π₯ + 1))) β ran (ballβπ·)) |
92 | 83, 90, 91 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β (π(,)π) β§ (π(,)π) β (π£ β© (π₯(ballβπ·)1))) β (if(π β€ (π₯ β 1), (π₯ β 1), π)(,)if(π β€ (π₯ + 1), π, (π₯ + 1))) β ran (ballβπ·)) |
93 | 57, 92 | eqeltrd 2834 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β (π(,)π) β§ (π(,)π) β (π£ β© (π₯(ballβπ·)1))) β (π(,)π) β ran (ballβπ·)) |
94 | | inss1 4192 |
. . . . . . . . . . . . . . . . . 18
β’ (π£ β© (π₯(ballβπ·)1)) β π£ |
95 | | sstr 3956 |
. . . . . . . . . . . . . . . . . 18
β’ (((π(,)π) β (π£ β© (π₯(ballβπ·)1)) β§ (π£ β© (π₯(ballβπ·)1)) β π£) β (π(,)π) β π£) |
96 | 94, 95 | mpan2 690 |
. . . . . . . . . . . . . . . . 17
β’ ((π(,)π) β (π£ β© (π₯(ballβπ·)1)) β (π(,)π) β π£) |
97 | 96 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β (π(,)π) β§ (π(,)π) β (π£ β© (π₯(ballβπ·)1))) β (π(,)π) β π£) |
98 | | sseq1 3973 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ = (π(,)π) β (π§ β π£ β (π(,)π) β π£)) |
99 | 38, 98 | anbi12d 632 |
. . . . . . . . . . . . . . . . 17
β’ (π§ = (π(,)π) β ((π₯ β π§ β§ π§ β π£) β (π₯ β (π(,)π) β§ (π(,)π) β π£))) |
100 | 99 | rspcev 3583 |
. . . . . . . . . . . . . . . 16
β’ (((π(,)π) β ran (ballβπ·) β§ (π₯ β (π(,)π) β§ (π(,)π) β π£)) β βπ§ β ran (ballβπ·)(π₯ β π§ β§ π§ β π£)) |
101 | 93, 74, 97, 100 | syl12anc 836 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β (π(,)π) β§ (π(,)π) β (π£ β© (π₯(ballβπ·)1))) β βπ§ β ran (ballβπ·)(π₯ β π§ β§ π§ β π£)) |
102 | | blssex 23803 |
. . . . . . . . . . . . . . . 16
β’ ((π· β
(βMetββ) β§ π₯ β β) β (βπ§ β ran (ballβπ·)(π₯ β π§ β§ π§ β π£) β βπ¦ β β+ (π₯(ballβπ·)π¦) β π£)) |
103 | 2, 46, 102 | sylancr 588 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β (π(,)π) β§ (π(,)π) β (π£ β© (π₯(ballβπ·)1))) β (βπ§ β ran (ballβπ·)(π₯ β π§ β§ π§ β π£) β βπ¦ β β+ (π₯(ballβπ·)π¦) β π£)) |
104 | 101, 103 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ ((π₯ β (π(,)π) β§ (π(,)π) β (π£ β© (π₯(ballβπ·)1))) β βπ¦ β β+ (π₯(ballβπ·)π¦) β π£) |
105 | 40, 104 | syl6bi 253 |
. . . . . . . . . . . . 13
β’ (π§ = (π(,)π) β ((π₯ β π§ β§ π§ β (π£ β© (π₯(ballβπ·)1))) β βπ¦ β β+ (π₯(ballβπ·)π¦) β π£)) |
106 | 105 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β β*
β§ π β
β*) β (π§ = (π(,)π) β ((π₯ β π§ β§ π§ β (π£ β© (π₯(ballβπ·)1))) β βπ¦ β β+ (π₯(ballβπ·)π¦) β π£))) |
107 | 106 | rexlimivv 3193 |
. . . . . . . . . . 11
β’
(βπ β
β* βπ β β* π§ = (π(,)π) β ((π₯ β π§ β§ π§ β (π£ β© (π₯(ballβπ·)1))) β βπ¦ β β+ (π₯(ballβπ·)π¦) β π£)) |
108 | 107 | imp 408 |
. . . . . . . . . 10
β’
((βπ β
β* βπ β β* π§ = (π(,)π) β§ (π₯ β π§ β§ π§ β (π£ β© (π₯(ballβπ·)1)))) β βπ¦ β β+ (π₯(ballβπ·)π¦) β π£) |
109 | 37, 108 | sylanb 582 |
. . . . . . . . 9
β’ ((π§ β ran (,) β§ (π₯ β π§ β§ π§ β (π£ β© (π₯(ballβπ·)1)))) β βπ¦ β β+ (π₯(ballβπ·)π¦) β π£) |
110 | 109 | rexlimiva 3141 |
. . . . . . . 8
β’
(βπ§ β ran
(,)(π₯ β π§ β§ π§ β (π£ β© (π₯(ballβπ·)1))) β βπ¦ β β+ (π₯(ballβπ·)π¦) β π£) |
111 | 35, 110 | syl 17 |
. . . . . . 7
β’ ((π£ β ran (,) β§ π₯ β π£) β βπ¦ β β+ (π₯(ballβπ·)π¦) β π£) |
112 | 111 | ralrimiva 3140 |
. . . . . 6
β’ (π£ β ran (,) β
βπ₯ β π£ βπ¦ β β+ (π₯(ballβπ·)π¦) β π£) |
113 | 3 | elmopn2 23821 |
. . . . . . 7
β’ (π· β
(βMetββ) β (π£ β π½ β (π£ β β β§ βπ₯ β π£ βπ¦ β β+ (π₯(ballβπ·)π¦) β π£))) |
114 | 2, 113 | ax-mp 5 |
. . . . . 6
β’ (π£ β π½ β (π£ β β β§ βπ₯ β π£ βπ¦ β β+ (π₯(ballβπ·)π¦) β π£)) |
115 | 9, 112, 114 | sylanbrc 584 |
. . . . 5
β’ (π£ β ran (,) β π£ β π½) |
116 | 115 | ssriv 3952 |
. . . 4
β’ ran (,)
β π½ |
117 | 116, 5 | sseqtri 3984 |
. . 3
β’ ran (,)
β (topGenβran (ballβπ·)) |
118 | | 2basgen 22363 |
. . 3
β’ ((ran
(ballβπ·) β ran
(,) β§ ran (,) β (topGenβran (ballβπ·))) β (topGenβran
(ballβπ·)) =
(topGenβran (,))) |
119 | 6, 117, 118 | mp2an 691 |
. 2
β’
(topGenβran (ballβπ·)) = (topGenβran (,)) |
120 | 5, 119 | eqtr2i 2762 |
1
β’
(topGenβran (,)) = π½ |