Metamath Proof Explorer


Theorem logcnlem2

Description: Lemma for logcn . (Contributed by Mario Carneiro, 25-Feb-2015)

Ref Expression
Hypotheses logcn.d
|- D = ( CC \ ( -oo (,] 0 ) )
logcnlem.s
|- S = if ( A e. RR+ , A , ( abs ` ( Im ` A ) ) )
logcnlem.t
|- T = ( ( abs ` A ) x. ( R / ( 1 + R ) ) )
logcnlem.a
|- ( ph -> A e. D )
logcnlem.r
|- ( ph -> R e. RR+ )
Assertion logcnlem2
|- ( ph -> if ( S <_ T , S , T ) e. RR+ )

Proof

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