MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-cht Structured version   Unicode version

Definition df-cht 22323
Description: Define the first Chebyshev function, which adds up the logarithms of all primes less than  x. 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 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
StepHypRef Expression
1 ccht 22317 . 2  class  theta
2 vx . . 3  setvar  x
3 cr 9273 . . 3  class  RR
4 cc0 9274 . . . . . 6  class  0
52cv 1363 . . . . . 6  class  x
6 cicc 11295 . . . . . 6  class  [,]
74, 5, 6co 6084 . . . . 5  class  ( 0 [,] x )
8 cprime 13750 . . . . 5  class  Prime
97, 8cin 3319 . . . 4  class  ( ( 0 [,] x )  i^i  Prime )
10 vp . . . . . 6  setvar  p
1110cv 1363 . . . . 5  class  p
12 clog 21895 . . . . 5  class  log
1311, 12cfv 5410 . . . 4  class  ( log `  p )
149, 13, 10csu 13151 . . 3  class  sum_ p  e.  ( ( 0 [,] x )  i^i  Prime ) ( log `  p
)
152, 3, 14cmpt 4342 . 2  class  ( x  e.  RR  |->  sum_ p  e.  ( ( 0 [,] x )  i^i  Prime ) ( log `  p
) )
161, 15wceq 1364 1  wff  theta  =  ( x  e.  RR  |->  sum_
p  e.  ( ( 0 [,] x )  i^i  Prime ) ( log `  p ) )
Colors of variables: wff setvar class
This definition is referenced by:  chtf  22335  chtval  22337
  Copyright terms: Public domain W3C validator