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