Step |
Hyp |
Ref |
Expression |
1 |
|
logcn.d |
|- D = ( CC \ ( -oo (,] 0 ) ) |
2 |
|
logcnlem.s |
|- S = if ( A e. RR+ , A , ( abs ` ( Im ` A ) ) ) |
3 |
|
logcnlem.t |
|- T = ( ( abs ` A ) x. ( R / ( 1 + R ) ) ) |
4 |
|
logcnlem.a |
|- ( ph -> A e. D ) |
5 |
|
logcnlem.r |
|- ( ph -> R e. RR+ ) |
6 |
|
simpr |
|- ( ( ph /\ A e. RR+ ) -> A e. RR+ ) |
7 |
1
|
ellogdm |
|- ( A e. D <-> ( A e. CC /\ ( A e. RR -> A e. RR+ ) ) ) |
8 |
7
|
simplbi |
|- ( A e. D -> A e. CC ) |
9 |
4 8
|
syl |
|- ( ph -> A e. CC ) |
10 |
9
|
imcld |
|- ( ph -> ( Im ` A ) e. RR ) |
11 |
10
|
adantr |
|- ( ( ph /\ -. A e. RR+ ) -> ( Im ` A ) e. RR ) |
12 |
11
|
recnd |
|- ( ( ph /\ -. A e. RR+ ) -> ( Im ` A ) e. CC ) |
13 |
|
reim0b |
|- ( A e. CC -> ( A e. RR <-> ( Im ` A ) = 0 ) ) |
14 |
9 13
|
syl |
|- ( ph -> ( A e. RR <-> ( Im ` A ) = 0 ) ) |
15 |
7
|
simprbi |
|- ( A e. D -> ( A e. RR -> A e. RR+ ) ) |
16 |
4 15
|
syl |
|- ( ph -> ( A e. RR -> A e. RR+ ) ) |
17 |
14 16
|
sylbird |
|- ( ph -> ( ( Im ` A ) = 0 -> A e. RR+ ) ) |
18 |
17
|
necon3bd |
|- ( ph -> ( -. A e. RR+ -> ( Im ` A ) =/= 0 ) ) |
19 |
18
|
imp |
|- ( ( ph /\ -. A e. RR+ ) -> ( Im ` A ) =/= 0 ) |
20 |
12 19
|
absrpcld |
|- ( ( ph /\ -. A e. RR+ ) -> ( abs ` ( Im ` A ) ) e. RR+ ) |
21 |
6 20
|
ifclda |
|- ( ph -> if ( A e. RR+ , A , ( abs ` ( Im ` A ) ) ) e. RR+ ) |
22 |
2 21
|
eqeltrid |
|- ( ph -> S e. RR+ ) |
23 |
1
|
logdmn0 |
|- ( A e. D -> A =/= 0 ) |
24 |
4 23
|
syl |
|- ( ph -> A =/= 0 ) |
25 |
9 24
|
absrpcld |
|- ( ph -> ( abs ` A ) e. RR+ ) |
26 |
|
1rp |
|- 1 e. RR+ |
27 |
|
rpaddcl |
|- ( ( 1 e. RR+ /\ R e. RR+ ) -> ( 1 + R ) e. RR+ ) |
28 |
26 5 27
|
sylancr |
|- ( ph -> ( 1 + R ) e. RR+ ) |
29 |
5 28
|
rpdivcld |
|- ( ph -> ( R / ( 1 + R ) ) e. RR+ ) |
30 |
25 29
|
rpmulcld |
|- ( ph -> ( ( abs ` A ) x. ( R / ( 1 + R ) ) ) e. RR+ ) |
31 |
3 30
|
eqeltrid |
|- ( ph -> T e. RR+ ) |
32 |
22 31
|
ifcld |
|- ( ph -> if ( S <_ T , S , T ) e. RR+ ) |