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 (1, +∞) \to 0 < \log B$

Step	Hyp	Ref	Expression
1		1xr	$⊢ 1 \in ℝ^{*}$
2		elioopnf	$⊢ 1 \in ℝ^{*} \to (B \in (1, +∞) \leftrightarrow (B \in ℝ \land 1 < B))$
3	1 2	ax-mp	$⊢ B \in (1, +∞) \leftrightarrow (B \in ℝ \land 1 < B)$
4	3	simprbi	$⊢ B \in (1, +∞) \to 1 < B$
5		log1	$⊢ \log 1 = 0$
6	5	eqcomi	$⊢ 0 = \log 1$
7	6	a1i	$⊢ B \in (1, +∞) \to 0 = \log 1$
8	7	breq1d	$⊢ B \in (1, +∞) \to (0 < \log B \leftrightarrow \log 1 < \log B)$
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	$⊢ (0 \in ℝ \land 1 \in ℝ \land B \in ℝ) \to ((0 < 1 \land 1 < B) \to 0 < B)$
15	11 12 13 14	syl3anc	$⊢ B \in ℝ \to ((0 < 1 \land 1 < B) \to 0 < B)$
16	10 15	mpani	$⊢ B \in ℝ \to (1 < B \to 0 < B)$
17	16	imdistani	$⊢ (B \in ℝ \land 1 < B) \to (B \in ℝ \land 0 < B)$
18		elrp	$⊢ B \in ℝ^{+} \leftrightarrow (B \in ℝ \land 0 < B)$
19	17 3 18	3imtr4i	$⊢ B \in (1, +∞) \to B \in ℝ^{+}$
20		logltb	$⊢ (1 \in ℝ^{+} \land B \in ℝ^{+}) \to (1 < B \leftrightarrow \log 1 < \log B)$
21	9 19 20	sylancr	$⊢ B \in (1, +∞) \to (1 < B \leftrightarrow \log 1 < \log B)$
22	8 21	bitr4d	$⊢ B \in (1, +∞) \to (0 < \log B \leftrightarrow 1 < B)$
23	4 22	mpbird	$⊢ B \in (1, +∞) \to 0 < \log B$

Metamath Proof Explorer