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

Definition df-ppi 20337
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 20331 . 2  class π
2 vx . . 3  set  x
3 cr 8736 . . 3  class  RR
4 cc0 8737 . . . . . 6  class  0
52cv 1622 . . . . . 6  class  x
6 cicc 10659 . . . . . 6  class  [,]
74, 5, 6co 5858 . . . . 5  class  ( 0 [,] x )
8 cprime 12758 . . . . 5  class  Prime
97, 8cin 3151 . . . 4  class  ( ( 0 [,] x )  i^i  Prime )
10 chash 11337 . . . 4  class  #
119, 10cfv 5255 . . 3  class  ( # `  ( ( 0 [,] x )  i^i  Prime ) )
122, 3, 11cmpt 4077 . 2  class  ( x  e.  RR  |->  ( # `  ( ( 0 [,] x )  i^i  Prime ) ) )
131, 12wceq 1623 1  wff π  =  ( x  e.  RR  |->  (
# `  ( (
0 [,] x )  i^i  Prime ) ) )
Colors of variables: wff set class
This definition is referenced by:  ppival  20365  ppif  20368
  Copyright terms: Public domain W3C validator