Definition df-ppi

Description: Define the prime π function, which counts the number of primes less than or equal to x , see definition in ApostolNT p. 8. (Contributed by Mario Carneiro, 15-Sep-2014)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cppi	⊢ π
1		vx	⊢ 𝑥
2		cr	⊢ ℝ
3		chash	⊢ ♯
4		cc0	⊢ 0
5		cicc	⊢ [,]
6	1	cv	⊢ 𝑥
7	4 6 5	co	⊢ ( 0 [,] 𝑥 )
8		cprime	⊢ ℙ
9	7 8	cin	⊢ ( ( 0 [,] 𝑥 ) ∩ ℙ )
10	9 3	cfv	⊢ ( ♯ ‘ ( ( 0 [,] 𝑥 ) ∩ ℙ ) )
11	1 2 10	cmpt	⊢ ( 𝑥 ∈ ℝ ↦ ( ♯ ‘ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ) )
12	0 11	wceq	⊢ π = ( 𝑥 ∈ ℝ ↦ ( ♯ ‘ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ) )