| Step | Hyp | Ref
| Expression |
| 1 | | dvlog2.s |
. . . . 5
⊢ 𝑆 = (1(ball‘(abs ∘
− ))1) |
| 2 | | cnxmet 24793 |
. . . . . 6
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
| 3 | | ax-1cn 11213 |
. . . . . 6
⊢ 1 ∈
ℂ |
| 4 | | 1xr 11320 |
. . . . . 6
⊢ 1 ∈
ℝ* |
| 5 | | blssm 24428 |
. . . . . 6
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ ℂ
∧ 1 ∈ ℝ*) → (1(ball‘(abs ∘ −
))1) ⊆ ℂ) |
| 6 | 2, 3, 4, 5 | mp3an 1463 |
. . . . 5
⊢
(1(ball‘(abs ∘ − ))1) ⊆ ℂ |
| 7 | 1, 6 | eqsstri 4030 |
. . . 4
⊢ 𝑆 ⊆
ℂ |
| 8 | 7 | sseli 3979 |
. . 3
⊢ (𝑥 ∈ 𝑆 → 𝑥 ∈ ℂ) |
| 9 | | 1red 11262 |
. . . . . . 7
⊢ (𝑥 ∈ (-∞(,]0) → 1
∈ ℝ) |
| 10 | | cnmet 24792 |
. . . . . . . 8
⊢ (abs
∘ − ) ∈ (Met‘ℂ) |
| 11 | | mnfxr 11318 |
. . . . . . . . . . 11
⊢ -∞
∈ ℝ* |
| 12 | | 0re 11263 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
| 13 | | iocssre 13467 |
. . . . . . . . . . 11
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ) →
(-∞(,]0) ⊆ ℝ) |
| 14 | 11, 12, 13 | mp2an 692 |
. . . . . . . . . 10
⊢
(-∞(,]0) ⊆ ℝ |
| 15 | | ax-resscn 11212 |
. . . . . . . . . 10
⊢ ℝ
⊆ ℂ |
| 16 | 14, 15 | sstri 3993 |
. . . . . . . . 9
⊢
(-∞(,]0) ⊆ ℂ |
| 17 | 16 | sseli 3979 |
. . . . . . . 8
⊢ (𝑥 ∈ (-∞(,]0) →
𝑥 ∈
ℂ) |
| 18 | | metcl 24342 |
. . . . . . . 8
⊢ (((abs
∘ − ) ∈ (Met‘ℂ) ∧ 1 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (1(abs
∘ − )𝑥) ∈
ℝ) |
| 19 | 10, 3, 17, 18 | mp3an12i 1467 |
. . . . . . 7
⊢ (𝑥 ∈ (-∞(,]0) →
(1(abs ∘ − )𝑥)
∈ ℝ) |
| 20 | | 1m0e1 12387 |
. . . . . . . . 9
⊢ (1
− 0) = 1 |
| 21 | 14 | sseli 3979 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (-∞(,]0) →
𝑥 ∈
ℝ) |
| 22 | 12 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (-∞(,]0) → 0
∈ ℝ) |
| 23 | | elioc2 13450 |
. . . . . . . . . . . 12
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ) →
(𝑥 ∈ (-∞(,]0)
↔ (𝑥 ∈ ℝ
∧ -∞ < 𝑥 ∧
𝑥 ≤
0))) |
| 24 | 11, 12, 23 | mp2an 692 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (-∞(,]0) ↔
(𝑥 ∈ ℝ ∧
-∞ < 𝑥 ∧ 𝑥 ≤ 0)) |
| 25 | 24 | simp3bi 1148 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (-∞(,]0) →
𝑥 ≤ 0) |
| 26 | 21, 22, 9, 25 | lesub2dd 11880 |
. . . . . . . . 9
⊢ (𝑥 ∈ (-∞(,]0) → (1
− 0) ≤ (1 − 𝑥)) |
| 27 | 20, 26 | eqbrtrrid 5179 |
. . . . . . . 8
⊢ (𝑥 ∈ (-∞(,]0) → 1
≤ (1 − 𝑥)) |
| 28 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (abs
∘ − ) = (abs ∘ − ) |
| 29 | 28 | cnmetdval 24791 |
. . . . . . . . . 10
⊢ ((1
∈ ℂ ∧ 𝑥
∈ ℂ) → (1(abs ∘ − )𝑥) = (abs‘(1 − 𝑥))) |
| 30 | 3, 17, 29 | sylancr 587 |
. . . . . . . . 9
⊢ (𝑥 ∈ (-∞(,]0) →
(1(abs ∘ − )𝑥)
= (abs‘(1 − 𝑥))) |
| 31 | | 0le1 11786 |
. . . . . . . . . . . 12
⊢ 0 ≤
1 |
| 32 | 31 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (-∞(,]0) → 0
≤ 1) |
| 33 | 21, 22, 9, 25, 32 | letrd 11418 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (-∞(,]0) →
𝑥 ≤ 1) |
| 34 | 21, 9, 33 | abssubge0d 15470 |
. . . . . . . . 9
⊢ (𝑥 ∈ (-∞(,]0) →
(abs‘(1 − 𝑥)) =
(1 − 𝑥)) |
| 35 | 30, 34 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝑥 ∈ (-∞(,]0) →
(1(abs ∘ − )𝑥)
= (1 − 𝑥)) |
| 36 | 27, 35 | breqtrrd 5171 |
. . . . . . 7
⊢ (𝑥 ∈ (-∞(,]0) → 1
≤ (1(abs ∘ − )𝑥)) |
| 37 | 9, 19, 36 | lensymd 11412 |
. . . . . 6
⊢ (𝑥 ∈ (-∞(,]0) →
¬ (1(abs ∘ − )𝑥) < 1) |
| 38 | 2 | a1i 11 |
. . . . . . 7
⊢ (𝑥 ∈ (-∞(,]0) →
(abs ∘ − ) ∈ (∞Met‘ℂ)) |
| 39 | 4 | a1i 11 |
. . . . . . 7
⊢ (𝑥 ∈ (-∞(,]0) → 1
∈ ℝ*) |
| 40 | 3 | a1i 11 |
. . . . . . 7
⊢ (𝑥 ∈ (-∞(,]0) → 1
∈ ℂ) |
| 41 | | elbl2 24400 |
. . . . . . 7
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈
ℝ*) ∧ (1 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑥 ∈ (1(ball‘(abs ∘ −
))1) ↔ (1(abs ∘ − )𝑥) < 1)) |
| 42 | 38, 39, 40, 17, 41 | syl22anc 839 |
. . . . . 6
⊢ (𝑥 ∈ (-∞(,]0) →
(𝑥 ∈
(1(ball‘(abs ∘ − ))1) ↔ (1(abs ∘ − )𝑥) < 1)) |
| 43 | 37, 42 | mtbird 325 |
. . . . 5
⊢ (𝑥 ∈ (-∞(,]0) →
¬ 𝑥 ∈
(1(ball‘(abs ∘ − ))1)) |
| 44 | 43 | con2i 139 |
. . . 4
⊢ (𝑥 ∈ (1(ball‘(abs
∘ − ))1) → ¬ 𝑥 ∈ (-∞(,]0)) |
| 45 | 44, 1 | eleq2s 2859 |
. . 3
⊢ (𝑥 ∈ 𝑆 → ¬ 𝑥 ∈ (-∞(,]0)) |
| 46 | 8, 45 | eldifd 3962 |
. 2
⊢ (𝑥 ∈ 𝑆 → 𝑥 ∈ (ℂ ∖
(-∞(,]0))) |
| 47 | 46 | ssriv 3987 |
1
⊢ 𝑆 ⊆ (ℂ ∖
(-∞(,]0)) |