Metamath Proof Explorer


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 = ( x e. RR |-> sum_ p e. ( ( 0 [,] x ) i^i Prime ) ( log ` p ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccht
 |-  theta
1 vx
 |-  x
2 cr
 |-  RR
3 vp
 |-  p
4 cc0
 |-  0
5 cicc
 |-  [,]
6 1 cv
 |-  x
7 4 6 5 co
 |-  ( 0 [,] x )
8 cprime
 |-  Prime
9 7 8 cin
 |-  ( ( 0 [,] x ) i^i Prime )
10 clog
 |-  log
11 3 cv
 |-  p
12 11 10 cfv
 |-  ( log ` p )
13 9 12 3 csu
 |-  sum_ p e. ( ( 0 [,] x ) i^i Prime ) ( log ` p )
14 1 2 13 cmpt
 |-  ( x e. RR |-> sum_ p e. ( ( 0 [,] x ) i^i Prime ) ( log ` p ) )
15 0 14 wceq
 |-  theta = ( x e. RR |-> sum_ p e. ( ( 0 [,] x ) i^i Prime ) ( log ` p ) )