Description: Closure of the second Chebyshev function in the positive reals. (Contributed by Mario Carneiro, 8-Apr-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | chprpcl | |- ( ( A e. RR /\ 2 <_ A ) -> ( psi ` A ) e. RR+ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | chpcl | |- ( A e. RR -> ( psi ` A ) e. RR ) |
|
2 | 1 | adantr | |- ( ( A e. RR /\ 2 <_ A ) -> ( psi ` A ) e. RR ) |
3 | chtrpcl | |- ( ( A e. RR /\ 2 <_ A ) -> ( theta ` A ) e. RR+ ) |
|
4 | chtlepsi | |- ( A e. RR -> ( theta ` A ) <_ ( psi ` A ) ) |
|
5 | 4 | adantr | |- ( ( A e. RR /\ 2 <_ A ) -> ( theta ` A ) <_ ( psi ` A ) ) |
6 | 2 3 5 | rpgecld | |- ( ( A e. RR /\ 2 <_ A ) -> ( psi ` A ) e. RR+ ) |