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}\in \left(1,\mathrm{+\infty }\right)\to 0<\mathrm{log}{B}$

Proof

Step Hyp Ref Expression
1 1xr ${⊢}1\in {ℝ}^{*}$
2 elioopnf ${⊢}1\in {ℝ}^{*}\to \left({B}\in \left(1,\mathrm{+\infty }\right)↔\left({B}\in ℝ\wedge 1<{B}\right)\right)$
3 1 2 ax-mp ${⊢}{B}\in \left(1,\mathrm{+\infty }\right)↔\left({B}\in ℝ\wedge 1<{B}\right)$
4 3 simprbi ${⊢}{B}\in \left(1,\mathrm{+\infty }\right)\to 1<{B}$
5 log1 ${⊢}\mathrm{log}1=0$
6 5 eqcomi ${⊢}0=\mathrm{log}1$
7 6 a1i ${⊢}{B}\in \left(1,\mathrm{+\infty }\right)\to 0=\mathrm{log}1$
8 7 breq1d ${⊢}{B}\in \left(1,\mathrm{+\infty }\right)\to \left(0<\mathrm{log}{B}↔\mathrm{log}1<\mathrm{log}{B}\right)$
9 1rp ${⊢}1\in {ℝ}^{+}$
10 0lt1 ${⊢}0<1$
11 0red ${⊢}{B}\in ℝ\to 0\in ℝ$
12 1red ${⊢}{B}\in ℝ\to 1\in ℝ$
13 id ${⊢}{B}\in ℝ\to {B}\in ℝ$
14 lttr ${⊢}\left(0\in ℝ\wedge 1\in ℝ\wedge {B}\in ℝ\right)\to \left(\left(0<1\wedge 1<{B}\right)\to 0<{B}\right)$
15 11 12 13 14 syl3anc ${⊢}{B}\in ℝ\to \left(\left(0<1\wedge 1<{B}\right)\to 0<{B}\right)$
16 10 15 mpani ${⊢}{B}\in ℝ\to \left(1<{B}\to 0<{B}\right)$
17 16 imdistani ${⊢}\left({B}\in ℝ\wedge 1<{B}\right)\to \left({B}\in ℝ\wedge 0<{B}\right)$
18 elrp ${⊢}{B}\in {ℝ}^{+}↔\left({B}\in ℝ\wedge 0<{B}\right)$
19 17 3 18 3imtr4i ${⊢}{B}\in \left(1,\mathrm{+\infty }\right)\to {B}\in {ℝ}^{+}$
20 logltb ${⊢}\left(1\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\to \left(1<{B}↔\mathrm{log}1<\mathrm{log}{B}\right)$
21 9 19 20 sylancr ${⊢}{B}\in \left(1,\mathrm{+\infty }\right)\to \left(1<{B}↔\mathrm{log}1<\mathrm{log}{B}\right)$
22 8 21 bitr4d ${⊢}{B}\in \left(1,\mathrm{+\infty }\right)\to \left(0<\mathrm{log}{B}↔1<{B}\right)$
23 4 22 mpbird ${⊢}{B}\in \left(1,\mathrm{+\infty }\right)\to 0<\mathrm{log}{B}$