Step |
Hyp |
Ref |
Expression |
1 |
|
logrncn |
|- ( A e. ran log -> A e. CC ) |
2 |
1
|
adantr |
|- ( ( A e. ran log /\ -. -u _pi = -u ( Im ` A ) ) -> A e. CC ) |
3 |
2
|
negcld |
|- ( ( A e. ran log /\ -. -u _pi = -u ( Im ` A ) ) -> -u A e. CC ) |
4 |
|
ellogrn |
|- ( A e. ran log <-> ( A e. CC /\ -u _pi < ( Im ` A ) /\ ( Im ` A ) <_ _pi ) ) |
5 |
4
|
biimpi |
|- ( A e. ran log -> ( A e. CC /\ -u _pi < ( Im ` A ) /\ ( Im ` A ) <_ _pi ) ) |
6 |
5
|
simp3d |
|- ( A e. ran log -> ( Im ` A ) <_ _pi ) |
7 |
|
imcl |
|- ( A e. CC -> ( Im ` A ) e. RR ) |
8 |
|
pire |
|- _pi e. RR |
9 |
|
leneg |
|- ( ( ( Im ` A ) e. RR /\ _pi e. RR ) -> ( ( Im ` A ) <_ _pi <-> -u _pi <_ -u ( Im ` A ) ) ) |
10 |
9
|
biimpd |
|- ( ( ( Im ` A ) e. RR /\ _pi e. RR ) -> ( ( Im ` A ) <_ _pi -> -u _pi <_ -u ( Im ` A ) ) ) |
11 |
7 8 10
|
sylancl |
|- ( A e. CC -> ( ( Im ` A ) <_ _pi -> -u _pi <_ -u ( Im ` A ) ) ) |
12 |
1 6 11
|
sylc |
|- ( A e. ran log -> -u _pi <_ -u ( Im ` A ) ) |
13 |
8
|
renegcli |
|- -u _pi e. RR |
14 |
13
|
a1i |
|- ( A e. CC -> -u _pi e. RR ) |
15 |
7
|
renegcld |
|- ( A e. CC -> -u ( Im ` A ) e. RR ) |
16 |
14 15
|
leloed |
|- ( A e. CC -> ( -u _pi <_ -u ( Im ` A ) <-> ( -u _pi < -u ( Im ` A ) \/ -u _pi = -u ( Im ` A ) ) ) ) |
17 |
16
|
biimpd |
|- ( A e. CC -> ( -u _pi <_ -u ( Im ` A ) -> ( -u _pi < -u ( Im ` A ) \/ -u _pi = -u ( Im ` A ) ) ) ) |
18 |
1 12 17
|
sylc |
|- ( A e. ran log -> ( -u _pi < -u ( Im ` A ) \/ -u _pi = -u ( Im ` A ) ) ) |
19 |
18
|
orcomd |
|- ( A e. ran log -> ( -u _pi = -u ( Im ` A ) \/ -u _pi < -u ( Im ` A ) ) ) |
20 |
19
|
orcanai |
|- ( ( A e. ran log /\ -. -u _pi = -u ( Im ` A ) ) -> -u _pi < -u ( Im ` A ) ) |
21 |
5
|
simp2d |
|- ( A e. ran log -> -u _pi < ( Im ` A ) ) |
22 |
|
ltnegcon1 |
|- ( ( _pi e. RR /\ ( Im ` A ) e. RR ) -> ( -u _pi < ( Im ` A ) <-> -u ( Im ` A ) < _pi ) ) |
23 |
22
|
biimpd |
|- ( ( _pi e. RR /\ ( Im ` A ) e. RR ) -> ( -u _pi < ( Im ` A ) -> -u ( Im ` A ) < _pi ) ) |
24 |
8 7 23
|
sylancr |
|- ( A e. CC -> ( -u _pi < ( Im ` A ) -> -u ( Im ` A ) < _pi ) ) |
25 |
1 21 24
|
sylc |
|- ( A e. ran log -> -u ( Im ` A ) < _pi ) |
26 |
25
|
adantr |
|- ( ( A e. ran log /\ -. -u _pi = -u ( Im ` A ) ) -> -u ( Im ` A ) < _pi ) |
27 |
|
ltle |
|- ( ( -u ( Im ` A ) e. RR /\ _pi e. RR ) -> ( -u ( Im ` A ) < _pi -> -u ( Im ` A ) <_ _pi ) ) |
28 |
15 8 27
|
sylancl |
|- ( A e. CC -> ( -u ( Im ` A ) < _pi -> -u ( Im ` A ) <_ _pi ) ) |
29 |
1 28
|
syl |
|- ( A e. ran log -> ( -u ( Im ` A ) < _pi -> -u ( Im ` A ) <_ _pi ) ) |
30 |
29
|
adantr |
|- ( ( A e. ran log /\ -. -u _pi = -u ( Im ` A ) ) -> ( -u ( Im ` A ) < _pi -> -u ( Im ` A ) <_ _pi ) ) |
31 |
26 30
|
mpd |
|- ( ( A e. ran log /\ -. -u _pi = -u ( Im ` A ) ) -> -u ( Im ` A ) <_ _pi ) |
32 |
|
imneg |
|- ( A e. CC -> ( Im ` -u A ) = -u ( Im ` A ) ) |
33 |
32
|
breq2d |
|- ( A e. CC -> ( -u _pi < ( Im ` -u A ) <-> -u _pi < -u ( Im ` A ) ) ) |
34 |
2 33
|
syl |
|- ( ( A e. ran log /\ -. -u _pi = -u ( Im ` A ) ) -> ( -u _pi < ( Im ` -u A ) <-> -u _pi < -u ( Im ` A ) ) ) |
35 |
32
|
breq1d |
|- ( A e. CC -> ( ( Im ` -u A ) <_ _pi <-> -u ( Im ` A ) <_ _pi ) ) |
36 |
2 35
|
syl |
|- ( ( A e. ran log /\ -. -u _pi = -u ( Im ` A ) ) -> ( ( Im ` -u A ) <_ _pi <-> -u ( Im ` A ) <_ _pi ) ) |
37 |
34 36
|
anbi12d |
|- ( ( A e. ran log /\ -. -u _pi = -u ( Im ` A ) ) -> ( ( -u _pi < ( Im ` -u A ) /\ ( Im ` -u A ) <_ _pi ) <-> ( -u _pi < -u ( Im ` A ) /\ -u ( Im ` A ) <_ _pi ) ) ) |
38 |
20 31 37
|
mpbir2and |
|- ( ( A e. ran log /\ -. -u _pi = -u ( Im ` A ) ) -> ( -u _pi < ( Im ` -u A ) /\ ( Im ` -u A ) <_ _pi ) ) |
39 |
|
3anass |
|- ( ( -u A e. CC /\ -u _pi < ( Im ` -u A ) /\ ( Im ` -u A ) <_ _pi ) <-> ( -u A e. CC /\ ( -u _pi < ( Im ` -u A ) /\ ( Im ` -u A ) <_ _pi ) ) ) |
40 |
3 38 39
|
sylanbrc |
|- ( ( A e. ran log /\ -. -u _pi = -u ( Im ` A ) ) -> ( -u A e. CC /\ -u _pi < ( Im ` -u A ) /\ ( Im ` -u A ) <_ _pi ) ) |
41 |
|
ellogrn |
|- ( -u A e. ran log <-> ( -u A e. CC /\ -u _pi < ( Im ` -u A ) /\ ( Im ` -u A ) <_ _pi ) ) |
42 |
40 41
|
sylibr |
|- ( ( A e. ran log /\ -. -u _pi = -u ( Im ` A ) ) -> -u A e. ran log ) |
43 |
42
|
ex |
|- ( A e. ran log -> ( -. -u _pi = -u ( Im ` A ) -> -u A e. ran log ) ) |
44 |
43
|
orrd |
|- ( A e. ran log -> ( -u _pi = -u ( Im ` A ) \/ -u A e. ran log ) ) |
45 |
|
recn |
|- ( _pi e. RR -> _pi e. CC ) |
46 |
|
recn |
|- ( ( Im ` A ) e. RR -> ( Im ` A ) e. CC ) |
47 |
45 46
|
anim12i |
|- ( ( _pi e. RR /\ ( Im ` A ) e. RR ) -> ( _pi e. CC /\ ( Im ` A ) e. CC ) ) |
48 |
8 7 47
|
sylancr |
|- ( A e. CC -> ( _pi e. CC /\ ( Im ` A ) e. CC ) ) |
49 |
1 48
|
syl |
|- ( A e. ran log -> ( _pi e. CC /\ ( Im ` A ) e. CC ) ) |
50 |
|
neg11 |
|- ( ( _pi e. CC /\ ( Im ` A ) e. CC ) -> ( -u _pi = -u ( Im ` A ) <-> _pi = ( Im ` A ) ) ) |
51 |
|
eqcom |
|- ( _pi = ( Im ` A ) <-> ( Im ` A ) = _pi ) |
52 |
50 51
|
bitrdi |
|- ( ( _pi e. CC /\ ( Im ` A ) e. CC ) -> ( -u _pi = -u ( Im ` A ) <-> ( Im ` A ) = _pi ) ) |
53 |
49 52
|
syl |
|- ( A e. ran log -> ( -u _pi = -u ( Im ` A ) <-> ( Im ` A ) = _pi ) ) |
54 |
53
|
orbi1d |
|- ( A e. ran log -> ( ( -u _pi = -u ( Im ` A ) \/ -u A e. ran log ) <-> ( ( Im ` A ) = _pi \/ -u A e. ran log ) ) ) |
55 |
44 54
|
mpbid |
|- ( A e. ran log -> ( ( Im ` A ) = _pi \/ -u A e. ran log ) ) |
56 |
55
|
orcanai |
|- ( ( A e. ran log /\ -. ( Im ` A ) = _pi ) -> -u A e. ran log ) |