Theorem logbge0b

Description: The logarithm of a number is nonnegative iff the number is greater than or equal to 1. (Contributed by AV, 30-May-2020)

	Ref	Expression
Assertion	logbge0b	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\right)\to \left(0\le {\log }_{B}X\leftrightarrow 1\le X\right)$$

Proof

Step	Hyp	Ref	Expression
1		relogbval	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\right)\to {\log }_{B}X=\frac{\log X}{\log B}$$
2	1	breq2d	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\right)\to \left(0\le {\log }_{B}X\leftrightarrow 0\le \frac{\log X}{\log B}\right)$$
3		relogcl	$$⊢X\in {ℝ}^{+}\to \log X\in ℝ$$
4	3	adantl	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\right)\to \log X\in ℝ$$
5		eluz2nn	$$⊢B\in {\mathbb{Z}}_{\ge 2}\to B\in \mathbb{N}$$
6	5	nnrpd	$$⊢B\in {\mathbb{Z}}_{\ge 2}\to B\in {ℝ}^{+}$$
7		relogcl	$$⊢B\in {ℝ}^{+}\to \log B\in ℝ$$
8	6 7	syl	$$⊢B\in {\mathbb{Z}}_{\ge 2}\to \log B\in ℝ$$
9	8	adantr	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\right)\to \log B\in ℝ$$
10		eluz2gt1	$$⊢B\in {\mathbb{Z}}_{\ge 2}\to 1<B$$
11		loggt0b	$$⊢B\in {ℝ}^{+}\to \left(0<\log B\leftrightarrow 1<B\right)$$
12	6 11	syl	$$⊢B\in {\mathbb{Z}}_{\ge 2}\to \left(0<\log B\leftrightarrow 1<B\right)$$
13	10 12	mpbird	$$⊢B\in {\mathbb{Z}}_{\ge 2}\to 0<\log B$$
14	13	adantr	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\right)\to 0<\log B$$
15		ge0div	$$⊢\left(\log X\in ℝ\wedge \log B\in ℝ\wedge 0<\log B\right)\to \left(0\le \log X\leftrightarrow 0\le \frac{\log X}{\log B}\right)$$
16	4 9 14 15	syl3anc	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\right)\to \left(0\le \log X\leftrightarrow 0\le \frac{\log X}{\log B}\right)$$
17		logge0b	$$⊢X\in {ℝ}^{+}\to \left(0\le \log X\leftrightarrow 1\le X\right)$$
18	17	adantl	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\right)\to \left(0\le \log X\leftrightarrow 1\le X\right)$$
19	2 16 18	3bitr2d	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\right)\to \left(0\le {\log }_{B}X\leftrightarrow 1\le X\right)$$