This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 θ = ( 𝑥 ∈ ℝ ↦ Σ 𝑝 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ( log ‘ 𝑝 ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccht ⊢ θ
1 vx ⊢ 𝑥
2 cr ⊢ ℝ
3 vp ⊢ 𝑝
4 cc0 ⊢ 0
5 cicc ⊢ [,]
6 1 cv ⊢ 𝑥
7 4 6 5 co ⊢ ( 0 [,] 𝑥 )
8 cprime ⊢ ℙ
9 7 8 cin ⊢ ( ( 0 [,] 𝑥 ) ∩ ℙ )
10 clog ⊢ log
11 3 cv ⊢ 𝑝
12 11 10 cfv ⊢ ( log ‘ 𝑝 )
13 9 12 3 csu ⊢ Σ 𝑝 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ( log ‘ 𝑝 )
14 1 2 13 cmpt ⊢ ( 𝑥 ∈ ℝ ↦ Σ 𝑝 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ( log ‘ 𝑝 ) )
15 0 14 wceq ⊢ θ = ( 𝑥 ∈ ℝ ↦ Σ 𝑝 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ( log ‘ 𝑝 ) )