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 ‘ 𝐴 ) ) |
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 ‘ 𝐴 ) ) |