Metamath Proof Explorer

Theorem rplogcl

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

Ref Expression
Assertion rplogcl ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → ( log ‘ 𝐴 ) ∈ ℝ+ )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → 𝐴 ∈ ℝ )
2 0red ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → 0 ∈ ℝ )
3 1red ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → 1 ∈ ℝ )
4 0lt1 ⊢ 0 < 1
5 4 a1i ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → 0 < 1 )
6 simpr ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → 1 < 𝐴 )
7 2 3 1 5 6 lttrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → 0 < 𝐴 )
8 1 7 elrpd ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → 𝐴 ∈ ℝ+ )
9 relogcl ⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ 𝐴 ) ∈ ℝ )
10 8 9 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → ( log ‘ 𝐴 ) ∈ ℝ )
11 log1 ⊢ ( log ‘ 1 ) = 0
12 1rp ⊢ 1 ∈ ℝ+
13 logltb ⊢ ( ( 1 ∈ ℝ+ ∧ 𝐴 ∈ ℝ+ ) → ( 1 < 𝐴 ↔ ( log ‘ 1 ) < ( log ‘ 𝐴 ) ) )
14 12 8 13 sylancr ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → ( 1 < 𝐴 ↔ ( log ‘ 1 ) < ( log ‘ 𝐴 ) ) )
15 6 14 mpbid ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → ( log ‘ 1 ) < ( log ‘ 𝐴 ) )
16 11 15 eqbrtrrid ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → 0 < ( log ‘ 𝐴 ) )
17 10 16 elrpd ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → ( log ‘ 𝐴 ) ∈ ℝ+ )