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 ⊢ θ = x ∈ ℝ ⟼ ∑ p ∈ 0 x ∩ ℙ log ⁡ p

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccht class θ
1 vx setvar x
2 cr class ℝ
3 vp setvar p
4 cc0 class 0
5 cicc class .
6 1 cv setvar x
7 4 6 5 co class 0 x
8 cprime class ℙ
9 7 8 cin class 0 x ∩ ℙ
10 clog class log
11 3 cv setvar p
12 11 10 cfv class log ⁡ p
13 9 12 3 csu class ∑ p ∈ 0 x ∩ ℙ log ⁡ p
14 1 2 13 cmpt class x ∈ ℝ ⟼ ∑ p ∈ 0 x ∩ ℙ log ⁡ p
15 0 14 wceq wff θ = x ∈ ℝ ⟼ ∑ p ∈ 0 x ∩ ℙ log ⁡ p