rege1logbrege0

Description: The general logarithm, with a real 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	rege1logbrege0	$⊢ (B \in (1, +∞) \land X \in [1, +∞)) \to 0 \leq \log_{B} X$

Proof

Step	Hyp	Ref	Expression
1		1re	$⊢ 1 \in ℝ$
2		elicopnf	$⊢ 1 \in ℝ \to (X \in [1, +∞) \leftrightarrow (X \in ℝ \land 1 \leq X))$
3	1 2	ax-mp	$⊢ X \in [1, +∞) \leftrightarrow (X \in ℝ \land 1 \leq X)$
4		id	$⊢ (X \in ℝ \land 1 \leq X) \to (X \in ℝ \land 1 \leq X)$
5	3 4	sylbi	$⊢ X \in [1, +∞) \to (X \in ℝ \land 1 \leq X)$
6	5	adantl	$⊢ (B \in (1, +∞) \land X \in [1, +∞)) \to (X \in ℝ \land 1 \leq X)$
7		logge0	$⊢ (X \in ℝ \land 1 \leq X) \to 0 \leq \log X$
8	6 7	syl	$⊢ (B \in (1, +∞) \land X \in [1, +∞)) \to 0 \leq \log X$
9		simpl	$⊢ (X \in ℝ \land 1 \leq X) \to X \in ℝ$
10		0lt1	$⊢ 0 < 1$
11		0red	$⊢ X \in ℝ \to 0 \in ℝ$
12		1red	$⊢ X \in ℝ \to 1 \in ℝ$
13		id	$⊢ X \in ℝ \to X \in ℝ$
14		ltletr	$⊢ (0 \in ℝ \land 1 \in ℝ \land X \in ℝ) \to ((0 < 1 \land 1 \leq X) \to 0 < X)$
15	11 12 13 14	syl3anc	$⊢ X \in ℝ \to ((0 < 1 \land 1 \leq X) \to 0 < X)$
16	10 15	mpani	$⊢ X \in ℝ \to (1 \leq X \to 0 < X)$
17	16	imp	$⊢ (X \in ℝ \land 1 \leq X) \to 0 < X$
18	9 17	elrpd	$⊢ (X \in ℝ \land 1 \leq X) \to X \in ℝ^{+}$
19	3 18	sylbi	$⊢ X \in [1, +∞) \to X \in ℝ^{+}$
20	19	relogcld	$⊢ X \in [1, +∞) \to \log X \in ℝ$
21	20	adantl	$⊢ (B \in (1, +∞) \land X \in [1, +∞)) \to \log X \in ℝ$
22		1xr	$⊢ 1 \in ℝ^{*}$
23		elioopnf	$⊢ 1 \in ℝ^{*} \to (B \in (1, +∞) \leftrightarrow (B \in ℝ \land 1 < B))$
24	22 23	ax-mp	$⊢ B \in (1, +∞) \leftrightarrow (B \in ℝ \land 1 < B)$
25		simpl	$⊢ (B \in ℝ \land 1 < B) \to B \in ℝ$
26		0red	$⊢ B \in ℝ \to 0 \in ℝ$
27		1red	$⊢ B \in ℝ \to 1 \in ℝ$
28		id	$⊢ B \in ℝ \to B \in ℝ$
29		lttr	$⊢ (0 \in ℝ \land 1 \in ℝ \land B \in ℝ) \to ((0 < 1 \land 1 < B) \to 0 < B)$
30	26 27 28 29	syl3anc	$⊢ B \in ℝ \to ((0 < 1 \land 1 < B) \to 0 < B)$
31	10 30	mpani	$⊢ B \in ℝ \to (1 < B \to 0 < B)$
32	31	imp	$⊢ (B \in ℝ \land 1 < B) \to 0 < B$
33	25 32	elrpd	$⊢ (B \in ℝ \land 1 < B) \to B \in ℝ^{+}$
34	24 33	sylbi	$⊢ B \in (1, +∞) \to B \in ℝ^{+}$
35	34	relogcld	$⊢ B \in (1, +∞) \to \log B \in ℝ$
36	35	adantr	$⊢ (B \in (1, +∞) \land X \in [1, +∞)) \to \log B \in ℝ$
37		regt1loggt0	$⊢ B \in (1, +∞) \to 0 < \log B$
38	37	adantr	$⊢ (B \in (1, +∞) \land X \in [1, +∞)) \to 0 < \log B$
39		ge0div	$⊢ (\log X \in ℝ \land \log B \in ℝ \land 0 < \log B) \to (0 \leq \log X \leftrightarrow 0 \leq \frac{\log X}{\log B})$
40	21 36 38 39	syl3anc	$⊢ (B \in (1, +∞) \land X \in [1, +∞)) \to (0 \leq \log X \leftrightarrow 0 \leq \frac{\log X}{\log B})$
41	8 40	mpbid	$⊢ (B \in (1, +∞) \land X \in [1, +∞)) \to 0 \leq \frac{\log X}{\log B}$
42		recn	$⊢ B \in ℝ \to B \in ℂ$
43	42	adantr	$⊢ (B \in ℝ \land 1 < B) \to B \in ℂ$
44	32	gt0ne0d	$⊢ (B \in ℝ \land 1 < B) \to B \neq 0$
45	27 28	ltlend	$⊢ B \in ℝ \to (1 < B \leftrightarrow (1 \leq B \land B \neq 1))$
46	45	simplbda	$⊢ (B \in ℝ \land 1 < B) \to B \neq 1$
47	43 44 46	3jca	$⊢ (B \in ℝ \land 1 < B) \to (B \in ℂ \land B \neq 0 \land B \neq 1)$
48		eldifpr	$⊢ B \in (ℂ ∖ \{0, 1\}) \leftrightarrow (B \in ℂ \land B \neq 0 \land B \neq 1)$
49	47 24 48	3imtr4i	$⊢ B \in (1, +∞) \to B \in (ℂ ∖ \{0, 1\})$
50		recn	$⊢ X \in ℝ \to X \in ℂ$
51	50	adantr	$⊢ (X \in ℝ \land 1 \leq X) \to X \in ℂ$
52	17	gt0ne0d	$⊢ (X \in ℝ \land 1 \leq X) \to X \neq 0$
53	51 52	jca	$⊢ (X \in ℝ \land 1 \leq X) \to (X \in ℂ \land X \neq 0)$
54		eldifsn	$⊢ X \in (ℂ ∖ \{0\}) \leftrightarrow (X \in ℂ \land X \neq 0)$
55	53 3 54	3imtr4i	$⊢ X \in [1, +∞) \to X \in (ℂ ∖ \{0\})$
56		logbval	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land X \in (ℂ ∖ \{0\})) \to \log_{B} X = \frac{\log X}{\log B}$
57	49 55 56	syl2an	$⊢ (B \in (1, +∞) \land X \in [1, +∞)) \to \log_{B} X = \frac{\log X}{\log B}$
58	41 57	breqtrrd	$⊢ (B \in (1, +∞) \land X \in [1, +∞)) \to 0 \leq \log_{B} X$

Metamath Proof Explorer

Theorem rege1logbrege0

Proof