This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rlimrecl

Description: The limit of a real sequence is real. (Contributed by Mario Carneiro, 9-May-2016)

Ref Expression
Hypotheses rlimcld2.1 
|- ( ph -> sup ( A , RR* , < ) = +oo )
rlimcld2.2 
|- ( ph -> ( x e. A |-> B ) ~~>r C )
rlimrecl.3 
|- ( ( ph /\ x e. A ) -> B e. RR )
Assertion rlimrecl 
|- ( ph -> C e. RR )

Proof

Step Hyp Ref Expression
1 rlimcld2.1 
 |-  ( ph -> sup ( A , RR* , < ) = +oo )
2 rlimcld2.2 
 |-  ( ph -> ( x e. A |-> B ) ~~>r C )
3 rlimrecl.3 
 |-  ( ( ph /\ x e. A ) -> B e. RR )
4 ax-resscn 
 |-  RR C_ CC
5 4 a1i 
 |-  ( ph -> RR C_ CC )
6 eldifi 
 |-  ( y e. ( CC \ RR ) -> y e. CC )
7 6 adantl 
 |-  ( ( ph /\ y e. ( CC \ RR ) ) -> y e. CC )
8 7 imcld 
 |-  ( ( ph /\ y e. ( CC \ RR ) ) -> ( Im ` y ) e. RR )
9 8 recnd 
 |-  ( ( ph /\ y e. ( CC \ RR ) ) -> ( Im ` y ) e. CC )
10 eldifn 
 |-  ( y e. ( CC \ RR ) -> -. y e. RR )
11 10 adantl 
 |-  ( ( ph /\ y e. ( CC \ RR ) ) -> -. y e. RR )
12 reim0b 
 |-  ( y e. CC -> ( y e. RR <-> ( Im ` y ) = 0 ) )
13 7 12 syl 
 |-  ( ( ph /\ y e. ( CC \ RR ) ) -> ( y e. RR <-> ( Im ` y ) = 0 ) )
14 13 necon3bbid 
 |-  ( ( ph /\ y e. ( CC \ RR ) ) -> ( -. y e. RR <-> ( Im ` y ) =/= 0 ) )
15 11 14 mpbid 
 |-  ( ( ph /\ y e. ( CC \ RR ) ) -> ( Im ` y ) =/= 0 )
16 9 15 absrpcld 
 |-  ( ( ph /\ y e. ( CC \ RR ) ) -> ( abs ` ( Im ` y ) ) e. RR+ )
17 7 adantr 
 |-  ( ( ( ph /\ y e. ( CC \ RR ) ) /\ z e. RR ) -> y e. CC )
18 simpr 
 |-  ( ( ( ph /\ y e. ( CC \ RR ) ) /\ z e. RR ) -> z e. RR )
19 18 recnd 
 |-  ( ( ( ph /\ y e. ( CC \ RR ) ) /\ z e. RR ) -> z e. CC )
20 17 19 subcld 
 |-  ( ( ( ph /\ y e. ( CC \ RR ) ) /\ z e. RR ) -> ( y - z ) e. CC )
21 absimle 
 |-  ( ( y - z ) e. CC -> ( abs ` ( Im ` ( y - z ) ) ) <_ ( abs ` ( y - z ) ) )
22 20 21 syl 
 |-  ( ( ( ph /\ y e. ( CC \ RR ) ) /\ z e. RR ) -> ( abs ` ( Im ` ( y - z ) ) ) <_ ( abs ` ( y - z ) ) )
23 17 19 imsubd 
 |-  ( ( ( ph /\ y e. ( CC \ RR ) ) /\ z e. RR ) -> ( Im ` ( y - z ) ) = ( ( Im ` y ) - ( Im ` z ) ) )
24 reim0 
 |-  ( z e. RR -> ( Im ` z ) = 0 )
25 24 adantl 
 |-  ( ( ( ph /\ y e. ( CC \ RR ) ) /\ z e. RR ) -> ( Im ` z ) = 0 )
26 25 oveq2d 
 |-  ( ( ( ph /\ y e. ( CC \ RR ) ) /\ z e. RR ) -> ( ( Im ` y ) - ( Im ` z ) ) = ( ( Im ` y ) - 0 ) )
27 9 adantr 
 |-  ( ( ( ph /\ y e. ( CC \ RR ) ) /\ z e. RR ) -> ( Im ` y ) e. CC )
28 27 subid1d 
 |-  ( ( ( ph /\ y e. ( CC \ RR ) ) /\ z e. RR ) -> ( ( Im ` y ) - 0 ) = ( Im ` y ) )
29 23 26 28 3eqtrrd 
 |-  ( ( ( ph /\ y e. ( CC \ RR ) ) /\ z e. RR ) -> ( Im ` y ) = ( Im ` ( y - z ) ) )
30 29 fveq2d 
 |-  ( ( ( ph /\ y e. ( CC \ RR ) ) /\ z e. RR ) -> ( abs ` ( Im ` y ) ) = ( abs ` ( Im ` ( y - z ) ) ) )
31 19 17 abssubd 
 |-  ( ( ( ph /\ y e. ( CC \ RR ) ) /\ z e. RR ) -> ( abs ` ( z - y ) ) = ( abs ` ( y - z ) ) )
32 22 30 31 3brtr4d 
 |-  ( ( ( ph /\ y e. ( CC \ RR ) ) /\ z e. RR ) -> ( abs ` ( Im ` y ) ) <_ ( abs ` ( z - y ) ) )
33 1 2 5 16 32 3 rlimcld2 
 |-  ( ph -> C e. RR )