Definition df-chp 26592

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 26586	. 2 class ψ
2		vx	. . 3 setvar 𝑥
3		cr 11105	. . 3 class ℝ
4		c1 11107	. . . . 5 class 1
5	2	cv 1540	. . . . . 6 class 𝑥
6		cfl 13751	. . . . . 6 class ⌊
7	5, 6	cfv 6540	. . . . 5 class (⌊‘𝑥)
8		cfz 13480	. . . . 5 class ...
9	4, 7, 8	co 7405	. . . 4 class (1...(⌊‘𝑥))
10		vn	. . . . . 6 setvar 𝑛
11	10	cv 1540	. . . . 5 class 𝑛
12		cvma 26585	. . . . 5 class Λ
13	11, 12	cfv 6540	. . . 4 class (Λ‘𝑛)
14	9, 13, 10	csu 15628	. . 3 class Σ𝑛 ∈ (1...(⌊‘𝑥))(Λ‘𝑛)
15	2, 3, 14	cmpt 5230	. 2 class (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(Λ‘𝑛))
16	1, 15	wceq 1541	1 wff ψ = (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(Λ‘𝑛))

This definition is referenced by:  chpval  26615  chpf  26616