chtrpcl

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

		Ref	Expression
	Assertion	chtrpcl	$⊢ (A \in ℝ \land 2 \leq A) \to θ (A) \in ℝ^{+}$

Step	Hyp	Ref	Expression
1		chtcl	$⊢ A \in ℝ \to θ (A) \in ℝ$
2	1	adantr	$⊢ (A \in ℝ \land 2 \leq A) \to θ (A) \in ℝ$
3		0red	$⊢ (A \in ℝ \land 2 \leq A) \to 0 \in ℝ$
4		2re	$⊢ 2 \in ℝ$
5		1lt2	$⊢ 1 < 2$
6		rplogcl	$⊢ (2 \in ℝ \land 1 < 2) \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	$⊢ (A \in ℝ \land 2 \leq A) \to \log 2 \in ℝ$
10		rpgt0	$⊢ \log 2 \in ℝ^{+} \to 0 < \log 2$
11	7 10	mp1i	$⊢ (A \in ℝ \land 2 \leq A) \to 0 < \log 2$
12		cht2	$⊢ θ (2) = \log 2$
13		chtwordi	$⊢ (2 \in ℝ \land A \in ℝ \land 2 \leq A) \to θ (2) \leq θ (A)$
14	4 13	mp3an1	$⊢ (A \in ℝ \land 2 \leq A) \to θ (2) \leq θ (A)$
15	12 14	eqbrtrrid	$⊢ (A \in ℝ \land 2 \leq A) \to \log 2 \leq θ (A)$
16	3 9 2 11 15	ltletrd	$⊢ (A \in ℝ \land 2 \leq A) \to 0 < θ (A)$
17	2 16	elrpd	$⊢ (A \in ℝ \land 2 \leq A) \to θ (A) \in ℝ^{+}$

Metamath Proof Explorer