Definition df-chp

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cchp	⊢ ψ
1		vx	⊢ 𝑥
2		cr	⊢ ℝ
3		vn	⊢ 𝑛
4		c1	⊢ 1
5		cfz	⊢ ...
6		cfl	⊢ ⌊
7	1	cv	⊢ 𝑥
8	7 6	cfv	⊢ ( ⌊ ‘ 𝑥 )
9	4 8 5	co	⊢ ( 1 ... ( ⌊ ‘ 𝑥 ) )
10		cvma	⊢ Λ
11	3	cv	⊢ 𝑛
12	11 10	cfv	⊢ ( Λ ‘ 𝑛 )
13	9 12 3	csu	⊢ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( Λ ‘ 𝑛 )
14	1 2 13	cmpt	⊢ ( 𝑥 ∈ ℝ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( Λ ‘ 𝑛 ) )
15	0 14	wceq	⊢ ψ = ( 𝑥 ∈ ℝ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( Λ ‘ 𝑛 ) )