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ψA=ψA

Proof

Step Hyp Ref Expression
1 flidm AA=A
2 1 oveq2d A1A=1A
3 2 sumeq1d Ax=1AΛx=x=1AΛx
4 reflcl AA
5 chpval AψA=x=1AΛx
6 4 5 syl AψA=x=1AΛx
7 chpval AψA=x=1AΛx
8 3 6 7 3eqtr4d AψA=ψA