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 o. - ) ) 1 )
Assertion dvlog2lem
|- S C_ ( CC \ ( -oo (,] 0 ) )

Proof

Step Hyp Ref Expression
1 dvlog2.s
 |-  S = ( 1 ( ball ` ( abs o. - ) ) 1 )
2 cnxmet
 |-  ( abs o. - ) e. ( *Met ` CC )
3 ax-1cn
 |-  1 e. CC
4 1xr
 |-  1 e. RR*
5 blssm
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ 1 e. CC /\ 1 e. RR* ) -> ( 1 ( ball ` ( abs o. - ) ) 1 ) C_ CC )
6 2 3 4 5 mp3an
 |-  ( 1 ( ball ` ( abs o. - ) ) 1 ) C_ CC
7 1 6 eqsstri
 |-  S C_ CC
8 7 sseli
 |-  ( x e. S -> x e. CC )
9 1red
 |-  ( x e. ( -oo (,] 0 ) -> 1 e. RR )
10 cnmet
 |-  ( abs o. - ) e. ( Met ` CC )
11 mnfxr
 |-  -oo e. RR*
12 0re
 |-  0 e. RR
13 iocssre
 |-  ( ( -oo e. RR* /\ 0 e. RR ) -> ( -oo (,] 0 ) C_ RR )
14 11 12 13 mp2an
 |-  ( -oo (,] 0 ) C_ RR
15 ax-resscn
 |-  RR C_ CC
16 14 15 sstri
 |-  ( -oo (,] 0 ) C_ CC
17 16 sseli
 |-  ( x e. ( -oo (,] 0 ) -> x e. CC )
18 metcl
 |-  ( ( ( abs o. - ) e. ( Met ` CC ) /\ 1 e. CC /\ x e. CC ) -> ( 1 ( abs o. - ) x ) e. RR )
19 10 3 17 18 mp3an12i
 |-  ( x e. ( -oo (,] 0 ) -> ( 1 ( abs o. - ) x ) e. RR )
20 1m0e1
 |-  ( 1 - 0 ) = 1
21 14 sseli
 |-  ( x e. ( -oo (,] 0 ) -> x e. RR )
22 12 a1i
 |-  ( x e. ( -oo (,] 0 ) -> 0 e. RR )
23 elioc2
 |-  ( ( -oo e. RR* /\ 0 e. RR ) -> ( x e. ( -oo (,] 0 ) <-> ( x e. RR /\ -oo < x /\ x <_ 0 ) ) )
24 11 12 23 mp2an
 |-  ( x e. ( -oo (,] 0 ) <-> ( x e. RR /\ -oo < x /\ x <_ 0 ) )
25 24 simp3bi
 |-  ( x e. ( -oo (,] 0 ) -> x <_ 0 )
26 21 22 9 25 lesub2dd
 |-  ( x e. ( -oo (,] 0 ) -> ( 1 - 0 ) <_ ( 1 - x ) )
27 20 26 eqbrtrrid
 |-  ( x e. ( -oo (,] 0 ) -> 1 <_ ( 1 - x ) )
28 eqid
 |-  ( abs o. - ) = ( abs o. - )
29 28 cnmetdval
 |-  ( ( 1 e. CC /\ x e. CC ) -> ( 1 ( abs o. - ) x ) = ( abs ` ( 1 - x ) ) )
30 3 17 29 sylancr
 |-  ( x e. ( -oo (,] 0 ) -> ( 1 ( abs o. - ) x ) = ( abs ` ( 1 - x ) ) )
31 0le1
 |-  0 <_ 1
32 31 a1i
 |-  ( x e. ( -oo (,] 0 ) -> 0 <_ 1 )
33 21 22 9 25 32 letrd
 |-  ( x e. ( -oo (,] 0 ) -> x <_ 1 )
34 21 9 33 abssubge0d
 |-  ( x e. ( -oo (,] 0 ) -> ( abs ` ( 1 - x ) ) = ( 1 - x ) )
35 30 34 eqtrd
 |-  ( x e. ( -oo (,] 0 ) -> ( 1 ( abs o. - ) x ) = ( 1 - x ) )
36 27 35 breqtrrd
 |-  ( x e. ( -oo (,] 0 ) -> 1 <_ ( 1 ( abs o. - ) x ) )
37 9 19 36 lensymd
 |-  ( x e. ( -oo (,] 0 ) -> -. ( 1 ( abs o. - ) x ) < 1 )
38 2 a1i
 |-  ( x e. ( -oo (,] 0 ) -> ( abs o. - ) e. ( *Met ` CC ) )
39 4 a1i
 |-  ( x e. ( -oo (,] 0 ) -> 1 e. RR* )
40 3 a1i
 |-  ( x e. ( -oo (,] 0 ) -> 1 e. CC )
41 elbl2
 |-  ( ( ( ( abs o. - ) e. ( *Met ` CC ) /\ 1 e. RR* ) /\ ( 1 e. CC /\ x e. CC ) ) -> ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) <-> ( 1 ( abs o. - ) x ) < 1 ) )
42 38 39 40 17 41 syl22anc
 |-  ( x e. ( -oo (,] 0 ) -> ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) <-> ( 1 ( abs o. - ) x ) < 1 ) )
43 37 42 mtbird
 |-  ( x e. ( -oo (,] 0 ) -> -. x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) )
44 43 con2i
 |-  ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) -> -. x e. ( -oo (,] 0 ) )
45 44 1 eleq2s
 |-  ( x e. S -> -. x e. ( -oo (,] 0 ) )
46 8 45 eldifd
 |-  ( x e. S -> x e. ( CC \ ( -oo (,] 0 ) ) )
47 46 ssriv
 |-  S C_ ( CC \ ( -oo (,] 0 ) )