Metamath Proof Explorer

Theorem dirith

Description: Dirichlet's theorem: there are infinitely many primes in any arithmetic progression coprime to N . Theorem 9.4.1 of Shapiro, p. 375. See https://metamath-blog.blogspot.com/2016/05/dirichlets-theorem.html for an informal exposition. This is Metamath 100 proof #48. (Contributed by Mario Carneiro, 12-May-2016)

Ref Expression
Assertion dirith 
|- ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> { p e. Prime | N || ( p - A ) } ~~ NN )

Proof

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 )