Theorem chtrpcl

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

	Ref	Expression
Assertion	chtrpcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ≤ 𝐴 ) → ( θ ‘ 𝐴 ) ∈ ℝ+ )

Proof

Step	Hyp	Ref	Expression
1		chtcl	⊢ ( 𝐴 ∈ ℝ → ( θ ‘ 𝐴 ) ∈ ℝ )
2	1	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ≤ 𝐴 ) → ( θ ‘ 𝐴 ) ∈ ℝ )
3		0red	⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ≤ 𝐴 ) → 0 ∈ ℝ )
4		2re	⊢ 2 ∈ ℝ
5		1lt2	⊢ 1 < 2
6		rplogcl	⊢ ( ( 2 ∈ ℝ ∧ 1 < 2 ) → ( log ‘ 2 ) ∈ ℝ+ )
7	4 5 6	mp2an	⊢ ( log ‘ 2 ) ∈ ℝ+
8		rpre	⊢ ( ( log ‘ 2 ) ∈ ℝ+ → ( log ‘ 2 ) ∈ ℝ )
9	7 8	mp1i	⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ≤ 𝐴 ) → ( log ‘ 2 ) ∈ ℝ )
10		rpgt0	⊢ ( ( log ‘ 2 ) ∈ ℝ+ → 0 < ( log ‘ 2 ) )
11	7 10	mp1i	⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ≤ 𝐴 ) → 0 < ( log ‘ 2 ) )
12		cht2	⊢ ( θ ‘ 2 ) = ( log ‘ 2 )
13		chtwordi	⊢ ( ( 2 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 2 ≤ 𝐴 ) → ( θ ‘ 2 ) ≤ ( θ ‘ 𝐴 ) )
14	4 13	mp3an1	⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ≤ 𝐴 ) → ( θ ‘ 2 ) ≤ ( θ ‘ 𝐴 ) )
15	12 14	eqbrtrrid	⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ≤ 𝐴 ) → ( log ‘ 2 ) ≤ ( θ ‘ 𝐴 ) )
16	3 9 2 11 15	ltletrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ≤ 𝐴 ) → 0 < ( θ ‘ 𝐴 ) )
17	2 16	elrpd	⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ≤ 𝐴 ) → ( θ ‘ 𝐴 ) ∈ ℝ+ )