Step |
Hyp |
Ref |
Expression |
1 |
|
prmz |
|- ( P e. Prime -> P e. ZZ ) |
2 |
|
lgsne0 |
|- ( ( A e. ZZ /\ P e. ZZ ) -> ( ( A /L P ) =/= 0 <-> ( A gcd P ) = 1 ) ) |
3 |
1 2
|
sylan2 |
|- ( ( A e. ZZ /\ P e. Prime ) -> ( ( A /L P ) =/= 0 <-> ( A gcd P ) = 1 ) ) |
4 |
|
coprm |
|- ( ( P e. Prime /\ A e. ZZ ) -> ( -. P || A <-> ( P gcd A ) = 1 ) ) |
5 |
4
|
ancoms |
|- ( ( A e. ZZ /\ P e. Prime ) -> ( -. P || A <-> ( P gcd A ) = 1 ) ) |
6 |
1
|
anim1i |
|- ( ( P e. Prime /\ A e. ZZ ) -> ( P e. ZZ /\ A e. ZZ ) ) |
7 |
6
|
ancoms |
|- ( ( A e. ZZ /\ P e. Prime ) -> ( P e. ZZ /\ A e. ZZ ) ) |
8 |
|
gcdcom |
|- ( ( P e. ZZ /\ A e. ZZ ) -> ( P gcd A ) = ( A gcd P ) ) |
9 |
7 8
|
syl |
|- ( ( A e. ZZ /\ P e. Prime ) -> ( P gcd A ) = ( A gcd P ) ) |
10 |
9
|
eqeq1d |
|- ( ( A e. ZZ /\ P e. Prime ) -> ( ( P gcd A ) = 1 <-> ( A gcd P ) = 1 ) ) |
11 |
5 10
|
bitr2d |
|- ( ( A e. ZZ /\ P e. Prime ) -> ( ( A gcd P ) = 1 <-> -. P || A ) ) |
12 |
|
prmnn |
|- ( P e. Prime -> P e. NN ) |
13 |
|
dvdsval3 |
|- ( ( P e. NN /\ A e. ZZ ) -> ( P || A <-> ( A mod P ) = 0 ) ) |
14 |
12 13
|
sylan |
|- ( ( P e. Prime /\ A e. ZZ ) -> ( P || A <-> ( A mod P ) = 0 ) ) |
15 |
14
|
ancoms |
|- ( ( A e. ZZ /\ P e. Prime ) -> ( P || A <-> ( A mod P ) = 0 ) ) |
16 |
15
|
notbid |
|- ( ( A e. ZZ /\ P e. Prime ) -> ( -. P || A <-> -. ( A mod P ) = 0 ) ) |
17 |
3 11 16
|
3bitrd |
|- ( ( A e. ZZ /\ P e. Prime ) -> ( ( A /L P ) =/= 0 <-> -. ( A mod P ) = 0 ) ) |
18 |
17
|
necon4abid |
|- ( ( A e. ZZ /\ P e. Prime ) -> ( ( A /L P ) = 0 <-> ( A mod P ) = 0 ) ) |