Metamath Proof Explorer


Theorem loglt1b

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

Ref Expression
Assertion loglt1b
|- ( A e. RR+ -> ( ( log ` A ) < 1 <-> A < _e ) )

Proof

Step Hyp Ref Expression
1 epr
 |-  _e e. RR+
2 logltb
 |-  ( ( A e. RR+ /\ _e e. RR+ ) -> ( A < _e <-> ( log ` A ) < ( log ` _e ) ) )
3 1 2 mpan2
 |-  ( A e. RR+ -> ( A < _e <-> ( log ` A ) < ( log ` _e ) ) )
4 loge
 |-  ( log ` _e ) = 1
5 4 a1i
 |-  ( A e. RR+ -> ( log ` _e ) = 1 )
6 5 breq2d
 |-  ( A e. RR+ -> ( ( log ` A ) < ( log ` _e ) <-> ( log ` A ) < 1 ) )
7 3 6 bitr2d
 |-  ( A e. RR+ -> ( ( log ` A ) < 1 <-> A < _e ) )