| Step |
Hyp |
Ref |
Expression |
| 1 |
|
simp1 |
|- ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> N e. NN ) |
| 2 |
1
|
nnnn0d |
|- ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> N e. NN0 ) |
| 3 |
2
|
adantr |
|- ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ p e. Prime ) -> N e. NN0 ) |
| 4 |
|
eqid |
|- ( Z/nZ ` N ) = ( Z/nZ ` N ) |
| 5 |
|
eqid |
|- ( Base ` ( Z/nZ ` N ) ) = ( Base ` ( Z/nZ ` N ) ) |
| 6 |
|
eqid |
|- ( ZRHom ` ( Z/nZ ` N ) ) = ( ZRHom ` ( Z/nZ ` N ) ) |
| 7 |
4 5 6
|
znzrhfo |
|- ( N e. NN0 -> ( ZRHom ` ( Z/nZ ` N ) ) : ZZ -onto-> ( Base ` ( Z/nZ ` N ) ) ) |
| 8 |
|
fofn |
|- ( ( ZRHom ` ( Z/nZ ` N ) ) : ZZ -onto-> ( Base ` ( Z/nZ ` N ) ) -> ( ZRHom ` ( Z/nZ ` N ) ) Fn ZZ ) |
| 9 |
3 7 8
|
3syl |
|- ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ p e. Prime ) -> ( ZRHom ` ( Z/nZ ` N ) ) Fn ZZ ) |
| 10 |
|
prmz |
|- ( p e. Prime -> p e. ZZ ) |
| 11 |
10
|
adantl |
|- ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ p e. Prime ) -> p e. ZZ ) |
| 12 |
|
fniniseg |
|- ( ( ZRHom ` ( Z/nZ ` N ) ) Fn ZZ -> ( p e. ( `' ( ZRHom ` ( Z/nZ ` N ) ) " { ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) } ) <-> ( p e. ZZ /\ ( ( ZRHom ` ( Z/nZ ` N ) ) ` p ) = ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) ) |
| 13 |
12
|
baibd |
|- ( ( ( ZRHom ` ( Z/nZ ` N ) ) Fn ZZ /\ p e. ZZ ) -> ( p e. ( `' ( ZRHom ` ( Z/nZ ` N ) ) " { ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) } ) <-> ( ( ZRHom ` ( Z/nZ ` N ) ) ` p ) = ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) |
| 14 |
9 11 13
|
syl2anc |
|- ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ p e. Prime ) -> ( p e. ( `' ( ZRHom ` ( Z/nZ ` N ) ) " { ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) } ) <-> ( ( ZRHom ` ( Z/nZ ` N ) ) ` p ) = ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) ) ) |
| 15 |
|
simp2 |
|- ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> A e. ZZ ) |
| 16 |
15
|
adantr |
|- ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ p e. Prime ) -> A e. ZZ ) |
| 17 |
4 6
|
zndvds |
|- ( ( N e. NN0 /\ p e. ZZ /\ A e. ZZ ) -> ( ( ( ZRHom ` ( Z/nZ ` N ) ) ` p ) = ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) <-> N || ( p - A ) ) ) |
| 18 |
3 11 16 17
|
syl3anc |
|- ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ p e. Prime ) -> ( ( ( ZRHom ` ( Z/nZ ` N ) ) ` p ) = ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) <-> N || ( p - A ) ) ) |
| 19 |
14 18
|
bitrd |
|- ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ p e. Prime ) -> ( p e. ( `' ( ZRHom ` ( Z/nZ ` N ) ) " { ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) } ) <-> N || ( p - A ) ) ) |
| 20 |
19
|
rabbi2dva |
|- ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> ( Prime i^i ( `' ( ZRHom ` ( Z/nZ ` N ) ) " { ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) } ) ) = { p e. Prime | N || ( p - A ) } ) |
| 21 |
|
eqid |
|- ( Unit ` ( Z/nZ ` N ) ) = ( Unit ` ( Z/nZ ` N ) ) |
| 22 |
|
simp3 |
|- ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> ( A gcd N ) = 1 ) |
| 23 |
4 21 6
|
znunit |
|- ( ( N e. NN0 /\ A e. ZZ ) -> ( ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) e. ( Unit ` ( Z/nZ ` N ) ) <-> ( A gcd N ) = 1 ) ) |
| 24 |
2 15 23
|
syl2anc |
|- ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> ( ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) e. ( Unit ` ( Z/nZ ` N ) ) <-> ( A gcd N ) = 1 ) ) |
| 25 |
22 24
|
mpbird |
|- ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) e. ( Unit ` ( Z/nZ ` N ) ) ) |
| 26 |
|
eqid |
|- ( `' ( ZRHom ` ( Z/nZ ` N ) ) " { ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) } ) = ( `' ( ZRHom ` ( Z/nZ ` N ) ) " { ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) } ) |
| 27 |
4 6 1 21 25 26
|
dirith2 |
|- ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> ( Prime i^i ( `' ( ZRHom ` ( Z/nZ ` N ) ) " { ( ( ZRHom ` ( Z/nZ ` N ) ) ` A ) } ) ) ~~ NN ) |
| 28 |
20 27
|
eqbrtrrd |
|- ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> { p e. Prime | N || ( p - A ) } ~~ NN ) |