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	$$⊢\theta =\left(x\in ℝ⟼\sum _{p\in \left[0,x\right]\cap \mathbb{P}}\log p\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccht	$$class\theta$$
1		vx	$$setvarx$$
2		cr	$$classℝ$$
3		vp	$$setvarp$$
4		cc0	$$class0$$
5		cicc	$$class\left[.\right]$$
6	1	cv	$$setvarx$$
7	4 6 5	co	$$class\left[0,x\right]$$
8		cprime	$$class\mathbb{P}$$
9	7 8	cin	$$class\left(\left[0,x\right]\cap \mathbb{P}\right)$$
10		clog	$$classlog$$
11	3	cv	$$setvarp$$
12	11 10	cfv	$$class\log p$$
13	9 12 3	csu	$$class\sum _{p\in \left[0,x\right]\cap \mathbb{P}}\log p$$
14	1 2 13	cmpt	$$class\left(x\in ℝ⟼\sum _{p\in \left[0,x\right]\cap \mathbb{P}}\log p\right)$$
15	0 14	wceq	$$wff\theta =\left(x\in ℝ⟼\sum _{p\in \left[0,x\right]\cap \mathbb{P}}\log p\right)$$