Metamath Proof Explorer

Theorem logrncn

Description: The range of the natural logarithm function is a subset of the complex numbers. (Contributed by Mario Carneiro, 13-May-2014)

Ref Expression
Assertion logrncn 
|- ( A e. ran log -> A e. CC )

Proof

Step Hyp Ref Expression
1 ellogrn 
 |-  ( A e. ran log <-> ( A e. CC /\ -u _pi < ( Im ` A ) /\ ( Im ` A ) <_ _pi ) )
2 1 simp1bi 
 |-  ( A e. ran log -> A e. CC )