Description: The restriction of a function converges if the original converges. (Contributed by Mario Carneiro, 16-Sep-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | rlimres | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | inss1 | |
|
2 | ssralv | |
|
3 | 1 2 | ax-mp | |
4 | 3 | reximi | |
5 | 4 | ralimi | |
6 | 5 | anim2i | |
7 | 6 | a1i | |
8 | rlimf | |
|
9 | rlimss | |
|
10 | eqidd | |
|
11 | 8 9 10 | rlim | |
12 | fssres | |
|
13 | 8 1 12 | sylancl | |
14 | resres | |
|
15 | ffn | |
|
16 | fnresdm | |
|
17 | 8 15 16 | 3syl | |
18 | 17 | reseq1d | |
19 | 14 18 | eqtr3id | |
20 | 19 | feq1d | |
21 | 13 20 | mpbid | |
22 | 1 9 | sstrid | |
23 | elinel2 | |
|
24 | 23 | fvresd | |
25 | 24 | adantl | |
26 | 21 22 25 | rlim | |
27 | 7 11 26 | 3imtr4d | |
28 | 27 | pm2.43i | |