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 ) )