Metamath Proof Explorer

Theorem ellogrn

Description: Write out the property A e. ran log explicitly. (Contributed by Mario Carneiro, 1-Apr-2015)

Ref Expression
Assertion ellogrn 
|- ( A e. ran log <-> ( A e. CC /\ -u _pi < ( Im ` A ) /\ ( Im ` A ) <_ _pi ) )

Proof

Step Hyp Ref Expression
1 imf 
 |-  Im : CC --> RR
2 ffn 
 |-  ( Im : CC --> RR -> Im Fn CC )
3 elpreima 
 |-  ( Im Fn CC -> ( A e. ( `' Im " ( -u _pi (,] _pi ) ) <-> ( A e. CC /\ ( Im ` A ) e. ( -u _pi (,] _pi ) ) ) )
4 1 2 3 mp2b 
 |-  ( A e. ( `' Im " ( -u _pi (,] _pi ) ) <-> ( A e. CC /\ ( Im ` A ) e. ( -u _pi (,] _pi ) ) )
5 pire 
 |-  _pi e. RR
6 5 renegcli 
 |-  -u _pi e. RR
7 6 rexri 
 |-  -u _pi e. RR*
8 elioc2 
 |-  ( ( -u _pi e. RR* /\ _pi e. RR ) -> ( ( Im ` A ) e. ( -u _pi (,] _pi ) <-> ( ( Im ` A ) e. RR /\ -u _pi < ( Im ` A ) /\ ( Im ` A ) <_ _pi ) ) )
9 7 5 8 mp2an 
 |-  ( ( Im ` A ) e. ( -u _pi (,] _pi ) <-> ( ( Im ` A ) e. RR /\ -u _pi < ( Im ` A ) /\ ( Im ` A ) <_ _pi ) )
10 3anass 
 |-  ( ( ( Im ` A ) e. RR /\ -u _pi < ( Im ` A ) /\ ( Im ` A ) <_ _pi ) <-> ( ( Im ` A ) e. RR /\ ( -u _pi < ( Im ` A ) /\ ( Im ` A ) <_ _pi ) ) )
11 9 10 bitri 
 |-  ( ( Im ` A ) e. ( -u _pi (,] _pi ) <-> ( ( Im ` A ) e. RR /\ ( -u _pi < ( Im ` A ) /\ ( Im ` A ) <_ _pi ) ) )
12 imcl 
 |-  ( A e. CC -> ( Im ` A ) e. RR )
13 12 biantrurd 
 |-  ( A e. CC -> ( ( -u _pi < ( Im ` A ) /\ ( Im ` A ) <_ _pi ) <-> ( ( Im ` A ) e. RR /\ ( -u _pi < ( Im ` A ) /\ ( Im ` A ) <_ _pi ) ) ) )
14 11 13 bitr4id 
 |-  ( A e. CC -> ( ( Im ` A ) e. ( -u _pi (,] _pi ) <-> ( -u _pi < ( Im ` A ) /\ ( Im ` A ) <_ _pi ) ) )
15 14 pm5.32i 
 |-  ( ( A e. CC /\ ( Im ` A ) e. ( -u _pi (,] _pi ) ) <-> ( A e. CC /\ ( -u _pi < ( Im ` A ) /\ ( Im ` A ) <_ _pi ) ) )
16 4 15 bitri 
 |-  ( A e. ( `' Im " ( -u _pi (,] _pi ) ) <-> ( A e. CC /\ ( -u _pi < ( Im ` A ) /\ ( Im ` A ) <_ _pi ) ) )
17 logrn 
 |-  ran log = ( `' Im " ( -u _pi (,] _pi ) )
18 17 eleq2i 
 |-  ( A e. ran log <-> A e. ( `' Im " ( -u _pi (,] _pi ) ) )
19 3anass 
 |-  ( ( A e. CC /\ -u _pi < ( Im ` A ) /\ ( Im ` A ) <_ _pi ) <-> ( A e. CC /\ ( -u _pi < ( Im ` A ) /\ ( Im ` A ) <_ _pi ) ) )
20 16 18 19 3bitr4i 
 |-  ( A e. ran log <-> ( A e. CC /\ -u _pi < ( Im ` A ) /\ ( Im ` A ) <_ _pi ) )