Metamath Proof Explorer


Theorem loggt0b

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

Proof

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