Step |
Hyp |
Ref |
Expression |
1 |
|
log1 |
|- ( log ` 1 ) = 0 |
2 |
|
simpr |
|- ( ( A e. RR /\ 1 <_ A ) -> 1 <_ A ) |
3 |
|
1rp |
|- 1 e. RR+ |
4 |
|
rpgecl |
|- ( ( 1 e. RR+ /\ A e. RR /\ 1 <_ A ) -> A e. RR+ ) |
5 |
3 4
|
mp3an1 |
|- ( ( A e. RR /\ 1 <_ A ) -> A e. RR+ ) |
6 |
|
logleb |
|- ( ( 1 e. RR+ /\ A e. RR+ ) -> ( 1 <_ A <-> ( log ` 1 ) <_ ( log ` A ) ) ) |
7 |
3 5 6
|
sylancr |
|- ( ( A e. RR /\ 1 <_ A ) -> ( 1 <_ A <-> ( log ` 1 ) <_ ( log ` A ) ) ) |
8 |
2 7
|
mpbid |
|- ( ( A e. RR /\ 1 <_ A ) -> ( log ` 1 ) <_ ( log ` A ) ) |
9 |
1 8
|
eqbrtrrid |
|- ( ( A e. RR /\ 1 <_ A ) -> 0 <_ ( log ` A ) ) |