Metamath Proof Explorer

Theorem chtfl

Description: The Chebyshev function does not change off the integers. (Contributed by Mario Carneiro, 22-Sep-2014)

Ref Expression
Assertion chtfl 
|- ( A e. RR -> ( theta ` ( |_ ` A ) ) = ( theta ` A ) )

Proof

Step Hyp Ref Expression
1 flidm 
 |-  ( A e. RR -> ( |_ ` ( |_ ` A ) ) = ( |_ ` A ) )
2 1 oveq2d 
 |-  ( A e. RR -> ( 2 ... ( |_ ` ( |_ ` A ) ) ) = ( 2 ... ( |_ ` A ) ) )
3 2 ineq1d 
 |-  ( A e. RR -> ( ( 2 ... ( |_ ` ( |_ ` A ) ) ) i^i Prime ) = ( ( 2 ... ( |_ ` A ) ) i^i Prime ) )
4 reflcl 
 |-  ( A e. RR -> ( |_ ` A ) e. RR )
5 ppisval 
 |-  ( ( |_ ` A ) e. RR -> ( ( 0 [,] ( |_ ` A ) ) i^i Prime ) = ( ( 2 ... ( |_ ` ( |_ ` A ) ) ) i^i Prime ) )
6 4 5 syl 
 |-  ( A e. RR -> ( ( 0 [,] ( |_ ` A ) ) i^i Prime ) = ( ( 2 ... ( |_ ` ( |_ ` A ) ) ) i^i Prime ) )
7 ppisval 
 |-  ( A e. RR -> ( ( 0 [,] A ) i^i Prime ) = ( ( 2 ... ( |_ ` A ) ) i^i Prime ) )
8 3 6 7 3eqtr4d 
 |-  ( A e. RR -> ( ( 0 [,] ( |_ ` A ) ) i^i Prime ) = ( ( 0 [,] A ) i^i Prime ) )
9 8 sumeq1d 
 |-  ( A e. RR -> sum_ p e. ( ( 0 [,] ( |_ ` A ) ) i^i Prime ) ( log ` p ) = sum_ p e. ( ( 0 [,] A ) i^i Prime ) ( log ` p ) )
10 chtval 
 |-  ( ( |_ ` A ) e. RR -> ( theta ` ( |_ ` A ) ) = sum_ p e. ( ( 0 [,] ( |_ ` A ) ) i^i Prime ) ( log ` p ) )
11 4 10 syl 
 |-  ( A e. RR -> ( theta ` ( |_ ` A ) ) = sum_ p e. ( ( 0 [,] ( |_ ` A ) ) i^i Prime ) ( log ` p ) )
12 chtval 
 |-  ( A e. RR -> ( theta ` A ) = sum_ p e. ( ( 0 [,] A ) i^i Prime ) ( log ` p ) )
13 9 11 12 3eqtr4d 
 |-  ( A e. RR -> ( theta ` ( |_ ` A ) ) = ( theta ` A ) )