Metamath Proof Explorer


Theorem xlimclim2lem

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 Z=M
xlimclim2lem.f φF:Z*
xlimclim2lem.a φA
xlimclim2lem.r φjZFj:j
Assertion xlimclim2lem φF*AFA

Proof

Step Hyp Ref Expression
1 xlimclim2lem.z Z=M
2 xlimclim2lem.f φF:Z*
3 xlimclim2lem.a φA
4 xlimclim2lem.r φjZFj:j
5 1 2 fuzxrpmcn φF*𝑝𝑚
6 5 ad2antrr φjZFj:jF*𝑝𝑚
7 1 eluzelz2 jZj
8 7 ad2antlr φjZFj:jj
9 6 8 xlimres φjZFj:jF*AFj*A
10 eqid j=j
11 simpr φjZFj:jFj:j
12 3 ad2antrr φjZFj:jA
13 8 10 11 12 xlimclim φjZFj:jFj*AFjA
14 1 fvexi ZV
15 14 a1i φZV
16 2 15 fexd φFV
17 climres jFVFjAFA
18 7 16 17 syl2anr φjZFjAFA
19 18 adantr φjZFj:jFjAFA
20 9 13 19 3bitrd φjZFj:jF*AFA
21 20 4 r19.29a φF*AFA