Metamath Proof Explorer

Theorem rlimrege0

Description: The limit of a sequence of complex numbers with nonnegative real part has nonnegative real part. (Contributed by Mario Carneiro, 10-May-2016)

Ref Expression
Hypotheses rlimcld2.1 
|- ( ph -> sup ( A , RR* , < ) = +oo )
rlimcld2.2 
|- ( ph -> ( x e. A |-> B ) ~~>r C )
rlimrege0.4 
|- ( ( ph /\ x e. A ) -> B e. CC )
rlimrege0.5 
|- ( ( ph /\ x e. A ) -> 0 <_ ( Re ` B ) )
Assertion rlimrege0 
|- ( ph -> 0 <_ ( Re ` C ) )

Proof

Step Hyp Ref Expression
1 rlimcld2.1 
 |-  ( ph -> sup ( A , RR* , < ) = +oo )
2 rlimcld2.2 
 |-  ( ph -> ( x e. A |-> B ) ~~>r C )
3 rlimrege0.4 
 |-  ( ( ph /\ x e. A ) -> B e. CC )
4 rlimrege0.5 
 |-  ( ( ph /\ x e. A ) -> 0 <_ ( Re ` B ) )
5 ssrab2 
 |-  { w e. CC | 0 <_ ( Re ` w ) } C_ CC
6 5 a1i 
 |-  ( ph -> { w e. CC | 0 <_ ( Re ` w ) } C_ CC )
7 eldifi 
 |-  ( y e. ( CC \ { w e. CC | 0 <_ ( Re ` w ) } ) -> y e. CC )
8 7 adantl 
 |-  ( ( ph /\ y e. ( CC \ { w e. CC | 0 <_ ( Re ` w ) } ) ) -> y e. CC )
9 8 recld 
 |-  ( ( ph /\ y e. ( CC \ { w e. CC | 0 <_ ( Re ` w ) } ) ) -> ( Re ` y ) e. RR )
10 fveq2 
 |-  ( w = y -> ( Re ` w ) = ( Re ` y ) )
11 10 breq2d 
 |-  ( w = y -> ( 0 <_ ( Re ` w ) <-> 0 <_ ( Re ` y ) ) )
12 11 notbid 
 |-  ( w = y -> ( -. 0 <_ ( Re ` w ) <-> -. 0 <_ ( Re ` y ) ) )
13 notrab 
 |-  ( CC \ { w e. CC | 0 <_ ( Re ` w ) } ) = { w e. CC | -. 0 <_ ( Re ` w ) }
14 12 13 elrab2 
 |-  ( y e. ( CC \ { w e. CC | 0 <_ ( Re ` w ) } ) <-> ( y e. CC /\ -. 0 <_ ( Re ` y ) ) )
15 14 simprbi 
 |-  ( y e. ( CC \ { w e. CC | 0 <_ ( Re ` w ) } ) -> -. 0 <_ ( Re ` y ) )
16 15 adantl 
 |-  ( ( ph /\ y e. ( CC \ { w e. CC | 0 <_ ( Re ` w ) } ) ) -> -. 0 <_ ( Re ` y ) )
17 0re 
 |-  0 e. RR
18 ltnle 
 |-  ( ( ( Re ` y ) e. RR /\ 0 e. RR ) -> ( ( Re ` y ) < 0 <-> -. 0 <_ ( Re ` y ) ) )
19 9 17 18 sylancl 
 |-  ( ( ph /\ y e. ( CC \ { w e. CC | 0 <_ ( Re ` w ) } ) ) -> ( ( Re ` y ) < 0 <-> -. 0 <_ ( Re ` y ) ) )
20 16 19 mpbird 
 |-  ( ( ph /\ y e. ( CC \ { w e. CC | 0 <_ ( Re ` w ) } ) ) -> ( Re ` y ) < 0 )
21 9 20 negelrpd 
 |-  ( ( ph /\ y e. ( CC \ { w e. CC | 0 <_ ( Re ` w ) } ) ) -> -u ( Re ` y ) e. RR+ )
22 9 renegcld 
 |-  ( ( ph /\ y e. ( CC \ { w e. CC | 0 <_ ( Re ` w ) } ) ) -> -u ( Re ` y ) e. RR )
23 22 adantr 
 |-  ( ( ( ph /\ y e. ( CC \ { w e. CC | 0 <_ ( Re ` w ) } ) ) /\ z e. { w e. CC | 0 <_ ( Re ` w ) } ) -> -u ( Re ` y ) e. RR )
24 elrabi 
 |-  ( z e. { w e. CC | 0 <_ ( Re ` w ) } -> z e. CC )
25 24 adantl 
 |-  ( ( ( ph /\ y e. ( CC \ { w e. CC | 0 <_ ( Re ` w ) } ) ) /\ z e. { w e. CC | 0 <_ ( Re ` w ) } ) -> z e. CC )
26 8 adantr 
 |-  ( ( ( ph /\ y e. ( CC \ { w e. CC | 0 <_ ( Re ` w ) } ) ) /\ z e. { w e. CC | 0 <_ ( Re ` w ) } ) -> y e. CC )
27 25 26 subcld 
 |-  ( ( ( ph /\ y e. ( CC \ { w e. CC | 0 <_ ( Re ` w ) } ) ) /\ z e. { w e. CC | 0 <_ ( Re ` w ) } ) -> ( z - y ) e. CC )
28 27 recld 
 |-  ( ( ( ph /\ y e. ( CC \ { w e. CC | 0 <_ ( Re ` w ) } ) ) /\ z e. { w e. CC | 0 <_ ( Re ` w ) } ) -> ( Re ` ( z - y ) ) e. RR )
29 27 abscld 
 |-  ( ( ( ph /\ y e. ( CC \ { w e. CC | 0 <_ ( Re ` w ) } ) ) /\ z e. { w e. CC | 0 <_ ( Re ` w ) } ) -> ( abs ` ( z - y ) ) e. RR )
30 0red 
 |-  ( ( ( ph /\ y e. ( CC \ { w e. CC | 0 <_ ( Re ` w ) } ) ) /\ z e. { w e. CC | 0 <_ ( Re ` w ) } ) -> 0 e. RR )
31 25 recld 
 |-  ( ( ( ph /\ y e. ( CC \ { w e. CC | 0 <_ ( Re ` w ) } ) ) /\ z e. { w e. CC | 0 <_ ( Re ` w ) } ) -> ( Re ` z ) e. RR )
32 26 recld 
 |-  ( ( ( ph /\ y e. ( CC \ { w e. CC | 0 <_ ( Re ` w ) } ) ) /\ z e. { w e. CC | 0 <_ ( Re ` w ) } ) -> ( Re ` y ) e. RR )
33 fveq2 
 |-  ( w = z -> ( Re ` w ) = ( Re ` z ) )
34 33 breq2d 
 |-  ( w = z -> ( 0 <_ ( Re ` w ) <-> 0 <_ ( Re ` z ) ) )
35 34 elrab 
 |-  ( z e. { w e. CC | 0 <_ ( Re ` w ) } <-> ( z e. CC /\ 0 <_ ( Re ` z ) ) )
36 35 simprbi 
 |-  ( z e. { w e. CC | 0 <_ ( Re ` w ) } -> 0 <_ ( Re ` z ) )
37 36 adantl 
 |-  ( ( ( ph /\ y e. ( CC \ { w e. CC | 0 <_ ( Re ` w ) } ) ) /\ z e. { w e. CC | 0 <_ ( Re ` w ) } ) -> 0 <_ ( Re ` z ) )
38 30 31 32 37 lesub1dd 
 |-  ( ( ( ph /\ y e. ( CC \ { w e. CC | 0 <_ ( Re ` w ) } ) ) /\ z e. { w e. CC | 0 <_ ( Re ` w ) } ) -> ( 0 - ( Re ` y ) ) <_ ( ( Re ` z ) - ( Re ` y ) ) )
39 df-neg 
 |-  -u ( Re ` y ) = ( 0 - ( Re ` y ) )
40 39 a1i 
 |-  ( ( ( ph /\ y e. ( CC \ { w e. CC | 0 <_ ( Re ` w ) } ) ) /\ z e. { w e. CC | 0 <_ ( Re ` w ) } ) -> -u ( Re ` y ) = ( 0 - ( Re ` y ) ) )
41 25 26 resubd 
 |-  ( ( ( ph /\ y e. ( CC \ { w e. CC | 0 <_ ( Re ` w ) } ) ) /\ z e. { w e. CC | 0 <_ ( Re ` w ) } ) -> ( Re ` ( z - y ) ) = ( ( Re ` z ) - ( Re ` y ) ) )
42 38 40 41 3brtr4d 
 |-  ( ( ( ph /\ y e. ( CC \ { w e. CC | 0 <_ ( Re ` w ) } ) ) /\ z e. { w e. CC | 0 <_ ( Re ` w ) } ) -> -u ( Re ` y ) <_ ( Re ` ( z - y ) ) )
43 27 releabsd 
 |-  ( ( ( ph /\ y e. ( CC \ { w e. CC | 0 <_ ( Re ` w ) } ) ) /\ z e. { w e. CC | 0 <_ ( Re ` w ) } ) -> ( Re ` ( z - y ) ) <_ ( abs ` ( z - y ) ) )
44 23 28 29 42 43 letrd 
 |-  ( ( ( ph /\ y e. ( CC \ { w e. CC | 0 <_ ( Re ` w ) } ) ) /\ z e. { w e. CC | 0 <_ ( Re ` w ) } ) -> -u ( Re ` y ) <_ ( abs ` ( z - y ) ) )
45 fveq2 
 |-  ( w = B -> ( Re ` w ) = ( Re ` B ) )
46 45 breq2d 
 |-  ( w = B -> ( 0 <_ ( Re ` w ) <-> 0 <_ ( Re ` B ) ) )
47 46 3 4 elrabd 
 |-  ( ( ph /\ x e. A ) -> B e. { w e. CC | 0 <_ ( Re ` w ) } )
48 1 2 6 21 44 47 rlimcld2 
 |-  ( ph -> C e. { w e. CC | 0 <_ ( Re ` w ) } )
49 fveq2 
 |-  ( w = C -> ( Re ` w ) = ( Re ` C ) )
50 49 breq2d 
 |-  ( w = C -> ( 0 <_ ( Re ` w ) <-> 0 <_ ( Re ` C ) ) )
51 50 elrab 
 |-  ( C e. { w e. CC | 0 <_ ( Re ` w ) } <-> ( C e. CC /\ 0 <_ ( Re ` C ) ) )
52 51 simprbi 
 |-  ( C e. { w e. CC | 0 <_ ( Re ` w ) } -> 0 <_ ( Re ` C ) )
53 48 52 syl 
 |-  ( ph -> 0 <_ ( Re ` C ) )