Metamath Proof Explorer

Theorem rlimcnp2

Description: Relate a limit of a real-valued sequence at infinity to the continuity of the function S ( y ) = R ( 1 / y ) at zero. (Contributed by Mario Carneiro, 1-Mar-2015)

Ref Expression
Hypotheses rlimcnp2.a 
|- ( ph -> A C_ ( 0 [,) +oo ) )
rlimcnp2.0 
|- ( ph -> 0 e. A )
rlimcnp2.b 
|- ( ph -> B C_ RR )
rlimcnp2.c 
|- ( ph -> C e. CC )
rlimcnp2.r 
|- ( ( ph /\ y e. B ) -> S e. CC )
rlimcnp2.d 
|- ( ( ph /\ y e. RR+ ) -> ( y e. B <-> ( 1 / y ) e. A ) )
rlimcnp2.s 
|- ( y = ( 1 / x ) -> S = R )
rlimcnp2.j 
|- J = ( TopOpen ` CCfld )
rlimcnp2.k 
|- K = ( J |`t A )
Assertion rlimcnp2 
|- ( ph -> ( ( y e. B |-> S ) ~~>r C <-> ( x e. A |-> if ( x = 0 , C , R ) ) e. ( ( K CnP J ) ` 0 ) ) )

Proof

Step Hyp Ref Expression
1 rlimcnp2.a 
 |-  ( ph -> A C_ ( 0 [,) +oo ) )
2 rlimcnp2.0 
 |-  ( ph -> 0 e. A )
3 rlimcnp2.b 
 |-  ( ph -> B C_ RR )
4 rlimcnp2.c 
 |-  ( ph -> C e. CC )
5 rlimcnp2.r 
 |-  ( ( ph /\ y e. B ) -> S e. CC )
6 rlimcnp2.d 
 |-  ( ( ph /\ y e. RR+ ) -> ( y e. B <-> ( 1 / y ) e. A ) )
7 rlimcnp2.s 
 |-  ( y = ( 1 / x ) -> S = R )
8 rlimcnp2.j 
 |-  J = ( TopOpen ` CCfld )
9 rlimcnp2.k 
 |-  K = ( J |`t A )
10 inss1 
 |-  ( B i^i ( 1 [,) +oo ) ) C_ B
11 resmpt 
 |-  ( ( B i^i ( 1 [,) +oo ) ) C_ B -> ( ( y e. B |-> S ) |` ( B i^i ( 1 [,) +oo ) ) ) = ( y e. ( B i^i ( 1 [,) +oo ) ) |-> S ) )
12 10 11 mp1i 
 |-  ( ph -> ( ( y e. B |-> S ) |` ( B i^i ( 1 [,) +oo ) ) ) = ( y e. ( B i^i ( 1 [,) +oo ) ) |-> S ) )
13 0xr 
 |-  0 e. RR*
14 0lt1 
 |-  0 < 1
15 df-ioo 
 |-  (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )
16 df-ico 
 |-  [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } )
17 xrltletr 
 |-  ( ( 0 e. RR* /\ 1 e. RR* /\ w e. RR* ) -> ( ( 0 < 1 /\ 1 <_ w ) -> 0 < w ) )
18 15 16 17 ixxss1 
 |-  ( ( 0 e. RR* /\ 0 < 1 ) -> ( 1 [,) +oo ) C_ ( 0 (,) +oo ) )
19 13 14 18 mp2an 
 |-  ( 1 [,) +oo ) C_ ( 0 (,) +oo )
20 ioorp 
 |-  ( 0 (,) +oo ) = RR+
21 19 20 sseqtri 
 |-  ( 1 [,) +oo ) C_ RR+
22 sslin 
 |-  ( ( 1 [,) +oo ) C_ RR+ -> ( B i^i ( 1 [,) +oo ) ) C_ ( B i^i RR+ ) )
23 21 22 ax-mp 
 |-  ( B i^i ( 1 [,) +oo ) ) C_ ( B i^i RR+ )
24 resmpt 
 |-  ( ( B i^i ( 1 [,) +oo ) ) C_ ( B i^i RR+ ) -> ( ( y e. ( B i^i RR+ ) |-> S ) |` ( B i^i ( 1 [,) +oo ) ) ) = ( y e. ( B i^i ( 1 [,) +oo ) ) |-> S ) )
25 23 24 mp1i 
 |-  ( ph -> ( ( y e. ( B i^i RR+ ) |-> S ) |` ( B i^i ( 1 [,) +oo ) ) ) = ( y e. ( B i^i ( 1 [,) +oo ) ) |-> S ) )
26 12 25 eqtr4d 
 |-  ( ph -> ( ( y e. B |-> S ) |` ( B i^i ( 1 [,) +oo ) ) ) = ( ( y e. ( B i^i RR+ ) |-> S ) |` ( B i^i ( 1 [,) +oo ) ) ) )
27 resres 
 |-  ( ( ( y e. B |-> S ) |` B ) |` ( 1 [,) +oo ) ) = ( ( y e. B |-> S ) |` ( B i^i ( 1 [,) +oo ) ) )
28 resres 
 |-  ( ( ( y e. ( B i^i RR+ ) |-> S ) |` B ) |` ( 1 [,) +oo ) ) = ( ( y e. ( B i^i RR+ ) |-> S ) |` ( B i^i ( 1 [,) +oo ) ) )
29 26 27 28 3eqtr4g 
 |-  ( ph -> ( ( ( y e. B |-> S ) |` B ) |` ( 1 [,) +oo ) ) = ( ( ( y e. ( B i^i RR+ ) |-> S ) |` B ) |` ( 1 [,) +oo ) ) )
30 5 fmpttd 
 |-  ( ph -> ( y e. B |-> S ) : B --> CC )
31 30 ffnd 
 |-  ( ph -> ( y e. B |-> S ) Fn B )
32 fnresdm 
 |-  ( ( y e. B |-> S ) Fn B -> ( ( y e. B |-> S ) |` B ) = ( y e. B |-> S ) )
33 31 32 syl 
 |-  ( ph -> ( ( y e. B |-> S ) |` B ) = ( y e. B |-> S ) )
34 33 reseq1d 
 |-  ( ph -> ( ( ( y e. B |-> S ) |` B ) |` ( 1 [,) +oo ) ) = ( ( y e. B |-> S ) |` ( 1 [,) +oo ) ) )
35 elinel1 
 |-  ( y e. ( B i^i RR+ ) -> y e. B )
36 35 5 sylan2 
 |-  ( ( ph /\ y e. ( B i^i RR+ ) ) -> S e. CC )
37 36 fmpttd 
 |-  ( ph -> ( y e. ( B i^i RR+ ) |-> S ) : ( B i^i RR+ ) --> CC )
38 frel 
 |-  ( ( y e. ( B i^i RR+ ) |-> S ) : ( B i^i RR+ ) --> CC -> Rel ( y e. ( B i^i RR+ ) |-> S ) )
39 37 38 syl 
 |-  ( ph -> Rel ( y e. ( B i^i RR+ ) |-> S ) )
40 eqid 
 |-  ( y e. ( B i^i RR+ ) |-> S ) = ( y e. ( B i^i RR+ ) |-> S )
41 40 36 dmmptd 
 |-  ( ph -> dom ( y e. ( B i^i RR+ ) |-> S ) = ( B i^i RR+ ) )
42 inss1 
 |-  ( B i^i RR+ ) C_ B
43 41 42 eqsstrdi 
 |-  ( ph -> dom ( y e. ( B i^i RR+ ) |-> S ) C_ B )
44 relssres 
 |-  ( ( Rel ( y e. ( B i^i RR+ ) |-> S ) /\ dom ( y e. ( B i^i RR+ ) |-> S ) C_ B ) -> ( ( y e. ( B i^i RR+ ) |-> S ) |` B ) = ( y e. ( B i^i RR+ ) |-> S ) )
45 39 43 44 syl2anc 
 |-  ( ph -> ( ( y e. ( B i^i RR+ ) |-> S ) |` B ) = ( y e. ( B i^i RR+ ) |-> S ) )
46 45 reseq1d 
 |-  ( ph -> ( ( ( y e. ( B i^i RR+ ) |-> S ) |` B ) |` ( 1 [,) +oo ) ) = ( ( y e. ( B i^i RR+ ) |-> S ) |` ( 1 [,) +oo ) ) )
47 29 34 46 3eqtr3d 
 |-  ( ph -> ( ( y e. B |-> S ) |` ( 1 [,) +oo ) ) = ( ( y e. ( B i^i RR+ ) |-> S ) |` ( 1 [,) +oo ) ) )
48 47 breq1d 
 |-  ( ph -> ( ( ( y e. B |-> S ) |` ( 1 [,) +oo ) ) ~~>r C <-> ( ( y e. ( B i^i RR+ ) |-> S ) |` ( 1 [,) +oo ) ) ~~>r C ) )
49 1red 
 |-  ( ph -> 1 e. RR )
50 30 3 49 rlimresb 
 |-  ( ph -> ( ( y e. B |-> S ) ~~>r C <-> ( ( y e. B |-> S ) |` ( 1 [,) +oo ) ) ~~>r C ) )
51 42 3 sstrid 
 |-  ( ph -> ( B i^i RR+ ) C_ RR )
52 37 51 49 rlimresb 
 |-  ( ph -> ( ( y e. ( B i^i RR+ ) |-> S ) ~~>r C <-> ( ( y e. ( B i^i RR+ ) |-> S ) |` ( 1 [,) +oo ) ) ~~>r C ) )
53 48 50 52 3bitr4d 
 |-  ( ph -> ( ( y e. B |-> S ) ~~>r C <-> ( y e. ( B i^i RR+ ) |-> S ) ~~>r C ) )
54 inss2 
 |-  ( B i^i RR+ ) C_ RR+
55 54 a1i 
 |-  ( ph -> ( B i^i RR+ ) C_ RR+ )
56 55 sselda 
 |-  ( ( ph /\ y e. ( B i^i RR+ ) ) -> y e. RR+ )
57 56 rpreccld 
 |-  ( ( ph /\ y e. ( B i^i RR+ ) ) -> ( 1 / y ) e. RR+ )
58 57 rpne0d 
 |-  ( ( ph /\ y e. ( B i^i RR+ ) ) -> ( 1 / y ) =/= 0 )
59 58 neneqd 
 |-  ( ( ph /\ y e. ( B i^i RR+ ) ) -> -. ( 1 / y ) = 0 )
60 59 iffalsed 
 |-  ( ( ph /\ y e. ( B i^i RR+ ) ) -> if ( ( 1 / y ) = 0 , C , [_ ( 1 / y ) / x ]_ R ) = [_ ( 1 / y ) / x ]_ R )
61 oveq2 
 |-  ( x = ( 1 / y ) -> ( 1 / x ) = ( 1 / ( 1 / y ) ) )
62 rpcnne0 
 |-  ( y e. RR+ -> ( y e. CC /\ y =/= 0 ) )
63 recrec 
 |-  ( ( y e. CC /\ y =/= 0 ) -> ( 1 / ( 1 / y ) ) = y )
64 56 62 63 3syl 
 |-  ( ( ph /\ y e. ( B i^i RR+ ) ) -> ( 1 / ( 1 / y ) ) = y )
65 61 64 sylan9eqr 
 |-  ( ( ( ph /\ y e. ( B i^i RR+ ) ) /\ x = ( 1 / y ) ) -> ( 1 / x ) = y )
66 65 eqcomd 
 |-  ( ( ( ph /\ y e. ( B i^i RR+ ) ) /\ x = ( 1 / y ) ) -> y = ( 1 / x ) )
67 66 7 syl 
 |-  ( ( ( ph /\ y e. ( B i^i RR+ ) ) /\ x = ( 1 / y ) ) -> S = R )
68 67 eqcomd 
 |-  ( ( ( ph /\ y e. ( B i^i RR+ ) ) /\ x = ( 1 / y ) ) -> R = S )
69 57 68 csbied 
 |-  ( ( ph /\ y e. ( B i^i RR+ ) ) -> [_ ( 1 / y ) / x ]_ R = S )
70 60 69 eqtrd 
 |-  ( ( ph /\ y e. ( B i^i RR+ ) ) -> if ( ( 1 / y ) = 0 , C , [_ ( 1 / y ) / x ]_ R ) = S )
71 70 mpteq2dva 
 |-  ( ph -> ( y e. ( B i^i RR+ ) |-> if ( ( 1 / y ) = 0 , C , [_ ( 1 / y ) / x ]_ R ) ) = ( y e. ( B i^i RR+ ) |-> S ) )
72 71 breq1d 
 |-  ( ph -> ( ( y e. ( B i^i RR+ ) |-> if ( ( 1 / y ) = 0 , C , [_ ( 1 / y ) / x ]_ R ) ) ~~>r C <-> ( y e. ( B i^i RR+ ) |-> S ) ~~>r C ) )
73 4 ad2antrr 
 |-  ( ( ( ph /\ w e. A ) /\ w = 0 ) -> C e. CC )
74 1 sselda 
 |-  ( ( ph /\ w e. A ) -> w e. ( 0 [,) +oo ) )
75 0re 
 |-  0 e. RR
76 pnfxr 
 |-  +oo e. RR*
77 elico2 
 |-  ( ( 0 e. RR /\ +oo e. RR* ) -> ( w e. ( 0 [,) +oo ) <-> ( w e. RR /\ 0 <_ w /\ w < +oo ) ) )
78 75 76 77 mp2an 
 |-  ( w e. ( 0 [,) +oo ) <-> ( w e. RR /\ 0 <_ w /\ w < +oo ) )
79 74 78 sylib 
 |-  ( ( ph /\ w e. A ) -> ( w e. RR /\ 0 <_ w /\ w < +oo ) )
80 79 simp1d 
 |-  ( ( ph /\ w e. A ) -> w e. RR )
81 80 adantr 
 |-  ( ( ( ph /\ w e. A ) /\ -. w = 0 ) -> w e. RR )
82 79 simp2d 
 |-  ( ( ph /\ w e. A ) -> 0 <_ w )
83 leloe 
 |-  ( ( 0 e. RR /\ w e. RR ) -> ( 0 <_ w <-> ( 0 < w \/ 0 = w ) ) )
84 75 80 83 sylancr 
 |-  ( ( ph /\ w e. A ) -> ( 0 <_ w <-> ( 0 < w \/ 0 = w ) ) )
85 82 84 mpbid 
 |-  ( ( ph /\ w e. A ) -> ( 0 < w \/ 0 = w ) )
86 85 ord 
 |-  ( ( ph /\ w e. A ) -> ( -. 0 < w -> 0 = w ) )
87 eqcom 
 |-  ( 0 = w <-> w = 0 )
88 86 87 syl6ib 
 |-  ( ( ph /\ w e. A ) -> ( -. 0 < w -> w = 0 ) )
89 88 con1d 
 |-  ( ( ph /\ w e. A ) -> ( -. w = 0 -> 0 < w ) )
90 89 imp 
 |-  ( ( ( ph /\ w e. A ) /\ -. w = 0 ) -> 0 < w )
91 81 90 elrpd 
 |-  ( ( ( ph /\ w e. A ) /\ -. w = 0 ) -> w e. RR+ )
92 rpcnne0 
 |-  ( w e. RR+ -> ( w e. CC /\ w =/= 0 ) )
93 recrec 
 |-  ( ( w e. CC /\ w =/= 0 ) -> ( 1 / ( 1 / w ) ) = w )
94 92 93 syl 
 |-  ( w e. RR+ -> ( 1 / ( 1 / w ) ) = w )
95 91 94 syl 
 |-  ( ( ( ph /\ w e. A ) /\ -. w = 0 ) -> ( 1 / ( 1 / w ) ) = w )
96 95 csbeq1d 
 |-  ( ( ( ph /\ w e. A ) /\ -. w = 0 ) -> [_ ( 1 / ( 1 / w ) ) / x ]_ R = [_ w / x ]_ R )
97 oveq2 
 |-  ( y = ( 1 / w ) -> ( 1 / y ) = ( 1 / ( 1 / w ) ) )
98 97 csbeq1d 
 |-  ( y = ( 1 / w ) -> [_ ( 1 / y ) / x ]_ R = [_ ( 1 / ( 1 / w ) ) / x ]_ R )
99 98 eleq1d 
 |-  ( y = ( 1 / w ) -> ( [_ ( 1 / y ) / x ]_ R e. CC <-> [_ ( 1 / ( 1 / w ) ) / x ]_ R e. CC ) )
100 69 36 eqeltrd 
 |-  ( ( ph /\ y e. ( B i^i RR+ ) ) -> [_ ( 1 / y ) / x ]_ R e. CC )
101 100 ralrimiva 
 |-  ( ph -> A. y e. ( B i^i RR+ ) [_ ( 1 / y ) / x ]_ R e. CC )
102 101 ad2antrr 
 |-  ( ( ( ph /\ w e. A ) /\ -. w = 0 ) -> A. y e. ( B i^i RR+ ) [_ ( 1 / y ) / x ]_ R e. CC )
103 simplr 
 |-  ( ( ( ph /\ w e. A ) /\ -. w = 0 ) -> w e. A )
104 simpll 
 |-  ( ( ( ph /\ w e. A ) /\ -. w = 0 ) -> ph )
105 eleq1 
 |-  ( y = ( 1 / w ) -> ( y e. B <-> ( 1 / w ) e. B ) )
106 97 eleq1d 
 |-  ( y = ( 1 / w ) -> ( ( 1 / y ) e. A <-> ( 1 / ( 1 / w ) ) e. A ) )
107 105 106 bibi12d 
 |-  ( y = ( 1 / w ) -> ( ( y e. B <-> ( 1 / y ) e. A ) <-> ( ( 1 / w ) e. B <-> ( 1 / ( 1 / w ) ) e. A ) ) )
108 6 ralrimiva 
 |-  ( ph -> A. y e. RR+ ( y e. B <-> ( 1 / y ) e. A ) )
109 108 adantr 
 |-  ( ( ph /\ w e. RR+ ) -> A. y e. RR+ ( y e. B <-> ( 1 / y ) e. A ) )
110 rpreccl 
 |-  ( w e. RR+ -> ( 1 / w ) e. RR+ )
111 110 adantl 
 |-  ( ( ph /\ w e. RR+ ) -> ( 1 / w ) e. RR+ )
112 107 109 111 rspcdva 
 |-  ( ( ph /\ w e. RR+ ) -> ( ( 1 / w ) e. B <-> ( 1 / ( 1 / w ) ) e. A ) )
113 94 adantl 
 |-  ( ( ph /\ w e. RR+ ) -> ( 1 / ( 1 / w ) ) = w )
114 113 eleq1d 
 |-  ( ( ph /\ w e. RR+ ) -> ( ( 1 / ( 1 / w ) ) e. A <-> w e. A ) )
115 112 114 bitr2d 
 |-  ( ( ph /\ w e. RR+ ) -> ( w e. A <-> ( 1 / w ) e. B ) )
116 104 91 115 syl2anc 
 |-  ( ( ( ph /\ w e. A ) /\ -. w = 0 ) -> ( w e. A <-> ( 1 / w ) e. B ) )
117 103 116 mpbid 
 |-  ( ( ( ph /\ w e. A ) /\ -. w = 0 ) -> ( 1 / w ) e. B )
118 91 rpreccld 
 |-  ( ( ( ph /\ w e. A ) /\ -. w = 0 ) -> ( 1 / w ) e. RR+ )
119 117 118 elind 
 |-  ( ( ( ph /\ w e. A ) /\ -. w = 0 ) -> ( 1 / w ) e. ( B i^i RR+ ) )
120 99 102 119 rspcdva 
 |-  ( ( ( ph /\ w e. A ) /\ -. w = 0 ) -> [_ ( 1 / ( 1 / w ) ) / x ]_ R e. CC )
121 96 120 eqeltrrd 
 |-  ( ( ( ph /\ w e. A ) /\ -. w = 0 ) -> [_ w / x ]_ R e. CC )
122 73 121 ifclda 
 |-  ( ( ph /\ w e. A ) -> if ( w = 0 , C , [_ w / x ]_ R ) e. CC )
123 111 biantrud 
 |-  ( ( ph /\ w e. RR+ ) -> ( ( 1 / w ) e. B <-> ( ( 1 / w ) e. B /\ ( 1 / w ) e. RR+ ) ) )
124 115 123 bitrd 
 |-  ( ( ph /\ w e. RR+ ) -> ( w e. A <-> ( ( 1 / w ) e. B /\ ( 1 / w ) e. RR+ ) ) )
125 elin 
 |-  ( ( 1 / w ) e. ( B i^i RR+ ) <-> ( ( 1 / w ) e. B /\ ( 1 / w ) e. RR+ ) )
126 124 125 bitr4di 
 |-  ( ( ph /\ w e. RR+ ) -> ( w e. A <-> ( 1 / w ) e. ( B i^i RR+ ) ) )
127 iftrue 
 |-  ( w = 0 -> if ( w = 0 , C , [_ w / x ]_ R ) = C )
128 eqeq1 
 |-  ( w = ( 1 / y ) -> ( w = 0 <-> ( 1 / y ) = 0 ) )
129 csbeq1 
 |-  ( w = ( 1 / y ) -> [_ w / x ]_ R = [_ ( 1 / y ) / x ]_ R )
130 128 129 ifbieq2d 
 |-  ( w = ( 1 / y ) -> if ( w = 0 , C , [_ w / x ]_ R ) = if ( ( 1 / y ) = 0 , C , [_ ( 1 / y ) / x ]_ R ) )
131 1 2 55 122 126 127 130 8 9 rlimcnp 
 |-  ( ph -> ( ( y e. ( B i^i RR+ ) |-> if ( ( 1 / y ) = 0 , C , [_ ( 1 / y ) / x ]_ R ) ) ~~>r C <-> ( w e. A |-> if ( w = 0 , C , [_ w / x ]_ R ) ) e. ( ( K CnP J ) ` 0 ) ) )
132 nfcv 
 |-  F/_ w if ( x = 0 , C , R )
133 nfv 
 |-  F/ x w = 0
134 nfcv 
 |-  F/_ x C
135 nfcsb1v 
 |-  F/_ x [_ w / x ]_ R
136 133 134 135 nfif 
 |-  F/_ x if ( w = 0 , C , [_ w / x ]_ R )
137 eqeq1 
 |-  ( x = w -> ( x = 0 <-> w = 0 ) )
138 csbeq1a 
 |-  ( x = w -> R = [_ w / x ]_ R )
139 137 138 ifbieq2d 
 |-  ( x = w -> if ( x = 0 , C , R ) = if ( w = 0 , C , [_ w / x ]_ R ) )
140 132 136 139 cbvmpt 
 |-  ( x e. A |-> if ( x = 0 , C , R ) ) = ( w e. A |-> if ( w = 0 , C , [_ w / x ]_ R ) )
141 140 eleq1i 
 |-  ( ( x e. A |-> if ( x = 0 , C , R ) ) e. ( ( K CnP J ) ` 0 ) <-> ( w e. A |-> if ( w = 0 , C , [_ w / x ]_ R ) ) e. ( ( K CnP J ) ` 0 ) )
142 131 141 bitr4di 
 |-  ( ph -> ( ( y e. ( B i^i RR+ ) |-> if ( ( 1 / y ) = 0 , C , [_ ( 1 / y ) / x ]_ R ) ) ~~>r C <-> ( x e. A |-> if ( x = 0 , C , R ) ) e. ( ( K CnP J ) ` 0 ) ) )
143 53 72 142 3bitr2d 
 |-  ( ph -> ( ( y e. B |-> S ) ~~>r C <-> ( x e. A |-> if ( x = 0 , C , R ) ) e. ( ( K CnP J ) ` 0 ) ) )