Step | Hyp | Ref
| Expression |
1 | | absf 15231 |
. . . . 5
β’
abs:ββΆβ |
2 | | ffn 6672 |
. . . . 5
β’
(abs:ββΆβ β abs Fn β) |
3 | | elpreima 7012 |
. . . . 5
β’ (abs Fn
β β (π₯ β
(β‘abs β (0[,]π
)) β (π₯ β β β§ (absβπ₯) β (0[,]π
)))) |
4 | 1, 2, 3 | mp2b 10 |
. . . 4
β’ (π₯ β (β‘abs β (0[,]π
)) β (π₯ β β β§ (absβπ₯) β (0[,]π
))) |
5 | | df-3an 1090 |
. . . . . . 7
β’
(((absβπ₯)
β β* β§ 0 β€ (absβπ₯) β§ (absβπ₯) β€ π
) β (((absβπ₯) β β* β§ 0 β€
(absβπ₯)) β§
(absβπ₯) β€ π
)) |
6 | | abscl 15172 |
. . . . . . . . . . 11
β’ (π₯ β β β
(absβπ₯) β
β) |
7 | 6 | rexrd 11213 |
. . . . . . . . . 10
β’ (π₯ β β β
(absβπ₯) β
β*) |
8 | | absge0 15181 |
. . . . . . . . . 10
β’ (π₯ β β β 0 β€
(absβπ₯)) |
9 | 7, 8 | jca 513 |
. . . . . . . . 9
β’ (π₯ β β β
((absβπ₯) β
β* β§ 0 β€ (absβπ₯))) |
10 | 9 | adantl 483 |
. . . . . . . 8
β’ ((π
β β*
β§ π₯ β β)
β ((absβπ₯)
β β* β§ 0 β€ (absβπ₯))) |
11 | 10 | biantrurd 534 |
. . . . . . 7
β’ ((π
β β*
β§ π₯ β β)
β ((absβπ₯) β€
π
β (((absβπ₯) β β*
β§ 0 β€ (absβπ₯))
β§ (absβπ₯) β€
π
))) |
12 | 5, 11 | bitr4id 290 |
. . . . . 6
β’ ((π
β β*
β§ π₯ β β)
β (((absβπ₯)
β β* β§ 0 β€ (absβπ₯) β§ (absβπ₯) β€ π
) β (absβπ₯) β€ π
)) |
13 | | 0xr 11210 |
. . . . . . 7
β’ 0 β
β* |
14 | | simpl 484 |
. . . . . . 7
β’ ((π
β β*
β§ π₯ β β)
β π
β
β*) |
15 | | elicc1 13317 |
. . . . . . 7
β’ ((0
β β* β§ π
β β*) β
((absβπ₯) β
(0[,]π
) β
((absβπ₯) β
β* β§ 0 β€ (absβπ₯) β§ (absβπ₯) β€ π
))) |
16 | 13, 14, 15 | sylancr 588 |
. . . . . 6
β’ ((π
β β*
β§ π₯ β β)
β ((absβπ₯)
β (0[,]π
) β
((absβπ₯) β
β* β§ 0 β€ (absβπ₯) β§ (absβπ₯) β€ π
))) |
17 | | 0cn 11155 |
. . . . . . . . . 10
β’ 0 β
β |
18 | | cnblcld.1 |
. . . . . . . . . . . 12
β’ π· = (abs β β
) |
19 | 18 | cnmetdval 24157 |
. . . . . . . . . . 11
β’ ((0
β β β§ π₯
β β) β (0π·π₯) = (absβ(0 β π₯))) |
20 | | abssub 15220 |
. . . . . . . . . . 11
β’ ((0
β β β§ π₯
β β) β (absβ(0 β π₯)) = (absβ(π₯ β 0))) |
21 | 19, 20 | eqtrd 2773 |
. . . . . . . . . 10
β’ ((0
β β β§ π₯
β β) β (0π·π₯) = (absβ(π₯ β 0))) |
22 | 17, 21 | mpan 689 |
. . . . . . . . 9
β’ (π₯ β β β (0π·π₯) = (absβ(π₯ β 0))) |
23 | | subid1 11429 |
. . . . . . . . . 10
β’ (π₯ β β β (π₯ β 0) = π₯) |
24 | 23 | fveq2d 6850 |
. . . . . . . . 9
β’ (π₯ β β β
(absβ(π₯ β 0)) =
(absβπ₯)) |
25 | 22, 24 | eqtrd 2773 |
. . . . . . . 8
β’ (π₯ β β β (0π·π₯) = (absβπ₯)) |
26 | 25 | adantl 483 |
. . . . . . 7
β’ ((π
β β*
β§ π₯ β β)
β (0π·π₯) = (absβπ₯)) |
27 | 26 | breq1d 5119 |
. . . . . 6
β’ ((π
β β*
β§ π₯ β β)
β ((0π·π₯) β€ π
β (absβπ₯) β€ π
)) |
28 | 12, 16, 27 | 3bitr4d 311 |
. . . . 5
β’ ((π
β β*
β§ π₯ β β)
β ((absβπ₯)
β (0[,]π
) β
(0π·π₯) β€ π
)) |
29 | 28 | pm5.32da 580 |
. . . 4
β’ (π
β β*
β ((π₯ β β
β§ (absβπ₯) β
(0[,]π
)) β (π₯ β β β§ (0π·π₯) β€ π
))) |
30 | 4, 29 | bitrid 283 |
. . 3
β’ (π
β β*
β (π₯ β (β‘abs β (0[,]π
)) β (π₯ β β β§ (0π·π₯) β€ π
))) |
31 | 30 | abbi2dv 2868 |
. 2
β’ (π
β β*
β (β‘abs β (0[,]π
)) = {π₯ β£ (π₯ β β β§ (0π·π₯) β€ π
)}) |
32 | | df-rab 3407 |
. 2
β’ {π₯ β β β£ (0π·π₯) β€ π
} = {π₯ β£ (π₯ β β β§ (0π·π₯) β€ π
)} |
33 | 31, 32 | eqtr4di 2791 |
1
β’ (π
β β*
β (β‘abs β (0[,]π
)) = {π₯ β β β£ (0π·π₯) β€ π
}) |