Metamath Proof Explorer

Theorem chtcl

Description: Real closure of the Chebyshev function. (Contributed by Mario Carneiro, 15-Sep-2014)

Ref Expression
Assertion chtcl 
|- ( A e. RR -> ( theta ` A ) e. RR )

Proof

Step Hyp Ref Expression
1 chtf 
 |-  theta : RR --> RR
2 1 ffvelcdmi 
 |-  ( A e. RR -> ( theta ` A ) e. RR )