Metamath Proof Explorer


Theorem chpcl

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

Ref Expression
Assertion chpcl ⊢ A ∈ ℝ → ψ ⁡ A ∈ ℝ

Proof

Step Hyp Ref Expression
1 chpf ⊢ ψ : ℝ ⟶ ℝ
2 1 ffvelcdmi ⊢ A ∈ ℝ → ψ ⁡ A ∈ ℝ