Metamath Proof Explorer

Theorem dvlog2lem

Description: Lemma for dvlog2 . (Contributed by Mario Carneiro, 1-Mar-2015)

Ref Expression
Hypothesis dvlog2.s ⊢ S = 1 ball ⁡ abs ∘ − 1
Assertion dvlog2lem ⊢ S ⊆ ℂ ∖ −∞ 0

Proof

Step Hyp Ref Expression
1 dvlog2.s ⊢ S = 1 ball ⁡ abs ∘ − 1
2 cnxmet ⊢ abs ∘ − ∈ ∞Met ⁡ ℂ
3 ax-1cn ⊢ 1 ∈ ℂ
4 1xr ⊢ 1 ∈ ℝ *
5 blssm ⊢ abs ∘ − ∈ ∞Met ⁡ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℝ * → 1 ball ⁡ abs ∘ − 1 ⊆ ℂ
6 2 3 4 5 mp3an ⊢ 1 ball ⁡ abs ∘ − 1 ⊆ ℂ
7 1 6 eqsstri ⊢ S ⊆ ℂ
8 7 sseli ⊢ x ∈ S → x ∈ ℂ
9 1red ⊢ x ∈ −∞ 0 → 1 ∈ ℝ
10 cnmet ⊢ abs ∘ − ∈ Met ⁡ ℂ
11 mnfxr ⊢ −∞ ∈ ℝ *
12 0re ⊢ 0 ∈ ℝ
13 iocssre ⊢ −∞ ∈ ℝ * ∧ 0 ∈ ℝ → −∞ 0 ⊆ ℝ
14 11 12 13 mp2an ⊢ −∞ 0 ⊆ ℝ
15 ax-resscn ⊢ ℝ ⊆ ℂ
16 14 15 sstri ⊢ −∞ 0 ⊆ ℂ
17 16 sseli ⊢ x ∈ −∞ 0 → x ∈ ℂ
18 metcl ⊢ abs ∘ − ∈ Met ⁡ ℂ ∧ 1 ∈ ℂ ∧ x ∈ ℂ → 1 abs ∘ − x ∈ ℝ
19 10 3 17 18 mp3an12i ⊢ x ∈ −∞ 0 → 1 abs ∘ − x ∈ ℝ
20 1m0e1 ⊢ 1 − 0 = 1
21 14 sseli ⊢ x ∈ −∞ 0 → x ∈ ℝ
22 12 a1i ⊢ x ∈ −∞ 0 → 0 ∈ ℝ
23 elioc2 ⊢ −∞ ∈ ℝ * ∧ 0 ∈ ℝ → x ∈ −∞ 0 ↔ x ∈ ℝ ∧ −∞ < x ∧ x ≤ 0
24 11 12 23 mp2an ⊢ x ∈ −∞ 0 ↔ x ∈ ℝ ∧ −∞ < x ∧ x ≤ 0
25 24 simp3bi ⊢ x ∈ −∞ 0 → x ≤ 0
26 21 22 9 25 lesub2dd ⊢ x ∈ −∞ 0 → 1 − 0 ≤ 1 − x
27 20 26 eqbrtrrid ⊢ x ∈ −∞ 0 → 1 ≤ 1 − x
28 eqid ⊢ abs ∘ − = abs ∘ −
29 28 cnmetdval ⊢ 1 ∈ ℂ ∧ x ∈ ℂ → 1 abs ∘ − x = 1 − x
30 3 17 29 sylancr ⊢ x ∈ −∞ 0 → 1 abs ∘ − x = 1 − x
31 0le1 ⊢ 0 ≤ 1
32 31 a1i ⊢ x ∈ −∞ 0 → 0 ≤ 1
33 21 22 9 25 32 letrd ⊢ x ∈ −∞ 0 → x ≤ 1
34 21 9 33 abssubge0d ⊢ x ∈ −∞ 0 → 1 − x = 1 − x
35 30 34 eqtrd ⊢ x ∈ −∞ 0 → 1 abs ∘ − x = 1 − x
36 27 35 breqtrrd ⊢ x ∈ −∞ 0 → 1 ≤ 1 abs ∘ − x
37 9 19 36 lensymd ⊢ x ∈ −∞ 0 → ¬ 1 abs ∘ − x < 1
38 2 a1i ⊢ x ∈ −∞ 0 → abs ∘ − ∈ ∞Met ⁡ ℂ
39 4 a1i ⊢ x ∈ −∞ 0 → 1 ∈ ℝ *
40 3 a1i ⊢ x ∈ −∞ 0 → 1 ∈ ℂ
41 elbl2 ⊢ abs ∘ − ∈ ∞Met ⁡ ℂ ∧ 1 ∈ ℝ * ∧ 1 ∈ ℂ ∧ x ∈ ℂ → x ∈ 1 ball ⁡ abs ∘ − 1 ↔ 1 abs ∘ − x < 1
42 38 39 40 17 41 syl22anc ⊢ x ∈ −∞ 0 → x ∈ 1 ball ⁡ abs ∘ − 1 ↔ 1 abs ∘ − x < 1
43 37 42 mtbird ⊢ x ∈ −∞ 0 → ¬ x ∈ 1 ball ⁡ abs ∘ − 1
44 43 con2i ⊢ x ∈ 1 ball ⁡ abs ∘ − 1 → ¬ x ∈ −∞ 0
45 44 1 eleq2s ⊢ x ∈ S → ¬ x ∈ −∞ 0
46 8 45 eldifd ⊢ x ∈ S → x ∈ ℂ ∖ −∞ 0
47 46 ssriv ⊢ S ⊆ ℂ ∖ −∞ 0