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