Definition df-ppi 16154

Description: Define the prime π function, which counts the number of primes less than or equal to x, see definition in [ApostolNT] p. 8. Most often x will be an integer, but many of our theorems support rational numbers (for example at ppiqsval 16156), 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	|- π = ( x e. RR |-> (♯ ` ( ( 0 [,] x ) i^i Prime ) ) )

Detailed syntax breakdown of Definition df-ppi

Step	Hyp	Ref	Expression
1		cppi 16152	. 2 class π
2		vx	. . 3 setvar x
3		cr 8178	. . 3 class RR
4		cc0 8179	. . . . . 6 class 0
5	2	cv 1401	. . . . . 6 class x
6		cicc 10303	. . . . . 6 class [,]
7	4, 5, 6	co 6085	. . . . 5 class ( 0 [,] x )
8		cprime 12901	. . . . 5 class Prime
9	7, 8	cin 3219	. . . 4 class ( ( 0 [,] x ) i^i Prime )
10		chash 11228	. . . 4 class ♯
11	9, 10	cfv 5377	. . 3 class (♯ ` ( ( 0 [,] x ) i^i Prime ) )
12	2, 3, 11	cmpt 4192	. 2 class ( x e. RR |-> (♯ ` ( ( 0 [,] x ) i^i Prime ) ) )
13	1, 12	wceq 1402	1 wff π = ( x e. RR |-> (♯ ` ( ( 0 [,] x ) i^i Prime ) ) )

This definition is used by:  ppiqval  16160