Description: Lemma for rlimsqz and rlimsqz2 . (Contributed by Mario Carneiro, 18-Sep-2014) (Revised by Mario Carneiro, 20-May-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | rlimsqzlem.m | |
|
rlimsqzlem.e | |
||
rlimsqzlem.1 | |
||
rlimsqzlem.2 | |
||
rlimsqzlem.3 | |
||
rlimsqzlem.4 | |
||
Assertion | rlimsqzlem | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rlimsqzlem.m | |
|
2 | rlimsqzlem.e | |
|
3 | rlimsqzlem.1 | |
|
4 | rlimsqzlem.2 | |
|
5 | rlimsqzlem.3 | |
|
6 | rlimsqzlem.4 | |
|
7 | 1 | ad3antrrr | |
8 | 1 | ad2antrr | |
9 | elicopnf | |
|
10 | 8 9 | syl | |
11 | 10 | simprbda | |
12 | 11 | adantrr | |
13 | eqid | |
|
14 | 13 4 | dmmptd | |
15 | rlimss | |
|
16 | 3 15 | syl | |
17 | 14 16 | eqsstrrd | |
18 | 17 | adantr | |
19 | 18 | sselda | |
20 | 19 | adantr | |
21 | 10 | simplbda | |
22 | 21 | adantrr | |
23 | simprr | |
|
24 | 7 12 20 22 23 | letrd | |
25 | 6 | anassrs | |
26 | 25 | adantllr | |
27 | 24 26 | syldan | |
28 | 2 | adantr | |
29 | 5 28 | subcld | |
30 | 29 | abscld | |
31 | 30 | ad4ant13 | |
32 | rlimcl | |
|
33 | 3 32 | syl | |
34 | 33 | adantr | |
35 | 4 34 | subcld | |
36 | 35 | abscld | |
37 | 36 | ad4ant13 | |
38 | rpre | |
|
39 | 38 | ad3antlr | |
40 | lelttr | |
|
41 | 31 37 39 40 | syl3anc | |
42 | 27 41 | mpand | |
43 | 42 | expr | |
44 | 43 | an32s | |
45 | 44 | a2d | |
46 | 45 | ralimdva | |
47 | 46 | reximdva | |
48 | 47 | ralimdva | |
49 | 4 | ralrimiva | |
50 | 49 17 33 1 | rlim3 | |
51 | 5 | ralrimiva | |
52 | 51 17 2 1 | rlim3 | |
53 | 48 50 52 | 3imtr4d | |
54 | 3 53 | mpd | |