Metamath Proof Explorer

Theorem logcnlem5

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

Ref Expression
Hypothesis logcn.d 
|- D = ( CC \ ( -oo (,] 0 ) )
Assertion logcnlem5 
|- ( x e. D |-> ( Im ` ( log ` x ) ) ) e. ( D -cn-> RR )

Proof

Step Hyp Ref Expression
1 logcn.d 
 |-  D = ( CC \ ( -oo (,] 0 ) )
2 difss 
 |-  ( CC \ ( -oo (,] 0 ) ) C_ CC
3 1 2 eqsstri 
 |-  D C_ CC
4 ax-resscn 
 |-  RR C_ CC
5 eqid 
 |-  ( x e. D |-> ( Im ` ( log ` x ) ) ) = ( x e. D |-> ( Im ` ( log ` x ) ) )
6 1 ellogdm 
 |-  ( x e. D <-> ( x e. CC /\ ( x e. RR -> x e. RR+ ) ) )
7 6 simplbi 
 |-  ( x e. D -> x e. CC )
8 1 logdmn0 
 |-  ( x e. D -> x =/= 0 )
9 7 8 logcld 
 |-  ( x e. D -> ( log ` x ) e. CC )
10 9 imcld 
 |-  ( x e. D -> ( Im ` ( log ` x ) ) e. RR )
11 5 10 fmpti 
 |-  ( x e. D |-> ( Im ` ( log ` x ) ) ) : D --> RR
12 eqid 
 |-  if ( y e. RR+ , y , ( abs ` ( Im ` y ) ) ) = if ( y e. RR+ , y , ( abs ` ( Im ` y ) ) )
13 eqid 
 |-  ( ( abs ` y ) x. ( z / ( 1 + z ) ) ) = ( ( abs ` y ) x. ( z / ( 1 + z ) ) )
14 simpl 
 |-  ( ( y e. D /\ z e. RR+ ) -> y e. D )
15 simpr 
 |-  ( ( y e. D /\ z e. RR+ ) -> z e. RR+ )
16 1 12 13 14 15 logcnlem2 
 |-  ( ( y e. D /\ z e. RR+ ) -> if ( if ( y e. RR+ , y , ( abs ` ( Im ` y ) ) ) <_ ( ( abs ` y ) x. ( z / ( 1 + z ) ) ) , if ( y e. RR+ , y , ( abs ` ( Im ` y ) ) ) , ( ( abs ` y ) x. ( z / ( 1 + z ) ) ) ) e. RR+ )
17 simpll 
 |-  ( ( ( y e. D /\ w e. D ) /\ ( z e. RR+ /\ ( abs ` ( y - w ) ) < if ( if ( y e. RR+ , y , ( abs ` ( Im ` y ) ) ) <_ ( ( abs ` y ) x. ( z / ( 1 + z ) ) ) , if ( y e. RR+ , y , ( abs ` ( Im ` y ) ) ) , ( ( abs ` y ) x. ( z / ( 1 + z ) ) ) ) ) ) -> y e. D )
18 simprl 
 |-  ( ( ( y e. D /\ w e. D ) /\ ( z e. RR+ /\ ( abs ` ( y - w ) ) < if ( if ( y e. RR+ , y , ( abs ` ( Im ` y ) ) ) <_ ( ( abs ` y ) x. ( z / ( 1 + z ) ) ) , if ( y e. RR+ , y , ( abs ` ( Im ` y ) ) ) , ( ( abs ` y ) x. ( z / ( 1 + z ) ) ) ) ) ) -> z e. RR+ )
19 simplr 
 |-  ( ( ( y e. D /\ w e. D ) /\ ( z e. RR+ /\ ( abs ` ( y - w ) ) < if ( if ( y e. RR+ , y , ( abs ` ( Im ` y ) ) ) <_ ( ( abs ` y ) x. ( z / ( 1 + z ) ) ) , if ( y e. RR+ , y , ( abs ` ( Im ` y ) ) ) , ( ( abs ` y ) x. ( z / ( 1 + z ) ) ) ) ) ) -> w e. D )
20 simprr 
 |-  ( ( ( y e. D /\ w e. D ) /\ ( z e. RR+ /\ ( abs ` ( y - w ) ) < if ( if ( y e. RR+ , y , ( abs ` ( Im ` y ) ) ) <_ ( ( abs ` y ) x. ( z / ( 1 + z ) ) ) , if ( y e. RR+ , y , ( abs ` ( Im ` y ) ) ) , ( ( abs ` y ) x. ( z / ( 1 + z ) ) ) ) ) ) -> ( abs ` ( y - w ) ) < if ( if ( y e. RR+ , y , ( abs ` ( Im ` y ) ) ) <_ ( ( abs ` y ) x. ( z / ( 1 + z ) ) ) , if ( y e. RR+ , y , ( abs ` ( Im ` y ) ) ) , ( ( abs ` y ) x. ( z / ( 1 + z ) ) ) ) )
21 1 12 13 17 18 19 20 logcnlem4 
 |-  ( ( ( y e. D /\ w e. D ) /\ ( z e. RR+ /\ ( abs ` ( y - w ) ) < if ( if ( y e. RR+ , y , ( abs ` ( Im ` y ) ) ) <_ ( ( abs ` y ) x. ( z / ( 1 + z ) ) ) , if ( y e. RR+ , y , ( abs ` ( Im ` y ) ) ) , ( ( abs ` y ) x. ( z / ( 1 + z ) ) ) ) ) ) -> ( abs ` ( ( Im ` ( log ` y ) ) - ( Im ` ( log ` w ) ) ) ) < z )
22 21 expr 
 |-  ( ( ( y e. D /\ w e. D ) /\ z e. RR+ ) -> ( ( abs ` ( y - w ) ) < if ( if ( y e. RR+ , y , ( abs ` ( Im ` y ) ) ) <_ ( ( abs ` y ) x. ( z / ( 1 + z ) ) ) , if ( y e. RR+ , y , ( abs ` ( Im ` y ) ) ) , ( ( abs ` y ) x. ( z / ( 1 + z ) ) ) ) -> ( abs ` ( ( Im ` ( log ` y ) ) - ( Im ` ( log ` w ) ) ) ) < z ) )
23 2fveq3 
 |-  ( x = y -> ( Im ` ( log ` x ) ) = ( Im ` ( log ` y ) ) )
24 fvex 
 |-  ( Im ` ( log ` y ) ) e. _V
25 23 5 24 fvmpt 
 |-  ( y e. D -> ( ( x e. D |-> ( Im ` ( log ` x ) ) ) ` y ) = ( Im ` ( log ` y ) ) )
26 25 ad2antrr 
 |-  ( ( ( y e. D /\ w e. D ) /\ z e. RR+ ) -> ( ( x e. D |-> ( Im ` ( log ` x ) ) ) ` y ) = ( Im ` ( log ` y ) ) )
27 2fveq3 
 |-  ( x = w -> ( Im ` ( log ` x ) ) = ( Im ` ( log ` w ) ) )
28 fvex 
 |-  ( Im ` ( log ` w ) ) e. _V
29 27 5 28 fvmpt 
 |-  ( w e. D -> ( ( x e. D |-> ( Im ` ( log ` x ) ) ) ` w ) = ( Im ` ( log ` w ) ) )
30 29 ad2antlr 
 |-  ( ( ( y e. D /\ w e. D ) /\ z e. RR+ ) -> ( ( x e. D |-> ( Im ` ( log ` x ) ) ) ` w ) = ( Im ` ( log ` w ) ) )
31 26 30 oveq12d 
 |-  ( ( ( y e. D /\ w e. D ) /\ z e. RR+ ) -> ( ( ( x e. D |-> ( Im ` ( log ` x ) ) ) ` y ) - ( ( x e. D |-> ( Im ` ( log ` x ) ) ) ` w ) ) = ( ( Im ` ( log ` y ) ) - ( Im ` ( log ` w ) ) ) )
32 31 fveq2d 
 |-  ( ( ( y e. D /\ w e. D ) /\ z e. RR+ ) -> ( abs ` ( ( ( x e. D |-> ( Im ` ( log ` x ) ) ) ` y ) - ( ( x e. D |-> ( Im ` ( log ` x ) ) ) ` w ) ) ) = ( abs ` ( ( Im ` ( log ` y ) ) - ( Im ` ( log ` w ) ) ) ) )
33 32 breq1d 
 |-  ( ( ( y e. D /\ w e. D ) /\ z e. RR+ ) -> ( ( abs ` ( ( ( x e. D |-> ( Im ` ( log ` x ) ) ) ` y ) - ( ( x e. D |-> ( Im ` ( log ` x ) ) ) ` w ) ) ) < z <-> ( abs ` ( ( Im ` ( log ` y ) ) - ( Im ` ( log ` w ) ) ) ) < z ) )
34 22 33 sylibrd 
 |-  ( ( ( y e. D /\ w e. D ) /\ z e. RR+ ) -> ( ( abs ` ( y - w ) ) < if ( if ( y e. RR+ , y , ( abs ` ( Im ` y ) ) ) <_ ( ( abs ` y ) x. ( z / ( 1 + z ) ) ) , if ( y e. RR+ , y , ( abs ` ( Im ` y ) ) ) , ( ( abs ` y ) x. ( z / ( 1 + z ) ) ) ) -> ( abs ` ( ( ( x e. D |-> ( Im ` ( log ` x ) ) ) ` y ) - ( ( x e. D |-> ( Im ` ( log ` x ) ) ) ` w ) ) ) < z ) )
35 11 16 34 elcncf1ii 
 |-  ( ( D C_ CC /\ RR C_ CC ) -> ( x e. D |-> ( Im ` ( log ` x ) ) ) e. ( D -cn-> RR ) )
36 3 4 35 mp2an 
 |-  ( x e. D |-> ( Im ` ( log ` x ) ) ) e. ( D -cn-> RR )