Metamath Proof Explorer

Theorem clim2cf

Description: Express the predicate F converges to A . Similar to clim2 , but without the disjoint var constraint F k . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses clim2cf.nf 
|- F/_ k F
clim2cf.z 
|- Z = ( ZZ>= ` M )
clim2cf.m 
|- ( ph -> M e. ZZ )
clim2cf.f 
|- ( ph -> F e. V )
clim2cf.fv 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )
clim2cf.a 
|- ( ph -> A e. CC )
clim2cf.b 
|- ( ( ph /\ k e. Z ) -> B e. CC )
Assertion clim2cf 
|- ( ph -> ( F ~~> A <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( B - A ) ) < x ) )

Proof

Step Hyp Ref Expression
1 clim2cf.nf 
 |-  F/_ k F
2 clim2cf.z 
 |-  Z = ( ZZ>= ` M )
3 clim2cf.m 
 |-  ( ph -> M e. ZZ )
4 clim2cf.f 
 |-  ( ph -> F e. V )
5 clim2cf.fv 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = B )
6 clim2cf.a 
 |-  ( ph -> A e. CC )
7 clim2cf.b 
 |-  ( ( ph /\ k e. Z ) -> B e. CC )
8 6 biantrurd 
 |-  ( ph -> ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - A ) ) < x ) <-> ( A e. CC /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - A ) ) < x ) ) ) )
9 2 uztrn2 
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
10 7 biantrurd 
 |-  ( ( ph /\ k e. Z ) -> ( ( abs ` ( B - A ) ) < x <-> ( B e. CC /\ ( abs ` ( B - A ) ) < x ) ) )
11 9 10 sylan2 
 |-  ( ( ph /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( ( abs ` ( B - A ) ) < x <-> ( B e. CC /\ ( abs ` ( B - A ) ) < x ) ) )
12 11 anassrs 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( ( abs ` ( B - A ) ) < x <-> ( B e. CC /\ ( abs ` ( B - A ) ) < x ) ) )
13 12 ralbidva 
 |-  ( ( ph /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( abs ` ( B - A ) ) < x <-> A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - A ) ) < x ) ) )
14 13 rexbidva 
 |-  ( ph -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( B - A ) ) < x <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - A ) ) < x ) ) )
15 14 ralbidv 
 |-  ( ph -> ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( B - A ) ) < x <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - A ) ) < x ) ) )
16 1 2 3 4 5 clim2f 
 |-  ( ph -> ( F ~~> A <-> ( A e. CC /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - A ) ) < x ) ) ) )
17 8 15 16 3bitr4rd 
 |-  ( ph -> ( F ~~> A <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( B - A ) ) < x ) )