Theorem relogrn

Description: The range of the natural logarithm function includes the real numbers. (Contributed by Paul Chapman, 21-Apr-2008) (Proof shortened by Mario Carneiro, 1-Apr-2015)

	Ref	Expression
Assertion	relogrn	$$⊢A\in ℝ\to A\in \mathrm{ran}log$$

Proof

Step	Hyp	Ref	Expression
1		recn	$$⊢A\in ℝ\to A\in ℂ$$
2		pipos	$$⊢0<\mathrm{\pi }$$
3		pire	$$⊢\mathrm{\pi }\in ℝ$$
4		lt0neg2	$$⊢\mathrm{\pi }\in ℝ\to \left(0<\mathrm{\pi }\leftrightarrow -\mathrm{\pi }<0\right)$$
5	3 4	ax-mp	$$⊢0<\mathrm{\pi }\leftrightarrow -\mathrm{\pi }<0$$
6	2 5	mpbi	$$⊢-\mathrm{\pi }<0$$
7		reim0	$$⊢A\in ℝ\to \Im \left(A\right)=0$$
8	6 7	breqtrrid	$$⊢A\in ℝ\to -\mathrm{\pi }<\Im \left(A\right)$$
9		0re	$$⊢0\in ℝ$$
10	9 3 2	ltleii	$$⊢0\le \mathrm{\pi }$$
11	7 10	eqbrtrdi	$$⊢A\in ℝ\to \Im \left(A\right)\le \mathrm{\pi }$$
12		ellogrn	$$⊢A\in \mathrm{ran}log\leftrightarrow \left(A\in ℂ\wedge -\mathrm{\pi }<\Im \left(A\right)\wedge \Im \left(A\right)\le \mathrm{\pi }\right)$$
13	1 8 11 12	syl3anbrc	$$⊢A\in ℝ\to A\in \mathrm{ran}log$$