Metamath Proof Explorer

Theorem ppifl

Description: The prime-counting function ppi does not change off the integers. (Contributed by Mario Carneiro, 18-Sep-2014)

Ref Expression
Assertion ppifl 
|- ( A e. RR -> ( ppi ` ( |_ ` A ) ) = ( ppi ` A ) )

Proof

Step Hyp Ref Expression
1 ppisval 
 |-  ( A e. RR -> ( ( 0 [,] A ) i^i Prime ) = ( ( 2 ... ( |_ ` A ) ) i^i Prime ) )
2 1 fveq2d 
 |-  ( A e. RR -> ( # ` ( ( 0 [,] A ) i^i Prime ) ) = ( # ` ( ( 2 ... ( |_ ` A ) ) i^i Prime ) ) )
3 ppival 
 |-  ( A e. RR -> ( ppi ` A ) = ( # ` ( ( 0 [,] A ) i^i Prime ) ) )
4 flcl 
 |-  ( A e. RR -> ( |_ ` A ) e. ZZ )
5 ppival2 
 |-  ( ( |_ ` A ) e. ZZ -> ( ppi ` ( |_ ` A ) ) = ( # ` ( ( 2 ... ( |_ ` A ) ) i^i Prime ) ) )
6 4 5 syl 
 |-  ( A e. RR -> ( ppi ` ( |_ ` A ) ) = ( # ` ( ( 2 ... ( |_ ` A ) ) i^i Prime ) ) )
7 2 3 6 3eqtr4rd 
 |-  ( A e. RR -> ( ppi ` ( |_ ` A ) ) = ( ppi ` A ) )