Step | Hyp | Ref
| Expression |
1 | | df-3an 980 |
. . . . . 6
β’
(((absβπ₯)
β β β§ 0 β€ (absβπ₯) β§ (absβπ₯) < π
) β (((absβπ₯) β β β§ 0 β€
(absβπ₯)) β§
(absβπ₯) < π
)) |
2 | | abscl 11059 |
. . . . . . . . 9
β’ (π₯ β β β
(absβπ₯) β
β) |
3 | | absge0 11068 |
. . . . . . . . 9
β’ (π₯ β β β 0 β€
(absβπ₯)) |
4 | 2, 3 | jca 306 |
. . . . . . . 8
β’ (π₯ β β β
((absβπ₯) β
β β§ 0 β€ (absβπ₯))) |
5 | 4 | adantl 277 |
. . . . . . 7
β’ ((π
β β*
β§ π₯ β β)
β ((absβπ₯)
β β β§ 0 β€ (absβπ₯))) |
6 | 5 | biantrurd 305 |
. . . . . 6
β’ ((π
β β*
β§ π₯ β β)
β ((absβπ₯) <
π
β (((absβπ₯) β β β§ 0 β€
(absβπ₯)) β§
(absβπ₯) < π
))) |
7 | 1, 6 | bitr4id 199 |
. . . . 5
β’ ((π
β β*
β§ π₯ β β)
β (((absβπ₯)
β β β§ 0 β€ (absβπ₯) β§ (absβπ₯) < π
) β (absβπ₯) < π
)) |
8 | | 0re 7956 |
. . . . . 6
β’ 0 β
β |
9 | | simpl 109 |
. . . . . 6
β’ ((π
β β*
β§ π₯ β β)
β π
β
β*) |
10 | | elico2 9936 |
. . . . . 6
β’ ((0
β β β§ π
β β*) β ((absβπ₯) β (0[,)π
) β ((absβπ₯) β β β§ 0 β€
(absβπ₯) β§
(absβπ₯) < π
))) |
11 | 8, 9, 10 | sylancr 414 |
. . . . 5
β’ ((π
β β*
β§ π₯ β β)
β ((absβπ₯)
β (0[,)π
) β
((absβπ₯) β
β β§ 0 β€ (absβπ₯) β§ (absβπ₯) < π
))) |
12 | | 0cn 7948 |
. . . . . . . . 9
β’ 0 β
β |
13 | | cnblcld.1 |
. . . . . . . . . . 11
β’ π· = (abs β β
) |
14 | 13 | cnmetdval 13999 |
. . . . . . . . . 10
β’ ((0
β β β§ π₯
β β) β (0π·π₯) = (absβ(0 β π₯))) |
15 | | abssub 11109 |
. . . . . . . . . 10
β’ ((0
β β β§ π₯
β β) β (absβ(0 β π₯)) = (absβ(π₯ β 0))) |
16 | 14, 15 | eqtrd 2210 |
. . . . . . . . 9
β’ ((0
β β β§ π₯
β β) β (0π·π₯) = (absβ(π₯ β 0))) |
17 | 12, 16 | mpan 424 |
. . . . . . . 8
β’ (π₯ β β β (0π·π₯) = (absβ(π₯ β 0))) |
18 | | subid1 8176 |
. . . . . . . . 9
β’ (π₯ β β β (π₯ β 0) = π₯) |
19 | 18 | fveq2d 5519 |
. . . . . . . 8
β’ (π₯ β β β
(absβ(π₯ β 0)) =
(absβπ₯)) |
20 | 17, 19 | eqtrd 2210 |
. . . . . . 7
β’ (π₯ β β β (0π·π₯) = (absβπ₯)) |
21 | 20 | adantl 277 |
. . . . . 6
β’ ((π
β β*
β§ π₯ β β)
β (0π·π₯) = (absβπ₯)) |
22 | 21 | breq1d 4013 |
. . . . 5
β’ ((π
β β*
β§ π₯ β β)
β ((0π·π₯) < π
β (absβπ₯) < π
)) |
23 | 7, 11, 22 | 3bitr4d 220 |
. . . 4
β’ ((π
β β*
β§ π₯ β β)
β ((absβπ₯)
β (0[,)π
) β
(0π·π₯) < π
)) |
24 | 23 | pm5.32da 452 |
. . 3
β’ (π
β β*
β ((π₯ β β
β§ (absβπ₯) β
(0[,)π
)) β (π₯ β β β§ (0π·π₯) < π
))) |
25 | | absf 11118 |
. . . . 5
β’
abs:ββΆβ |
26 | | ffn 5365 |
. . . . 5
β’
(abs:ββΆβ β abs Fn β) |
27 | 25, 26 | ax-mp 5 |
. . . 4
β’ abs Fn
β |
28 | | elpreima 5635 |
. . . 4
β’ (abs Fn
β β (π₯ β
(β‘abs β (0[,)π
)) β (π₯ β β β§ (absβπ₯) β (0[,)π
)))) |
29 | 27, 28 | mp1i 10 |
. . 3
β’ (π
β β*
β (π₯ β (β‘abs β (0[,)π
)) β (π₯ β β β§ (absβπ₯) β (0[,)π
)))) |
30 | | cnxmet 14001 |
. . . . 5
β’ (abs
β β ) β (βMetββ) |
31 | 13, 30 | eqeltri 2250 |
. . . 4
β’ π· β
(βMetββ) |
32 | | elbl 13861 |
. . . 4
β’ ((π· β
(βMetββ) β§ 0 β β β§ π
β β*) β (π₯ β (0(ballβπ·)π
) β (π₯ β β β§ (0π·π₯) < π
))) |
33 | 31, 12, 32 | mp3an12 1327 |
. . 3
β’ (π
β β*
β (π₯ β
(0(ballβπ·)π
) β (π₯ β β β§ (0π·π₯) < π
))) |
34 | 24, 29, 33 | 3bitr4d 220 |
. 2
β’ (π
β β*
β (π₯ β (β‘abs β (0[,)π
)) β π₯ β (0(ballβπ·)π
))) |
35 | 34 | eqrdv 2175 |
1
β’ (π
β β*
β (β‘abs β (0[,)π
)) = (0(ballβπ·)π
)) |