Theorem logbge0b

Description: The logarithm of a number is nonnegative iff the number is greater than or equal to 1. (Contributed by AV, 30-May-2020)

	Ref	Expression
Assertion	logbge0b	|- ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ ) -> ( 0 <_ ( B logb X ) <-> 1 <_ X ) )

Proof

Step	Hyp	Ref	Expression
1		relogbval	|- ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ ) -> ( B logb X ) = ( ( log ` X ) / ( log ` B ) ) )
2	1	breq2d	|- ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ ) -> ( 0 <_ ( B logb X ) <-> 0 <_ ( ( log ` X ) / ( log ` B ) ) ) )
3		relogcl	|- ( X e. RR+ -> ( log ` X ) e. RR )
4	3	adantl	|- ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ ) -> ( log ` X ) e. RR )
5		eluz2nn	|- ( B e. ( ZZ>= ` 2 ) -> B e. NN )
6	5	nnrpd	|- ( B e. ( ZZ>= ` 2 ) -> B e. RR+ )
7		relogcl	|- ( B e. RR+ -> ( log ` B ) e. RR )
8	6 7	syl	|- ( B e. ( ZZ>= ` 2 ) -> ( log ` B ) e. RR )
9	8	adantr	|- ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ ) -> ( log ` B ) e. RR )
10		eluz2gt1	|- ( B e. ( ZZ>= ` 2 ) -> 1 < B )
11		loggt0b	|- ( B e. RR+ -> ( 0 < ( log ` B ) <-> 1 < B ) )
12	6 11	syl	|- ( B e. ( ZZ>= ` 2 ) -> ( 0 < ( log ` B ) <-> 1 < B ) )
13	10 12	mpbird	|- ( B e. ( ZZ>= ` 2 ) -> 0 < ( log ` B ) )
14	13	adantr	|- ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ ) -> 0 < ( log ` B ) )
15		ge0div	|- ( ( ( log ` X ) e. RR /\ ( log ` B ) e. RR /\ 0 < ( log ` B ) ) -> ( 0 <_ ( log ` X ) <-> 0 <_ ( ( log ` X ) / ( log ` B ) ) ) )
16	4 9 14 15	syl3anc	|- ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ ) -> ( 0 <_ ( log ` X ) <-> 0 <_ ( ( log ` X ) / ( log ` B ) ) ) )
17		logge0b	|- ( X e. RR+ -> ( 0 <_ ( log ` X ) <-> 1 <_ X ) )
18	17	adantl	|- ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ ) -> ( 0 <_ ( log ` X ) <-> 1 <_ X ) )
19	2 16 18	3bitr2d	|- ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ ) -> ( 0 <_ ( B logb X ) <-> 1 <_ X ) )