Metamath Proof Explorer


Theorem chpf

Description: Functionality of the second Chebyshev function. (Contributed by Mario Carneiro, 7-Apr-2016)

Ref Expression
Assertion chpf ψ:

Proof

Step Hyp Ref Expression
1 df-chp ψ=xn=1xΛn
2 fzfid x1xFin
3 elfznn n1xn
4 3 adantl xn1xn
5 vmacl nΛn
6 4 5 syl xn1xΛn
7 2 6 fsumrecl xn=1xΛn
8 1 7 fmpti ψ: