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<\log B$$

Proof

Step	Hyp	Ref	Expression
1		1xr	$$⊢1\in {ℝ}^{*}$$
2		elioopnf	$$⊢1\in {ℝ}^{*}\to \left(B\in \left(1,\mathrm{+\infty }\right)\leftrightarrow \left(B\in ℝ\wedge 1<B\right)\right)$$
3	1 2	ax-mp	$$⊢B\in \left(1,\mathrm{+\infty }\right)\leftrightarrow \left(B\in ℝ\wedge 1<B\right)$$
4	3	simprbi	$$⊢B\in \left(1,\mathrm{+\infty }\right)\to 1<B$$
5		log1	$$⊢\log 1=0$$
6	5	eqcomi	$$⊢0=\log 1$$
7	6	a1i	$$⊢B\in \left(1,\mathrm{+\infty }\right)\to 0=\log 1$$
8	7	breq1d	$$⊢B\in \left(1,\mathrm{+\infty }\right)\to \left(0<\log B\leftrightarrow \log 1<\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 {ℝ}^{+}\leftrightarrow \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\leftrightarrow \log 1<\log B\right)$$
21	9 19 20	sylancr	$$⊢B\in \left(1,\mathrm{+\infty }\right)\to \left(1<B\leftrightarrow \log 1<\log B\right)$$
22	8 21	bitr4d	$$⊢B\in \left(1,\mathrm{+\infty }\right)\to \left(0<\log B\leftrightarrow 1<B\right)$$
23	4 22	mpbird	$$⊢B\in \left(1,\mathrm{+\infty }\right)\to 0<\log B$$