Description: Lemma for xlimclim2 . Here it is additionally assumed that the sequence will eventually become (and stay) real. (Contributed by Glauco Siliprandi, 5-Feb-2022)
Ref | Expression | ||
---|---|---|---|
Hypotheses | xlimclim2lem.z | |
|
xlimclim2lem.f | |
||
xlimclim2lem.a | |
||
xlimclim2lem.r | |
||
Assertion | xlimclim2lem | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xlimclim2lem.z | |
|
2 | xlimclim2lem.f | |
|
3 | xlimclim2lem.a | |
|
4 | xlimclim2lem.r | |
|
5 | 1 2 | fuzxrpmcn | |
6 | 5 | ad2antrr | |
7 | 1 | eluzelz2 | |
8 | 7 | ad2antlr | |
9 | 6 8 | xlimres | |
10 | eqid | |
|
11 | simpr | |
|
12 | 3 | ad2antrr | |
13 | 8 10 11 12 | xlimclim | |
14 | 1 | fvexi | |
15 | 14 | a1i | |
16 | 2 15 | fexd | |
17 | climres | |
|
18 | 7 16 17 | syl2anr | |
19 | 18 | adantr | |
20 | 9 13 19 | 3bitrd | |
21 | 20 4 | r19.29a | |