Step | Hyp | Ref
| Expression |
1 | | remet.1 |
. . . . 5
⊢ 𝐷 = ((abs ∘ − )
↾ (ℝ × ℝ)) |
2 | 1 | rexmet 22402 |
. . . 4
⊢ 𝐷 ∈
(∞Met‘ℝ) |
3 | | blrn 22024 |
. . . 4
⊢ (𝐷 ∈
(∞Met‘ℝ) → (𝑧 ∈ ran (ball‘𝐷) ↔ ∃𝑦 ∈ ℝ ∃𝑟 ∈ ℝ* 𝑧 = (𝑦(ball‘𝐷)𝑟))) |
4 | 2, 3 | ax-mp 5 |
. . 3
⊢ (𝑧 ∈ ran (ball‘𝐷) ↔ ∃𝑦 ∈ ℝ ∃𝑟 ∈ ℝ*
𝑧 = (𝑦(ball‘𝐷)𝑟)) |
5 | | elxr 11826 |
. . . . . 6
⊢ (𝑟 ∈ ℝ*
↔ (𝑟 ∈ ℝ
∨ 𝑟 = +∞ ∨
𝑟 =
-∞)) |
6 | 1 | bl2ioo 22403 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℝ ∧ 𝑟 ∈ ℝ) → (𝑦(ball‘𝐷)𝑟) = ((𝑦 − 𝑟)(,)(𝑦 + 𝑟))) |
7 | | resubcl 10224 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℝ ∧ 𝑟 ∈ ℝ) → (𝑦 − 𝑟) ∈ ℝ) |
8 | | readdcl 9898 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℝ ∧ 𝑟 ∈ ℝ) → (𝑦 + 𝑟) ∈ ℝ) |
9 | | rexr 9964 |
. . . . . . . . . 10
⊢ ((𝑦 − 𝑟) ∈ ℝ → (𝑦 − 𝑟) ∈
ℝ*) |
10 | | rexr 9964 |
. . . . . . . . . 10
⊢ ((𝑦 + 𝑟) ∈ ℝ → (𝑦 + 𝑟) ∈
ℝ*) |
11 | | ioof 12142 |
. . . . . . . . . . . 12
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
12 | | ffn 5958 |
. . . . . . . . . . . 12
⊢
((,):(ℝ* × ℝ*)⟶𝒫
ℝ → (,) Fn (ℝ* ×
ℝ*)) |
13 | 11, 12 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (,) Fn
(ℝ* × ℝ*) |
14 | | fnovrn 6707 |
. . . . . . . . . . 11
⊢ (((,) Fn
(ℝ* × ℝ*) ∧ (𝑦 − 𝑟) ∈ ℝ* ∧ (𝑦 + 𝑟) ∈ ℝ*) → ((𝑦 − 𝑟)(,)(𝑦 + 𝑟)) ∈ ran (,)) |
15 | 13, 14 | mp3an1 1403 |
. . . . . . . . . 10
⊢ (((𝑦 − 𝑟) ∈ ℝ* ∧ (𝑦 + 𝑟) ∈ ℝ*) → ((𝑦 − 𝑟)(,)(𝑦 + 𝑟)) ∈ ran (,)) |
16 | 9, 10, 15 | syl2an 493 |
. . . . . . . . 9
⊢ (((𝑦 − 𝑟) ∈ ℝ ∧ (𝑦 + 𝑟) ∈ ℝ) → ((𝑦 − 𝑟)(,)(𝑦 + 𝑟)) ∈ ran (,)) |
17 | 7, 8, 16 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℝ ∧ 𝑟 ∈ ℝ) → ((𝑦 − 𝑟)(,)(𝑦 + 𝑟)) ∈ ran (,)) |
18 | 6, 17 | eqeltrd 2688 |
. . . . . . 7
⊢ ((𝑦 ∈ ℝ ∧ 𝑟 ∈ ℝ) → (𝑦(ball‘𝐷)𝑟) ∈ ran (,)) |
19 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑟 = +∞ → (𝑦(ball‘𝐷)𝑟) = (𝑦(ball‘𝐷)+∞)) |
20 | 1 | remet 22401 |
. . . . . . . . . 10
⊢ 𝐷 ∈
(Met‘ℝ) |
21 | | blpnf 22012 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (Met‘ℝ)
∧ 𝑦 ∈ ℝ)
→ (𝑦(ball‘𝐷)+∞) =
ℝ) |
22 | 20, 21 | mpan 702 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ → (𝑦(ball‘𝐷)+∞) = ℝ) |
23 | 19, 22 | sylan9eqr 2666 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℝ ∧ 𝑟 = +∞) → (𝑦(ball‘𝐷)𝑟) = ℝ) |
24 | | ioomax 12119 |
. . . . . . . . 9
⊢
(-∞(,)+∞) = ℝ |
25 | | ioorebas 12146 |
. . . . . . . . 9
⊢
(-∞(,)+∞) ∈ ran (,) |
26 | 24, 25 | eqeltrri 2685 |
. . . . . . . 8
⊢ ℝ
∈ ran (,) |
27 | 23, 26 | syl6eqel 2696 |
. . . . . . 7
⊢ ((𝑦 ∈ ℝ ∧ 𝑟 = +∞) → (𝑦(ball‘𝐷)𝑟) ∈ ran (,)) |
28 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑟 = -∞ → (𝑦(ball‘𝐷)𝑟) = (𝑦(ball‘𝐷)-∞)) |
29 | | 0xr 9965 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ* |
30 | | nltmnf 11839 |
. . . . . . . . . . 11
⊢ (0 ∈
ℝ* → ¬ 0 < -∞) |
31 | 29, 30 | ax-mp 5 |
. . . . . . . . . 10
⊢ ¬ 0
< -∞ |
32 | | mnfxr 9975 |
. . . . . . . . . . . 12
⊢ -∞
∈ ℝ* |
33 | | xbln0 22029 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈
(∞Met‘ℝ) ∧ 𝑦 ∈ ℝ ∧ -∞ ∈
ℝ*) → ((𝑦(ball‘𝐷)-∞) ≠ ∅ ↔ 0 <
-∞)) |
34 | 2, 32, 33 | mp3an13 1407 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ → ((𝑦(ball‘𝐷)-∞) ≠ ∅ ↔ 0 <
-∞)) |
35 | 34 | necon1bbid 2821 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ → (¬ 0
< -∞ ↔ (𝑦(ball‘𝐷)-∞) = ∅)) |
36 | 31, 35 | mpbii 222 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ → (𝑦(ball‘𝐷)-∞) = ∅) |
37 | 28, 36 | sylan9eqr 2666 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℝ ∧ 𝑟 = -∞) → (𝑦(ball‘𝐷)𝑟) = ∅) |
38 | | iooid 12074 |
. . . . . . . . 9
⊢ (0(,)0) =
∅ |
39 | | ioorebas 12146 |
. . . . . . . . 9
⊢ (0(,)0)
∈ ran (,) |
40 | 38, 39 | eqeltrri 2685 |
. . . . . . . 8
⊢ ∅
∈ ran (,) |
41 | 37, 40 | syl6eqel 2696 |
. . . . . . 7
⊢ ((𝑦 ∈ ℝ ∧ 𝑟 = -∞) → (𝑦(ball‘𝐷)𝑟) ∈ ran (,)) |
42 | 18, 27, 41 | 3jaodan 1386 |
. . . . . 6
⊢ ((𝑦 ∈ ℝ ∧ (𝑟 ∈ ℝ ∨ 𝑟 = +∞ ∨ 𝑟 = -∞)) → (𝑦(ball‘𝐷)𝑟) ∈ ran (,)) |
43 | 5, 42 | sylan2b 491 |
. . . . 5
⊢ ((𝑦 ∈ ℝ ∧ 𝑟 ∈ ℝ*)
→ (𝑦(ball‘𝐷)𝑟) ∈ ran (,)) |
44 | | eleq1 2676 |
. . . . 5
⊢ (𝑧 = (𝑦(ball‘𝐷)𝑟) → (𝑧 ∈ ran (,) ↔ (𝑦(ball‘𝐷)𝑟) ∈ ran (,))) |
45 | 43, 44 | syl5ibrcom 236 |
. . . 4
⊢ ((𝑦 ∈ ℝ ∧ 𝑟 ∈ ℝ*)
→ (𝑧 = (𝑦(ball‘𝐷)𝑟) → 𝑧 ∈ ran (,))) |
46 | 45 | rexlimivv 3018 |
. . 3
⊢
(∃𝑦 ∈
ℝ ∃𝑟 ∈
ℝ* 𝑧 =
(𝑦(ball‘𝐷)𝑟) → 𝑧 ∈ ran (,)) |
47 | 4, 46 | sylbi 206 |
. 2
⊢ (𝑧 ∈ ran (ball‘𝐷) → 𝑧 ∈ ran (,)) |
48 | 47 | ssriv 3572 |
1
⊢ ran
(ball‘𝐷) ⊆ ran
(,) |