Step |
Hyp |
Ref |
Expression |
1 |
|
logrncl |
|- ( ( A e. CC /\ A =/= 0 ) -> ( log ` A ) e. ran log ) |
2 |
|
ellogrn |
|- ( ( log ` A ) e. ran log <-> ( ( log ` A ) e. CC /\ -u _pi < ( Im ` ( log ` A ) ) /\ ( Im ` ( log ` A ) ) <_ _pi ) ) |
3 |
1 2
|
sylib |
|- ( ( A e. CC /\ A =/= 0 ) -> ( ( log ` A ) e. CC /\ -u _pi < ( Im ` ( log ` A ) ) /\ ( Im ` ( log ` A ) ) <_ _pi ) ) |
4 |
|
3simpc |
|- ( ( ( log ` A ) e. CC /\ -u _pi < ( Im ` ( log ` A ) ) /\ ( Im ` ( log ` A ) ) <_ _pi ) -> ( -u _pi < ( Im ` ( log ` A ) ) /\ ( Im ` ( log ` A ) ) <_ _pi ) ) |
5 |
3 4
|
syl |
|- ( ( A e. CC /\ A =/= 0 ) -> ( -u _pi < ( Im ` ( log ` A ) ) /\ ( Im ` ( log ` A ) ) <_ _pi ) ) |