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

Proof

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

Metamath Proof Explorer

Theorem dirith2

Proof