Metamath Proof Explorer

Theorem chpfl

Description: The second Chebyshev function does not change off the integers. (Contributed by Mario Carneiro, 9-Apr-2016)

Ref Expression
Assertion chpfl 
|- ( A e. RR -> ( psi ` ( |_ ` A ) ) = ( psi ` A ) )

Proof

Step Hyp Ref Expression
1 flidm 
 |-  ( A e. RR -> ( |_ ` ( |_ ` A ) ) = ( |_ ` A ) )
2 1 oveq2d 
 |-  ( A e. RR -> ( 1 ... ( |_ ` ( |_ ` A ) ) ) = ( 1 ... ( |_ ` A ) ) )
3 2 sumeq1d 
 |-  ( A e. RR -> sum_ x e. ( 1 ... ( |_ ` ( |_ ` A ) ) ) ( Lam ` x ) = sum_ x e. ( 1 ... ( |_ ` A ) ) ( Lam ` x ) )
4 reflcl 
 |-  ( A e. RR -> ( |_ ` A ) e. RR )
5 chpval 
 |-  ( ( |_ ` A ) e. RR -> ( psi ` ( |_ ` A ) ) = sum_ x e. ( 1 ... ( |_ ` ( |_ ` A ) ) ) ( Lam ` x ) )
6 4 5 syl 
 |-  ( A e. RR -> ( psi ` ( |_ ` A ) ) = sum_ x e. ( 1 ... ( |_ ` ( |_ ` A ) ) ) ( Lam ` x ) )
7 chpval 
 |-  ( A e. RR -> ( psi ` A ) = sum_ x e. ( 1 ... ( |_ ` A ) ) ( Lam ` x ) )
8 3 6 7 3eqtr4d 
 |-  ( A e. RR -> ( psi ` ( |_ ` A ) ) = ( psi ` A ) )