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	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ran log )

Proof

Step	Hyp	Ref	Expression
1		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
2		pipos	⊢ 0 < π
3		pire	⊢ π ∈ ℝ
4		lt0neg2	⊢ ( π ∈ ℝ → ( 0 < π ↔ - π < 0 ) )
5	3 4	ax-mp	⊢ ( 0 < π ↔ - π < 0 )
6	2 5	mpbi	⊢ - π < 0
7		reim0	⊢ ( 𝐴 ∈ ℝ → ( ℑ ‘ 𝐴 ) = 0 )
8	6 7	breqtrrid	⊢ ( 𝐴 ∈ ℝ → - π < ( ℑ ‘ 𝐴 ) )
9		0re	⊢ 0 ∈ ℝ
10	9 3 2	ltleii	⊢ 0 ≤ π
11	7 10	eqbrtrdi	⊢ ( 𝐴 ∈ ℝ → ( ℑ ‘ 𝐴 ) ≤ π )
12		ellogrn	⊢ ( 𝐴 ∈ ran log ↔ ( 𝐴 ∈ ℂ ∧ - π < ( ℑ ‘ 𝐴 ) ∧ ( ℑ ‘ 𝐴 ) ≤ π ) )
13	1 8 11 12	syl3anbrc	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ran log )