Metamath Proof Explorer


Theorem rlimres

Description: The restriction of a function converges if the original converges. (Contributed by Mario Carneiro, 16-Sep-2014)

Ref Expression
Assertion rlimres FAFBA

Proof

Step Hyp Ref Expression
1 inss1 domFBdomF
2 ssralv domFBdomFzdomFyzFzA<xzdomFByzFzA<x
3 1 2 ax-mp zdomFyzFzA<xzdomFByzFzA<x
4 3 reximi yzdomFyzFzA<xyzdomFByzFzA<x
5 4 ralimi x+yzdomFyzFzA<xx+yzdomFByzFzA<x
6 5 anim2i Ax+yzdomFyzFzA<xAx+yzdomFByzFzA<x
7 6 a1i FAAx+yzdomFyzFzA<xAx+yzdomFByzFzA<x
8 rlimf FAF:domF
9 rlimss FAdomF
10 eqidd FAzdomFFz=Fz
11 8 9 10 rlim FAFAAx+yzdomFyzFzA<x
12 fssres F:domFdomFBdomFFdomFB:domFB
13 8 1 12 sylancl FAFdomFB:domFB
14 resres FdomFB=FdomFB
15 ffn F:domFFFndomF
16 fnresdm FFndomFFdomF=F
17 8 15 16 3syl FAFdomF=F
18 17 reseq1d FAFdomFB=FB
19 14 18 eqtr3id FAFdomFB=FB
20 19 feq1d FAFdomFB:domFBFB:domFB
21 13 20 mpbid FAFB:domFB
22 1 9 sstrid FAdomFB
23 elinel2 zdomFBzB
24 23 fvresd zdomFBFBz=Fz
25 24 adantl FAzdomFBFBz=Fz
26 21 22 25 rlim FAFBAAx+yzdomFByzFzA<x
27 7 11 26 3imtr4d FAFAFBA
28 27 pm2.43i FAFBA