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

Metamath Proof Explorer

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

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