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