Metamath Proof Explorer

Theorem ppival2g

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

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

Proof

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