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 θ=xp0xlogp

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccht classθ
1 vx setvarx
2 cr class
3 vp setvarp
4 cc0 class0
5 cicc class.
6 1 cv setvarx
7 4 6 5 co class0x
8 cprime class
9 7 8 cin class0x
10 clog classlog
11 3 cv setvarp
12 11 10 cfv classlogp
13 9 12 3 csu classp0xlogp
14 1 2 13 cmpt classxp0xlogp
15 0 14 wceq wffθ=xp0xlogp