Theorem ppival

Description: Value of the prime-counting function pi. (Contributed by Mario Carneiro, 15-Sep-2014)

	Ref	Expression
Assertion	ppival	|- ( A e. RR -> ( ppi ` A ) = ( # ` ( ( 0 [,] A ) i^i Prime ) ) )

Proof

Step	Hyp	Ref	Expression
1		oveq2	|- ( x = A -> ( 0 [,] x ) = ( 0 [,] A ) )
2	1	ineq1d	|- ( x = A -> ( ( 0 [,] x ) i^i Prime ) = ( ( 0 [,] A ) i^i Prime ) )
3	2	fveq2d	|- ( x = A -> ( # ` ( ( 0 [,] x ) i^i Prime ) ) = ( # ` ( ( 0 [,] A ) i^i Prime ) ) )
4		df-ppi	|- ppi = ( x e. RR |-> ( # ` ( ( 0 [,] x ) i^i Prime ) ) )
5		fvex	|- ( # ` ( ( 0 [,] A ) i^i Prime ) ) e. _V
6	3 4 5	fvmpt	|- ( A e. RR -> ( ppi ` A ) = ( # ` ( ( 0 [,] A ) i^i Prime ) ) )