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 ⊢ ψ = x ∈ ℝ ⟼ ∑ n = 1 x Λ ⁡ n

Detailed syntax breakdown

Step Hyp Ref Expression
0 cchp class ψ
1 vx setvar x
2 cr class ℝ
3 vn setvar n
4 c1 class 1
5 cfz class …
6 cfl class .
7 1 cv setvar x
8 7 6 cfv class x
9 4 8 5 co class 1 … x
10 cvma class Λ
11 3 cv setvar n
12 11 10 cfv class Λ ⁡ n
13 9 12 3 csu class ∑ n = 1 x Λ ⁡ n
14 1 2 13 cmpt class x ∈ ℝ ⟼ ∑ n = 1 x Λ ⁡ n
15 0 14 wceq wff ψ = x ∈ ℝ ⟼ ∑ n = 1 x Λ ⁡ n