Metamath Proof Explorer

Theorem clim2f

Description: Express the predicate: The limit of complex number sequence F is A , or F converges to A , with more general quantifier restrictions than clim . Similar to clim2 , but without the disjoint var constraint F k . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses nf 
|- F/_ k F
clim2f.z 
|- Z = ( ZZ>= ` M )
clim2f.m 
|- ( ph -> M e. ZZ )
clim2f.f 
|- ( ph -> F e. V )
clim2f.b 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )
Assertion 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 ) ) ) )

Proof

Step Hyp Ref Expression
1 nf 
 |-  F/_ k F
2 clim2f.z 
 |-  Z = ( ZZ>= ` M )
3 clim2f.m 
 |-  ( ph -> M e. ZZ )
4 clim2f.f 
 |-  ( ph -> F e. V )
5 clim2f.b 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = B )
6 eqidd 
 |-  ( ( ph /\ k e. ZZ ) -> ( F ` k ) = ( F ` k ) )
7 1 4 6 climf 
 |-  ( ph -> ( F ~~> A <-> ( A e. CC /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) ) ) )
8 2 uztrn2 
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
9 5 eleq1d 
 |-  ( ( ph /\ k e. Z ) -> ( ( F ` k ) e. CC <-> B e. CC ) )
10 5 fvoveq1d 
 |-  ( ( ph /\ k e. Z ) -> ( abs ` ( ( F ` k ) - A ) ) = ( abs ` ( B - A ) ) )
11 10 breq1d 
 |-  ( ( ph /\ k e. Z ) -> ( ( abs ` ( ( F ` k ) - A ) ) < x <-> ( abs ` ( B - A ) ) < x ) )
12 9 11 anbi12d 
 |-  ( ( ph /\ k e. Z ) -> ( ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) <-> ( B e. CC /\ ( abs ` ( B - A ) ) < x ) ) )
13 8 12 sylan2 
 |-  ( ( ph /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) <-> ( B e. CC /\ ( abs ` ( B - A ) ) < x ) ) )
14 13 anassrs 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) <-> ( B e. CC /\ ( abs ` ( B - A ) ) < x ) ) )
15 14 ralbidva 
 |-  ( ( ph /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) <-> A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - A ) ) < x ) ) )
16 15 rexbidva 
 |-  ( ph -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - A ) ) < x ) ) )
17 2 rexuz3 
 |-  ( M e. ZZ -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) ) )
18 3 17 syl 
 |-  ( ph -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) ) )
19 16 18 bitr3d 
 |-  ( ph -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - A ) ) < x ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) ) )
20 19 ralbidv 
 |-  ( ph -> ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - A ) ) < x ) <-> A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) ) )
21 20 anbi2d 
 |-  ( ph -> ( ( A e. CC /\ 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. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) ) ) )
22 7 21 bitr4d 
 |-  ( 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 ) ) ) )