Definition df-cht 24823

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 24825. See https://en.wikipedia.org/wiki/Chebyshev_function for a discussion of the two functions. (Contributed by Mario Carneiro, 15-Sep-2014.)

Assertion

Ref	Expression
df-cht	|- theta = ( x e. RR |-> sum_ p e. ( ( 0 [,] x ) i^i Prime ) ( log ` p ) )

Distinct variable group:   x, p

Detailed syntax breakdown of Definition df-cht

Step	Hyp	Ref	Expression
1		ccht 24817	. 2 class theta
2		vx	. . 3 setvar x
3		cr 9935	. . 3 class RR
4		cc0 9936	. . . . . 6 class 0
5	2	cv 1482	. . . . . 6 class x
6		cicc 12178	. . . . . 6 class [,]
7	4, 5, 6	co 6650	. . . . 5 class ( 0 [,] x )
8		cprime 15385	. . . . 5 class Prime
9	7, 8	cin 3573	. . . 4 class ( ( 0 [,] x ) i^i Prime )
10		vp	. . . . . 6 setvar p
11	10	cv 1482	. . . . 5 class p
12		clog 24301	. . . . 5 class log
13	11, 12	cfv 5888	. . . 4 class ( log ` p )
14	9, 13, 10	csu 14416	. . 3 class sum_ p e. ( ( 0 [,] x ) i^i Prime ) ( log ` p )
15	2, 3, 14	cmpt 4729	. 2 class ( x e. RR |-> sum_ p e. ( ( 0 [,] x ) i^i Prime ) ( log ` p ) )
16	1, 15	wceq 1483	1 wff theta = ( x e. RR |-> sum_ p e. ( ( 0 [,] x ) i^i Prime ) ( log ` p ) )

This definition is referenced by:  chtf  24834  chtval  24836