rege1logbzge0

Description: The general logarithm, with an integer base greater than 1, for a real number greater than or equal to 1 is greater than or equal to 0. (Contributed by AV, 25-May-2020)

		Ref	Expression
	Assertion	rege1logbzge0	$⊢ (B \in ℤ_{\geq 2} \land X \in [1, +∞)) \to 0 \leq \log_{B} X$

Proof

Step	Hyp	Ref	Expression
1		zre	$⊢ B \in ℤ \to B \in ℝ$
2	1	3ad2ant2	$⊢ (2 \in ℤ \land B \in ℤ \land 2 \leq B) \to B \in ℝ$
3		1lt2	$⊢ 1 < 2$
4		1re	$⊢ 1 \in ℝ$
5	4	a1i	$⊢ (2 \in ℤ \land B \in ℤ) \to 1 \in ℝ$
6		2re	$⊢ 2 \in ℝ$
7	6	a1i	$⊢ (2 \in ℤ \land B \in ℤ) \to 2 \in ℝ$
8	1	adantl	$⊢ (2 \in ℤ \land B \in ℤ) \to B \in ℝ$
9		ltletr	$⊢ (1 \in ℝ \land 2 \in ℝ \land B \in ℝ) \to ((1 < 2 \land 2 \leq B) \to 1 < B)$
10	5 7 8 9	syl3anc	$⊢ (2 \in ℤ \land B \in ℤ) \to ((1 < 2 \land 2 \leq B) \to 1 < B)$
11	3 10	mpani	$⊢ (2 \in ℤ \land B \in ℤ) \to (2 \leq B \to 1 < B)$
12	11	3impia	$⊢ (2 \in ℤ \land B \in ℤ \land 2 \leq B) \to 1 < B$
13	2 12	jca	$⊢ (2 \in ℤ \land B \in ℤ \land 2 \leq B) \to (B \in ℝ \land 1 < B)$
14		eluz2	$⊢ B \in ℤ_{\geq 2} \leftrightarrow (2 \in ℤ \land B \in ℤ \land 2 \leq B)$
15		1xr	$⊢ 1 \in ℝ^{*}$
16		elioopnf	$⊢ 1 \in ℝ^{*} \to (B \in (1, +∞) \leftrightarrow (B \in ℝ \land 1 < B))$
17	15 16	ax-mp	$⊢ B \in (1, +∞) \leftrightarrow (B \in ℝ \land 1 < B)$
18	13 14 17	3imtr4i	$⊢ B \in ℤ_{\geq 2} \to B \in (1, +∞)$
19		rege1logbrege0	$⊢ (B \in (1, +∞) \land X \in [1, +∞)) \to 0 \leq \log_{B} X$
20	18 19	sylan	$⊢ (B \in ℤ_{\geq 2} \land X \in [1, +∞)) \to 0 \leq \log_{B} X$

Metamath Proof Explorer

Theorem rege1logbzge0

Proof