Definition df-ppi 16237

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 16240), 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 16234	. 2 class π
2		vx	. . 3 setvar x
3		cr 8184	. . 3 class RR
4		cc0 8185	. . . . . 6 class 0
5	2	cv 1401	. . . . . 6 class x
6		cicc 10310	. . . . . 6 class [,]
7	4, 5, 6	co 6088	. . . . 5 class ( 0 [,] x )
8		cprime 12910	. . . . 5 class Prime
9	7, 8	cin 3219	. . . 4 class ( ( 0 [,] x ) i^i Prime )
10		chash 11236	. . . 4 class ♯
11	9, 10	cfv 5380	. . 3 class (♯ ` ( ( 0 [,] x ) i^i Prime ) )
12	2, 3, 11	cmpt 4193	. 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  16248