Theorem rege1logbzge0

Description: The general logarithm, with an integer 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	rege1logbzge0	|- ( ( B e. ( ZZ>= ` 2 ) /\ X e. ( 1 [,) +oo ) ) -> 0 <_ ( B logb X ) )

Proof

Step	Hyp	Ref	Expression
1		zre	|- ( B e. ZZ -> B e. RR )
2	1	3ad2ant2	|- ( ( 2 e. ZZ /\ B e. ZZ /\ 2 <_ B ) -> B e. RR )
3		1lt2	|- 1 < 2
4		1re	|- 1 e. RR
5	4	a1i	|- ( ( 2 e. ZZ /\ B e. ZZ ) -> 1 e. RR )
6		2re	|- 2 e. RR
7	6	a1i	|- ( ( 2 e. ZZ /\ B e. ZZ ) -> 2 e. RR )
8	1	adantl	|- ( ( 2 e. ZZ /\ B e. ZZ ) -> B e. RR )
9		ltletr	|- ( ( 1 e. RR /\ 2 e. RR /\ B e. RR ) -> ( ( 1 < 2 /\ 2 <_ B ) -> 1 < B ) )
10	5 7 8 9	syl3anc	|- ( ( 2 e. ZZ /\ B e. ZZ ) -> ( ( 1 < 2 /\ 2 <_ B ) -> 1 < B ) )
11	3 10	mpani	|- ( ( 2 e. ZZ /\ B e. ZZ ) -> ( 2 <_ B -> 1 < B ) )
12	11	3impia	|- ( ( 2 e. ZZ /\ B e. ZZ /\ 2 <_ B ) -> 1 < B )
13	2 12	jca	|- ( ( 2 e. ZZ /\ B e. ZZ /\ 2 <_ B ) -> ( B e. RR /\ 1 < B ) )
14		eluz2	|- ( B e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ B e. ZZ /\ 2 <_ B ) )
15		1xr	|- 1 e. RR*
16		elioopnf	|- ( 1 e. RR* -> ( B e. ( 1 (,) +oo ) <-> ( B e. RR /\ 1 < B ) ) )
17	15 16	ax-mp	|- ( B e. ( 1 (,) +oo ) <-> ( B e. RR /\ 1 < B ) )
18	13 14 17	3imtr4i	|- ( B e. ( ZZ>= ` 2 ) -> B e. ( 1 (,) +oo ) )
19		rege1logbrege0	|- ( ( B e. ( 1 (,) +oo ) /\ X e. ( 1 [,) +oo ) ) -> 0 <_ ( B logb X ) )
20	18 19	sylan	|- ( ( B e. ( ZZ>= ` 2 ) /\ X e. ( 1 [,) +oo ) ) -> 0 <_ ( B logb X ) )