Definition df-chp 24825

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.)

Assertion

Ref	Expression
df-chp	|- ψ = ( x e. RR |-> sum_ n e. ( 1 ... ( |_ ` x ) ) (Λ ` n ) )

Distinct variable group:   x, n

Detailed syntax breakdown of Definition df-chp

Step	Hyp	Ref	Expression
1		cchp 24819	. 2 class ψ
2		vx	. . 3 setvar x
3		cr 9935	. . 3 class RR
4		c1 9937	. . . . 5 class 1
5	2	cv 1482	. . . . . 6 class x
6		cfl 12591	. . . . . 6 class |_
7	5, 6	cfv 5888	. . . . 5 class ( |_ ` x )
8		cfz 12326	. . . . 5 class ...
9	4, 7, 8	co 6650	. . . 4 class ( 1 ... ( |_ ` x ) )
10		vn	. . . . . 6 setvar n
11	10	cv 1482	. . . . 5 class n
12		cvma 24818	. . . . 5 class Λ
13	11, 12	cfv 5888	. . . 4 class (Λ ` n )
14	9, 13, 10	csu 14416	. . 3 class sum_ n e. ( 1 ... ( |_ ` x ) ) (Λ ` n )
15	2, 3, 14	cmpt 4729	. 2 class ( x e. RR |-> sum_ n e. ( 1 ... ( |_ ` x ) ) (Λ ` n ) )
16	1, 15	wceq 1483	1 wff ψ = ( x e. RR |-> sum_ n e. ( 1 ... ( |_ ` x ) ) (Λ ` n ) )

This definition is referenced by:  chpval  24848  chpf  24849