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