# 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 ${⊢}\psi =\left({x}\in ℝ⟼\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cchp ${class}\psi$
1 vx ${setvar}{x}$
2 cr ${class}ℝ$
3 vn ${setvar}{n}$
4 c1 ${class}1$
5 cfz ${class}\dots$
6 cfl ${class}⌊.⌋$
7 1 cv ${setvar}{x}$
8 7 6 cfv ${class}⌊{x}⌋$
9 4 8 5 co ${class}\left(1\dots ⌊{x}⌋\right)$
10 cvma ${class}\Lambda$
11 3 cv ${setvar}{n}$
12 11 10 cfv ${class}\Lambda \left({n}\right)$
13 9 12 3 csu ${class}\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)$
14 1 2 13 cmpt ${class}\left({x}\in ℝ⟼\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\right)$
15 0 14 wceq ${wff}\psi =\left({x}\in ℝ⟼\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\right)$