Theorem logblt1b

Description: The logarithm of a number is less than 1 iff the number is less than the base of the logarithm. (Contributed by AV, 30-May-2020)

	Ref	Expression
Assertion	logblt1b	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\right)\to \left({\log }_{B}X<1\leftrightarrow X<B\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	breq1d	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\right)\to \left({\log }_{B}X<1\leftrightarrow \frac{\log X}{\log B}<1\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		1red	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\right)\to 1\in ℝ$$
6		eluz2nn	$$⊢B\in {\mathbb{Z}}_{\ge 2}\to B\in \mathbb{N}$$
7	6	nnrpd	$$⊢B\in {\mathbb{Z}}_{\ge 2}\to B\in {ℝ}^{+}$$
8		relogcl	$$⊢B\in {ℝ}^{+}\to \log B\in ℝ$$
9	7 8	syl	$$⊢B\in {\mathbb{Z}}_{\ge 2}\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	7 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	9 13	jca	$$⊢B\in {\mathbb{Z}}_{\ge 2}\to \left(\log B\in ℝ\wedge 0<\log B\right)$$
15	14	adantr	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\right)\to \left(\log B\in ℝ\wedge 0<\log B\right)$$
16		ltdivmul	$$⊢\left(\log X\in ℝ\wedge 1\in ℝ\wedge \left(\log B\in ℝ\wedge 0<\log B\right)\right)\to \left(\frac{\log X}{\log B}<1\leftrightarrow \log X<\log B\cdot 1\right)$$
17	4 5 15 16	syl3anc	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\right)\to \left(\frac{\log X}{\log B}<1\leftrightarrow \log X<\log B\cdot 1\right)$$
18	9	recnd	$$⊢B\in {\mathbb{Z}}_{\ge 2}\to \log B\in ℂ$$
19	18	mulid1d	$$⊢B\in {\mathbb{Z}}_{\ge 2}\to \log B\cdot 1=\log B$$
20	19	adantr	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\right)\to \log B\cdot 1=\log B$$
21	20	breq2d	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\right)\to \left(\log X<\log B\cdot 1\leftrightarrow \log X<\log B\right)$$
22	7	anim2i	$$⊢\left(X\in {ℝ}^{+}\wedge B\in {\mathbb{Z}}_{\ge 2}\right)\to \left(X\in {ℝ}^{+}\wedge B\in {ℝ}^{+}\right)$$
23	22	ancoms	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\right)\to \left(X\in {ℝ}^{+}\wedge B\in {ℝ}^{+}\right)$$
24		logltb	$$⊢\left(X\in {ℝ}^{+}\wedge B\in {ℝ}^{+}\right)\to \left(X<B\leftrightarrow \log X<\log B\right)$$
25	24	bicomd	$$⊢\left(X\in {ℝ}^{+}\wedge B\in {ℝ}^{+}\right)\to \left(\log X<\log B\leftrightarrow X<B\right)$$
26	23 25	syl	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\right)\to \left(\log X<\log B\leftrightarrow X<B\right)$$
27	21 26	bitrd	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\right)\to \left(\log X<\log B\cdot 1\leftrightarrow X<B\right)$$
28	17 27	bitrd	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\right)\to \left(\frac{\log X}{\log B}<1\leftrightarrow X<B\right)$$
29	2 28	bitrd	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\right)\to \left({\log }_{B}X<1\leftrightarrow X<B\right)$$