Step | Hyp | Ref
| Expression |
1 | | absf 15283 |
. . . . 5
β’
abs:ββΆβ |
2 | | ffn 6717 |
. . . . 5
β’
(abs:ββΆβ β abs Fn β) |
3 | | elpreima 7059 |
. . . . 5
β’ (abs Fn
β β (π₯ β
(β‘abs β (0[,]π
)) β (π₯ β β β§ (absβπ₯) β (0[,]π
)))) |
4 | 1, 2, 3 | mp2b 10 |
. . . 4
β’ (π₯ β (β‘abs β (0[,]π
)) β (π₯ β β β§ (absβπ₯) β (0[,]π
))) |
5 | | df-3an 1089 |
. . . . . . 7
β’
(((absβπ₯)
β β* β§ 0 β€ (absβπ₯) β§ (absβπ₯) β€ π
) β (((absβπ₯) β β* β§ 0 β€
(absβπ₯)) β§
(absβπ₯) β€ π
)) |
6 | | abscl 15224 |
. . . . . . . . . . 11
β’ (π₯ β β β
(absβπ₯) β
β) |
7 | 6 | rexrd 11263 |
. . . . . . . . . 10
β’ (π₯ β β β
(absβπ₯) β
β*) |
8 | | absge0 15233 |
. . . . . . . . . 10
β’ (π₯ β β β 0 β€
(absβπ₯)) |
9 | 7, 8 | jca 512 |
. . . . . . . . 9
β’ (π₯ β β β
((absβπ₯) β
β* β§ 0 β€ (absβπ₯))) |
10 | 9 | adantl 482 |
. . . . . . . 8
β’ ((π
β β*
β§ π₯ β β)
β ((absβπ₯)
β β* β§ 0 β€ (absβπ₯))) |
11 | 10 | biantrurd 533 |
. . . . . . 7
β’ ((π
β β*
β§ π₯ β β)
β ((absβπ₯) β€
π
β (((absβπ₯) β β*
β§ 0 β€ (absβπ₯))
β§ (absβπ₯) β€
π
))) |
12 | 5, 11 | bitr4id 289 |
. . . . . 6
β’ ((π
β β*
β§ π₯ β β)
β (((absβπ₯)
β β* β§ 0 β€ (absβπ₯) β§ (absβπ₯) β€ π
) β (absβπ₯) β€ π
)) |
13 | | 0xr 11260 |
. . . . . . 7
β’ 0 β
β* |
14 | | simpl 483 |
. . . . . . 7
β’ ((π
β β*
β§ π₯ β β)
β π
β
β*) |
15 | | elicc1 13367 |
. . . . . . 7
β’ ((0
β β* β§ π
β β*) β
((absβπ₯) β
(0[,]π
) β
((absβπ₯) β
β* β§ 0 β€ (absβπ₯) β§ (absβπ₯) β€ π
))) |
16 | 13, 14, 15 | sylancr 587 |
. . . . . 6
β’ ((π
β β*
β§ π₯ β β)
β ((absβπ₯)
β (0[,]π
) β
((absβπ₯) β
β* β§ 0 β€ (absβπ₯) β§ (absβπ₯) β€ π
))) |
17 | | 0cn 11205 |
. . . . . . . . . 10
β’ 0 β
β |
18 | | cnblcld.1 |
. . . . . . . . . . . 12
β’ π· = (abs β β
) |
19 | 18 | cnmetdval 24286 |
. . . . . . . . . . 11
β’ ((0
β β β§ π₯
β β) β (0π·π₯) = (absβ(0 β π₯))) |
20 | | abssub 15272 |
. . . . . . . . . . 11
β’ ((0
β β β§ π₯
β β) β (absβ(0 β π₯)) = (absβ(π₯ β 0))) |
21 | 19, 20 | eqtrd 2772 |
. . . . . . . . . 10
β’ ((0
β β β§ π₯
β β) β (0π·π₯) = (absβ(π₯ β 0))) |
22 | 17, 21 | mpan 688 |
. . . . . . . . 9
β’ (π₯ β β β (0π·π₯) = (absβ(π₯ β 0))) |
23 | | subid1 11479 |
. . . . . . . . . 10
β’ (π₯ β β β (π₯ β 0) = π₯) |
24 | 23 | fveq2d 6895 |
. . . . . . . . 9
β’ (π₯ β β β
(absβ(π₯ β 0)) =
(absβπ₯)) |
25 | 22, 24 | eqtrd 2772 |
. . . . . . . 8
β’ (π₯ β β β (0π·π₯) = (absβπ₯)) |
26 | 25 | adantl 482 |
. . . . . . 7
β’ ((π
β β*
β§ π₯ β β)
β (0π·π₯) = (absβπ₯)) |
27 | 26 | breq1d 5158 |
. . . . . 6
β’ ((π
β β*
β§ π₯ β β)
β ((0π·π₯) β€ π
β (absβπ₯) β€ π
)) |
28 | 12, 16, 27 | 3bitr4d 310 |
. . . . 5
β’ ((π
β β*
β§ π₯ β β)
β ((absβπ₯)
β (0[,]π
) β
(0π·π₯) β€ π
)) |
29 | 28 | pm5.32da 579 |
. . . 4
β’ (π
β β*
β ((π₯ β β
β§ (absβπ₯) β
(0[,]π
)) β (π₯ β β β§ (0π·π₯) β€ π
))) |
30 | 4, 29 | bitrid 282 |
. . 3
β’ (π
β β*
β (π₯ β (β‘abs β (0[,]π
)) β (π₯ β β β§ (0π·π₯) β€ π
))) |
31 | 30 | eqabdv 2867 |
. 2
β’ (π
β β*
β (β‘abs β (0[,]π
)) = {π₯ β£ (π₯ β β β§ (0π·π₯) β€ π
)}) |
32 | | df-rab 3433 |
. 2
β’ {π₯ β β β£ (0π·π₯) β€ π
} = {π₯ β£ (π₯ β β β§ (0π·π₯) β€ π
)} |
33 | 31, 32 | eqtr4di 2790 |
1
β’ (π
β β*
β (β‘abs β (0[,]π
)) = {π₯ β β β£ (0π·π₯) β€ π
}) |