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	|- ( A e. RR+ -> ( ( log ` A ) <_ 1 <-> A <_ _e ) )

Proof

Step	Hyp	Ref	Expression
1		id	|- ( A e. RR+ -> A e. RR+ )
2		epr	|- _e e. RR+
3	2	a1i	|- ( A e. RR+ -> _e e. RR+ )
4	1 3	logled	|- ( A e. RR+ -> ( A <_ _e <-> ( log ` A ) <_ ( log ` _e ) ) )
5		loge	|- ( log ` _e ) = 1
6	5	a1i	|- ( A e. RR+ -> ( log ` _e ) = 1 )
7	6	breq2d	|- ( A e. RR+ -> ( ( log ` A ) <_ ( log ` _e ) <-> ( log ` A ) <_ 1 ) )
8	4 7	bitr2d	|- ( A e. RR+ -> ( ( log ` A ) <_ 1 <-> A <_ _e ) )