Metamath Proof Explorer


Theorem chprpcl

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+ )

Proof

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+ )