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

Metamath Proof Explorer

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 ≤ 𝐴 ) → ( θ ‘ 𝐴 ) ∈ ℝ+ )