This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 (0 \leq \log A \leftrightarrow 1 \leq A)$

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 (1 \leq A \leftrightarrow \log 1 \leq \log A)$
5		log1	$⊢ \log 1 = 0$
6	5	a1i	$⊢ A \in ℝ^{+} \to \log 1 = 0$
7	6	breq1d	$⊢ A \in ℝ^{+} \to (\log 1 \leq \log A \leftrightarrow 0 \leq \log A)$
8	4 7	bitr2d	$⊢ A \in ℝ^{+} \to (0 \leq \log A \leftrightarrow 1 \leq A)$