logge0

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

		Ref	Expression
	Assertion	logge0	$⊢ (A \in ℝ \land 1 \leq A) \to 0 \leq \log A$

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

Metamath Proof Explorer