Step | Hyp | Ref
| Expression |
1 | | dvlog2.s |
. . . . 5
⊢ 𝑆 = (1(ball‘(abs ∘
− ))1) |
2 | | cnxmet 22777 |
. . . . . 6
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
3 | | ax-1cn 10186 |
. . . . . 6
⊢ 1 ∈
ℂ |
4 | | 1re 10231 |
. . . . . . 7
⊢ 1 ∈
ℝ |
5 | 4 | rexri 10289 |
. . . . . 6
⊢ 1 ∈
ℝ* |
6 | | blssm 22424 |
. . . . . 6
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ ℂ
∧ 1 ∈ ℝ*) → (1(ball‘(abs ∘ −
))1) ⊆ ℂ) |
7 | 2, 3, 5, 6 | mp3an 1573 |
. . . . 5
⊢
(1(ball‘(abs ∘ − ))1) ⊆ ℂ |
8 | 1, 7 | eqsstri 3776 |
. . . 4
⊢ 𝑆 ⊆
ℂ |
9 | 8 | sseli 3740 |
. . 3
⊢ (𝑥 ∈ 𝑆 → 𝑥 ∈ ℂ) |
10 | | 1m0e1 11323 |
. . . . . . . . 9
⊢ (1
− 0) = 1 |
11 | | mnfxr 10288 |
. . . . . . . . . . . 12
⊢ -∞
∈ ℝ* |
12 | | 0re 10232 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℝ |
13 | | iocssre 12446 |
. . . . . . . . . . . 12
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ) →
(-∞(,]0) ⊆ ℝ) |
14 | 11, 12, 13 | mp2an 710 |
. . . . . . . . . . 11
⊢
(-∞(,]0) ⊆ ℝ |
15 | 14 | sseli 3740 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (-∞(,]0) →
𝑥 ∈
ℝ) |
16 | 12 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (-∞(,]0) → 0
∈ ℝ) |
17 | 4 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (-∞(,]0) → 1
∈ ℝ) |
18 | | elioc2 12429 |
. . . . . . . . . . . 12
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ) →
(𝑥 ∈ (-∞(,]0)
↔ (𝑥 ∈ ℝ
∧ -∞ < 𝑥 ∧
𝑥 ≤
0))) |
19 | 11, 12, 18 | mp2an 710 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (-∞(,]0) ↔
(𝑥 ∈ ℝ ∧
-∞ < 𝑥 ∧ 𝑥 ≤ 0)) |
20 | 19 | simp3bi 1142 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (-∞(,]0) →
𝑥 ≤ 0) |
21 | 15, 16, 17, 20 | lesub2dd 10836 |
. . . . . . . . 9
⊢ (𝑥 ∈ (-∞(,]0) → (1
− 0) ≤ (1 − 𝑥)) |
22 | 10, 21 | syl5eqbrr 4840 |
. . . . . . . 8
⊢ (𝑥 ∈ (-∞(,]0) → 1
≤ (1 − 𝑥)) |
23 | | ax-resscn 10185 |
. . . . . . . . . . . 12
⊢ ℝ
⊆ ℂ |
24 | 14, 23 | sstri 3753 |
. . . . . . . . . . 11
⊢
(-∞(,]0) ⊆ ℂ |
25 | 24 | sseli 3740 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (-∞(,]0) →
𝑥 ∈
ℂ) |
26 | | eqid 2760 |
. . . . . . . . . . 11
⊢ (abs
∘ − ) = (abs ∘ − ) |
27 | 26 | cnmetdval 22775 |
. . . . . . . . . 10
⊢ ((1
∈ ℂ ∧ 𝑥
∈ ℂ) → (1(abs ∘ − )𝑥) = (abs‘(1 − 𝑥))) |
28 | 3, 25, 27 | sylancr 698 |
. . . . . . . . 9
⊢ (𝑥 ∈ (-∞(,]0) →
(1(abs ∘ − )𝑥)
= (abs‘(1 − 𝑥))) |
29 | | 0le1 10743 |
. . . . . . . . . . . 12
⊢ 0 ≤
1 |
30 | 29 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (-∞(,]0) → 0
≤ 1) |
31 | 15, 16, 17, 20, 30 | letrd 10386 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (-∞(,]0) →
𝑥 ≤ 1) |
32 | 15, 17, 31 | abssubge0d 14369 |
. . . . . . . . 9
⊢ (𝑥 ∈ (-∞(,]0) →
(abs‘(1 − 𝑥)) =
(1 − 𝑥)) |
33 | 28, 32 | eqtrd 2794 |
. . . . . . . 8
⊢ (𝑥 ∈ (-∞(,]0) →
(1(abs ∘ − )𝑥)
= (1 − 𝑥)) |
34 | 22, 33 | breqtrrd 4832 |
. . . . . . 7
⊢ (𝑥 ∈ (-∞(,]0) → 1
≤ (1(abs ∘ − )𝑥)) |
35 | | cnmet 22776 |
. . . . . . . . . 10
⊢ (abs
∘ − ) ∈ (Met‘ℂ) |
36 | 35 | a1i 11 |
. . . . . . . . 9
⊢ (𝑥 ∈ (-∞(,]0) →
(abs ∘ − ) ∈ (Met‘ℂ)) |
37 | 3 | a1i 11 |
. . . . . . . . 9
⊢ (𝑥 ∈ (-∞(,]0) → 1
∈ ℂ) |
38 | | metcl 22338 |
. . . . . . . . 9
⊢ (((abs
∘ − ) ∈ (Met‘ℂ) ∧ 1 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (1(abs
∘ − )𝑥) ∈
ℝ) |
39 | 36, 37, 25, 38 | syl3anc 1477 |
. . . . . . . 8
⊢ (𝑥 ∈ (-∞(,]0) →
(1(abs ∘ − )𝑥)
∈ ℝ) |
40 | | lenlt 10308 |
. . . . . . . 8
⊢ ((1
∈ ℝ ∧ (1(abs ∘ − )𝑥) ∈ ℝ) → (1 ≤ (1(abs
∘ − )𝑥) ↔
¬ (1(abs ∘ − )𝑥) < 1)) |
41 | 4, 39, 40 | sylancr 698 |
. . . . . . 7
⊢ (𝑥 ∈ (-∞(,]0) → (1
≤ (1(abs ∘ − )𝑥) ↔ ¬ (1(abs ∘ − )𝑥) < 1)) |
42 | 34, 41 | mpbid 222 |
. . . . . 6
⊢ (𝑥 ∈ (-∞(,]0) →
¬ (1(abs ∘ − )𝑥) < 1) |
43 | 2 | a1i 11 |
. . . . . . 7
⊢ (𝑥 ∈ (-∞(,]0) →
(abs ∘ − ) ∈ (∞Met‘ℂ)) |
44 | 5 | a1i 11 |
. . . . . . 7
⊢ (𝑥 ∈ (-∞(,]0) → 1
∈ ℝ*) |
45 | | elbl2 22396 |
. . . . . . 7
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈
ℝ*) ∧ (1 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑥 ∈ (1(ball‘(abs ∘ −
))1) ↔ (1(abs ∘ − )𝑥) < 1)) |
46 | 43, 44, 37, 25, 45 | syl22anc 1478 |
. . . . . 6
⊢ (𝑥 ∈ (-∞(,]0) →
(𝑥 ∈
(1(ball‘(abs ∘ − ))1) ↔ (1(abs ∘ − )𝑥) < 1)) |
47 | 42, 46 | mtbird 314 |
. . . . 5
⊢ (𝑥 ∈ (-∞(,]0) →
¬ 𝑥 ∈
(1(ball‘(abs ∘ − ))1)) |
48 | 47 | con2i 134 |
. . . 4
⊢ (𝑥 ∈ (1(ball‘(abs
∘ − ))1) → ¬ 𝑥 ∈ (-∞(,]0)) |
49 | 48, 1 | eleq2s 2857 |
. . 3
⊢ (𝑥 ∈ 𝑆 → ¬ 𝑥 ∈ (-∞(,]0)) |
50 | 9, 49 | eldifd 3726 |
. 2
⊢ (𝑥 ∈ 𝑆 → 𝑥 ∈ (ℂ ∖
(-∞(,]0))) |
51 | 50 | ssriv 3748 |
1
⊢ 𝑆 ⊆ (ℂ ∖
(-∞(,]0)) |