Definition df-cht 27140

Description: Define the first Chebyshev function, which adds up the logarithms of all primes less than 𝑥, 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 27142. See https://en.wikipedia.org/wiki/Chebyshev_function 27142 for a discussion of the two functions. (Contributed by Mario Carneiro, 15-Sep-2014.)

Assertion

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

Distinct variable group:   𝑥,𝑝

Detailed syntax breakdown of Definition df-cht

Step	Hyp	Ref	Expression
1		ccht 27134	. 2 class θ
2		vx	. . 3 setvar 𝑥
3		cr 11154	. . 3 class ℝ
4		cc0 11155	. . . . . 6 class 0
5	2	cv 1539	. . . . . 6 class 𝑥
6		cicc 13390	. . . . . 6 class [,]
7	4, 5, 6	co 7431	. . . . 5 class (0[,]𝑥)
8		cprime 16708	. . . . 5 class ℙ
9	7, 8	cin 3950	. . . 4 class ((0[,]𝑥) ∩ ℙ)
10		vp	. . . . . 6 setvar 𝑝
11	10	cv 1539	. . . . 5 class 𝑝
12		clog 26596	. . . . 5 class log
13	11, 12	cfv 6561	. . . 4 class (log‘𝑝)
14	9, 13, 10	csu 15722	. . 3 class Σ𝑝 ∈ ((0[,]𝑥) ∩ ℙ)(log‘𝑝)
15	2, 3, 14	cmpt 5225	. 2 class (𝑥 ∈ ℝ ↦ Σ𝑝 ∈ ((0[,]𝑥) ∩ ℙ)(log‘𝑝))
16	1, 15	wceq 1540	1 wff θ = (𝑥 ∈ ℝ ↦ Σ𝑝 ∈ ((0[,]𝑥) ∩ ℙ)(log‘𝑝))

This definition is referenced by:  chtf  27151  chtval  27153