chtvalz

Description: Value of the Chebyshev function for integers. (Contributed by Thierry Arnoux, 28-Dec-2021)

		Ref	Expression
	Assertion	chtvalz	$⊢ N \in ℤ \to θ (N) = \sum_{n \in (1 \dots N) \cap ℙ} \log n$

Proof

Step	Hyp	Ref	Expression
1		zre	$⊢ N \in ℤ \to N \in ℝ$
2		chtval	$⊢ N \in ℝ \to θ (N) = \sum_{n \in [0, N] \cap ℙ} \log n$
3	1 2	syl	$⊢ N \in ℤ \to θ (N) = \sum_{n \in [0, N] \cap ℙ} \log n$
4		nnz	$⊢ N \in ℕ \to N \in ℤ$
5		ppisval	$⊢ N \in ℝ \to [0, N] \cap ℙ = (2 \dots ⌊N⌋) \cap ℙ$
6	1 5	syl	$⊢ N \in ℤ \to [0, N] \cap ℙ = (2 \dots ⌊N⌋) \cap ℙ$
7		flid	$⊢ N \in ℤ \to ⌊N⌋ = N$
8	7	oveq2d	$⊢ N \in ℤ \to (2 \dots ⌊N⌋) = (2 \dots N)$
9	8	ineq1d	$⊢ N \in ℤ \to (2 \dots ⌊N⌋) \cap ℙ = (2 \dots N) \cap ℙ$
10	6 9	eqtrd	$⊢ N \in ℤ \to [0, N] \cap ℙ = (2 \dots N) \cap ℙ$
11	4 10	syl	$⊢ N \in ℕ \to [0, N] \cap ℙ = (2 \dots N) \cap ℙ$
12		2nn	$⊢ 2 \in ℕ$
13		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
14	12 13	eleqtri	$⊢ 2 \in ℤ_{\geq 1}$
15		fzss1	$⊢ 2 \in ℤ_{\geq 1} \to (2 \dots N) \subseteq (1 \dots N)$
16	14 15	ax-mp	$⊢ (2 \dots N) \subseteq (1 \dots N)$
17		ssdif0	$⊢ (2 \dots N) \subseteq (1 \dots N) \leftrightarrow (2 \dots N) ∖ (1 \dots N) = \emptyset$
18	16 17	mpbi	$⊢ (2 \dots N) ∖ (1 \dots N) = \emptyset$
19	18	ineq1i	$⊢ ((2 \dots N) ∖ (1 \dots N)) \cap ℙ = \emptyset \cap ℙ$
20		0in	$⊢ \emptyset \cap ℙ = \emptyset$
21	19 20	eqtri	$⊢ ((2 \dots N) ∖ (1 \dots N)) \cap ℙ = \emptyset$
22	21	a1i	$⊢ N \in ℕ \to ((2 \dots N) ∖ (1 \dots N)) \cap ℙ = \emptyset$
23	13	eleq2i	$⊢ N \in ℕ \leftrightarrow N \in ℤ_{\geq 1}$
24		fzpred	$⊢ N \in ℤ_{\geq 1} \to (1 \dots N) = \{1\} \cup (1 + 1 \dots N)$
25	23 24	sylbi	$⊢ N \in ℕ \to (1 \dots N) = \{1\} \cup (1 + 1 \dots N)$
26	25	eqcomd	$⊢ N \in ℕ \to \{1\} \cup (1 + 1 \dots N) = (1 \dots N)$
27		1p1e2	$⊢ 1 + 1 = 2$
28	27	oveq1i	$⊢ (1 + 1 \dots N) = (2 \dots N)$
29	28	a1i	$⊢ N \in ℕ \to (1 + 1 \dots N) = (2 \dots N)$
30	26 29	difeq12d	$⊢ N \in ℕ \to (\{1\} \cup (1 + 1 \dots N)) ∖ (1 + 1 \dots N) = (1 \dots N) ∖ (2 \dots N)$
31		difun2	$⊢ (\{1\} \cup (1 + 1 \dots N)) ∖ (1 + 1 \dots N) = \{1\} ∖ (1 + 1 \dots N)$
32		fzpreddisj	$⊢ N \in ℤ_{\geq 1} \to \{1\} \cap (1 + 1 \dots N) = \emptyset$
33	23 32	sylbi	$⊢ N \in ℕ \to \{1\} \cap (1 + 1 \dots N) = \emptyset$
34		disjdif2	$⊢ \{1\} \cap (1 + 1 \dots N) = \emptyset \to \{1\} ∖ (1 + 1 \dots N) = \{1\}$
35	33 34	syl	$⊢ N \in ℕ \to \{1\} ∖ (1 + 1 \dots N) = \{1\}$
36	31 35	syl5eq	$⊢ N \in ℕ \to (\{1\} \cup (1 + 1 \dots N)) ∖ (1 + 1 \dots N) = \{1\}$
37	30 36	eqtr3d	$⊢ N \in ℕ \to (1 \dots N) ∖ (2 \dots N) = \{1\}$
38	37	ineq1d	$⊢ N \in ℕ \to ((1 \dots N) ∖ (2 \dots N)) \cap ℙ = \{1\} \cap ℙ$
39		incom	$⊢ ℙ \cap \{1\} = \{1\} \cap ℙ$
40		1nprm	$⊢ \neg 1 \in ℙ$
41		disjsn	$⊢ ℙ \cap \{1\} = \emptyset \leftrightarrow \neg 1 \in ℙ$
42	40 41	mpbir	$⊢ ℙ \cap \{1\} = \emptyset$
43	39 42	eqtr3i	$⊢ \{1\} \cap ℙ = \emptyset$
44	38 43	eqtrdi	$⊢ N \in ℕ \to ((1 \dots N) ∖ (2 \dots N)) \cap ℙ = \emptyset$
45		difininv	$⊢ (((2 \dots N) ∖ (1 \dots N)) \cap ℙ = \emptyset \land ((1 \dots N) ∖ (2 \dots N)) \cap ℙ = \emptyset) \to (2 \dots N) \cap ℙ = (1 \dots N) \cap ℙ$
46	22 44 45	syl2anc	$⊢ N \in ℕ \to (2 \dots N) \cap ℙ = (1 \dots N) \cap ℙ$
47	11 46	eqtrd	$⊢ N \in ℕ \to [0, N] \cap ℙ = (1 \dots N) \cap ℙ$
48	47	adantl	$⊢ (N \in ℤ \land N \in ℕ) \to [0, N] \cap ℙ = (1 \dots N) \cap ℙ$
49		znnnlt1	$⊢ N \in ℤ \to (\neg N \in ℕ \leftrightarrow N < 1)$
50	49	biimpa	$⊢ (N \in ℤ \land \neg N \in ℕ) \to N < 1$
51		incom	$⊢ [0, N] \cap ℙ = ℙ \cap [0, N]$
52		isprm3	$⊢ n \in ℙ \leftrightarrow (n \in ℤ_{\geq 2} \land \forall i \in (2 \dots n - 1) \neg i ∥ n)$
53	52	simplbi	$⊢ n \in ℙ \to n \in ℤ_{\geq 2}$
54	53	ssriv	$⊢ ℙ \subseteq ℤ_{\geq 2}$
55	12	nnzi	$⊢ 2 \in ℤ$
56		uzssico	$⊢ 2 \in ℤ \to ℤ_{\geq 2} \subseteq [2, +∞)$
57	55 56	ax-mp	$⊢ ℤ_{\geq 2} \subseteq [2, +∞)$
58	54 57	sstri	$⊢ ℙ \subseteq [2, +∞)$
59		incom	$⊢ [0, N] \cap [2, +∞) = [2, +∞) \cap [0, N]$
60		0xr	$⊢ 0 \in ℝ^{*}$
61	60	a1i	$⊢ (N \in ℤ \land N < 1) \to 0 \in ℝ^{*}$
62	12	nnrei	$⊢ 2 \in ℝ$
63	62	rexri	$⊢ 2 \in ℝ^{*}$
64	63	a1i	$⊢ (N \in ℤ \land N < 1) \to 2 \in ℝ^{*}$
65		0le0	$⊢ 0 \leq 0$
66	65	a1i	$⊢ (N \in ℤ \land N < 1) \to 0 \leq 0$
67	1	adantr	$⊢ (N \in ℤ \land N < 1) \to N \in ℝ$
68		1red	$⊢ (N \in ℤ \land N < 1) \to 1 \in ℝ$
69	62	a1i	$⊢ (N \in ℤ \land N < 1) \to 2 \in ℝ$
70		simpr	$⊢ (N \in ℤ \land N < 1) \to N < 1$
71		1lt2	$⊢ 1 < 2$
72	71	a1i	$⊢ (N \in ℤ \land N < 1) \to 1 < 2$
73	67 68 69 70 72	lttrd	$⊢ (N \in ℤ \land N < 1) \to N < 2$
74		iccssico	$⊢ ((0 \in ℝ^{} \land 2 \in ℝ^{}) \land (0 \leq 0 \land N < 2)) \to [0, N] \subseteq [0, 2)$
75	61 64 66 73 74	syl22anc	$⊢ (N \in ℤ \land N < 1) \to [0, N] \subseteq [0, 2)$
76		pnfxr	$⊢ +∞ \in ℝ^{*}$
77		icodisj	$⊢ (0 \in ℝ^{} \land 2 \in ℝ^{} \land +∞ \in ℝ^{*}) \to [0, 2) \cap [2, +∞) = \emptyset$
78	60 63 76 77	mp3an	$⊢ [0, 2) \cap [2, +∞) = \emptyset$
79		ssdisj	$⊢ ([0, N] \subseteq [0, 2) \land [0, 2) \cap [2, +∞) = \emptyset) \to [0, N] \cap [2, +∞) = \emptyset$
80	75 78 79	sylancl	$⊢ (N \in ℤ \land N < 1) \to [0, N] \cap [2, +∞) = \emptyset$
81	59 80	syl5eqr	$⊢ (N \in ℤ \land N < 1) \to [2, +∞) \cap [0, N] = \emptyset$
82		ssdisj	$⊢ (ℙ \subseteq [2, +∞) \land [2, +∞) \cap [0, N] = \emptyset) \to ℙ \cap [0, N] = \emptyset$
83	58 81 82	sylancr	$⊢ (N \in ℤ \land N < 1) \to ℙ \cap [0, N] = \emptyset$
84	51 83	syl5eq	$⊢ (N \in ℤ \land N < 1) \to [0, N] \cap ℙ = \emptyset$
85		1zzd	$⊢ (N \in ℤ \land N < 1) \to 1 \in ℤ$
86		simpl	$⊢ (N \in ℤ \land N < 1) \to N \in ℤ$
87		fzn	$⊢ (1 \in ℤ \land N \in ℤ) \to (N < 1 \leftrightarrow (1 \dots N) = \emptyset)$
88	87	biimpa	$⊢ ((1 \in ℤ \land N \in ℤ) \land N < 1) \to (1 \dots N) = \emptyset$
89	85 86 70 88	syl21anc	$⊢ (N \in ℤ \land N < 1) \to (1 \dots N) = \emptyset$
90	89	ineq1d	$⊢ (N \in ℤ \land N < 1) \to (1 \dots N) \cap ℙ = \emptyset \cap ℙ$
91	90 20	eqtrdi	$⊢ (N \in ℤ \land N < 1) \to (1 \dots N) \cap ℙ = \emptyset$
92	84 91	eqtr4d	$⊢ (N \in ℤ \land N < 1) \to [0, N] \cap ℙ = (1 \dots N) \cap ℙ$
93	50 92	syldan	$⊢ (N \in ℤ \land \neg N \in ℕ) \to [0, N] \cap ℙ = (1 \dots N) \cap ℙ$
94		exmidd	$⊢ N \in ℤ \to (N \in ℕ \lor \neg N \in ℕ)$
95	48 93 94	mpjaodan	$⊢ N \in ℤ \to [0, N] \cap ℙ = (1 \dots N) \cap ℙ$
96	95	sumeq1d	$⊢ N \in ℤ \to \sum_{n \in [0, N] \cap ℙ} \log n = \sum_{n \in (1 \dots N) \cap ℙ} \log n$
97	3 96	eqtrd	$⊢ N \in ℤ \to θ (N) = \sum_{n \in (1 \dots N) \cap ℙ} \log n$

Metamath Proof Explorer

Theorem chtvalz

Proof