Metamath Proof Explorer


Theorem logge0

Description: The logarithm of a number greater than 1 is nonnegative. (Contributed by Mario Carneiro, 29-May-2016)

Ref Expression
Assertion logge0 ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 0 ≤ ( log ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 log1 ( log ‘ 1 ) = 0
2 simpr ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 1 ≤ 𝐴 )
3 1rp 1 ∈ ℝ+
4 rpgecl ( ( 1 ∈ ℝ+𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 𝐴 ∈ ℝ+ )
5 3 4 mp3an1 ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 𝐴 ∈ ℝ+ )
6 logleb ( ( 1 ∈ ℝ+𝐴 ∈ ℝ+ ) → ( 1 ≤ 𝐴 ↔ ( log ‘ 1 ) ≤ ( log ‘ 𝐴 ) ) )
7 3 5 6 sylancr ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( 1 ≤ 𝐴 ↔ ( log ‘ 1 ) ≤ ( log ‘ 𝐴 ) ) )
8 2 7 mpbid ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( log ‘ 1 ) ≤ ( log ‘ 𝐴 ) )
9 1 8 eqbrtrrid ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 0 ≤ ( log ‘ 𝐴 ) )