Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. 2
β’ ((π΄ β β β§ π₯ β β+)
β π₯ β
β+) |
2 | | simpr 486 |
. . . . 5
β’ (((π΄ β β β§ π₯ β β+)
β§ π§ β β)
β π§ β
β) |
3 | | simpll 766 |
. . . . 5
β’ (((π΄ β β β§ π₯ β β+)
β§ π§ β β)
β π΄ β
β) |
4 | | cn1lem.2 |
. . . . 5
β’ ((π§ β β β§ π΄ β β) β
(absβ((πΉβπ§) β (πΉβπ΄))) β€ (absβ(π§ β π΄))) |
5 | 2, 3, 4 | syl2anc 585 |
. . . 4
β’ (((π΄ β β β§ π₯ β β+)
β§ π§ β β)
β (absβ((πΉβπ§) β (πΉβπ΄))) β€ (absβ(π§ β π΄))) |
6 | | cn1lem.1 |
. . . . . . . . 9
β’ πΉ:ββΆβ |
7 | 6 | ffvelcdmi 7035 |
. . . . . . . 8
β’ (π§ β β β (πΉβπ§) β β) |
8 | 2, 7 | syl 17 |
. . . . . . 7
β’ (((π΄ β β β§ π₯ β β+)
β§ π§ β β)
β (πΉβπ§) β
β) |
9 | 6 | ffvelcdmi 7035 |
. . . . . . . 8
β’ (π΄ β β β (πΉβπ΄) β β) |
10 | 3, 9 | syl 17 |
. . . . . . 7
β’ (((π΄ β β β§ π₯ β β+)
β§ π§ β β)
β (πΉβπ΄) β
β) |
11 | 8, 10 | subcld 11517 |
. . . . . 6
β’ (((π΄ β β β§ π₯ β β+)
β§ π§ β β)
β ((πΉβπ§) β (πΉβπ΄)) β β) |
12 | 11 | abscld 15327 |
. . . . 5
β’ (((π΄ β β β§ π₯ β β+)
β§ π§ β β)
β (absβ((πΉβπ§) β (πΉβπ΄))) β β) |
13 | 2, 3 | subcld 11517 |
. . . . . 6
β’ (((π΄ β β β§ π₯ β β+)
β§ π§ β β)
β (π§ β π΄) β
β) |
14 | 13 | abscld 15327 |
. . . . 5
β’ (((π΄ β β β§ π₯ β β+)
β§ π§ β β)
β (absβ(π§
β π΄)) β
β) |
15 | | rpre 12928 |
. . . . . 6
β’ (π₯ β β+
β π₯ β
β) |
16 | 15 | ad2antlr 726 |
. . . . 5
β’ (((π΄ β β β§ π₯ β β+)
β§ π§ β β)
β π₯ β
β) |
17 | | lelttr 11250 |
. . . . 5
β’
(((absβ((πΉβπ§) β (πΉβπ΄))) β β β§ (absβ(π§ β π΄)) β β β§ π₯ β β) β (((absβ((πΉβπ§) β (πΉβπ΄))) β€ (absβ(π§ β π΄)) β§ (absβ(π§ β π΄)) < π₯) β (absβ((πΉβπ§) β (πΉβπ΄))) < π₯)) |
18 | 12, 14, 16, 17 | syl3anc 1372 |
. . . 4
β’ (((π΄ β β β§ π₯ β β+)
β§ π§ β β)
β (((absβ((πΉβπ§) β (πΉβπ΄))) β€ (absβ(π§ β π΄)) β§ (absβ(π§ β π΄)) < π₯) β (absβ((πΉβπ§) β (πΉβπ΄))) < π₯)) |
19 | 5, 18 | mpand 694 |
. . 3
β’ (((π΄ β β β§ π₯ β β+)
β§ π§ β β)
β ((absβ(π§
β π΄)) < π₯ β (absβ((πΉβπ§) β (πΉβπ΄))) < π₯)) |
20 | 19 | ralrimiva 3140 |
. 2
β’ ((π΄ β β β§ π₯ β β+)
β βπ§ β
β ((absβ(π§
β π΄)) < π₯ β (absβ((πΉβπ§) β (πΉβπ΄))) < π₯)) |
21 | | breq2 5110 |
. . 3
β’ (π¦ = π₯ β ((absβ(π§ β π΄)) < π¦ β (absβ(π§ β π΄)) < π₯)) |
22 | 21 | rspceaimv 3584 |
. 2
β’ ((π₯ β β+
β§ βπ§ β
β ((absβ(π§
β π΄)) < π₯ β (absβ((πΉβπ§) β (πΉβπ΄))) < π₯)) β βπ¦ β β+ βπ§ β β
((absβ(π§ β
π΄)) < π¦ β (absβ((πΉβπ§) β (πΉβπ΄))) < π₯)) |
23 | 1, 20, 22 | syl2anc 585 |
1
β’ ((π΄ β β β§ π₯ β β+)
β βπ¦ β
β+ βπ§ β β ((absβ(π§ β π΄)) < π¦ β (absβ((πΉβπ§) β (πΉβπ΄))) < π₯)) |