Theorem logge0b

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	logge0b	|- ( A e. RR+ -> ( 0 <_ ( log ` A ) <-> 1 <_ A ) )

Proof

Step	Hyp	Ref	Expression
1		1rp	|- 1 e. RR+
2	1	a1i	|- ( A e. RR+ -> 1 e. RR+ )
3		id	|- ( A e. RR+ -> A e. RR+ )
4	2 3	logled	|- ( A e. RR+ -> ( 1 <_ A <-> ( log ` 1 ) <_ ( log ` A ) ) )
5		log1	|- ( log ` 1 ) = 0
6	5	a1i	|- ( A e. RR+ -> ( log ` 1 ) = 0 )
7	6	breq1d	|- ( A e. RR+ -> ( ( log ` 1 ) <_ ( log ` A ) <-> 0 <_ ( log ` A ) ) )
8	4 7	bitr2d	|- ( A e. RR+ -> ( 0 <_ ( log ` A ) <-> 1 <_ A ) )