Metamath Proof Explorer

Theorem ppival2

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

Ref Expression
Assertion ppival2 
|- ( A e. ZZ -> ( ppi ` A ) = ( # ` ( ( 2 ... A ) i^i Prime ) ) )

Proof

Step Hyp Ref Expression
1 zre 
 |-  ( A e. ZZ -> A e. RR )
2 ppival 
 |-  ( A e. RR -> ( ppi ` A ) = ( # ` ( ( 0 [,] A ) i^i Prime ) ) )
3 1 2 syl 
 |-  ( A e. ZZ -> ( ppi ` A ) = ( # ` ( ( 0 [,] A ) i^i Prime ) ) )
4 ppisval 
 |-  ( A e. RR -> ( ( 0 [,] A ) i^i Prime ) = ( ( 2 ... ( |_ ` A ) ) i^i Prime ) )
5 1 4 syl 
 |-  ( A e. ZZ -> ( ( 0 [,] A ) i^i Prime ) = ( ( 2 ... ( |_ ` A ) ) i^i Prime ) )
6 flid 
 |-  ( A e. ZZ -> ( |_ ` A ) = A )
7 6 oveq2d 
 |-  ( A e. ZZ -> ( 2 ... ( |_ ` A ) ) = ( 2 ... A ) )
8 7 ineq1d 
 |-  ( A e. ZZ -> ( ( 2 ... ( |_ ` A ) ) i^i Prime ) = ( ( 2 ... A ) i^i Prime ) )
9 5 8 eqtrd 
 |-  ( A e. ZZ -> ( ( 0 [,] A ) i^i Prime ) = ( ( 2 ... A ) i^i Prime ) )
10 9 fveq2d 
 |-  ( A e. ZZ -> ( # ` ( ( 0 [,] A ) i^i Prime ) ) = ( # ` ( ( 2 ... A ) i^i Prime ) ) )
11 3 10 eqtrd 
 |-  ( A e. ZZ -> ( ppi ` A ) = ( # ` ( ( 2 ... A ) i^i Prime ) ) )