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

### Detailed syntax breakdown

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