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 = ( x e. RR |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( Lam ` n ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cchp
 |-  psi
1 vx
 |-  x
2 cr
 |-  RR
3 vn
 |-  n
4 c1
 |-  1
5 cfz
 |-  ...
6 cfl
 |-  |_
7 1 cv
 |-  x
8 7 6 cfv
 |-  ( |_ ` x )
9 4 8 5 co
 |-  ( 1 ... ( |_ ` x ) )
10 cvma
 |-  Lam
11 3 cv
 |-  n
12 11 10 cfv
 |-  ( Lam ` n )
13 9 12 3 csu
 |-  sum_ n e. ( 1 ... ( |_ ` x ) ) ( Lam ` n )
14 1 2 13 cmpt
 |-  ( x e. RR |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( Lam ` n ) )
15 0 14 wceq
 |-  psi = ( x e. RR |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( Lam ` n ) )