Definition df-cht

Description: Define the first Chebyshev function, which adds up the logarithms of all primes less than x , see definition in ApostolNT p. 75. The symbol used to represent this function is sometimes the variant greek letter theta shown here and sometimes the greek letter psi, ψ; however, this notation can also refer to the second Chebyshev function, which adds up the logarithms of prime powers instead, see df-chp . See https://en.wikipedia.org/wiki/Chebyshev_function for a discussion of the two functions. (Contributed by Mario Carneiro, 15-Sep-2014)

	Ref	Expression
Assertion	df-cht	⊢ θ = ( 𝑥 ∈ ℝ ↦ Σ 𝑝 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ( log ‘ 𝑝 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccht	⊢ θ
1		vx	⊢ 𝑥
2		cr	⊢ ℝ
3		vp	⊢ 𝑝
4		cc0	⊢ 0
5		cicc	⊢ [,]
6	1	cv	⊢ 𝑥
7	4 6 5	co	⊢ ( 0 [,] 𝑥 )
8		cprime	⊢ ℙ
9	7 8	cin	⊢ ( ( 0 [,] 𝑥 ) ∩ ℙ )
10		clog	⊢ log
11	3	cv	⊢ 𝑝
12	11 10	cfv	⊢ ( log ‘ 𝑝 )
13	9 12 3	csu	⊢ Σ 𝑝 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ( log ‘ 𝑝 )
14	1 2 13	cmpt	⊢ ( 𝑥 ∈ ℝ ↦ Σ 𝑝 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ( log ‘ 𝑝 ) )
15	0 14	wceq	⊢ θ = ( 𝑥 ∈ ℝ ↦ Σ 𝑝 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ( log ‘ 𝑝 ) )