Theorem chprpcl

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

	Ref	Expression
Assertion	chprpcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ≤ 𝐴 ) → ( ψ ‘ 𝐴 ) ∈ ℝ+ )

Proof

Step	Hyp	Ref	Expression
1		chpcl	⊢ ( 𝐴 ∈ ℝ → ( ψ ‘ 𝐴 ) ∈ ℝ )
2	1	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ≤ 𝐴 ) → ( ψ ‘ 𝐴 ) ∈ ℝ )
3		chtrpcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ≤ 𝐴 ) → ( θ ‘ 𝐴 ) ∈ ℝ+ )
4		chtlepsi	⊢ ( 𝐴 ∈ ℝ → ( θ ‘ 𝐴 ) ≤ ( ψ ‘ 𝐴 ) )
5	4	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ≤ 𝐴 ) → ( θ ‘ 𝐴 ) ≤ ( ψ ‘ 𝐴 ) )
6	2 3 5	rpgecld	⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ≤ 𝐴 ) → ( ψ ‘ 𝐴 ) ∈ ℝ+ )