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