Definition df-chp 25676

Description: Define the second Chebyshev function, which adds up the logarithms of the primes corresponding to the prime powers less than 𝑥, see definition in [ApostolNT] p. 75. (Contributed by Mario Carneiro, 7-Apr-2016.)

Assertion

Ref	Expression
df-chp	⊢ ψ = (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(Λ‘𝑛))

Distinct variable group:   𝑥,𝑛

Detailed syntax breakdown of Definition df-chp

Step	Hyp	Ref	Expression
1		cchp 25670	. 2 class ψ
2		vx	. . 3 setvar 𝑥
3		cr 10536	. . 3 class ℝ
4		c1 10538	. . . . 5 class 1
5	2	cv 1536	. . . . . 6 class 𝑥
6		cfl 13161	. . . . . 6 class ⌊
7	5, 6	cfv 6355	. . . . 5 class (⌊‘𝑥)
8		cfz 12893	. . . . 5 class ...
9	4, 7, 8	co 7156	. . . 4 class (1...(⌊‘𝑥))
10		vn	. . . . . 6 setvar 𝑛
11	10	cv 1536	. . . . 5 class 𝑛
12		cvma 25669	. . . . 5 class Λ
13	11, 12	cfv 6355	. . . 4 class (Λ‘𝑛)
14	9, 13, 10	csu 15042	. . 3 class Σ𝑛 ∈ (1...(⌊‘𝑥))(Λ‘𝑛)
15	2, 3, 14	cmpt 5146	. 2 class (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(Λ‘𝑛))
16	1, 15	wceq 1537	1 wff ψ = (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(Λ‘𝑛))

This definition is referenced by:  chpval  25699  chpf  25700