Step | Hyp | Ref
| Expression |
1 | | dvlog2.s |
. . . . 5
⊢ 𝑆 = (1(ball‘(abs ∘
− ))1) |
2 | | cnxmet 22386 |
. . . . . 6
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
3 | | ax-1cn 9873 |
. . . . . 6
⊢ 1 ∈
ℂ |
4 | | 1re 9918 |
. . . . . . 7
⊢ 1 ∈
ℝ |
5 | 4 | rexri 9976 |
. . . . . 6
⊢ 1 ∈
ℝ* |
6 | | blssm 22033 |
. . . . . 6
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ ℂ
∧ 1 ∈ ℝ*) → (1(ball‘(abs ∘ −
))1) ⊆ ℂ) |
7 | 2, 3, 5, 6 | mp3an 1416 |
. . . . 5
⊢
(1(ball‘(abs ∘ − ))1) ⊆ ℂ |
8 | 1, 7 | eqsstri 3598 |
. . . 4
⊢ 𝑆 ⊆
ℂ |
9 | 8 | sseli 3564 |
. . 3
⊢ (𝑥 ∈ 𝑆 → 𝑥 ∈ ℂ) |
10 | | 1m0e1 11008 |
. . . . . . . . 9
⊢ (1
− 0) = 1 |
11 | | mnfxr 9975 |
. . . . . . . . . . . 12
⊢ -∞
∈ ℝ* |
12 | | 0re 9919 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℝ |
13 | | iocssre 12124 |
. . . . . . . . . . . 12
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ) →
(-∞(,]0) ⊆ ℝ) |
14 | 11, 12, 13 | mp2an 704 |
. . . . . . . . . . 11
⊢
(-∞(,]0) ⊆ ℝ |
15 | 14 | sseli 3564 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (-∞(,]0) →
𝑥 ∈
ℝ) |
16 | 12 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (-∞(,]0) → 0
∈ ℝ) |
17 | 4 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (-∞(,]0) → 1
∈ ℝ) |
18 | | elioc2 12107 |
. . . . . . . . . . . 12
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ) →
(𝑥 ∈ (-∞(,]0)
↔ (𝑥 ∈ ℝ
∧ -∞ < 𝑥 ∧
𝑥 ≤
0))) |
19 | 11, 12, 18 | mp2an 704 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (-∞(,]0) ↔
(𝑥 ∈ ℝ ∧
-∞ < 𝑥 ∧ 𝑥 ≤ 0)) |
20 | 19 | simp3bi 1071 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (-∞(,]0) →
𝑥 ≤ 0) |
21 | 15, 16, 17, 20 | lesub2dd 10523 |
. . . . . . . . 9
⊢ (𝑥 ∈ (-∞(,]0) → (1
− 0) ≤ (1 − 𝑥)) |
22 | 10, 21 | syl5eqbrr 4619 |
. . . . . . . 8
⊢ (𝑥 ∈ (-∞(,]0) → 1
≤ (1 − 𝑥)) |
23 | | ax-resscn 9872 |
. . . . . . . . . . . 12
⊢ ℝ
⊆ ℂ |
24 | 14, 23 | sstri 3577 |
. . . . . . . . . . 11
⊢
(-∞(,]0) ⊆ ℂ |
25 | 24 | sseli 3564 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (-∞(,]0) →
𝑥 ∈
ℂ) |
26 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (abs
∘ − ) = (abs ∘ − ) |
27 | 26 | cnmetdval 22384 |
. . . . . . . . . 10
⊢ ((1
∈ ℂ ∧ 𝑥
∈ ℂ) → (1(abs ∘ − )𝑥) = (abs‘(1 − 𝑥))) |
28 | 3, 25, 27 | sylancr 694 |
. . . . . . . . 9
⊢ (𝑥 ∈ (-∞(,]0) →
(1(abs ∘ − )𝑥)
= (abs‘(1 − 𝑥))) |
29 | | 0le1 10430 |
. . . . . . . . . . . 12
⊢ 0 ≤
1 |
30 | 29 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (-∞(,]0) → 0
≤ 1) |
31 | 15, 16, 17, 20, 30 | letrd 10073 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (-∞(,]0) →
𝑥 ≤ 1) |
32 | 15, 17, 31 | abssubge0d 14018 |
. . . . . . . . 9
⊢ (𝑥 ∈ (-∞(,]0) →
(abs‘(1 − 𝑥)) =
(1 − 𝑥)) |
33 | 28, 32 | eqtrd 2644 |
. . . . . . . 8
⊢ (𝑥 ∈ (-∞(,]0) →
(1(abs ∘ − )𝑥)
= (1 − 𝑥)) |
34 | 22, 33 | breqtrrd 4611 |
. . . . . . 7
⊢ (𝑥 ∈ (-∞(,]0) → 1
≤ (1(abs ∘ − )𝑥)) |
35 | | cnmet 22385 |
. . . . . . . . . 10
⊢ (abs
∘ − ) ∈ (Met‘ℂ) |
36 | 35 | a1i 11 |
. . . . . . . . 9
⊢ (𝑥 ∈ (-∞(,]0) →
(abs ∘ − ) ∈ (Met‘ℂ)) |
37 | 3 | a1i 11 |
. . . . . . . . 9
⊢ (𝑥 ∈ (-∞(,]0) → 1
∈ ℂ) |
38 | | metcl 21947 |
. . . . . . . . 9
⊢ (((abs
∘ − ) ∈ (Met‘ℂ) ∧ 1 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (1(abs
∘ − )𝑥) ∈
ℝ) |
39 | 36, 37, 25, 38 | syl3anc 1318 |
. . . . . . . 8
⊢ (𝑥 ∈ (-∞(,]0) →
(1(abs ∘ − )𝑥)
∈ ℝ) |
40 | | lenlt 9995 |
. . . . . . . 8
⊢ ((1
∈ ℝ ∧ (1(abs ∘ − )𝑥) ∈ ℝ) → (1 ≤ (1(abs
∘ − )𝑥) ↔
¬ (1(abs ∘ − )𝑥) < 1)) |
41 | 4, 39, 40 | sylancr 694 |
. . . . . . 7
⊢ (𝑥 ∈ (-∞(,]0) → (1
≤ (1(abs ∘ − )𝑥) ↔ ¬ (1(abs ∘ − )𝑥) < 1)) |
42 | 34, 41 | mpbid 221 |
. . . . . 6
⊢ (𝑥 ∈ (-∞(,]0) →
¬ (1(abs ∘ − )𝑥) < 1) |
43 | 2 | a1i 11 |
. . . . . . 7
⊢ (𝑥 ∈ (-∞(,]0) →
(abs ∘ − ) ∈ (∞Met‘ℂ)) |
44 | 5 | a1i 11 |
. . . . . . 7
⊢ (𝑥 ∈ (-∞(,]0) → 1
∈ ℝ*) |
45 | | elbl2 22005 |
. . . . . . 7
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈
ℝ*) ∧ (1 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑥 ∈ (1(ball‘(abs ∘ −
))1) ↔ (1(abs ∘ − )𝑥) < 1)) |
46 | 43, 44, 37, 25, 45 | syl22anc 1319 |
. . . . . 6
⊢ (𝑥 ∈ (-∞(,]0) →
(𝑥 ∈
(1(ball‘(abs ∘ − ))1) ↔ (1(abs ∘ − )𝑥) < 1)) |
47 | 42, 46 | mtbird 314 |
. . . . 5
⊢ (𝑥 ∈ (-∞(,]0) →
¬ 𝑥 ∈
(1(ball‘(abs ∘ − ))1)) |
48 | 47 | con2i 133 |
. . . 4
⊢ (𝑥 ∈ (1(ball‘(abs
∘ − ))1) → ¬ 𝑥 ∈ (-∞(,]0)) |
49 | 48, 1 | eleq2s 2706 |
. . 3
⊢ (𝑥 ∈ 𝑆 → ¬ 𝑥 ∈ (-∞(,]0)) |
50 | 9, 49 | eldifd 3551 |
. 2
⊢ (𝑥 ∈ 𝑆 → 𝑥 ∈ (ℂ ∖
(-∞(,]0))) |
51 | 50 | ssriv 3572 |
1
⊢ 𝑆 ⊆ (ℂ ∖
(-∞(,]0)) |