Theorem loggt0b

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

	Ref	Expression
Assertion	loggt0b	|- ( A e. RR+ -> ( 0 < ( log ` A ) <-> 1 < A ) )

Proof

Step	Hyp	Ref	Expression
1		1rp	|- 1 e. RR+
2		logltb	|- ( ( 1 e. RR+ /\ A e. RR+ ) -> ( 1 < A <-> ( log ` 1 ) < ( log ` A ) ) )
3	1 2	mpan	|- ( A e. RR+ -> ( 1 < A <-> ( log ` 1 ) < ( log ` A ) ) )
4		log1	|- ( log ` 1 ) = 0
5	4	a1i	|- ( A e. RR+ -> ( log ` 1 ) = 0 )
6	5	breq1d	|- ( A e. RR+ -> ( ( log ` 1 ) < ( log ` A ) <-> 0 < ( log ` A ) ) )
7	3 6	bitr2d	|- ( A e. RR+ -> ( 0 < ( log ` A ) <-> 1 < A ) )