Definition df-chp 26248

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 26242	. 2 class ψ
2		vx	. . 3 setvar 𝑥
3		cr 10870	. . 3 class ℝ
4		c1 10872	. . . . 5 class 1
5	2	cv 1538	. . . . . 6 class 𝑥
6		cfl 13510	. . . . . 6 class ⌊
7	5, 6	cfv 6433	. . . . 5 class (⌊‘𝑥)
8		cfz 13239	. . . . 5 class ...
9	4, 7, 8	co 7275	. . . 4 class (1...(⌊‘𝑥))
10		vn	. . . . . 6 setvar 𝑛
11	10	cv 1538	. . . . 5 class 𝑛
12		cvma 26241	. . . . 5 class Λ
13	11, 12	cfv 6433	. . . 4 class (Λ‘𝑛)
14	9, 13, 10	csu 15397	. . 3 class Σ𝑛 ∈ (1...(⌊‘𝑥))(Λ‘𝑛)
15	2, 3, 14	cmpt 5157	. 2 class (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(Λ‘𝑛))
16	1, 15	wceq 1539	1 wff ψ = (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(Λ‘𝑛))

This definition is referenced by:  chpval  26271  chpf  26272