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