Step |
Hyp |
Ref |
Expression |
1 |
|
1xr |
|- 1 e. RR* |
2 |
|
elioopnf |
|- ( 1 e. RR* -> ( B e. ( 1 (,) +oo ) <-> ( B e. RR /\ 1 < B ) ) ) |
3 |
1 2
|
ax-mp |
|- ( B e. ( 1 (,) +oo ) <-> ( B e. RR /\ 1 < B ) ) |
4 |
3
|
simprbi |
|- ( B e. ( 1 (,) +oo ) -> 1 < B ) |
5 |
|
log1 |
|- ( log ` 1 ) = 0 |
6 |
5
|
eqcomi |
|- 0 = ( log ` 1 ) |
7 |
6
|
a1i |
|- ( B e. ( 1 (,) +oo ) -> 0 = ( log ` 1 ) ) |
8 |
7
|
breq1d |
|- ( B e. ( 1 (,) +oo ) -> ( 0 < ( log ` B ) <-> ( log ` 1 ) < ( log ` B ) ) ) |
9 |
|
1rp |
|- 1 e. RR+ |
10 |
|
0lt1 |
|- 0 < 1 |
11 |
|
0red |
|- ( B e. RR -> 0 e. RR ) |
12 |
|
1red |
|- ( B e. RR -> 1 e. RR ) |
13 |
|
id |
|- ( B e. RR -> B e. RR ) |
14 |
|
lttr |
|- ( ( 0 e. RR /\ 1 e. RR /\ B e. RR ) -> ( ( 0 < 1 /\ 1 < B ) -> 0 < B ) ) |
15 |
11 12 13 14
|
syl3anc |
|- ( B e. RR -> ( ( 0 < 1 /\ 1 < B ) -> 0 < B ) ) |
16 |
10 15
|
mpani |
|- ( B e. RR -> ( 1 < B -> 0 < B ) ) |
17 |
16
|
imdistani |
|- ( ( B e. RR /\ 1 < B ) -> ( B e. RR /\ 0 < B ) ) |
18 |
|
elrp |
|- ( B e. RR+ <-> ( B e. RR /\ 0 < B ) ) |
19 |
17 3 18
|
3imtr4i |
|- ( B e. ( 1 (,) +oo ) -> B e. RR+ ) |
20 |
|
logltb |
|- ( ( 1 e. RR+ /\ B e. RR+ ) -> ( 1 < B <-> ( log ` 1 ) < ( log ` B ) ) ) |
21 |
9 19 20
|
sylancr |
|- ( B e. ( 1 (,) +oo ) -> ( 1 < B <-> ( log ` 1 ) < ( log ` B ) ) ) |
22 |
8 21
|
bitr4d |
|- ( B e. ( 1 (,) +oo ) -> ( 0 < ( log ` B ) <-> 1 < B ) ) |
23 |
4 22
|
mpbird |
|- ( B e. ( 1 (,) +oo ) -> 0 < ( log ` B ) ) |