Description: Define the prime π function, which counts the number of primes less than or equal to x , see definition in ApostolNT p. 8. (Contributed by Mario Carneiro, 15-Sep-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | df-ppi | |- ppi = ( x e. RR |-> ( # ` ( ( 0 [,] x ) i^i Prime ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cppi | |- ppi |
|
1 | vx | |- x |
|
2 | cr | |- RR |
|
3 | chash | |- # |
|
4 | cc0 | |- 0 |
|
5 | cicc | |- [,] |
|
6 | 1 | cv | |- x |
7 | 4 6 5 | co | |- ( 0 [,] x ) |
8 | cprime | |- Prime |
|
9 | 7 8 | cin | |- ( ( 0 [,] x ) i^i Prime ) |
10 | 9 3 | cfv | |- ( # ` ( ( 0 [,] x ) i^i Prime ) ) |
11 | 1 2 10 | cmpt | |- ( x e. RR |-> ( # ` ( ( 0 [,] x ) i^i Prime ) ) ) |
12 | 0 11 | wceq | |- ppi = ( x e. RR |-> ( # ` ( ( 0 [,] x ) i^i Prime ) ) ) |