Theorem logge0

Description: The logarithm of a number greater than 1 is nonnegative. (Contributed by Mario Carneiro, 29-May-2016)

	Ref	Expression
Assertion	logge0	$$⊢\left(A\in ℝ\wedge 1\le A\right)\to 0\le \log A$$

Proof

Step	Hyp	Ref	Expression
1		log1	$$⊢\log 1=0$$
2		simpr	$$⊢\left(A\in ℝ\wedge 1\le A\right)\to 1\le A$$
3		1rp	$$⊢1\in {ℝ}^{+}$$
4		rpgecl	$$⊢\left(1\in {ℝ}^{+}\wedge A\in ℝ\wedge 1\le A\right)\to A\in {ℝ}^{+}$$
5	3 4	mp3an1	$$⊢\left(A\in ℝ\wedge 1\le A\right)\to A\in {ℝ}^{+}$$
6		logleb	$$⊢\left(1\in {ℝ}^{+}\wedge A\in {ℝ}^{+}\right)\to \left(1\le A\leftrightarrow \log 1\le \log A\right)$$
7	3 5 6	sylancr	$$⊢\left(A\in ℝ\wedge 1\le A\right)\to \left(1\le A\leftrightarrow \log 1\le \log A\right)$$
8	2 7	mpbid	$$⊢\left(A\in ℝ\wedge 1\le A\right)\to \log 1\le \log A$$
9	1 8	eqbrtrrid	$$⊢\left(A\in ℝ\wedge 1\le A\right)\to 0\le \log A$$