Definition df-chp 27142

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 27136	. 2 class ψ
2		vx	. . 3 setvar 𝑥
3		cr 11154	. . 3 class ℝ
4		c1 11156	. . . . 5 class 1
5	2	cv 1539	. . . . . 6 class 𝑥
6		cfl 13830	. . . . . 6 class ⌊
7	5, 6	cfv 6561	. . . . 5 class (⌊‘𝑥)
8		cfz 13547	. . . . 5 class ...
9	4, 7, 8	co 7431	. . . 4 class (1...(⌊‘𝑥))
10		vn	. . . . . 6 setvar 𝑛
11	10	cv 1539	. . . . 5 class 𝑛
12		cvma 27135	. . . . 5 class Λ
13	11, 12	cfv 6561	. . . 4 class (Λ‘𝑛)
14	9, 13, 10	csu 15722	. . 3 class Σ𝑛 ∈ (1...(⌊‘𝑥))(Λ‘𝑛)
15	2, 3, 14	cmpt 5225	. 2 class (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(Λ‘𝑛))
16	1, 15	wceq 1540	1 wff ψ = (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(Λ‘𝑛))

This definition is referenced by:  chpval  27165  chpf  27166