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 ) → { 𝑝 ∈ ℙ ∣ 𝑁 ∥ ( 𝑝 − 𝐴 ) } ≈ ℕ )