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

Definition df-cht 24535
Description: Define the first Chebyshev function, which adds up the logarithms of all primes less than 𝑥, 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 24537. 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 θ = (𝑥 ∈ ℝ ↦ Σ𝑝 ∈ ((0[,]𝑥) ∩ ℙ)(log‘𝑝))
Distinct variable group:   𝑥,𝑝

Detailed syntax breakdown of Definition df-cht
StepHypRef Expression
1 ccht 24529 . 2 class θ
2 vx . . 3 setvar 𝑥
3 cr 9786 . . 3 class
4 cc0 9787 . . . . . 6 class 0
52cv 1473 . . . . . 6 class 𝑥
6 cicc 12000 . . . . . 6 class [,]
74, 5, 6co 6522 . . . . 5 class (0[,]𝑥)
8 cprime 15164 . . . . 5 class
97, 8cin 3533 . . . 4 class ((0[,]𝑥) ∩ ℙ)
10 vp . . . . . 6 setvar 𝑝
1110cv 1473 . . . . 5 class 𝑝
12 clog 24017 . . . . 5 class log
1311, 12cfv 5785 . . . 4 class (log‘𝑝)
149, 13, 10csu 14205 . . 3 class Σ𝑝 ∈ ((0[,]𝑥) ∩ ℙ)(log‘𝑝)
152, 3, 14cmpt 4632 . 2 class (𝑥 ∈ ℝ ↦ Σ𝑝 ∈ ((0[,]𝑥) ∩ ℙ)(log‘𝑝))
161, 15wceq 1474 1 wff θ = (𝑥 ∈ ℝ ↦ Σ𝑝 ∈ ((0[,]𝑥) ∩ ℙ)(log‘𝑝))
Colors of variables: wff setvar class
This definition is referenced by:  chtf  24546  chtval  24548
  Copyright terms: Public domain W3C validator