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	⊢ ( 𝜑 → ( ℙ ∩ 𝑇 ) ≈ ℕ )