Definition df-ppi 26593

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

Step	Hyp	Ref	Expression
1		cppi 26587	. 2 class π
2		vx	. . 3 setvar 𝑥
3		cr 11105	. . 3 class ℝ
4		cc0 11106	. . . . . 6 class 0
5	2	cv 1540	. . . . . 6 class 𝑥
6		cicc 13323	. . . . . 6 class [,]
7	4, 5, 6	co 7405	. . . . 5 class (0[,]𝑥)
8		cprime 16604	. . . . 5 class ℙ
9	7, 8	cin 3946	. . . 4 class ((0[,]𝑥) ∩ ℙ)
10		chash 14286	. . . 4 class ♯
11	9, 10	cfv 6540	. . 3 class (♯‘((0[,]𝑥) ∩ ℙ))
12	2, 3, 11	cmpt 5230	. 2 class (𝑥 ∈ ℝ ↦ (♯‘((0[,]𝑥) ∩ ℙ)))
13	1, 12	wceq 1541	1 wff π = (𝑥 ∈ ℝ ↦ (♯‘((0[,]𝑥) ∩ ℙ)))

This definition is referenced by:  ppival  26620  ppif  26623