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

Metamath Proof Explorer

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 ran log$

Proof

Step	Hyp	Ref	Expression
1		recn	$⊢ A \in ℝ \to A \in ℂ$
2		pipos	$⊢ 0 < π$
3		pire	$⊢ π \in ℝ$
4		lt0neg2	$⊢ π \in ℝ \to (0 < π \leftrightarrow - π < 0)$
5	3 4	ax-mp	$⊢ 0 < π \leftrightarrow - π < 0$
6	2 5	mpbi	$⊢ - π < 0$
7		reim0	$⊢ A \in ℝ \to ℑ (A) = 0$
8	6 7	breqtrrid	$⊢ A \in ℝ \to - π < ℑ (A)$
9		0re	$⊢ 0 \in ℝ$
10	9 3 2	ltleii	$⊢ 0 \leq π$
11	7 10	eqbrtrdi	$⊢ A \in ℝ \to ℑ (A) \leq π$
12		ellogrn	$⊢ A \in ran log \leftrightarrow (A \in ℂ \land - π < ℑ (A) \land ℑ (A) \leq π)$
13	1 8 11 12	syl3anbrc	$⊢ A \in ℝ \to A \in ran log$