Metamath Proof Explorer

Theorem clim2

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 . (Contributed by NM, 6-Jan-2007) (Revised by Mario Carneiro, 31-Jan-2014)

Ref Expression
Hypotheses clim2.1 
|- Z = ( ZZ>= ` M )
clim2.2 
|- ( ph -> M e. ZZ )
clim2.3 
|- ( ph -> F e. V )
clim2.4 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )
Assertion clim2 
|- ( 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 clim2.1 
 |-  Z = ( ZZ>= ` M )
2 clim2.2 
 |-  ( ph -> M e. ZZ )
3 clim2.3 
 |-  ( ph -> F e. V )
4 clim2.4 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = B )
5 eqidd 
 |-  ( ( ph /\ k e. ZZ ) -> ( F ` k ) = ( F ` k ) )
6 3 5 clim 
 |-  ( 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 ) ) ) )
7 1 uztrn2 
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
8 4 eleq1d 
 |-  ( ( ph /\ k e. Z ) -> ( ( F ` k ) e. CC <-> B e. CC ) )
9 4 fvoveq1d 
 |-  ( ( ph /\ k e. Z ) -> ( abs ` ( ( F ` k ) - A ) ) = ( abs ` ( B - A ) ) )
10 9 breq1d 
 |-  ( ( ph /\ k e. Z ) -> ( ( abs ` ( ( F ` k ) - A ) ) < x <-> ( abs ` ( B - A ) ) < x ) )
11 8 10 anbi12d 
 |-  ( ( ph /\ k e. Z ) -> ( ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) <-> ( B e. CC /\ ( abs ` ( B - A ) ) < x ) ) )
12 7 11 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 ) ) )
13 12 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 ) ) )
14 13 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 ) ) )
15 14 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 ) ) )
16 1 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 ) ) )
17 2 16 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 ) ) )
18 15 17 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 ) ) )
19 18 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 ) ) )
20 19 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 ) ) ) )
21 6 20 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 ) ) ) )