Definition df-ppi 16198

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 16201), 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 16195	. 2 class π
2		vx	. . 3 setvar 𝑥
3		cr 8179	. . 3 class ℝ
4		cc0 8180	. . . . . 6 class 0
5	2	cv 1401	. . . . . 6 class 𝑥
6		cicc 10304	. . . . . 6 class [,]
7	4, 5, 6	co 6085	. . . . 5 class (0[,]𝑥)
8		cprime 12904	. . . . 5 class ℙ
9	7, 8	cin 3219	. . . 4 class ((0[,]𝑥) ∩ ℙ)
10		chash 11230	. . . 4 class ♯
11	9, 10	cfv 5377	. . 3 class (♯‘((0[,]𝑥) ∩ ℙ))
12	2, 3, 11	cmpt 4192	. 2 class (𝑥 ∈ ℝ ↦ (♯‘((0[,]𝑥) ∩ ℙ)))
13	1, 12	wceq 1402	1 wff π = (𝑥 ∈ ℝ ↦ (♯‘((0[,]𝑥) ∩ ℙ)))

This definition is used by:  ppiqval  16209