MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ppi Unicode version

Definition df-ppi 20331
Description: Define the prime π function, which counts the number of primes less than or equal to  x. (Contributed by Mario Carneiro, 15-Sep-2014.)
Assertion
Ref Expression
df-ppi  |- π  =  ( x  e.  RR  |->  (
# `  ( (
0 [,] x )  i^i  Prime ) ) )

Detailed syntax breakdown of Definition df-ppi
StepHypRef Expression
1 cppi 20325 . 2  class π
2 vx . . 3  set  x
3 cr 8731 . . 3  class  RR
4 cc0 8732 . . . . . 6  class  0
52cv 1623 . . . . . 6  class  x
6 cicc 10653 . . . . . 6  class  [,]
74, 5, 6co 5819 . . . . 5  class  ( 0 [,] x )
8 cprime 12752 . . . . 5  class  Prime
97, 8cin 3152 . . . 4  class  ( ( 0 [,] x )  i^i  Prime )
10 chash 11331 . . . 4  class  #
119, 10cfv 5221 . . 3  class  ( # `  ( ( 0 [,] x )  i^i  Prime ) )
122, 3, 11cmpt 4078 . 2  class  ( x  e.  RR  |->  ( # `  ( ( 0 [,] x )  i^i  Prime ) ) )
131, 12wceq 1624 1  wff π  =  ( x  e.  RR  |->  (
# `  ( (
0 [,] x )  i^i  Prime ) ) )
Colors of variables: wff set class
This definition is referenced by:  ppival  20359  ppif  20362
  Copyright terms: Public domain W3C validator