This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dirith2

Description: Dirichlet's theorem: there are infinitely many primes in any arithmetic progression coprime to N . Theorem 9.4.1 of Shapiro, p. 375. (Contributed by Mario Carneiro, 30-Apr-2016) (Proof shortened by Mario Carneiro, 26-May-2016)

Ref Expression
Hypotheses rpvmasum.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
rpvmasum.l ⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
rpvmasum.a ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
rpvmasum.u ⊢ 𝑈 = ( Unit ‘ 𝑍 )
rpvmasum.b ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
rpvmasum.t ⊢ 𝑇 = ( ◡ 𝐿 “ { 𝐴 } )
Assertion dirith2 ( 𝜑 → ( ℙ ∩ 𝑇 ) ≈ ℕ )

Proof

Step Hyp Ref Expression
1 rpvmasum.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
2 rpvmasum.l ⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
3 rpvmasum.a ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4 rpvmasum.u ⊢ 𝑈 = ( Unit ‘ 𝑍 )
5 rpvmasum.b ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
6 rpvmasum.t ⊢ 𝑇 = ( ◡ 𝐿 “ { 𝐴 } )
7 nnex ⊢ ℕ ∈ V
8 inss1 ⊢ ( ℙ ∩ 𝑇 ) ⊆ ℙ
9 prmssnn ⊢ ℙ ⊆ ℕ
10 8 9 sstri ⊢ ( ℙ ∩ 𝑇 ) ⊆ ℕ
11 ssdomg ⊢ ( ℕ ∈ V → ( ( ℙ ∩ 𝑇 ) ⊆ ℕ → ( ℙ ∩ 𝑇 ) ≼ ℕ ) )
12 7 10 11 mp2 ⊢ ( ℙ ∩ 𝑇 ) ≼ ℕ
13 12 a1i ⊢ ( 𝜑 → ( ℙ ∩ 𝑇 ) ≼ ℕ )
14 logno1 ⊢ ¬ ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ∈ 𝑂(1)
15 3 adantr ⊢ ( ( 𝜑 ∧ ( ℙ ∩ 𝑇 ) ∈ Fin ) → 𝑁 ∈ ℕ )
16 15 phicld ⊢ ( ( 𝜑 ∧ ( ℙ ∩ 𝑇 ) ∈ Fin ) → ( ϕ ‘ 𝑁 ) ∈ ℕ )
17 16 nnred ⊢ ( ( 𝜑 ∧ ( ℙ ∩ 𝑇 ) ∈ Fin ) → ( ϕ ‘ 𝑁 ) ∈ ℝ )
18 17 adantr ⊢ ( ( ( 𝜑 ∧ ( ℙ ∩ 𝑇 ) ∈ Fin ) ∧ 𝑥 ∈ ℝ+ ) → ( ϕ ‘ 𝑁 ) ∈ ℝ )
19 simpr ⊢ ( ( 𝜑 ∧ ( ℙ ∩ 𝑇 ) ∈ Fin ) → ( ℙ ∩ 𝑇 ) ∈ Fin )
20 inss2 ⊢ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ⊆ ( ℙ ∩ 𝑇 )
21 ssfi ⊢ ( ( ( ℙ ∩ 𝑇 ) ∈ Fin ∧ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ⊆ ( ℙ ∩ 𝑇 ) ) → ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ∈ Fin )
22 19 20 21 sylancl ⊢ ( ( 𝜑 ∧ ( ℙ ∩ 𝑇 ) ∈ Fin ) → ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ∈ Fin )
23 elinel2 ⊢ ( 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) → 𝑛 ∈ ( ℙ ∩ 𝑇 ) )
24 simpr ⊢ ( ( ( 𝜑 ∧ ( ℙ ∩ 𝑇 ) ∈ Fin ) ∧ 𝑛 ∈ ( ℙ ∩ 𝑇 ) ) → 𝑛 ∈ ( ℙ ∩ 𝑇 ) )
25 10 24 sselid ⊢ ( ( ( 𝜑 ∧ ( ℙ ∩ 𝑇 ) ∈ Fin ) ∧ 𝑛 ∈ ( ℙ ∩ 𝑇 ) ) → 𝑛 ∈ ℕ )
26 25 nnrpd ⊢ ( ( ( 𝜑 ∧ ( ℙ ∩ 𝑇 ) ∈ Fin ) ∧ 𝑛 ∈ ( ℙ ∩ 𝑇 ) ) → 𝑛 ∈ ℝ+ )
27 relogcl ⊢ ( 𝑛 ∈ ℝ+ → ( log ‘ 𝑛 ) ∈ ℝ )
28 26 27 syl ⊢ ( ( ( 𝜑 ∧ ( ℙ ∩ 𝑇 ) ∈ Fin ) ∧ 𝑛 ∈ ( ℙ ∩ 𝑇 ) ) → ( log ‘ 𝑛 ) ∈ ℝ )
29 28 25 nndivred ⊢ ( ( ( 𝜑 ∧ ( ℙ ∩ 𝑇 ) ∈ Fin ) ∧ 𝑛 ∈ ( ℙ ∩ 𝑇 ) ) → ( ( log ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
30 23 29 sylan2 ⊢ ( ( ( 𝜑 ∧ ( ℙ ∩ 𝑇 ) ∈ Fin ) ∧ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ) → ( ( log ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
31 22 30 fsumrecl ⊢ ( ( 𝜑 ∧ ( ℙ ∩ 𝑇 ) ∈ Fin ) → Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ( ( log ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
32 31 adantr ⊢ ( ( ( 𝜑 ∧ ( ℙ ∩ 𝑇 ) ∈ Fin ) ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ( ( log ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
33 rpssre ⊢ ℝ+ ⊆ ℝ
34 17 recnd ⊢ ( ( 𝜑 ∧ ( ℙ ∩ 𝑇 ) ∈ Fin ) → ( ϕ ‘ 𝑁 ) ∈ ℂ )
35 o1const ⊢ ( ( ℝ+ ⊆ ℝ ∧ ( ϕ ‘ 𝑁 ) ∈ ℂ ) → ( 𝑥 ∈ ℝ+ ↦ ( ϕ ‘ 𝑁 ) ) ∈ 𝑂(1) )
36 33 34 35 sylancr ⊢ ( ( 𝜑 ∧ ( ℙ ∩ 𝑇 ) ∈ Fin ) → ( 𝑥 ∈ ℝ+ ↦ ( ϕ ‘ 𝑁 ) ) ∈ 𝑂(1) )
37 33 a1i ⊢ ( ( 𝜑 ∧ ( ℙ ∩ 𝑇 ) ∈ Fin ) → ℝ+ ⊆ ℝ )
38 1red ⊢ ( ( 𝜑 ∧ ( ℙ ∩ 𝑇 ) ∈ Fin ) → 1 ∈ ℝ )
39 19 29 fsumrecl ⊢ ( ( 𝜑 ∧ ( ℙ ∩ 𝑇 ) ∈ Fin ) → Σ 𝑛 ∈ ( ℙ ∩ 𝑇 ) ( ( log ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
40 log1 ⊢ ( log ‘ 1 ) = 0
41 25 nnge1d ⊢ ( ( ( 𝜑 ∧ ( ℙ ∩ 𝑇 ) ∈ Fin ) ∧ 𝑛 ∈ ( ℙ ∩ 𝑇 ) ) → 1 ≤ 𝑛 )
42 1rp ⊢ 1 ∈ ℝ+
43 logleb ⊢ ( ( 1 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) → ( 1 ≤ 𝑛 ↔ ( log ‘ 1 ) ≤ ( log ‘ 𝑛 ) ) )
44 42 26 43 sylancr ⊢ ( ( ( 𝜑 ∧ ( ℙ ∩ 𝑇 ) ∈ Fin ) ∧ 𝑛 ∈ ( ℙ ∩ 𝑇 ) ) → ( 1 ≤ 𝑛 ↔ ( log ‘ 1 ) ≤ ( log ‘ 𝑛 ) ) )
45 41 44 mpbid ⊢ ( ( ( 𝜑 ∧ ( ℙ ∩ 𝑇 ) ∈ Fin ) ∧ 𝑛 ∈ ( ℙ ∩ 𝑇 ) ) → ( log ‘ 1 ) ≤ ( log ‘ 𝑛 ) )
46 40 45 eqbrtrrid ⊢ ( ( ( 𝜑 ∧ ( ℙ ∩ 𝑇 ) ∈ Fin ) ∧ 𝑛 ∈ ( ℙ ∩ 𝑇 ) ) → 0 ≤ ( log ‘ 𝑛 ) )
47 28 26 46 divge0d ⊢ ( ( ( 𝜑 ∧ ( ℙ ∩ 𝑇 ) ∈ Fin ) ∧ 𝑛 ∈ ( ℙ ∩ 𝑇 ) ) → 0 ≤ ( ( log ‘ 𝑛 ) / 𝑛 ) )
48 20 a1i ⊢ ( ( 𝜑 ∧ ( ℙ ∩ 𝑇 ) ∈ Fin ) → ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ⊆ ( ℙ ∩ 𝑇 ) )
49 19 29 47 48 fsumless ⊢ ( ( 𝜑 ∧ ( ℙ ∩ 𝑇 ) ∈ Fin ) → Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ( ( log ‘ 𝑛 ) / 𝑛 ) ≤ Σ 𝑛 ∈ ( ℙ ∩ 𝑇 ) ( ( log ‘ 𝑛 ) / 𝑛 ) )
50 49 adantr ⊢ ( ( ( 𝜑 ∧ ( ℙ ∩ 𝑇 ) ∈ Fin ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ( ( log ‘ 𝑛 ) / 𝑛 ) ≤ Σ 𝑛 ∈ ( ℙ ∩ 𝑇 ) ( ( log ‘ 𝑛 ) / 𝑛 ) )
51 37 32 38 39 50 ello1d ⊢ ( ( 𝜑 ∧ ( ℙ ∩ 𝑇 ) ∈ Fin ) → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ( ( log ‘ 𝑛 ) / 𝑛 ) ) ∈ ≤𝑂(1) )
52 0red ⊢ ( ( 𝜑 ∧ ( ℙ ∩ 𝑇 ) ∈ Fin ) → 0 ∈ ℝ )
53 23 47 sylan2 ⊢ ( ( ( 𝜑 ∧ ( ℙ ∩ 𝑇 ) ∈ Fin ) ∧ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ) → 0 ≤ ( ( log ‘ 𝑛 ) / 𝑛 ) )
54 22 30 53 fsumge0 ⊢ ( ( 𝜑 ∧ ( ℙ ∩ 𝑇 ) ∈ Fin ) → 0 ≤ Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ( ( log ‘ 𝑛 ) / 𝑛 ) )
55 54 adantr ⊢ ( ( ( 𝜑 ∧ ( ℙ ∩ 𝑇 ) ∈ Fin ) ∧ 𝑥 ∈ ℝ+ ) → 0 ≤ Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ( ( log ‘ 𝑛 ) / 𝑛 ) )
56 32 52 55 o1lo12 ⊢ ( ( 𝜑 ∧ ( ℙ ∩ 𝑇 ) ∈ Fin ) → ( ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ( ( log ‘ 𝑛 ) / 𝑛 ) ) ∈ 𝑂(1) ↔ ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ( ( log ‘ 𝑛 ) / 𝑛 ) ) ∈ ≤𝑂(1) ) )
57 51 56 mpbird ⊢ ( ( 𝜑 ∧ ( ℙ ∩ 𝑇 ) ∈ Fin ) → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ( ( log ‘ 𝑛 ) / 𝑛 ) ) ∈ 𝑂(1) )
58 18 32 36 57 o1mul2 ⊢ ( ( 𝜑 ∧ ( ℙ ∩ 𝑇 ) ∈ Fin ) → ( 𝑥 ∈ ℝ+ ↦ ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ( ( log ‘ 𝑛 ) / 𝑛 ) ) ) ∈ 𝑂(1) )
59 17 31 remulcld ⊢ ( ( 𝜑 ∧ ( ℙ ∩ 𝑇 ) ∈ Fin ) → ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ( ( log ‘ 𝑛 ) / 𝑛 ) ) ∈ ℝ )
60 59 recnd ⊢ ( ( 𝜑 ∧ ( ℙ ∩ 𝑇 ) ∈ Fin ) → ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ( ( log ‘ 𝑛 ) / 𝑛 ) ) ∈ ℂ )
61 60 adantr ⊢ ( ( ( 𝜑 ∧ ( ℙ ∩ 𝑇 ) ∈ Fin ) ∧ 𝑥 ∈ ℝ+ ) → ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ( ( log ‘ 𝑛 ) / 𝑛 ) ) ∈ ℂ )
62 relogcl ⊢ ( 𝑥 ∈ ℝ+ → ( log ‘ 𝑥 ) ∈ ℝ )
63 62 adantl ⊢ ( ( ( 𝜑 ∧ ( ℙ ∩ 𝑇 ) ∈ Fin ) ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ 𝑥 ) ∈ ℝ )
64 63 recnd ⊢ ( ( ( 𝜑 ∧ ( ℙ ∩ 𝑇 ) ∈ Fin ) ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ 𝑥 ) ∈ ℂ )
65 1 2 3 4 5 6 rplogsum ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ( ( log ‘ 𝑛 ) / 𝑛 ) ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) )
66 65 adantr ⊢ ( ( 𝜑 ∧ ( ℙ ∩ 𝑇 ) ∈ Fin ) → ( 𝑥 ∈ ℝ+ ↦ ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ( ( log ‘ 𝑛 ) / 𝑛 ) ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) )
67 61 64 66 o1dif ⊢ ( ( 𝜑 ∧ ( ℙ ∩ 𝑇 ) ∈ Fin ) → ( ( 𝑥 ∈ ℝ+ ↦ ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ( ( log ‘ 𝑛 ) / 𝑛 ) ) ) ∈ 𝑂(1) ↔ ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ∈ 𝑂(1) ) )
68 58 67 mpbid ⊢ ( ( 𝜑 ∧ ( ℙ ∩ 𝑇 ) ∈ Fin ) → ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ∈ 𝑂(1) )
69 68 ex ⊢ ( 𝜑 → ( ( ℙ ∩ 𝑇 ) ∈ Fin → ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ∈ 𝑂(1) ) )
70 14 69 mtoi ⊢ ( 𝜑 → ¬ ( ℙ ∩ 𝑇 ) ∈ Fin )
71 nnenom ⊢ ℕ ≈ ω
72 sdomentr ⊢ ( ( ( ℙ ∩ 𝑇 ) ≺ ℕ ∧ ℕ ≈ ω ) → ( ℙ ∩ 𝑇 ) ≺ ω )
73 71 72 mpan2 ⊢ ( ( ℙ ∩ 𝑇 ) ≺ ℕ → ( ℙ ∩ 𝑇 ) ≺ ω )
74 isfinite2 ⊢ ( ( ℙ ∩ 𝑇 ) ≺ ω → ( ℙ ∩ 𝑇 ) ∈ Fin )
75 73 74 syl ⊢ ( ( ℙ ∩ 𝑇 ) ≺ ℕ → ( ℙ ∩ 𝑇 ) ∈ Fin )
76 70 75 nsyl ⊢ ( 𝜑 → ¬ ( ℙ ∩ 𝑇 ) ≺ ℕ )
77 bren2 ⊢ ( ( ℙ ∩ 𝑇 ) ≈ ℕ ↔ ( ( ℙ ∩ 𝑇 ) ≼ ℕ ∧ ¬ ( ℙ ∩ 𝑇 ) ≺ ℕ ) )
78 13 76 77 sylanbrc ⊢ ( 𝜑 → ( ℙ ∩ 𝑇 ) ≈ ℕ )