Metamath Proof Explorer

Theorem dvlog2lem

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

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

Proof

Step Hyp Ref Expression
1 dvlog2.s ⊢S=1ball⁡abs∘−1
2 cnxmet ⊢abs∘−∈∞Met⁡ℂ
3 ax-1cn ⊢1∈ℂ
4 1xr ⊢1∈ℝ*
5 blssm ⊢abs∘−∈∞Met⁡ℂ∧1∈ℂ∧1∈ℝ*→1ball⁡abs∘−1⊆ℂ
6 2 3 4 5 mp3an ⊢1ball⁡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∈ℂ→1abs∘−x∈ℝ
19 10 3 17 18 mp3an12i ⊢x∈−∞0→1abs∘−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∈ℂ→1abs∘−x=1−x
30 3 17 29 sylancr ⊢x∈−∞0→1abs∘−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→1abs∘−x=1−x
36 27 35 breqtrrd ⊢x∈−∞0→1≤1abs∘−x
37 9 19 36 lensymd ⊢x∈−∞0→¬1abs∘−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∈1ball⁡abs∘−1↔1abs∘−x<1
42 38 39 40 17 41 syl22anc ⊢x∈−∞0→x∈1ball⁡abs∘−1↔1abs∘−x<1
43 37 42 mtbird ⊢x∈−∞0→¬x∈1ball⁡abs∘−1
44 43 con2i ⊢x∈1ball⁡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