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

Definition df-ppi 24946
Description: Define the prime π function, which counts the number of primes less than or equal to 𝑥, see definition in [ApostolNT] p. 8. (Contributed by Mario Carneiro, 15-Sep-2014.)
Assertion
Ref Expression
df-ppi π = (𝑥 ∈ ℝ ↦ (♯‘((0[,]𝑥) ∩ ℙ)))

Detailed syntax breakdown of Definition df-ppi
StepHypRef Expression
1 cppi 24940 . 2 class π
2 vx . . 3 setvar 𝑥
3 cr 10048 . . 3 class
4 cc0 10049 . . . . . 6 class 0
52cv 1595 . . . . . 6 class 𝑥
6 cicc 12292 . . . . . 6 class [,]
74, 5, 6co 6765 . . . . 5 class (0[,]𝑥)
8 cprime 15508 . . . . 5 class
97, 8cin 3679 . . . 4 class ((0[,]𝑥) ∩ ℙ)
10 chash 13232 . . . 4 class
119, 10cfv 6001 . . 3 class (♯‘((0[,]𝑥) ∩ ℙ))
122, 3, 11cmpt 4837 . 2 class (𝑥 ∈ ℝ ↦ (♯‘((0[,]𝑥) ∩ ℙ)))
131, 12wceq 1596 1 wff π = (𝑥 ∈ ℝ ↦ (♯‘((0[,]𝑥) ∩ ℙ)))
Colors of variables: wff setvar class
This definition is referenced by:  ppival  24973  ppif  24976
  Copyright terms: Public domain W3C validator