Metamath Proof Explorer


Definition df-ppi

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

Detailed syntax breakdown

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