Theorem chtrpcl

Description: Closure of the Chebyshev function in the positive reals. (Contributed by Mario Carneiro, 22-Sep-2014)

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

Proof

Step	Hyp	Ref	Expression
1		chtcl	$$⊢A\in ℝ\to \theta \left(A\right)\in ℝ$$
2	1	adantr	$$⊢\left(A\in ℝ\wedge 2\le A\right)\to \theta \left(A\right)\in ℝ$$
3		0red	$$⊢\left(A\in ℝ\wedge 2\le A\right)\to 0\in ℝ$$
4		2re	$$⊢2\in ℝ$$
5		1lt2	$$⊢1<2$$
6		rplogcl	$$⊢\left(2\in ℝ\wedge 1<2\right)\to \log 2\in {ℝ}^{+}$$
7	4 5 6	mp2an	$$⊢\log 2\in {ℝ}^{+}$$
8		rpre	$$⊢\log 2\in {ℝ}^{+}\to \log 2\in ℝ$$
9	7 8	mp1i	$$⊢\left(A\in ℝ\wedge 2\le A\right)\to \log 2\in ℝ$$
10		rpgt0	$$⊢\log 2\in {ℝ}^{+}\to 0<\log 2$$
11	7 10	mp1i	$$⊢\left(A\in ℝ\wedge 2\le A\right)\to 0<\log 2$$
12		cht2	$$⊢\theta \left(2\right)=\log 2$$
13		chtwordi	$$⊢\left(2\in ℝ\wedge A\in ℝ\wedge 2\le A\right)\to \theta \left(2\right)\le \theta \left(A\right)$$
14	4 13	mp3an1	$$⊢\left(A\in ℝ\wedge 2\le A\right)\to \theta \left(2\right)\le \theta \left(A\right)$$
15	12 14	eqbrtrrid	$$⊢\left(A\in ℝ\wedge 2\le A\right)\to \log 2\le \theta \left(A\right)$$
16	3 9 2 11 15	ltletrd	$$⊢\left(A\in ℝ\wedge 2\le A\right)\to 0<\theta \left(A\right)$$
17	2 16	elrpd	$$⊢\left(A\in ℝ\wedge 2\le A\right)\to \theta \left(A\right)\in {ℝ}^{+}$$