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 ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → { 𝑝 ∈ ℙ ∣ 𝑁 ∥ ( 𝑝𝐴 ) } ≈ ℕ )

Proof

Step Hyp Ref Expression
1 simp1 ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → 𝑁 ∈ ℕ )
2 1 nnnn0d ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → 𝑁 ∈ ℕ0 )
3 2 adantr ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → 𝑁 ∈ ℕ0 )
4 eqid ( ℤ/nℤ ‘ 𝑁 ) = ( ℤ/nℤ ‘ 𝑁 )
5 eqid ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) = ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) )
6 eqid ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) = ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) )
7 4 5 6 znzrhfo ( 𝑁 ∈ ℕ0 → ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) : ℤ –onto→ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
8 fofn ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) : ℤ –onto→ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) → ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) Fn ℤ )
9 3 7 8 3syl ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) Fn ℤ )
10 prmz ( 𝑝 ∈ ℙ → 𝑝 ∈ ℤ )
11 10 adantl ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℤ )
12 fniniseg ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) Fn ℤ → ( 𝑝 ∈ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) “ { ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) } ) ↔ ( 𝑝 ∈ ℤ ∧ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝑝 ) = ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) )
13 12 baibd ( ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) Fn ℤ ∧ 𝑝 ∈ ℤ ) → ( 𝑝 ∈ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) “ { ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) } ) ↔ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝑝 ) = ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) )
14 9 11 13 syl2anc ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∈ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) “ { ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) } ) ↔ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝑝 ) = ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) )
15 simp2 ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → 𝐴 ∈ ℤ )
16 15 adantr ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → 𝐴 ∈ ℤ )
17 4 6 zndvds ( ( 𝑁 ∈ ℕ0𝑝 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝑝 ) = ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ↔ 𝑁 ∥ ( 𝑝𝐴 ) ) )
18 3 11 16 17 syl3anc ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝑝 ) = ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ↔ 𝑁 ∥ ( 𝑝𝐴 ) ) )
19 14 18 bitrd ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∈ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) “ { ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) } ) ↔ 𝑁 ∥ ( 𝑝𝐴 ) ) )
20 19 rabbi2dva ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ( ℙ ∩ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) “ { ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) } ) ) = { 𝑝 ∈ ℙ ∣ 𝑁 ∥ ( 𝑝𝐴 ) } )
21 eqid ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) = ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) )
22 simp3 ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ( 𝐴 gcd 𝑁 ) = 1 )
23 4 21 6 znunit ( ( 𝑁 ∈ ℕ0𝐴 ∈ ℤ ) → ( ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↔ ( 𝐴 gcd 𝑁 ) = 1 ) )
24 2 15 23 syl2anc ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ( ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↔ ( 𝐴 gcd 𝑁 ) = 1 ) )
25 22 24 mpbird ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
26 eqid ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) “ { ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) } ) = ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) “ { ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) } )
27 4 6 1 21 25 26 dirith2 ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ( ℙ ∩ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) “ { ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) } ) ) ≈ ℕ )
28 20 27 eqbrtrrd ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → { 𝑝 ∈ ℙ ∣ 𝑁 ∥ ( 𝑝𝐴 ) } ≈ ℕ )