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	$$setvarx$$
2		cr	$$classℝ$$
3		vn	$$setvarn$$
4		c1	$$class1$$
5		cfz	$$class\dots$$
6		cfl	$$class⌊.⌋$$
7	1	cv	$$setvarx$$
8	7 6	cfv	$$class⌊x⌋$$
9	4 8 5	co	$$class\left(1\dots ⌊x⌋\right)$$
10		cvma	$$class\Lambda$$
11	3	cv	$$setvarn$$
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)$$