Step | Hyp | Ref
| Expression |
1 | | isrprm.1 |
. . . 4
β’ π΅ = (Baseβπ
) |
2 | | isrprm.2 |
. . . 4
β’ π = (Unitβπ
) |
3 | | isrprm.3 |
. . . 4
β’ 0 =
(0gβπ
) |
4 | | isrprm.5 |
. . . 4
β’ Β· =
(.rβπ
) |
5 | | isrprm.4 |
. . . 4
β’ β₯ =
(β₯rβπ
) |
6 | 1, 2, 3, 4, 5 | rprmval 32316 |
. . 3
β’ (π
β π β (RPrimeβπ
) = {π β (π΅ β (π βͺ { 0 })) β£ βπ₯ β π΅ βπ¦ β π΅ (π β₯ (π₯ Β· π¦) β (π β₯ π₯ β¨ π β₯ π¦))}) |
7 | 6 | eleq2d 2820 |
. 2
β’ (π
β π β (π β (RPrimeβπ
) β π β {π β (π΅ β (π βͺ { 0 })) β£ βπ₯ β π΅ βπ¦ β π΅ (π β₯ (π₯ Β· π¦) β (π β₯ π₯ β¨ π β₯ π¦))})) |
8 | | breq1 5112 |
. . . . 5
β’ (π = π β (π β₯ (π₯ Β· π¦) β π β₯ (π₯ Β· π¦))) |
9 | | breq1 5112 |
. . . . . 6
β’ (π = π β (π β₯ π₯ β π β₯ π₯)) |
10 | | breq1 5112 |
. . . . . 6
β’ (π = π β (π β₯ π¦ β π β₯ π¦)) |
11 | 9, 10 | orbi12d 918 |
. . . . 5
β’ (π = π β ((π β₯ π₯ β¨ π β₯ π¦) β (π β₯ π₯ β¨ π β₯ π¦))) |
12 | 8, 11 | imbi12d 345 |
. . . 4
β’ (π = π β ((π β₯ (π₯ Β· π¦) β (π β₯ π₯ β¨ π β₯ π¦)) β (π β₯ (π₯ Β· π¦) β (π β₯ π₯ β¨ π β₯ π¦)))) |
13 | 12 | 2ralbidv 3209 |
. . 3
β’ (π = π β (βπ₯ β π΅ βπ¦ β π΅ (π β₯ (π₯ Β· π¦) β (π β₯ π₯ β¨ π β₯ π¦)) β βπ₯ β π΅ βπ¦ β π΅ (π β₯ (π₯ Β· π¦) β (π β₯ π₯ β¨ π β₯ π¦)))) |
14 | 13 | elrab 3649 |
. 2
β’ (π β {π β (π΅ β (π βͺ { 0 })) β£ βπ₯ β π΅ βπ¦ β π΅ (π β₯ (π₯ Β· π¦) β (π β₯ π₯ β¨ π β₯ π¦))} β (π β (π΅ β (π βͺ { 0 })) β§ βπ₯ β π΅ βπ¦ β π΅ (π β₯ (π₯ Β· π¦) β (π β₯ π₯ β¨ π β₯ π¦)))) |
15 | 7, 14 | bitrdi 287 |
1
β’ (π
β π β (π β (RPrimeβπ
) β (π β (π΅ β (π βͺ { 0 })) β§ βπ₯ β π΅ βπ¦ β π΅ (π β₯ (π₯ Β· π¦) β (π β₯ π₯ β¨ π β₯ π¦))))) |