Step | Hyp | Ref
| Expression |
1 | | simplr 765 |
. . . 4
β’ ((((π΄ β β+
β§ π΅ β
β+) β§ π β β) β§ (0 < π β§ (absβ(π β π΄)) < π΅ β§ (absβ(π β π΄)) < ((denomβπ)β-2))) β π β β) |
2 | | simpr1 1192 |
. . . . 5
β’ ((((π΄ β β+
β§ π΅ β
β+) β§ π β β) β§ (0 < π β§ (absβ(π β π΄)) < π΅ β§ (absβ(π β π΄)) < ((denomβπ)β-2))) β 0 < π) |
3 | | simpr3 1194 |
. . . . 5
β’ ((((π΄ β β+
β§ π΅ β
β+) β§ π β β) β§ (0 < π β§ (absβ(π β π΄)) < π΅ β§ (absβ(π β π΄)) < ((denomβπ)β-2))) β (absβ(π β π΄)) < ((denomβπ)β-2)) |
4 | 2, 3 | jca 510 |
. . . 4
β’ ((((π΄ β β+
β§ π΅ β
β+) β§ π β β) β§ (0 < π β§ (absβ(π β π΄)) < π΅ β§ (absβ(π β π΄)) < ((denomβπ)β-2))) β (0 < π β§ (absβ(π β π΄)) < ((denomβπ)β-2))) |
5 | | breq2 5151 |
. . . . . 6
β’ (π¦ = π β (0 < π¦ β 0 < π)) |
6 | | fvoveq1 7434 |
. . . . . . 7
β’ (π¦ = π β (absβ(π¦ β π΄)) = (absβ(π β π΄))) |
7 | | fveq2 6890 |
. . . . . . . 8
β’ (π¦ = π β (denomβπ¦) = (denomβπ)) |
8 | 7 | oveq1d 7426 |
. . . . . . 7
β’ (π¦ = π β ((denomβπ¦)β-2) = ((denomβπ)β-2)) |
9 | 6, 8 | breq12d 5160 |
. . . . . 6
β’ (π¦ = π β ((absβ(π¦ β π΄)) < ((denomβπ¦)β-2) β (absβ(π β π΄)) < ((denomβπ)β-2))) |
10 | 5, 9 | anbi12d 629 |
. . . . 5
β’ (π¦ = π β ((0 < π¦ β§ (absβ(π¦ β π΄)) < ((denomβπ¦)β-2)) β (0 < π β§ (absβ(π β π΄)) < ((denomβπ)β-2)))) |
11 | 10 | elrab 3682 |
. . . 4
β’ (π β {π¦ β β β£ (0 < π¦ β§ (absβ(π¦ β π΄)) < ((denomβπ¦)β-2))} β (π β β β§ (0 < π β§ (absβ(π β π΄)) < ((denomβπ)β-2)))) |
12 | 1, 4, 11 | sylanbrc 581 |
. . 3
β’ ((((π΄ β β+
β§ π΅ β
β+) β§ π β β) β§ (0 < π β§ (absβ(π β π΄)) < π΅ β§ (absβ(π β π΄)) < ((denomβπ)β-2))) β π β {π¦ β β β£ (0 < π¦ β§ (absβ(π¦ β π΄)) < ((denomβπ¦)β-2))}) |
13 | | simpr2 1193 |
. . 3
β’ ((((π΄ β β+
β§ π΅ β
β+) β§ π β β) β§ (0 < π β§ (absβ(π β π΄)) < π΅ β§ (absβ(π β π΄)) < ((denomβπ)β-2))) β (absβ(π β π΄)) < π΅) |
14 | | fvoveq1 7434 |
. . . . 5
β’ (π₯ = π β (absβ(π₯ β π΄)) = (absβ(π β π΄))) |
15 | 14 | breq1d 5157 |
. . . 4
β’ (π₯ = π β ((absβ(π₯ β π΄)) < π΅ β (absβ(π β π΄)) < π΅)) |
16 | 15 | rspcev 3611 |
. . 3
β’ ((π β {π¦ β β β£ (0 < π¦ β§ (absβ(π¦ β π΄)) < ((denomβπ¦)β-2))} β§ (absβ(π β π΄)) < π΅) β βπ₯ β {π¦ β β β£ (0 < π¦ β§ (absβ(π¦ β π΄)) < ((denomβπ¦)β-2))} (absβ(π₯ β π΄)) < π΅) |
17 | 12, 13, 16 | syl2anc 582 |
. 2
β’ ((((π΄ β β+
β§ π΅ β
β+) β§ π β β) β§ (0 < π β§ (absβ(π β π΄)) < π΅ β§ (absβ(π β π΄)) < ((denomβπ)β-2))) β βπ₯ β {π¦ β β β£ (0 < π¦ β§ (absβ(π¦ β π΄)) < ((denomβπ¦)β-2))} (absβ(π₯ β π΄)) < π΅) |
18 | | irrapxlem5 41866 |
. 2
β’ ((π΄ β β+
β§ π΅ β
β+) β βπ β β (0 < π β§ (absβ(π β π΄)) < π΅ β§ (absβ(π β π΄)) < ((denomβπ)β-2))) |
19 | 17, 18 | r19.29a 3160 |
1
β’ ((π΄ β β+
β§ π΅ β
β+) β βπ₯ β {π¦ β β β£ (0 < π¦ β§ (absβ(π¦ β π΄)) < ((denomβπ¦)β-2))} (absβ(π₯ β π΄)) < π΅) |