This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvlog2lem

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

Ref Expression
Hypothesis dvlog2.s ⊢ 𝑆 = ( 1 ( ball ‘ ( abs ∘ − ) ) 1 )
Assertion dvlog2lem 𝑆 ⊆ ( ℂ ∖ ( -∞ (,] 0 ) )

Proof

Step Hyp Ref Expression
1 dvlog2.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 ⊢ 𝑆 ⊆ ℂ
8 7 sseli ⊢ ( 𝑥 ∈ 𝑆 → 𝑥 ∈ ℂ )
9 1red ⊢ ( 𝑥 ∈ ( -∞ (,] 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 ⊢ ( 𝑥 ∈ ( -∞ (,] 0 ) → 𝑥 ∈ ℂ )
18 metcl ⊢ ( ( ( abs ∘ − ) ∈ ( Met ‘ ℂ ) ∧ 1 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 1 ( abs ∘ − ) 𝑥 ) ∈ ℝ )
19 10 3 17 18 mp3an12i ⊢ ( 𝑥 ∈ ( -∞ (,] 0 ) → ( 1 ( abs ∘ − ) 𝑥 ) ∈ ℝ )
20 1m0e1 ⊢ ( 1 − 0 ) = 1
21 14 sseli ⊢ ( 𝑥 ∈ ( -∞ (,] 0 ) → 𝑥 ∈ ℝ )
22 12 a1i ⊢ ( 𝑥 ∈ ( -∞ (,] 0 ) → 0 ∈ ℝ )
23 elioc2 ⊢ ( ( -∞ ∈ ℝ* ∧ 0 ∈ ℝ ) → ( 𝑥 ∈ ( -∞ (,] 0 ) ↔ ( 𝑥 ∈ ℝ ∧ -∞ < 𝑥 ∧ 𝑥 ≤ 0 ) ) )
24 11 12 23 mp2an ⊢ ( 𝑥 ∈ ( -∞ (,] 0 ) ↔ ( 𝑥 ∈ ℝ ∧ -∞ < 𝑥 ∧ 𝑥 ≤ 0 ) )
25 24 simp3bi ⊢ ( 𝑥 ∈ ( -∞ (,] 0 ) → 𝑥 ≤ 0 )
26 21 22 9 25 lesub2dd ⊢ ( 𝑥 ∈ ( -∞ (,] 0 ) → ( 1 − 0 ) ≤ ( 1 − 𝑥 ) )
27 20 26 eqbrtrrid ⊢ ( 𝑥 ∈ ( -∞ (,] 0 ) → 1 ≤ ( 1 − 𝑥 ) )
28 eqid ⊢ ( abs ∘ − ) = ( abs ∘ − )
29 28 cnmetdval ⊢ ( ( 1 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 1 ( abs ∘ − ) 𝑥 ) = ( abs ‘ ( 1 − 𝑥 ) ) )
30 3 17 29 sylancr ⊢ ( 𝑥 ∈ ( -∞ (,] 0 ) → ( 1 ( abs ∘ − ) 𝑥 ) = ( abs ‘ ( 1 − 𝑥 ) ) )
31 0le1 ⊢ 0 ≤ 1
32 31 a1i ⊢ ( 𝑥 ∈ ( -∞ (,] 0 ) → 0 ≤ 1 )
33 21 22 9 25 32 letrd ⊢ ( 𝑥 ∈ ( -∞ (,] 0 ) → 𝑥 ≤ 1 )
34 21 9 33 abssubge0d ⊢ ( 𝑥 ∈ ( -∞ (,] 0 ) → ( abs ‘ ( 1 − 𝑥 ) ) = ( 1 − 𝑥 ) )
35 30 34 eqtrd ⊢ ( 𝑥 ∈ ( -∞ (,] 0 ) → ( 1 ( abs ∘ − ) 𝑥 ) = ( 1 − 𝑥 ) )
36 27 35 breqtrrd ⊢ ( 𝑥 ∈ ( -∞ (,] 0 ) → 1 ≤ ( 1 ( abs ∘ − ) 𝑥 ) )
37 9 19 36 lensymd ⊢ ( 𝑥 ∈ ( -∞ (,] 0 ) → ¬ ( 1 ( abs ∘ − ) 𝑥 ) < 1 )
38 2 a1i ⊢ ( 𝑥 ∈ ( -∞ (,] 0 ) → ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) )
39 4 a1i ⊢ ( 𝑥 ∈ ( -∞ (,] 0 ) → 1 ∈ ℝ* )
40 3 a1i ⊢ ( 𝑥 ∈ ( -∞ (,] 0 ) → 1 ∈ ℂ )
41 elbl2 ⊢ ( ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 1 ∈ ℝ* ) ∧ ( 1 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( 𝑥 ∈ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) ↔ ( 1 ( abs ∘ − ) 𝑥 ) < 1 ) )
42 38 39 40 17 41 syl22anc ⊢ ( 𝑥 ∈ ( -∞ (,] 0 ) → ( 𝑥 ∈ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) ↔ ( 1 ( abs ∘ − ) 𝑥 ) < 1 ) )
43 37 42 mtbird ⊢ ( 𝑥 ∈ ( -∞ (,] 0 ) → ¬ 𝑥 ∈ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) )
44 43 con2i ⊢ ( 𝑥 ∈ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) → ¬ 𝑥 ∈ ( -∞ (,] 0 ) )
45 44 1 eleq2s ⊢ ( 𝑥 ∈ 𝑆 → ¬ 𝑥 ∈ ( -∞ (,] 0 ) )
46 8 45 eldifd ⊢ ( 𝑥 ∈ 𝑆 → 𝑥 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) )
47 46 ssriv ⊢ 𝑆 ⊆ ( ℂ ∖ ( -∞ (,] 0 ) )