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 F A F B A

Proof

Step Hyp Ref Expression
1 inss1 dom F B dom F
2 ssralv dom F B dom F z dom F y z F z A < x z dom F B y z F z A < x
3 1 2 ax-mp z dom F y z F z A < x z dom F B y z F z A < x
4 3 reximi y z dom F y z F z A < x y z dom F B y z F z A < x
5 4 ralimi x + y z dom F y z F z A < x x + y z dom F B y z F z A < x
6 5 anim2i A x + y z dom F y z F z A < x A x + y z dom F B y z F z A < x
7 6 a1i F A A x + y z dom F y z F z A < x A x + y z dom F B y z F z A < x
8 rlimf F A F : dom F
9 rlimss F A dom F
10 eqidd F A z dom F F z = F z
11 8 9 10 rlim F A F A A x + y z dom F y z F z A < x
12 fssres F : dom F dom F B dom F F dom F B : dom F B
13 8 1 12 sylancl F A F dom F B : dom F B
14 resres F dom F B = F dom F B
15 ffn F : dom F F Fn dom F
16 fnresdm F Fn dom F F dom F = F
17 8 15 16 3syl F A F dom F = F
18 17 reseq1d F A F dom F B = F B
19 14 18 eqtr3id F A F dom F B = F B
20 19 feq1d F A F dom F B : dom F B F B : dom F B
21 13 20 mpbid F A F B : dom F B
22 1 9 sstrid F A dom F B
23 elinel2 z dom F B z B
24 23 fvresd z dom F B F B z = F z
25 24 adantl F A z dom F B F B z = F z
26 21 22 25 rlim F A F B A A x + y z dom F B y z F z A < x
27 7 11 26 3imtr4d F A F A F B A
28 27 pm2.43i F A F B A