Step | Hyp | Ref
| Expression |
1 | | dvlog2.s |
. . . . 5
β’ π = (1(ballβ(abs β
β ))1) |
2 | | cnxmet 24288 |
. . . . . 6
β’ (abs
β β ) β (βMetββ) |
3 | | ax-1cn 11167 |
. . . . . 6
β’ 1 β
β |
4 | | 1xr 11272 |
. . . . . 6
β’ 1 β
β* |
5 | | blssm 23923 |
. . . . . 6
β’ (((abs
β β ) β (βMetββ) β§ 1 β β
β§ 1 β β*) β (1(ballβ(abs β β
))1) β β) |
6 | 2, 3, 4, 5 | mp3an 1461 |
. . . . 5
β’
(1(ballβ(abs β β ))1) β β |
7 | 1, 6 | eqsstri 4016 |
. . . 4
β’ π β
β |
8 | 7 | sseli 3978 |
. . 3
β’ (π₯ β π β π₯ β β) |
9 | | 1red 11214 |
. . . . . . 7
β’ (π₯ β (-β(,]0) β 1
β β) |
10 | | cnmet 24287 |
. . . . . . . 8
β’ (abs
β β ) β (Metββ) |
11 | | mnfxr 11270 |
. . . . . . . . . . 11
β’ -β
β β* |
12 | | 0re 11215 |
. . . . . . . . . . 11
β’ 0 β
β |
13 | | iocssre 13403 |
. . . . . . . . . . 11
β’
((-β β β* β§ 0 β β) β
(-β(,]0) β β) |
14 | 11, 12, 13 | mp2an 690 |
. . . . . . . . . 10
β’
(-β(,]0) β β |
15 | | ax-resscn 11166 |
. . . . . . . . . 10
β’ β
β β |
16 | 14, 15 | sstri 3991 |
. . . . . . . . 9
β’
(-β(,]0) β β |
17 | 16 | sseli 3978 |
. . . . . . . 8
β’ (π₯ β (-β(,]0) β
π₯ β
β) |
18 | | metcl 23837 |
. . . . . . . 8
β’ (((abs
β β ) β (Metββ) β§ 1 β β β§ π₯ β β) β (1(abs
β β )π₯) β
β) |
19 | 10, 3, 17, 18 | mp3an12i 1465 |
. . . . . . 7
β’ (π₯ β (-β(,]0) β
(1(abs β β )π₯)
β β) |
20 | | 1m0e1 12332 |
. . . . . . . . 9
β’ (1
β 0) = 1 |
21 | 14 | sseli 3978 |
. . . . . . . . . 10
β’ (π₯ β (-β(,]0) β
π₯ β
β) |
22 | 12 | a1i 11 |
. . . . . . . . . 10
β’ (π₯ β (-β(,]0) β 0
β β) |
23 | | elioc2 13386 |
. . . . . . . . . . . 12
β’
((-β β β* β§ 0 β β) β
(π₯ β (-β(,]0)
β (π₯ β β
β§ -β < π₯ β§
π₯ β€
0))) |
24 | 11, 12, 23 | mp2an 690 |
. . . . . . . . . . 11
β’ (π₯ β (-β(,]0) β
(π₯ β β β§
-β < π₯ β§ π₯ β€ 0)) |
25 | 24 | simp3bi 1147 |
. . . . . . . . . 10
β’ (π₯ β (-β(,]0) β
π₯ β€ 0) |
26 | 21, 22, 9, 25 | lesub2dd 11830 |
. . . . . . . . 9
β’ (π₯ β (-β(,]0) β (1
β 0) β€ (1 β π₯)) |
27 | 20, 26 | eqbrtrrid 5184 |
. . . . . . . 8
β’ (π₯ β (-β(,]0) β 1
β€ (1 β π₯)) |
28 | | eqid 2732 |
. . . . . . . . . . 11
β’ (abs
β β ) = (abs β β ) |
29 | 28 | cnmetdval 24286 |
. . . . . . . . . 10
β’ ((1
β β β§ π₯
β β) β (1(abs β β )π₯) = (absβ(1 β π₯))) |
30 | 3, 17, 29 | sylancr 587 |
. . . . . . . . 9
β’ (π₯ β (-β(,]0) β
(1(abs β β )π₯)
= (absβ(1 β π₯))) |
31 | | 0le1 11736 |
. . . . . . . . . . . 12
β’ 0 β€
1 |
32 | 31 | a1i 11 |
. . . . . . . . . . 11
β’ (π₯ β (-β(,]0) β 0
β€ 1) |
33 | 21, 22, 9, 25, 32 | letrd 11370 |
. . . . . . . . . 10
β’ (π₯ β (-β(,]0) β
π₯ β€ 1) |
34 | 21, 9, 33 | abssubge0d 15377 |
. . . . . . . . 9
β’ (π₯ β (-β(,]0) β
(absβ(1 β π₯)) =
(1 β π₯)) |
35 | 30, 34 | eqtrd 2772 |
. . . . . . . 8
β’ (π₯ β (-β(,]0) β
(1(abs β β )π₯)
= (1 β π₯)) |
36 | 27, 35 | breqtrrd 5176 |
. . . . . . 7
β’ (π₯ β (-β(,]0) β 1
β€ (1(abs β β )π₯)) |
37 | 9, 19, 36 | lensymd 11364 |
. . . . . 6
β’ (π₯ β (-β(,]0) β
Β¬ (1(abs β β )π₯) < 1) |
38 | 2 | a1i 11 |
. . . . . . 7
β’ (π₯ β (-β(,]0) β
(abs β β ) β (βMetββ)) |
39 | 4 | a1i 11 |
. . . . . . 7
β’ (π₯ β (-β(,]0) β 1
β β*) |
40 | 3 | a1i 11 |
. . . . . . 7
β’ (π₯ β (-β(,]0) β 1
β β) |
41 | | elbl2 23895 |
. . . . . . 7
β’ ((((abs
β β ) β (βMetββ) β§ 1 β
β*) β§ (1 β β β§ π₯ β β)) β (π₯ β (1(ballβ(abs β β
))1) β (1(abs β β )π₯) < 1)) |
42 | 38, 39, 40, 17, 41 | syl22anc 837 |
. . . . . 6
β’ (π₯ β (-β(,]0) β
(π₯ β
(1(ballβ(abs β β ))1) β (1(abs β β )π₯) < 1)) |
43 | 37, 42 | mtbird 324 |
. . . . 5
β’ (π₯ β (-β(,]0) β
Β¬ π₯ β
(1(ballβ(abs β β ))1)) |
44 | 43 | con2i 139 |
. . . 4
β’ (π₯ β (1(ballβ(abs
β β ))1) β Β¬ π₯ β (-β(,]0)) |
45 | 44, 1 | eleq2s 2851 |
. . 3
β’ (π₯ β π β Β¬ π₯ β (-β(,]0)) |
46 | 8, 45 | eldifd 3959 |
. 2
β’ (π₯ β π β π₯ β (β β
(-β(,]0))) |
47 | 46 | ssriv 3986 |
1
β’ π β (β β
(-β(,]0)) |