Theorem rplogcl

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

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

Proof

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