Metamath Proof Explorer

Theorem rlimcld2

Description: If D is a closed set in the topology of the complex numbers (stated here in basic form), and all the elements of the sequence lie in D , then the limit of the sequence also lies in D . (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 )
rlimcld2.3 
|- ( ph -> D C_ CC )
rlimcld2.4 
|- ( ( ph /\ y e. ( CC \ D ) ) -> R e. RR+ )
rlimcld2.5 
|- ( ( ( ph /\ y e. ( CC \ D ) ) /\ z e. D ) -> R <_ ( abs ` ( z - y ) ) )
rlimcld2.6 
|- ( ( ph /\ x e. A ) -> B e. D )
Assertion rlimcld2 
|- ( ph -> C e. D )

Proof

Step Hyp Ref Expression
1 rlimcld2.1 
 |-  ( ph -> sup ( A , RR* , < ) = +oo )
2 rlimcld2.2 
 |-  ( ph -> ( x e. A |-> B ) ~~>r C )
3 rlimcld2.3 
 |-  ( ph -> D C_ CC )
4 rlimcld2.4 
 |-  ( ( ph /\ y e. ( CC \ D ) ) -> R e. RR+ )
5 rlimcld2.5 
 |-  ( ( ( ph /\ y e. ( CC \ D ) ) /\ z e. D ) -> R <_ ( abs ` ( z - y ) ) )
6 rlimcld2.6 
 |-  ( ( ph /\ x e. A ) -> B e. D )
7 6 ralrimiva 
 |-  ( ph -> A. x e. A B e. D )
8 7 adantr 
 |-  ( ( ph /\ -. C e. D ) -> A. x e. A B e. D )
9 2 adantr 
 |-  ( ( ph /\ -. C e. D ) -> ( x e. A |-> B ) ~~>r C )
10 rlimcl 
 |-  ( ( x e. A |-> B ) ~~>r C -> C e. CC )
11 9 10 syl 
 |-  ( ( ph /\ -. C e. D ) -> C e. CC )
12 simpr 
 |-  ( ( ph /\ -. C e. D ) -> -. C e. D )
13 11 12 eldifd 
 |-  ( ( ph /\ -. C e. D ) -> C e. ( CC \ D ) )
14 4 ralrimiva 
 |-  ( ph -> A. y e. ( CC \ D ) R e. RR+ )
15 14 adantr 
 |-  ( ( ph /\ -. C e. D ) -> A. y e. ( CC \ D ) R e. RR+ )
16 nfcsb1v 
 |-  F/_ y [_ C / y ]_ R
17 16 nfel1 
 |-  F/ y [_ C / y ]_ R e. RR+
18 csbeq1a 
 |-  ( y = C -> R = [_ C / y ]_ R )
19 18 eleq1d 
 |-  ( y = C -> ( R e. RR+ <-> [_ C / y ]_ R e. RR+ ) )
20 17 19 rspc 
 |-  ( C e. ( CC \ D ) -> ( A. y e. ( CC \ D ) R e. RR+ -> [_ C / y ]_ R e. RR+ ) )
21 13 15 20 sylc 
 |-  ( ( ph /\ -. C e. D ) -> [_ C / y ]_ R e. RR+ )
22 8 21 9 rlimi 
 |-  ( ( ph /\ -. C e. D ) -> E. r e. RR A. x e. A ( r <_ x -> ( abs ` ( B - C ) ) < [_ C / y ]_ R ) )
23 21 ad2antrr 
 |-  ( ( ( ( ph /\ -. C e. D ) /\ r e. RR ) /\ x e. A ) -> [_ C / y ]_ R e. RR+ )
24 23 rpred 
 |-  ( ( ( ( ph /\ -. C e. D ) /\ r e. RR ) /\ x e. A ) -> [_ C / y ]_ R e. RR )
25 3 ad3antrrr 
 |-  ( ( ( ( ph /\ -. C e. D ) /\ r e. RR ) /\ x e. A ) -> D C_ CC )
26 6 ad4ant14 
 |-  ( ( ( ( ph /\ -. C e. D ) /\ r e. RR ) /\ x e. A ) -> B e. D )
27 25 26 sseldd 
 |-  ( ( ( ( ph /\ -. C e. D ) /\ r e. RR ) /\ x e. A ) -> B e. CC )
28 11 ad2antrr 
 |-  ( ( ( ( ph /\ -. C e. D ) /\ r e. RR ) /\ x e. A ) -> C e. CC )
29 27 28 subcld 
 |-  ( ( ( ( ph /\ -. C e. D ) /\ r e. RR ) /\ x e. A ) -> ( B - C ) e. CC )
30 29 abscld 
 |-  ( ( ( ( ph /\ -. C e. D ) /\ r e. RR ) /\ x e. A ) -> ( abs ` ( B - C ) ) e. RR )
31 5 ralrimiva 
 |-  ( ( ph /\ y e. ( CC \ D ) ) -> A. z e. D R <_ ( abs ` ( z - y ) ) )
32 31 ralrimiva 
 |-  ( ph -> A. y e. ( CC \ D ) A. z e. D R <_ ( abs ` ( z - y ) ) )
33 32 adantr 
 |-  ( ( ph /\ -. C e. D ) -> A. y e. ( CC \ D ) A. z e. D R <_ ( abs ` ( z - y ) ) )
34 nfcv 
 |-  F/_ y D
35 nfcv 
 |-  F/_ y <_
36 nfcv 
 |-  F/_ y ( abs ` ( z - C ) )
37 16 35 36 nfbr 
 |-  F/ y [_ C / y ]_ R <_ ( abs ` ( z - C ) )
38 34 37 nfralw 
 |-  F/ y A. z e. D [_ C / y ]_ R <_ ( abs ` ( z - C ) )
39 oveq2 
 |-  ( y = C -> ( z - y ) = ( z - C ) )
40 39 fveq2d 
 |-  ( y = C -> ( abs ` ( z - y ) ) = ( abs ` ( z - C ) ) )
41 18 40 breq12d 
 |-  ( y = C -> ( R <_ ( abs ` ( z - y ) ) <-> [_ C / y ]_ R <_ ( abs ` ( z - C ) ) ) )
42 41 ralbidv 
 |-  ( y = C -> ( A. z e. D R <_ ( abs ` ( z - y ) ) <-> A. z e. D [_ C / y ]_ R <_ ( abs ` ( z - C ) ) ) )
43 38 42 rspc 
 |-  ( C e. ( CC \ D ) -> ( A. y e. ( CC \ D ) A. z e. D R <_ ( abs ` ( z - y ) ) -> A. z e. D [_ C / y ]_ R <_ ( abs ` ( z - C ) ) ) )
44 13 33 43 sylc 
 |-  ( ( ph /\ -. C e. D ) -> A. z e. D [_ C / y ]_ R <_ ( abs ` ( z - C ) ) )
45 44 ad2antrr 
 |-  ( ( ( ( ph /\ -. C e. D ) /\ r e. RR ) /\ x e. A ) -> A. z e. D [_ C / y ]_ R <_ ( abs ` ( z - C ) ) )
46 fvoveq1 
 |-  ( z = B -> ( abs ` ( z - C ) ) = ( abs ` ( B - C ) ) )
47 46 breq2d 
 |-  ( z = B -> ( [_ C / y ]_ R <_ ( abs ` ( z - C ) ) <-> [_ C / y ]_ R <_ ( abs ` ( B - C ) ) ) )
48 47 rspcv 
 |-  ( B e. D -> ( A. z e. D [_ C / y ]_ R <_ ( abs ` ( z - C ) ) -> [_ C / y ]_ R <_ ( abs ` ( B - C ) ) ) )
49 26 45 48 sylc 
 |-  ( ( ( ( ph /\ -. C e. D ) /\ r e. RR ) /\ x e. A ) -> [_ C / y ]_ R <_ ( abs ` ( B - C ) ) )
50 24 30 49 lensymd 
 |-  ( ( ( ( ph /\ -. C e. D ) /\ r e. RR ) /\ x e. A ) -> -. ( abs ` ( B - C ) ) < [_ C / y ]_ R )
51 id 
 |-  ( ( r <_ x -> ( abs ` ( B - C ) ) < [_ C / y ]_ R ) -> ( r <_ x -> ( abs ` ( B - C ) ) < [_ C / y ]_ R ) )
52 51 imp 
 |-  ( ( ( r <_ x -> ( abs ` ( B - C ) ) < [_ C / y ]_ R ) /\ r <_ x ) -> ( abs ` ( B - C ) ) < [_ C / y ]_ R )
53 50 52 nsyl 
 |-  ( ( ( ( ph /\ -. C e. D ) /\ r e. RR ) /\ x e. A ) -> -. ( ( r <_ x -> ( abs ` ( B - C ) ) < [_ C / y ]_ R ) /\ r <_ x ) )
54 53 nrexdv 
 |-  ( ( ( ph /\ -. C e. D ) /\ r e. RR ) -> -. E. x e. A ( ( r <_ x -> ( abs ` ( B - C ) ) < [_ C / y ]_ R ) /\ r <_ x ) )
55 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
56 55 6 dmmptd 
 |-  ( ph -> dom ( x e. A |-> B ) = A )
57 rlimss 
 |-  ( ( x e. A |-> B ) ~~>r C -> dom ( x e. A |-> B ) C_ RR )
58 2 57 syl 
 |-  ( ph -> dom ( x e. A |-> B ) C_ RR )
59 56 58 eqsstrrd 
 |-  ( ph -> A C_ RR )
60 ressxr 
 |-  RR C_ RR*
61 59 60 sstrdi 
 |-  ( ph -> A C_ RR* )
62 supxrunb1 
 |-  ( A C_ RR* -> ( A. r e. RR E. x e. A r <_ x <-> sup ( A , RR* , < ) = +oo ) )
63 61 62 syl 
 |-  ( ph -> ( A. r e. RR E. x e. A r <_ x <-> sup ( A , RR* , < ) = +oo ) )
64 1 63 mpbird 
 |-  ( ph -> A. r e. RR E. x e. A r <_ x )
65 64 adantr 
 |-  ( ( ph /\ -. C e. D ) -> A. r e. RR E. x e. A r <_ x )
66 65 r19.21bi 
 |-  ( ( ( ph /\ -. C e. D ) /\ r e. RR ) -> E. x e. A r <_ x )
67 r19.29 
 |-  ( ( A. x e. A ( r <_ x -> ( abs ` ( B - C ) ) < [_ C / y ]_ R ) /\ E. x e. A r <_ x ) -> E. x e. A ( ( r <_ x -> ( abs ` ( B - C ) ) < [_ C / y ]_ R ) /\ r <_ x ) )
68 67 expcom 
 |-  ( E. x e. A r <_ x -> ( A. x e. A ( r <_ x -> ( abs ` ( B - C ) ) < [_ C / y ]_ R ) -> E. x e. A ( ( r <_ x -> ( abs ` ( B - C ) ) < [_ C / y ]_ R ) /\ r <_ x ) ) )
69 66 68 syl 
 |-  ( ( ( ph /\ -. C e. D ) /\ r e. RR ) -> ( A. x e. A ( r <_ x -> ( abs ` ( B - C ) ) < [_ C / y ]_ R ) -> E. x e. A ( ( r <_ x -> ( abs ` ( B - C ) ) < [_ C / y ]_ R ) /\ r <_ x ) ) )
70 54 69 mtod 
 |-  ( ( ( ph /\ -. C e. D ) /\ r e. RR ) -> -. A. x e. A ( r <_ x -> ( abs ` ( B - C ) ) < [_ C / y ]_ R ) )
71 70 nrexdv 
 |-  ( ( ph /\ -. C e. D ) -> -. E. r e. RR A. x e. A ( r <_ x -> ( abs ` ( B - C ) ) < [_ C / y ]_ R ) )
72 22 71 condan 
 |-  ( ph -> C e. D )