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\in {ℝ}^{+}\to \left(0<\log A\leftrightarrow 1<A\right)$$

Proof

Step	Hyp	Ref	Expression
1		1rp	$$⊢1\in {ℝ}^{+}$$
2		logltb	$$⊢\left(1\in {ℝ}^{+}\wedge A\in {ℝ}^{+}\right)\to \left(1<A\leftrightarrow \log 1<\log A\right)$$
3	1 2	mpan	$$⊢A\in {ℝ}^{+}\to \left(1<A\leftrightarrow \log 1<\log A\right)$$
4		log1	$$⊢\log 1=0$$
5	4	a1i	$$⊢A\in {ℝ}^{+}\to \log 1=0$$
6	5	breq1d	$$⊢A\in {ℝ}^{+}\to \left(\log 1<\log A\leftrightarrow 0<\log A\right)$$
7	3 6	bitr2d	$$⊢A\in {ℝ}^{+}\to \left(0<\log A\leftrightarrow 1<A\right)$$