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