Metamath Proof Explorer


Theorem logle1b

Description: The logarithm of a number is less than or equal to 1 iff the number is less than or equal to Euler's constant. (Contributed by AV, 30-May-2020)

Ref Expression
Assertion logle1b ( 𝐴 ∈ ℝ+ → ( ( log ‘ 𝐴 ) ≤ 1 ↔ 𝐴 ≤ e ) )

Proof

Step Hyp Ref Expression
1 id ( 𝐴 ∈ ℝ+𝐴 ∈ ℝ+ )
2 epr e ∈ ℝ+
3 2 a1i ( 𝐴 ∈ ℝ+ → e ∈ ℝ+ )
4 1 3 logled ( 𝐴 ∈ ℝ+ → ( 𝐴 ≤ e ↔ ( log ‘ 𝐴 ) ≤ ( log ‘ e ) ) )
5 loge ( log ‘ e ) = 1
6 5 a1i ( 𝐴 ∈ ℝ+ → ( log ‘ e ) = 1 )
7 6 breq2d ( 𝐴 ∈ ℝ+ → ( ( log ‘ 𝐴 ) ≤ ( log ‘ e ) ↔ ( log ‘ 𝐴 ) ≤ 1 ) )
8 4 7 bitr2d ( 𝐴 ∈ ℝ+ → ( ( log ‘ 𝐴 ) ≤ 1 ↔ 𝐴 ≤ e ) )