Definition df-ppi 16254

Description: Define the prime π function, which counts the number of primes less than or equal to 𝑥, see definition in [ApostolNT] p. 8. Most often 𝑥 will be an integer, but many of our theorems support rational numbers (for example at ppiqsval 16257), and the definition would also work for cases such as numbers known to be irrational. (Contributed by Mario Carneiro, 15-Sep-2014.)

Assertion

Ref	Expression
df-ppi	⊢ π = (𝑥 ∈ ℝ ↦ (♯‘((0[,]𝑥) ∩ ℙ)))

Detailed syntax breakdown of Definition df-ppi

Step	Hyp	Ref	Expression
1		cppi 16251	. 2 class π
2		vx	. . 3 setvar 𝑥
3		cr 8184	. . 3 class ℝ
4		cc0 8185	. . . . . 6 class 0
5	2	cv 1401	. . . . . 6 class 𝑥
6		cicc 10309	. . . . . 6 class [,]
7	4, 5, 6	co 6088	. . . . 5 class (0[,]𝑥)
8		cprime 12909	. . . . 5 class ℙ
9	7, 8	cin 3219	. . . 4 class ((0[,]𝑥) ∩ ℙ)
10		chash 11235	. . . 4 class ♯
11	9, 10	cfv 5380	. . 3 class (♯‘((0[,]𝑥) ∩ ℙ))
12	2, 3, 11	cmpt 4193	. 2 class (𝑥 ∈ ℝ ↦ (♯‘((0[,]𝑥) ∩ ℙ)))
13	1, 12	wceq 1402	1 wff π = (𝑥 ∈ ℝ ↦ (♯‘((0[,]𝑥) ∩ ℙ)))

This definition is used by:  ppiqval  16265