Definition df-ppi 24826

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.)

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 24820	. 2 class π
2		vx	. . 3 setvar x
3		cr 9935	. . 3 class RR
4		cc0 9936	. . . . . 6 class 0
5	2	cv 1482	. . . . . 6 class x
6		cicc 12178	. . . . . 6 class [,]
7	4, 5, 6	co 6650	. . . . 5 class ( 0 [,] x )
8		cprime 15385	. . . . 5 class Prime
9	7, 8	cin 3573	. . . 4 class ( ( 0 [,] x ) i^i Prime )
10		chash 13117	. . . 4 class #
11	9, 10	cfv 5888	. . 3 class ( # ` ( ( 0 [,] x ) i^i Prime ) )
12	2, 3, 11	cmpt 4729	. 2 class ( x e. RR |-> ( # ` ( ( 0 [,] x ) i^i Prime ) ) )
13	1, 12	wceq 1483	1 wff π = ( x e. RR |-> ( # ` ( ( 0 [,] x ) i^i Prime ) ) )

This definition is referenced by:  ppival  24853  ppif  24856