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