This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem chpf

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

Ref Expression
Assertion chpf 
|- psi : RR --> RR

Proof

Step Hyp Ref Expression
1 df-chp 
 |-  psi = ( x e. RR |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( Lam ` n ) )
2 fzfid 
 |-  ( x e. RR -> ( 1 ... ( |_ ` x ) ) e. Fin )
3 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
4 3 adantl 
 |-  ( ( x e. RR /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
5 vmacl 
 |-  ( n e. NN -> ( Lam ` n ) e. RR )
6 4 5 syl 
 |-  ( ( x e. RR /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` n ) e. RR )
7 2 6 fsumrecl 
 |-  ( x e. RR -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( Lam ` n ) e. RR )
8 1 7 fmpti 
 |-  psi : RR --> RR