rplogcl

Description: Closure of the logarithm function in the positive reals. (Contributed by Mario Carneiro, 21-Sep-2014)

		Ref	Expression
	Assertion	rplogcl	$⊢ (A \in ℝ \land 1 < A) \to \log A \in ℝ^{+}$

Step	Hyp	Ref	Expression
1		simpl	$⊢ (A \in ℝ \land 1 < A) \to A \in ℝ$
2		0red	$⊢ (A \in ℝ \land 1 < A) \to 0 \in ℝ$
3		1red	$⊢ (A \in ℝ \land 1 < A) \to 1 \in ℝ$
4		0lt1	$⊢ 0 < 1$
5	4	a1i	$⊢ (A \in ℝ \land 1 < A) \to 0 < 1$
6		simpr	$⊢ (A \in ℝ \land 1 < A) \to 1 < A$
7	2 3 1 5 6	lttrd	$⊢ (A \in ℝ \land 1 < A) \to 0 < A$
8	1 7	elrpd	$⊢ (A \in ℝ \land 1 < A) \to A \in ℝ^{+}$
9		relogcl	$⊢ A \in ℝ^{+} \to \log A \in ℝ$
10	8 9	syl	$⊢ (A \in ℝ \land 1 < A) \to \log A \in ℝ$
11		log1	$⊢ \log 1 = 0$
12		1rp	$⊢ 1 \in ℝ^{+}$
13		logltb	$⊢ (1 \in ℝ^{+} \land A \in ℝ^{+}) \to (1 < A \leftrightarrow \log 1 < \log A)$
14	12 8 13	sylancr	$⊢ (A \in ℝ \land 1 < A) \to (1 < A \leftrightarrow \log 1 < \log A)$
15	6 14	mpbid	$⊢ (A \in ℝ \land 1 < A) \to \log 1 < \log A$
16	11 15	eqbrtrrid	$⊢ (A \in ℝ \land 1 < A) \to 0 < \log A$
17	10 16	elrpd	$⊢ (A \in ℝ \land 1 < A) \to \log A \in ℝ^{+}$

Metamath Proof Explorer