| 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+ ) |