Database
BASIC REAL AND COMPLEX FUNCTIONS
Basic number theory
Number-theoretical functions
chtcl
Next ⟩
chtval
Metamath Proof Explorer
Ascii
Unicode
Theorem
chtcl
Description:
Real closure of the Chebyshev function.
(Contributed by
Mario Carneiro
, 15-Sep-2014)
Ref
Expression
Assertion
chtcl
⊢
A
∈
ℝ
→
θ
⁡
A
∈
ℝ
Proof
Step
Hyp
Ref
Expression
1
chtf
⊢
θ
:
ℝ
⟶
ℝ
2
1
ffvelrni
⊢
A
∈
ℝ
→
θ
⁡
A
∈
ℝ