| Step |
Hyp |
Ref |
Expression |
| 1 |
|
dvdszzq.1 |
|- N = ( A / B ) |
| 2 |
|
dvdszzq.2 |
|- ( ph -> P e. Prime ) |
| 3 |
|
dvdszzq.3 |
|- ( ph -> N e. ZZ ) |
| 4 |
|
dvdszzq.4 |
|- ( ph -> B e. ZZ ) |
| 5 |
|
dvdszzq.5 |
|- ( ph -> B =/= 0 ) |
| 6 |
|
dvdszzq.6 |
|- ( ph -> P || A ) |
| 7 |
|
dvdszzq.7 |
|- ( ph -> -. P || B ) |
| 8 |
3
|
zcnd |
|- ( ph -> N e. CC ) |
| 9 |
4
|
zcnd |
|- ( ph -> B e. CC ) |
| 10 |
|
dvdszrcl |
|- ( P || A -> ( P e. ZZ /\ A e. ZZ ) ) |
| 11 |
10
|
simprd |
|- ( P || A -> A e. ZZ ) |
| 12 |
6 11
|
syl |
|- ( ph -> A e. ZZ ) |
| 13 |
12
|
zcnd |
|- ( ph -> A e. CC ) |
| 14 |
8 9 13 5
|
ldiv |
|- ( ph -> ( ( N x. B ) = A <-> N = ( A / B ) ) ) |
| 15 |
1 14
|
mpbiri |
|- ( ph -> ( N x. B ) = A ) |
| 16 |
6 15
|
breqtrrd |
|- ( ph -> P || ( N x. B ) ) |
| 17 |
|
euclemma |
|- ( ( P e. Prime /\ N e. ZZ /\ B e. ZZ ) -> ( P || ( N x. B ) <-> ( P || N \/ P || B ) ) ) |
| 18 |
17
|
biimpa |
|- ( ( ( P e. Prime /\ N e. ZZ /\ B e. ZZ ) /\ P || ( N x. B ) ) -> ( P || N \/ P || B ) ) |
| 19 |
2 3 4 16 18
|
syl31anc |
|- ( ph -> ( P || N \/ P || B ) ) |
| 20 |
|
orcom |
|- ( ( P || N \/ P || B ) <-> ( P || B \/ P || N ) ) |
| 21 |
|
df-or |
|- ( ( P || B \/ P || N ) <-> ( -. P || B -> P || N ) ) |
| 22 |
20 21
|
sylbb |
|- ( ( P || N \/ P || B ) -> ( -. P || B -> P || N ) ) |
| 23 |
19 7 22
|
sylc |
|- ( ph -> P || N ) |