Step |
Hyp |
Ref |
Expression |
1 |
|
simpl |
|- ( ( A e. RR /\ 1 < A ) -> A e. RR ) |
2 |
|
0red |
|- ( ( A e. RR /\ 1 < A ) -> 0 e. RR ) |
3 |
|
1red |
|- ( ( A e. RR /\ 1 < A ) -> 1 e. RR ) |
4 |
|
0lt1 |
|- 0 < 1 |
5 |
4
|
a1i |
|- ( ( A e. RR /\ 1 < A ) -> 0 < 1 ) |
6 |
|
simpr |
|- ( ( A e. RR /\ 1 < A ) -> 1 < A ) |
7 |
2 3 1 5 6
|
lttrd |
|- ( ( A e. RR /\ 1 < A ) -> 0 < A ) |
8 |
1 7
|
elrpd |
|- ( ( A e. RR /\ 1 < A ) -> A e. RR+ ) |
9 |
|
relogcl |
|- ( A e. RR+ -> ( log ` A ) e. RR ) |
10 |
8 9
|
syl |
|- ( ( A e. RR /\ 1 < A ) -> ( log ` A ) e. RR ) |
11 |
|
log1 |
|- ( log ` 1 ) = 0 |
12 |
|
1rp |
|- 1 e. RR+ |
13 |
|
logltb |
|- ( ( 1 e. RR+ /\ A e. RR+ ) -> ( 1 < A <-> ( log ` 1 ) < ( log ` A ) ) ) |
14 |
12 8 13
|
sylancr |
|- ( ( A e. RR /\ 1 < A ) -> ( 1 < A <-> ( log ` 1 ) < ( log ` A ) ) ) |
15 |
6 14
|
mpbid |
|- ( ( A e. RR /\ 1 < A ) -> ( log ` 1 ) < ( log ` A ) ) |
16 |
11 15
|
eqbrtrrid |
|- ( ( A e. RR /\ 1 < A ) -> 0 < ( log ` A ) ) |
17 |
10 16
|
elrpd |
|- ( ( A e. RR /\ 1 < A ) -> ( log ` A ) e. RR+ ) |