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