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

Proof

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