Description: Functionality of the second Chebyshev function. (Contributed by Mario Carneiro, 7-Apr-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | chpf | ⊢ ψ : ℝ ⟶ ℝ |
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 | ⊢ ψ : ℝ ⟶ ℝ |