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