Step | Hyp | Ref
| Expression |
1 | | remet.1 |
. . . . 5
β’ π· = ((abs β β )
βΎ (β Γ β)) |
2 | 1 | rexmet 24527 |
. . . 4
β’ π· β
(βMetββ) |
3 | | blrn 24135 |
. . . 4
β’ (π· β
(βMetββ) β (π§ β ran (ballβπ·) β βπ¦ β β βπ β β* π§ = (π¦(ballβπ·)π))) |
4 | 2, 3 | ax-mp 5 |
. . 3
β’ (π§ β ran (ballβπ·) β βπ¦ β β βπ β β*
π§ = (π¦(ballβπ·)π)) |
5 | | elxr 13100 |
. . . . . 6
β’ (π β β*
β (π β β
β¨ π = +β β¨
π =
-β)) |
6 | 1 | bl2ioo 24528 |
. . . . . . . 8
β’ ((π¦ β β β§ π β β) β (π¦(ballβπ·)π) = ((π¦ β π)(,)(π¦ + π))) |
7 | | resubcl 11528 |
. . . . . . . . 9
β’ ((π¦ β β β§ π β β) β (π¦ β π) β β) |
8 | | readdcl 11195 |
. . . . . . . . 9
β’ ((π¦ β β β§ π β β) β (π¦ + π) β β) |
9 | | ioof 13428 |
. . . . . . . . . . 11
β’
(,):(β* Γ β*)βΆπ«
β |
10 | | ffn 6716 |
. . . . . . . . . . 11
β’
((,):(β* Γ β*)βΆπ«
β β (,) Fn (β* Γ
β*)) |
11 | 9, 10 | ax-mp 5 |
. . . . . . . . . 10
β’ (,) Fn
(β* Γ β*) |
12 | | rexr 11264 |
. . . . . . . . . 10
β’ ((π¦ β π) β β β (π¦ β π) β
β*) |
13 | | rexr 11264 |
. . . . . . . . . 10
β’ ((π¦ + π) β β β (π¦ + π) β
β*) |
14 | | fnovrn 7584 |
. . . . . . . . . 10
β’ (((,) Fn
(β* Γ β*) β§ (π¦ β π) β β* β§ (π¦ + π) β β*) β ((π¦ β π)(,)(π¦ + π)) β ran (,)) |
15 | 11, 12, 13, 14 | mp3an3an 1465 |
. . . . . . . . 9
β’ (((π¦ β π) β β β§ (π¦ + π) β β) β ((π¦ β π)(,)(π¦ + π)) β ran (,)) |
16 | 7, 8, 15 | syl2anc 582 |
. . . . . . . 8
β’ ((π¦ β β β§ π β β) β ((π¦ β π)(,)(π¦ + π)) β ran (,)) |
17 | 6, 16 | eqeltrd 2831 |
. . . . . . 7
β’ ((π¦ β β β§ π β β) β (π¦(ballβπ·)π) β ran (,)) |
18 | | oveq2 7419 |
. . . . . . . . 9
β’ (π = +β β (π¦(ballβπ·)π) = (π¦(ballβπ·)+β)) |
19 | 1 | remet 24526 |
. . . . . . . . . 10
β’ π· β
(Metββ) |
20 | | blpnf 24123 |
. . . . . . . . . 10
β’ ((π· β (Metββ)
β§ π¦ β β)
β (π¦(ballβπ·)+β) =
β) |
21 | 19, 20 | mpan 686 |
. . . . . . . . 9
β’ (π¦ β β β (π¦(ballβπ·)+β) = β) |
22 | 18, 21 | sylan9eqr 2792 |
. . . . . . . 8
β’ ((π¦ β β β§ π = +β) β (π¦(ballβπ·)π) = β) |
23 | | ioomax 13403 |
. . . . . . . . 9
β’
(-β(,)+β) = β |
24 | | ioorebas 13432 |
. . . . . . . . 9
β’
(-β(,)+β) β ran (,) |
25 | 23, 24 | eqeltrri 2828 |
. . . . . . . 8
β’ β
β ran (,) |
26 | 22, 25 | eqeltrdi 2839 |
. . . . . . 7
β’ ((π¦ β β β§ π = +β) β (π¦(ballβπ·)π) β ran (,)) |
27 | | oveq2 7419 |
. . . . . . . . 9
β’ (π = -β β (π¦(ballβπ·)π) = (π¦(ballβπ·)-β)) |
28 | | 0xr 11265 |
. . . . . . . . . . 11
β’ 0 β
β* |
29 | | nltmnf 13113 |
. . . . . . . . . . 11
β’ (0 β
β* β Β¬ 0 < -β) |
30 | 28, 29 | ax-mp 5 |
. . . . . . . . . 10
β’ Β¬ 0
< -β |
31 | | mnfxr 11275 |
. . . . . . . . . . . 12
β’ -β
β β* |
32 | | xbln0 24140 |
. . . . . . . . . . . 12
β’ ((π· β
(βMetββ) β§ π¦ β β β§ -β β
β*) β ((π¦(ballβπ·)-β) β β
β 0 <
-β)) |
33 | 2, 31, 32 | mp3an13 1450 |
. . . . . . . . . . 11
β’ (π¦ β β β ((π¦(ballβπ·)-β) β β
β 0 <
-β)) |
34 | 33 | necon1bbid 2978 |
. . . . . . . . . 10
β’ (π¦ β β β (Β¬ 0
< -β β (π¦(ballβπ·)-β) = β
)) |
35 | 30, 34 | mpbii 232 |
. . . . . . . . 9
β’ (π¦ β β β (π¦(ballβπ·)-β) = β
) |
36 | 27, 35 | sylan9eqr 2792 |
. . . . . . . 8
β’ ((π¦ β β β§ π = -β) β (π¦(ballβπ·)π) = β
) |
37 | | iooid 13356 |
. . . . . . . . 9
β’ (0(,)0) =
β
|
38 | | ioorebas 13432 |
. . . . . . . . 9
β’ (0(,)0)
β ran (,) |
39 | 37, 38 | eqeltrri 2828 |
. . . . . . . 8
β’ β
β ran (,) |
40 | 36, 39 | eqeltrdi 2839 |
. . . . . . 7
β’ ((π¦ β β β§ π = -β) β (π¦(ballβπ·)π) β ran (,)) |
41 | 17, 26, 40 | 3jaodan 1428 |
. . . . . 6
β’ ((π¦ β β β§ (π β β β¨ π = +β β¨ π = -β)) β (π¦(ballβπ·)π) β ran (,)) |
42 | 5, 41 | sylan2b 592 |
. . . . 5
β’ ((π¦ β β β§ π β β*)
β (π¦(ballβπ·)π) β ran (,)) |
43 | | eleq1 2819 |
. . . . 5
β’ (π§ = (π¦(ballβπ·)π) β (π§ β ran (,) β (π¦(ballβπ·)π) β ran (,))) |
44 | 42, 43 | syl5ibrcom 246 |
. . . 4
β’ ((π¦ β β β§ π β β*)
β (π§ = (π¦(ballβπ·)π) β π§ β ran (,))) |
45 | 44 | rexlimivv 3197 |
. . 3
β’
(βπ¦ β
β βπ β
β* π§ =
(π¦(ballβπ·)π) β π§ β ran (,)) |
46 | 4, 45 | sylbi 216 |
. 2
β’ (π§ β ran (ballβπ·) β π§ β ran (,)) |
47 | 46 | ssriv 3985 |
1
β’ ran
(ballβπ·) β ran
(,) |