chpval2

Description: Express the second Chebyshev function directly as a sum over the primes less than A (instead of indirectly through the von Mangoldt function). (Contributed by Mario Carneiro, 8-Apr-2016)

		Ref	Expression
	Assertion	chpval2	$⊢ A \in ℝ \to ψ (A) = \sum_{p \in [0, A] \cap ℙ} \log p ⌊\frac{\log A}{\log p}⌋$

Proof

Step	Hyp	Ref	Expression
1		chpval	$⊢ A \in ℝ \to ψ (A) = \sum_{n = 1}^{⌊A⌋} Λ (n)$
2		fveq2	$⊢ n = p^{k} \to Λ (n) = Λ (p^{k})$
3		id	$⊢ A \in ℝ \to A \in ℝ$
4		elfznn	$⊢ n \in (1 \dots ⌊A⌋) \to n \in ℕ$
5	4	adantl	$⊢ (A \in ℝ \land n \in (1 \dots ⌊A⌋)) \to n \in ℕ$
6		vmacl	$⊢ n \in ℕ \to Λ (n) \in ℝ$
7	5 6	syl	$⊢ (A \in ℝ \land n \in (1 \dots ⌊A⌋)) \to Λ (n) \in ℝ$
8	7	recnd	$⊢ (A \in ℝ \land n \in (1 \dots ⌊A⌋)) \to Λ (n) \in ℂ$
9		simprr	$⊢ (A \in ℝ \land (n \in (1 \dots ⌊A⌋) \land Λ (n) = 0)) \to Λ (n) = 0$
10	2 3 8 9	fsumvma2	$⊢ A \in ℝ \to \sum_{n = 1}^{⌊A⌋} Λ (n) = \sum_{p \in [0, A] \cap ℙ} \sum_{k = 1}^{⌊\frac{\log A}{\log p}⌋} Λ (p^{k})$
11		simpr	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to p \in ([0, A] \cap ℙ)$
12	11	elin2d	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to p \in ℙ$
13		elfznn	$⊢ k \in (1 \dots ⌊\frac{\log A}{\log p}⌋) \to k \in ℕ$
14		vmappw	$⊢ (p \in ℙ \land k \in ℕ) \to Λ (p^{k}) = \log p$
15	12 13 14	syl2an	$⊢ ((A \in ℝ \land p \in ([0, A] \cap ℙ)) \land k \in (1 \dots ⌊\frac{\log A}{\log p}⌋)) \to Λ (p^{k}) = \log p$
16	15	sumeq2dv	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to \sum_{k = 1}^{⌊\frac{\log A}{\log p}⌋} Λ (p^{k}) = \sum_{k = 1}^{⌊\frac{\log A}{\log p}⌋} \log p$
17		fzfid	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to (1 \dots ⌊\frac{\log A}{\log p}⌋) \in Fin$
18		prmuz2	$⊢ p \in ℙ \to p \in ℤ_{\geq 2}$
19		eluzelre	$⊢ p \in ℤ_{\geq 2} \to p \in ℝ$
20		eluz2gt1	$⊢ p \in ℤ_{\geq 2} \to 1 < p$
21	19 20	rplogcld	$⊢ p \in ℤ_{\geq 2} \to \log p \in ℝ^{+}$
22	12 18 21	3syl	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to \log p \in ℝ^{+}$
23	22	rpcnd	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to \log p \in ℂ$
24		fsumconst	$⊢ ((1 \dots ⌊\frac{\log A}{\log p}⌋) \in Fin \land \log p \in ℂ) \to \sum_{k = 1}^{⌊\frac{\log A}{\log p}⌋} \log p = \|(1 \dots ⌊\frac{\log A}{\log p}⌋)\| \log p$
25	17 23 24	syl2anc	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to \sum_{k = 1}^{⌊\frac{\log A}{\log p}⌋} \log p = \|(1 \dots ⌊\frac{\log A}{\log p}⌋)\| \log p$
26		ppisval	$⊢ A \in ℝ \to [0, A] \cap ℙ = (2 \dots ⌊A⌋) \cap ℙ$
27		inss1	$⊢ (2 \dots ⌊A⌋) \cap ℙ \subseteq (2 \dots ⌊A⌋)$
28	26 27	eqsstrdi	$⊢ A \in ℝ \to [0, A] \cap ℙ \subseteq (2 \dots ⌊A⌋)$
29	28	sselda	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to p \in (2 \dots ⌊A⌋)$
30		elfzuz2	$⊢ p \in (2 \dots ⌊A⌋) \to ⌊A⌋ \in ℤ_{\geq 2}$
31	29 30	syl	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to ⌊A⌋ \in ℤ_{\geq 2}$
32		simpl	$⊢ (A \in ℝ \land ⌊A⌋ \in ℤ_{\geq 2}) \to A \in ℝ$
33		0red	$⊢ (A \in ℝ \land ⌊A⌋ \in ℤ_{\geq 2}) \to 0 \in ℝ$
34		2re	$⊢ 2 \in ℝ$
35	34	a1i	$⊢ (A \in ℝ \land ⌊A⌋ \in ℤ_{\geq 2}) \to 2 \in ℝ$
36		2pos	$⊢ 0 < 2$
37	36	a1i	$⊢ (A \in ℝ \land ⌊A⌋ \in ℤ_{\geq 2}) \to 0 < 2$
38		eluzle	$⊢ ⌊A⌋ \in ℤ_{\geq 2} \to 2 \leq ⌊A⌋$
39		2z	$⊢ 2 \in ℤ$
40		flge	$⊢ (A \in ℝ \land 2 \in ℤ) \to (2 \leq A \leftrightarrow 2 \leq ⌊A⌋)$
41	39 40	mpan2	$⊢ A \in ℝ \to (2 \leq A \leftrightarrow 2 \leq ⌊A⌋)$
42	38 41	imbitrrid	$⊢ A \in ℝ \to (⌊A⌋ \in ℤ_{\geq 2} \to 2 \leq A)$
43	42	imp	$⊢ (A \in ℝ \land ⌊A⌋ \in ℤ_{\geq 2}) \to 2 \leq A$
44	33 35 32 37 43	ltletrd	$⊢ (A \in ℝ \land ⌊A⌋ \in ℤ_{\geq 2}) \to 0 < A$
45	32 44	elrpd	$⊢ (A \in ℝ \land ⌊A⌋ \in ℤ_{\geq 2}) \to A \in ℝ^{+}$
46	31 45	syldan	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to A \in ℝ^{+}$
47	46	relogcld	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to \log A \in ℝ$
48	47 22	rerpdivcld	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to \frac{\log A}{\log p} \in ℝ$
49		1red	$⊢ (A \in ℝ \land ⌊A⌋ \in ℤ_{\geq 2}) \to 1 \in ℝ$
50		1lt2	$⊢ 1 < 2$
51	50	a1i	$⊢ (A \in ℝ \land ⌊A⌋ \in ℤ_{\geq 2}) \to 1 < 2$
52	49 35 32 51 43	ltletrd	$⊢ (A \in ℝ \land ⌊A⌋ \in ℤ_{\geq 2}) \to 1 < A$
53	31 52	syldan	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to 1 < A$
54		rplogcl	$⊢ (A \in ℝ \land 1 < A) \to \log A \in ℝ^{+}$
55	53 54	syldan	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to \log A \in ℝ^{+}$
56	55 22	rpdivcld	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to \frac{\log A}{\log p} \in ℝ^{+}$
57	56	rpge0d	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to 0 \leq \frac{\log A}{\log p}$
58		flge0nn0	$⊢ (\frac{\log A}{\log p} \in ℝ \land 0 \leq \frac{\log A}{\log p}) \to ⌊\frac{\log A}{\log p}⌋ \in ℕ_{0}$
59	48 57 58	syl2anc	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to ⌊\frac{\log A}{\log p}⌋ \in ℕ_{0}$
60		hashfz1	$⊢ ⌊\frac{\log A}{\log p}⌋ \in ℕ_{0} \to \|(1 \dots ⌊\frac{\log A}{\log p}⌋)\| = ⌊\frac{\log A}{\log p}⌋$
61	59 60	syl	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to \|(1 \dots ⌊\frac{\log A}{\log p}⌋)\| = ⌊\frac{\log A}{\log p}⌋$
62	61	oveq1d	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to \|(1 \dots ⌊\frac{\log A}{\log p}⌋)\| \log p = ⌊\frac{\log A}{\log p}⌋ \log p$
63	59	nn0cnd	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to ⌊\frac{\log A}{\log p}⌋ \in ℂ$
64	63 23	mulcomd	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to ⌊\frac{\log A}{\log p}⌋ \log p = \log p ⌊\frac{\log A}{\log p}⌋$
65	25 62 64	3eqtrd	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to \sum_{k = 1}^{⌊\frac{\log A}{\log p}⌋} \log p = \log p ⌊\frac{\log A}{\log p}⌋$
66	16 65	eqtrd	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to \sum_{k = 1}^{⌊\frac{\log A}{\log p}⌋} Λ (p^{k}) = \log p ⌊\frac{\log A}{\log p}⌋$
67	66	sumeq2dv	$⊢ A \in ℝ \to \sum_{p \in [0, A] \cap ℙ} \sum_{k = 1}^{⌊\frac{\log A}{\log p}⌋} Λ (p^{k}) = \sum_{p \in [0, A] \cap ℙ} \log p ⌊\frac{\log A}{\log p}⌋$
68	1 10 67	3eqtrd	$⊢ A \in ℝ \to ψ (A) = \sum_{p \in [0, A] \cap ℙ} \log p ⌊\frac{\log A}{\log p}⌋$

Metamath Proof Explorer

Theorem chpval2

Proof