Description: The logarithm of a number is positive iff the number is greater than 1. (Contributed by AV, 30-May-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | loggt0b | ⊢ ( 𝐴 ∈ ℝ+ → ( 0 < ( log ‘ 𝐴 ) ↔ 1 < 𝐴 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1rp | ⊢ 1 ∈ ℝ+ | |
2 | logltb | ⊢ ( ( 1 ∈ ℝ+ ∧ 𝐴 ∈ ℝ+ ) → ( 1 < 𝐴 ↔ ( log ‘ 1 ) < ( log ‘ 𝐴 ) ) ) | |
3 | 1 2 | mpan | ⊢ ( 𝐴 ∈ ℝ+ → ( 1 < 𝐴 ↔ ( log ‘ 1 ) < ( log ‘ 𝐴 ) ) ) |
4 | log1 | ⊢ ( log ‘ 1 ) = 0 | |
5 | 4 | a1i | ⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ 1 ) = 0 ) |
6 | 5 | breq1d | ⊢ ( 𝐴 ∈ ℝ+ → ( ( log ‘ 1 ) < ( log ‘ 𝐴 ) ↔ 0 < ( log ‘ 𝐴 ) ) ) |
7 | 3 6 | bitr2d | ⊢ ( 𝐴 ∈ ℝ+ → ( 0 < ( log ‘ 𝐴 ) ↔ 1 < 𝐴 ) ) |