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

Metamath Proof Explorer

Theorem rege1logbrege0

Proof