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