Database
BASIC REAL AND COMPLEX FUNCTIONS
Basic number theory
Number-theoretical functions
chpcl
Next ⟩
efchpcl
Metamath Proof Explorer
Ascii
Unicode
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
ffvelrni
⊢
A
∈
ℝ
→
ψ
⁡
A
∈
ℝ