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 ψ = ( 𝑥 ∈ ℝ ↦ Σ 𝑛 ∈ ( 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 ψ : ℝ ⟶ ℝ