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

Metamath Proof Explorer

Definition df-chp

Description: Define the second Chebyshev function, which adds up the logarithms of the primes corresponding to the prime powers less than x , see definition in ApostolNT p. 75. (Contributed by Mario Carneiro, 7-Apr-2016)

Ref Expression
Assertion df-chp ψ = ( 𝑥 ∈ ℝ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( Λ ‘ 𝑛 ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cchp ⊢ ψ
1 vx ⊢ 𝑥
2 cr ⊢ ℝ
3 vn ⊢ 𝑛
4 c1 ⊢ 1
5 cfz ⊢ ...
6 cfl ⊢ ⌊
7 1 cv ⊢ 𝑥
8 7 6 cfv ⊢ ( ⌊ ‘ 𝑥 )
9 4 8 5 co ⊢ ( 1 ... ( ⌊ ‘ 𝑥 ) )
10 cvma ⊢ Λ
11 3 cv ⊢ 𝑛
12 11 10 cfv ⊢ ( Λ ‘ 𝑛 )
13 9 12 3 csu ⊢ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( Λ ‘ 𝑛 )
14 1 2 13 cmpt ⊢ ( 𝑥 ∈ ℝ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( Λ ‘ 𝑛 ) )
15 0 14 wceq ⊢ ψ = ( 𝑥 ∈ ℝ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( Λ ‘ 𝑛 ) )