Metamath Proof Explorer


Theorem regt1loggt0

Description: The natural logarithm for a real number greater than 1 is greater than 0. (Contributed by AV, 25-May-2020)

Ref Expression
Assertion regt1loggt0 B 1 +∞ 0 < log B

Proof

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