Theorem 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	⊢ ( ( 𝐵 ∈ ( 1 (,) +∞ ) ∧ 𝑋 ∈ ( 1 [,) +∞ ) ) → 0 ≤ ( 𝐵 logb 𝑋 ) )

Proof

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