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