# 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 ${⊢}{Z}=ℤ/{N}ℤ$
rpvmasum.l ${⊢}{L}=\mathrm{ℤRHom}\left({Z}\right)$
rpvmasum.a ${⊢}{\phi }\to {N}\in ℕ$
rpvmasum.u ${⊢}{U}=\mathrm{Unit}\left({Z}\right)$
rpvmasum.b ${⊢}{\phi }\to {A}\in {U}$
rpvmasum.t ${⊢}{T}={{L}}^{-1}\left[\left\{{A}\right\}\right]$
Assertion dirith2 ${⊢}{\phi }\to \left(ℙ\cap {T}\right)\approx ℕ$

### Proof

Step Hyp Ref Expression
1 rpvmasum.z ${⊢}{Z}=ℤ/{N}ℤ$
2 rpvmasum.l ${⊢}{L}=\mathrm{ℤRHom}\left({Z}\right)$
3 rpvmasum.a ${⊢}{\phi }\to {N}\in ℕ$
4 rpvmasum.u ${⊢}{U}=\mathrm{Unit}\left({Z}\right)$
5 rpvmasum.b ${⊢}{\phi }\to {A}\in {U}$
6 rpvmasum.t ${⊢}{T}={{L}}^{-1}\left[\left\{{A}\right\}\right]$
7 nnex ${⊢}ℕ\in \mathrm{V}$
8 inss1 ${⊢}ℙ\cap {T}\subseteq ℙ$
9 prmssnn ${⊢}ℙ\subseteq ℕ$
10 8 9 sstri ${⊢}ℙ\cap {T}\subseteq ℕ$
11 ssdomg ${⊢}ℕ\in \mathrm{V}\to \left(ℙ\cap {T}\subseteq ℕ\to \left(ℙ\cap {T}\right)\preccurlyeq ℕ\right)$
12 7 10 11 mp2 ${⊢}\left(ℙ\cap {T}\right)\preccurlyeq ℕ$
13 12 a1i ${⊢}{\phi }\to \left(ℙ\cap {T}\right)\preccurlyeq ℕ$
14 logno1 ${⊢}¬\left({x}\in {ℝ}^{+}⟼\mathrm{log}{x}\right)\in 𝑂\left(1\right)$
15 3 adantr ${⊢}\left({\phi }\wedge ℙ\cap {T}\in \mathrm{Fin}\right)\to {N}\in ℕ$
16 15 phicld ${⊢}\left({\phi }\wedge ℙ\cap {T}\in \mathrm{Fin}\right)\to \mathrm{\varphi }\left({N}\right)\in ℕ$
17 16 nnred ${⊢}\left({\phi }\wedge ℙ\cap {T}\in \mathrm{Fin}\right)\to \mathrm{\varphi }\left({N}\right)\in ℝ$
18 17 adantr ${⊢}\left(\left({\phi }\wedge ℙ\cap {T}\in \mathrm{Fin}\right)\wedge {x}\in {ℝ}^{+}\right)\to \mathrm{\varphi }\left({N}\right)\in ℝ$
19 simpr ${⊢}\left({\phi }\wedge ℙ\cap {T}\in \mathrm{Fin}\right)\to ℙ\cap {T}\in \mathrm{Fin}$
20 inss2 ${⊢}\left(1\dots ⌊{x}⌋\right)\cap \left(ℙ\cap {T}\right)\subseteq ℙ\cap {T}$
21 ssfi ${⊢}\left(ℙ\cap {T}\in \mathrm{Fin}\wedge \left(1\dots ⌊{x}⌋\right)\cap \left(ℙ\cap {T}\right)\subseteq ℙ\cap {T}\right)\to \left(1\dots ⌊{x}⌋\right)\cap \left(ℙ\cap {T}\right)\in \mathrm{Fin}$
22 19 20 21 sylancl ${⊢}\left({\phi }\wedge ℙ\cap {T}\in \mathrm{Fin}\right)\to \left(1\dots ⌊{x}⌋\right)\cap \left(ℙ\cap {T}\right)\in \mathrm{Fin}$
23 elinel2 ${⊢}{n}\in \left(\left(1\dots ⌊{x}⌋\right)\cap \left(ℙ\cap {T}\right)\right)\to {n}\in \left(ℙ\cap {T}\right)$
24 simpr ${⊢}\left(\left({\phi }\wedge ℙ\cap {T}\in \mathrm{Fin}\right)\wedge {n}\in \left(ℙ\cap {T}\right)\right)\to {n}\in \left(ℙ\cap {T}\right)$
25 10 24 sseldi ${⊢}\left(\left({\phi }\wedge ℙ\cap {T}\in \mathrm{Fin}\right)\wedge {n}\in \left(ℙ\cap {T}\right)\right)\to {n}\in ℕ$
26 25 nnrpd ${⊢}\left(\left({\phi }\wedge ℙ\cap {T}\in \mathrm{Fin}\right)\wedge {n}\in \left(ℙ\cap {T}\right)\right)\to {n}\in {ℝ}^{+}$
27 relogcl ${⊢}{n}\in {ℝ}^{+}\to \mathrm{log}{n}\in ℝ$
28 26 27 syl ${⊢}\left(\left({\phi }\wedge ℙ\cap {T}\in \mathrm{Fin}\right)\wedge {n}\in \left(ℙ\cap {T}\right)\right)\to \mathrm{log}{n}\in ℝ$
29 28 25 nndivred ${⊢}\left(\left({\phi }\wedge ℙ\cap {T}\in \mathrm{Fin}\right)\wedge {n}\in \left(ℙ\cap {T}\right)\right)\to \frac{\mathrm{log}{n}}{{n}}\in ℝ$
30 23 29 sylan2 ${⊢}\left(\left({\phi }\wedge ℙ\cap {T}\in \mathrm{Fin}\right)\wedge {n}\in \left(\left(1\dots ⌊{x}⌋\right)\cap \left(ℙ\cap {T}\right)\right)\right)\to \frac{\mathrm{log}{n}}{{n}}\in ℝ$
31 22 30 fsumrecl ${⊢}\left({\phi }\wedge ℙ\cap {T}\in \mathrm{Fin}\right)\to \sum _{{n}\in \left(1\dots ⌊{x}⌋\right)\cap \left(ℙ\cap {T}\right)}\left(\frac{\mathrm{log}{n}}{{n}}\right)\in ℝ$
32 31 adantr ${⊢}\left(\left({\phi }\wedge ℙ\cap {T}\in \mathrm{Fin}\right)\wedge {x}\in {ℝ}^{+}\right)\to \sum _{{n}\in \left(1\dots ⌊{x}⌋\right)\cap \left(ℙ\cap {T}\right)}\left(\frac{\mathrm{log}{n}}{{n}}\right)\in ℝ$
33 rpssre ${⊢}{ℝ}^{+}\subseteq ℝ$
34 17 recnd ${⊢}\left({\phi }\wedge ℙ\cap {T}\in \mathrm{Fin}\right)\to \mathrm{\varphi }\left({N}\right)\in ℂ$
35 o1const ${⊢}\left({ℝ}^{+}\subseteq ℝ\wedge \mathrm{\varphi }\left({N}\right)\in ℂ\right)\to \left({x}\in {ℝ}^{+}⟼\mathrm{\varphi }\left({N}\right)\right)\in 𝑂\left(1\right)$
36 33 34 35 sylancr ${⊢}\left({\phi }\wedge ℙ\cap {T}\in \mathrm{Fin}\right)\to \left({x}\in {ℝ}^{+}⟼\mathrm{\varphi }\left({N}\right)\right)\in 𝑂\left(1\right)$
37 33 a1i ${⊢}\left({\phi }\wedge ℙ\cap {T}\in \mathrm{Fin}\right)\to {ℝ}^{+}\subseteq ℝ$
38 1red ${⊢}\left({\phi }\wedge ℙ\cap {T}\in \mathrm{Fin}\right)\to 1\in ℝ$
39 19 29 fsumrecl ${⊢}\left({\phi }\wedge ℙ\cap {T}\in \mathrm{Fin}\right)\to \sum _{{n}\in ℙ\cap {T}}\left(\frac{\mathrm{log}{n}}{{n}}\right)\in ℝ$
40 log1 ${⊢}\mathrm{log}1=0$
41 25 nnge1d ${⊢}\left(\left({\phi }\wedge ℙ\cap {T}\in \mathrm{Fin}\right)\wedge {n}\in \left(ℙ\cap {T}\right)\right)\to 1\le {n}$
42 1rp ${⊢}1\in {ℝ}^{+}$
43 logleb ${⊢}\left(1\in {ℝ}^{+}\wedge {n}\in {ℝ}^{+}\right)\to \left(1\le {n}↔\mathrm{log}1\le \mathrm{log}{n}\right)$
44 42 26 43 sylancr ${⊢}\left(\left({\phi }\wedge ℙ\cap {T}\in \mathrm{Fin}\right)\wedge {n}\in \left(ℙ\cap {T}\right)\right)\to \left(1\le {n}↔\mathrm{log}1\le \mathrm{log}{n}\right)$
45 41 44 mpbid ${⊢}\left(\left({\phi }\wedge ℙ\cap {T}\in \mathrm{Fin}\right)\wedge {n}\in \left(ℙ\cap {T}\right)\right)\to \mathrm{log}1\le \mathrm{log}{n}$
46 40 45 eqbrtrrid ${⊢}\left(\left({\phi }\wedge ℙ\cap {T}\in \mathrm{Fin}\right)\wedge {n}\in \left(ℙ\cap {T}\right)\right)\to 0\le \mathrm{log}{n}$
47 28 26 46 divge0d ${⊢}\left(\left({\phi }\wedge ℙ\cap {T}\in \mathrm{Fin}\right)\wedge {n}\in \left(ℙ\cap {T}\right)\right)\to 0\le \frac{\mathrm{log}{n}}{{n}}$
48 20 a1i ${⊢}\left({\phi }\wedge ℙ\cap {T}\in \mathrm{Fin}\right)\to \left(1\dots ⌊{x}⌋\right)\cap \left(ℙ\cap {T}\right)\subseteq ℙ\cap {T}$
49 19 29 47 48 fsumless ${⊢}\left({\phi }\wedge ℙ\cap {T}\in \mathrm{Fin}\right)\to \sum _{{n}\in \left(1\dots ⌊{x}⌋\right)\cap \left(ℙ\cap {T}\right)}\left(\frac{\mathrm{log}{n}}{{n}}\right)\le \sum _{{n}\in ℙ\cap {T}}\left(\frac{\mathrm{log}{n}}{{n}}\right)$
50 49 adantr ${⊢}\left(\left({\phi }\wedge ℙ\cap {T}\in \mathrm{Fin}\right)\wedge \left({x}\in {ℝ}^{+}\wedge 1\le {x}\right)\right)\to \sum _{{n}\in \left(1\dots ⌊{x}⌋\right)\cap \left(ℙ\cap {T}\right)}\left(\frac{\mathrm{log}{n}}{{n}}\right)\le \sum _{{n}\in ℙ\cap {T}}\left(\frac{\mathrm{log}{n}}{{n}}\right)$
51 37 32 38 39 50 ello1d ${⊢}\left({\phi }\wedge ℙ\cap {T}\in \mathrm{Fin}\right)\to \left({x}\in {ℝ}^{+}⟼\sum _{{n}\in \left(1\dots ⌊{x}⌋\right)\cap \left(ℙ\cap {T}\right)}\left(\frac{\mathrm{log}{n}}{{n}}\right)\right)\in \le 𝑂\left(1\right)$
52 0red ${⊢}\left({\phi }\wedge ℙ\cap {T}\in \mathrm{Fin}\right)\to 0\in ℝ$
53 23 47 sylan2 ${⊢}\left(\left({\phi }\wedge ℙ\cap {T}\in \mathrm{Fin}\right)\wedge {n}\in \left(\left(1\dots ⌊{x}⌋\right)\cap \left(ℙ\cap {T}\right)\right)\right)\to 0\le \frac{\mathrm{log}{n}}{{n}}$
54 22 30 53 fsumge0 ${⊢}\left({\phi }\wedge ℙ\cap {T}\in \mathrm{Fin}\right)\to 0\le \sum _{{n}\in \left(1\dots ⌊{x}⌋\right)\cap \left(ℙ\cap {T}\right)}\left(\frac{\mathrm{log}{n}}{{n}}\right)$
55 54 adantr ${⊢}\left(\left({\phi }\wedge ℙ\cap {T}\in \mathrm{Fin}\right)\wedge {x}\in {ℝ}^{+}\right)\to 0\le \sum _{{n}\in \left(1\dots ⌊{x}⌋\right)\cap \left(ℙ\cap {T}\right)}\left(\frac{\mathrm{log}{n}}{{n}}\right)$
56 32 52 55 o1lo12 ${⊢}\left({\phi }\wedge ℙ\cap {T}\in \mathrm{Fin}\right)\to \left(\left({x}\in {ℝ}^{+}⟼\sum _{{n}\in \left(1\dots ⌊{x}⌋\right)\cap \left(ℙ\cap {T}\right)}\left(\frac{\mathrm{log}{n}}{{n}}\right)\right)\in 𝑂\left(1\right)↔\left({x}\in {ℝ}^{+}⟼\sum _{{n}\in \left(1\dots ⌊{x}⌋\right)\cap \left(ℙ\cap {T}\right)}\left(\frac{\mathrm{log}{n}}{{n}}\right)\right)\in \le 𝑂\left(1\right)\right)$
57 51 56 mpbird ${⊢}\left({\phi }\wedge ℙ\cap {T}\in \mathrm{Fin}\right)\to \left({x}\in {ℝ}^{+}⟼\sum _{{n}\in \left(1\dots ⌊{x}⌋\right)\cap \left(ℙ\cap {T}\right)}\left(\frac{\mathrm{log}{n}}{{n}}\right)\right)\in 𝑂\left(1\right)$
58 18 32 36 57 o1mul2 ${⊢}\left({\phi }\wedge ℙ\cap {T}\in \mathrm{Fin}\right)\to \left({x}\in {ℝ}^{+}⟼\mathrm{\varphi }\left({N}\right)\sum _{{n}\in \left(1\dots ⌊{x}⌋\right)\cap \left(ℙ\cap {T}\right)}\left(\frac{\mathrm{log}{n}}{{n}}\right)\right)\in 𝑂\left(1\right)$
59 17 31 remulcld ${⊢}\left({\phi }\wedge ℙ\cap {T}\in \mathrm{Fin}\right)\to \mathrm{\varphi }\left({N}\right)\sum _{{n}\in \left(1\dots ⌊{x}⌋\right)\cap \left(ℙ\cap {T}\right)}\left(\frac{\mathrm{log}{n}}{{n}}\right)\in ℝ$
60 59 recnd ${⊢}\left({\phi }\wedge ℙ\cap {T}\in \mathrm{Fin}\right)\to \mathrm{\varphi }\left({N}\right)\sum _{{n}\in \left(1\dots ⌊{x}⌋\right)\cap \left(ℙ\cap {T}\right)}\left(\frac{\mathrm{log}{n}}{{n}}\right)\in ℂ$
61 60 adantr ${⊢}\left(\left({\phi }\wedge ℙ\cap {T}\in \mathrm{Fin}\right)\wedge {x}\in {ℝ}^{+}\right)\to \mathrm{\varphi }\left({N}\right)\sum _{{n}\in \left(1\dots ⌊{x}⌋\right)\cap \left(ℙ\cap {T}\right)}\left(\frac{\mathrm{log}{n}}{{n}}\right)\in ℂ$
62 relogcl ${⊢}{x}\in {ℝ}^{+}\to \mathrm{log}{x}\in ℝ$
63 62 adantl ${⊢}\left(\left({\phi }\wedge ℙ\cap {T}\in \mathrm{Fin}\right)\wedge {x}\in {ℝ}^{+}\right)\to \mathrm{log}{x}\in ℝ$
64 63 recnd ${⊢}\left(\left({\phi }\wedge ℙ\cap {T}\in \mathrm{Fin}\right)\wedge {x}\in {ℝ}^{+}\right)\to \mathrm{log}{x}\in ℂ$
65 1 2 3 4 5 6 rplogsum ${⊢}{\phi }\to \left({x}\in {ℝ}^{+}⟼\mathrm{\varphi }\left({N}\right)\sum _{{n}\in \left(1\dots ⌊{x}⌋\right)\cap \left(ℙ\cap {T}\right)}\left(\frac{\mathrm{log}{n}}{{n}}\right)-\mathrm{log}{x}\right)\in 𝑂\left(1\right)$
66 65 adantr ${⊢}\left({\phi }\wedge ℙ\cap {T}\in \mathrm{Fin}\right)\to \left({x}\in {ℝ}^{+}⟼\mathrm{\varphi }\left({N}\right)\sum _{{n}\in \left(1\dots ⌊{x}⌋\right)\cap \left(ℙ\cap {T}\right)}\left(\frac{\mathrm{log}{n}}{{n}}\right)-\mathrm{log}{x}\right)\in 𝑂\left(1\right)$
67 61 64 66 o1dif ${⊢}\left({\phi }\wedge ℙ\cap {T}\in \mathrm{Fin}\right)\to \left(\left({x}\in {ℝ}^{+}⟼\mathrm{\varphi }\left({N}\right)\sum _{{n}\in \left(1\dots ⌊{x}⌋\right)\cap \left(ℙ\cap {T}\right)}\left(\frac{\mathrm{log}{n}}{{n}}\right)\right)\in 𝑂\left(1\right)↔\left({x}\in {ℝ}^{+}⟼\mathrm{log}{x}\right)\in 𝑂\left(1\right)\right)$
68 58 67 mpbid ${⊢}\left({\phi }\wedge ℙ\cap {T}\in \mathrm{Fin}\right)\to \left({x}\in {ℝ}^{+}⟼\mathrm{log}{x}\right)\in 𝑂\left(1\right)$
69 68 ex ${⊢}{\phi }\to \left(ℙ\cap {T}\in \mathrm{Fin}\to \left({x}\in {ℝ}^{+}⟼\mathrm{log}{x}\right)\in 𝑂\left(1\right)\right)$
70 14 69 mtoi ${⊢}{\phi }\to ¬ℙ\cap {T}\in \mathrm{Fin}$
71 nnenom ${⊢}ℕ\approx \mathrm{\omega }$
72 sdomentr ${⊢}\left(\left(ℙ\cap {T}\right)\prec ℕ\wedge ℕ\approx \mathrm{\omega }\right)\to \left(ℙ\cap {T}\right)\prec \mathrm{\omega }$
73 71 72 mpan2 ${⊢}\left(ℙ\cap {T}\right)\prec ℕ\to \left(ℙ\cap {T}\right)\prec \mathrm{\omega }$
74 isfinite2 ${⊢}\left(ℙ\cap {T}\right)\prec \mathrm{\omega }\to ℙ\cap {T}\in \mathrm{Fin}$
75 73 74 syl ${⊢}\left(ℙ\cap {T}\right)\prec ℕ\to ℙ\cap {T}\in \mathrm{Fin}$
76 70 75 nsyl ${⊢}{\phi }\to ¬\left(ℙ\cap {T}\right)\prec ℕ$
77 bren2 ${⊢}\left(ℙ\cap {T}\right)\approx ℕ↔\left(\left(ℙ\cap {T}\right)\preccurlyeq ℕ\wedge ¬\left(ℙ\cap {T}\right)\prec ℕ\right)$
78 13 76 77 sylanbrc ${⊢}{\phi }\to \left(ℙ\cap {T}\right)\approx ℕ$