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