This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in ℝ \land 2 \leq A) \to ψ (A) \in ℝ^{+}$

Step	Hyp	Ref	Expression
1		chpcl	$⊢ A \in ℝ \to ψ (A) \in ℝ$
2	1	adantr	$⊢ (A \in ℝ \land 2 \leq A) \to ψ (A) \in ℝ$
3		chtrpcl	$⊢ (A \in ℝ \land 2 \leq A) \to θ (A) \in ℝ^{+}$
4		chtlepsi	$⊢ A \in ℝ \to θ (A) \leq ψ (A)$
5	4	adantr	$⊢ (A \in ℝ \land 2 \leq A) \to θ (A) \leq ψ (A)$
6	2 3 5	rpgecld	$⊢ (A \in ℝ \land 2 \leq A) \to ψ (A) \in ℝ^{+}$