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	⊢ ψ = ( 𝑥 ∈ ℝ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( Λ ‘ 𝑛 ) )
2		fzfid	⊢ ( 𝑥 ∈ ℝ → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
3		elfznn	⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ )
4	3	adantl	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ )
5		vmacl	⊢ ( 𝑛 ∈ ℕ → ( Λ ‘ 𝑛 ) ∈ ℝ )
6	4 5	syl	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ )
7	2 6	fsumrecl	⊢ ( 𝑥 ∈ ℝ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( Λ ‘ 𝑛 ) ∈ ℝ )
8	1 7	fmpti	⊢ ψ : ℝ ⟶ ℝ