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 = ( ZZ>= ` M )
xlimclim2lem.f 
|- ( ph -> F : Z --> RR* )
xlimclim2lem.a 
|- ( ph -> A e. RR )
xlimclim2lem.r 
|- ( ph -> E. j e. Z ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR )
Assertion xlimclim2lem 
|- ( ph -> ( F ~~>* A <-> F ~~> A ) )

Proof

Step Hyp Ref Expression
1 xlimclim2lem.z 
 |-  Z = ( ZZ>= ` M )
2 xlimclim2lem.f 
 |-  ( ph -> F : Z --> RR* )
3 xlimclim2lem.a 
 |-  ( ph -> A e. RR )
4 xlimclim2lem.r 
 |-  ( ph -> E. j e. Z ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR )
5 1 2 fuzxrpmcn 
 |-  ( ph -> F e. ( RR* ^pm CC ) )
6 5 ad2antrr 
 |-  ( ( ( ph /\ j e. Z ) /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR ) -> F e. ( RR* ^pm CC ) )
7 1 eluzelz2 
 |-  ( j e. Z -> j e. ZZ )
8 7 ad2antlr 
 |-  ( ( ( ph /\ j e. Z ) /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR ) -> j e. ZZ )
9 6 8 xlimres 
 |-  ( ( ( ph /\ j e. Z ) /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR ) -> ( F ~~>* A <-> ( F |` ( ZZ>= ` j ) ) ~~>* A ) )
10 eqid 
 |-  ( ZZ>= ` j ) = ( ZZ>= ` j )
11 simpr 
 |-  ( ( ( ph /\ j e. Z ) /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR ) -> ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR )
12 3 ad2antrr 
 |-  ( ( ( ph /\ j e. Z ) /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR ) -> A e. RR )
13 8 10 11 12 xlimclim 
 |-  ( ( ( ph /\ j e. Z ) /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR ) -> ( ( F |` ( ZZ>= ` j ) ) ~~>* A <-> ( F |` ( ZZ>= ` j ) ) ~~> A ) )
14 1 fvexi 
 |-  Z e. _V
15 14 a1i 
 |-  ( ph -> Z e. _V )
16 2 15 fexd 
 |-  ( ph -> F e. _V )
17 climres 
 |-  ( ( j e. ZZ /\ F e. _V ) -> ( ( F |` ( ZZ>= ` j ) ) ~~> A <-> F ~~> A ) )
18 7 16 17 syl2anr 
 |-  ( ( ph /\ j e. Z ) -> ( ( F |` ( ZZ>= ` j ) ) ~~> A <-> F ~~> A ) )
19 18 adantr 
 |-  ( ( ( ph /\ j e. Z ) /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR ) -> ( ( F |` ( ZZ>= ` j ) ) ~~> A <-> F ~~> A ) )
20 9 13 19 3bitrd 
 |-  ( ( ( ph /\ j e. Z ) /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR ) -> ( F ~~>* A <-> F ~~> A ) )
21 20 4 r19.29a 
 |-  ( ph -> ( F ~~>* A <-> F ~~> A ) )