Step | Hyp | Ref
| Expression |
1 | | remet.1 |
. . . . 5
β’ π· = ((abs β β )
βΎ (β Γ β)) |
2 | 1 | rexmet 24307 |
. . . 4
β’ π· β
(βMetββ) |
3 | | blrn 23915 |
. . . 4
β’ (π· β
(βMetββ) β (π§ β ran (ballβπ·) β βπ¦ β β βπ β β* π§ = (π¦(ballβπ·)π))) |
4 | 2, 3 | ax-mp 5 |
. . 3
β’ (π§ β ran (ballβπ·) β βπ¦ β β βπ β β*
π§ = (π¦(ballβπ·)π)) |
5 | | elxr 13096 |
. . . . . 6
β’ (π β β*
β (π β β
β¨ π = +β β¨
π =
-β)) |
6 | 1 | bl2ioo 24308 |
. . . . . . . 8
β’ ((π¦ β β β§ π β β) β (π¦(ballβπ·)π) = ((π¦ β π)(,)(π¦ + π))) |
7 | | resubcl 11524 |
. . . . . . . . 9
β’ ((π¦ β β β§ π β β) β (π¦ β π) β β) |
8 | | readdcl 11193 |
. . . . . . . . 9
β’ ((π¦ β β β§ π β β) β (π¦ + π) β β) |
9 | | ioof 13424 |
. . . . . . . . . . 11
β’
(,):(β* Γ β*)βΆπ«
β |
10 | | ffn 6718 |
. . . . . . . . . . 11
β’
((,):(β* Γ β*)βΆπ«
β β (,) Fn (β* Γ
β*)) |
11 | 9, 10 | ax-mp 5 |
. . . . . . . . . 10
β’ (,) Fn
(β* Γ β*) |
12 | | rexr 11260 |
. . . . . . . . . 10
β’ ((π¦ β π) β β β (π¦ β π) β
β*) |
13 | | rexr 11260 |
. . . . . . . . . 10
β’ ((π¦ + π) β β β (π¦ + π) β
β*) |
14 | | fnovrn 7582 |
. . . . . . . . . 10
β’ (((,) Fn
(β* Γ β*) β§ (π¦ β π) β β* β§ (π¦ + π) β β*) β ((π¦ β π)(,)(π¦ + π)) β ran (,)) |
15 | 11, 12, 13, 14 | mp3an3an 1468 |
. . . . . . . . 9
β’ (((π¦ β π) β β β§ (π¦ + π) β β) β ((π¦ β π)(,)(π¦ + π)) β ran (,)) |
16 | 7, 8, 15 | syl2anc 585 |
. . . . . . . 8
β’ ((π¦ β β β§ π β β) β ((π¦ β π)(,)(π¦ + π)) β ran (,)) |
17 | 6, 16 | eqeltrd 2834 |
. . . . . . 7
β’ ((π¦ β β β§ π β β) β (π¦(ballβπ·)π) β ran (,)) |
18 | | oveq2 7417 |
. . . . . . . . 9
β’ (π = +β β (π¦(ballβπ·)π) = (π¦(ballβπ·)+β)) |
19 | 1 | remet 24306 |
. . . . . . . . . 10
β’ π· β
(Metββ) |
20 | | blpnf 23903 |
. . . . . . . . . 10
β’ ((π· β (Metββ)
β§ π¦ β β)
β (π¦(ballβπ·)+β) =
β) |
21 | 19, 20 | mpan 689 |
. . . . . . . . 9
β’ (π¦ β β β (π¦(ballβπ·)+β) = β) |
22 | 18, 21 | sylan9eqr 2795 |
. . . . . . . 8
β’ ((π¦ β β β§ π = +β) β (π¦(ballβπ·)π) = β) |
23 | | ioomax 13399 |
. . . . . . . . 9
β’
(-β(,)+β) = β |
24 | | ioorebas 13428 |
. . . . . . . . 9
β’
(-β(,)+β) β ran (,) |
25 | 23, 24 | eqeltrri 2831 |
. . . . . . . 8
β’ β
β ran (,) |
26 | 22, 25 | eqeltrdi 2842 |
. . . . . . 7
β’ ((π¦ β β β§ π = +β) β (π¦(ballβπ·)π) β ran (,)) |
27 | | oveq2 7417 |
. . . . . . . . 9
β’ (π = -β β (π¦(ballβπ·)π) = (π¦(ballβπ·)-β)) |
28 | | 0xr 11261 |
. . . . . . . . . . 11
β’ 0 β
β* |
29 | | nltmnf 13109 |
. . . . . . . . . . 11
β’ (0 β
β* β Β¬ 0 < -β) |
30 | 28, 29 | ax-mp 5 |
. . . . . . . . . 10
β’ Β¬ 0
< -β |
31 | | mnfxr 11271 |
. . . . . . . . . . . 12
β’ -β
β β* |
32 | | xbln0 23920 |
. . . . . . . . . . . 12
β’ ((π· β
(βMetββ) β§ π¦ β β β§ -β β
β*) β ((π¦(ballβπ·)-β) β β
β 0 <
-β)) |
33 | 2, 31, 32 | mp3an13 1453 |
. . . . . . . . . . 11
β’ (π¦ β β β ((π¦(ballβπ·)-β) β β
β 0 <
-β)) |
34 | 33 | necon1bbid 2981 |
. . . . . . . . . 10
β’ (π¦ β β β (Β¬ 0
< -β β (π¦(ballβπ·)-β) = β
)) |
35 | 30, 34 | mpbii 232 |
. . . . . . . . 9
β’ (π¦ β β β (π¦(ballβπ·)-β) = β
) |
36 | 27, 35 | sylan9eqr 2795 |
. . . . . . . 8
β’ ((π¦ β β β§ π = -β) β (π¦(ballβπ·)π) = β
) |
37 | | iooid 13352 |
. . . . . . . . 9
β’ (0(,)0) =
β
|
38 | | ioorebas 13428 |
. . . . . . . . 9
β’ (0(,)0)
β ran (,) |
39 | 37, 38 | eqeltrri 2831 |
. . . . . . . 8
β’ β
β ran (,) |
40 | 36, 39 | eqeltrdi 2842 |
. . . . . . 7
β’ ((π¦ β β β§ π = -β) β (π¦(ballβπ·)π) β ran (,)) |
41 | 17, 26, 40 | 3jaodan 1431 |
. . . . . 6
β’ ((π¦ β β β§ (π β β β¨ π = +β β¨ π = -β)) β (π¦(ballβπ·)π) β ran (,)) |
42 | 5, 41 | sylan2b 595 |
. . . . 5
β’ ((π¦ β β β§ π β β*)
β (π¦(ballβπ·)π) β ran (,)) |
43 | | eleq1 2822 |
. . . . 5
β’ (π§ = (π¦(ballβπ·)π) β (π§ β ran (,) β (π¦(ballβπ·)π) β ran (,))) |
44 | 42, 43 | syl5ibrcom 246 |
. . . 4
β’ ((π¦ β β β§ π β β*)
β (π§ = (π¦(ballβπ·)π) β π§ β ran (,))) |
45 | 44 | rexlimivv 3200 |
. . 3
β’
(βπ¦ β
β βπ β
β* π§ =
(π¦(ballβπ·)π) β π§ β ran (,)) |
46 | 4, 45 | sylbi 216 |
. 2
β’ (π§ β ran (ballβπ·) β π§ β ran (,)) |
47 | 46 | ssriv 3987 |
1
β’ ran
(ballβπ·) β ran
(,) |