Theorem chprpcl

Description: Closure of the second Chebyshev function in the positive reals. (Contributed by Mario Carneiro, 8-Apr-2016)

	Ref	Expression
Assertion	chprpcl	$$⊢\left(A\in ℝ\wedge 2\le A\right)\to \psi \left(A\right)\in {ℝ}^{+}$$

Proof

Step	Hyp	Ref	Expression
1		chpcl	$$⊢A\in ℝ\to \psi \left(A\right)\in ℝ$$
2	1	adantr	$$⊢\left(A\in ℝ\wedge 2\le A\right)\to \psi \left(A\right)\in ℝ$$
3		chtrpcl	$$⊢\left(A\in ℝ\wedge 2\le A\right)\to \theta \left(A\right)\in {ℝ}^{+}$$
4		chtlepsi	$$⊢A\in ℝ\to \theta \left(A\right)\le \psi \left(A\right)$$
5	4	adantr	$$⊢\left(A\in ℝ\wedge 2\le A\right)\to \theta \left(A\right)\le \psi \left(A\right)$$
6	2 3 5	rpgecld	$$⊢\left(A\in ℝ\wedge 2\le A\right)\to \psi \left(A\right)\in {ℝ}^{+}$$