This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem clim2f2

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 clim2f2.p 
|- F/ k ph
clim2f2.k 
|- F/_ k F
clim2f2.z 
|- Z = ( ZZ>= ` M )
clim2f2.m 
|- ( ph -> M e. ZZ )
clim2f2.f 
|- ( ph -> F e. V )
clim2f2.b 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )
Assertion clim2f2 
|- ( 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 clim2f2.p 
 |-  F/ k ph
2 clim2f2.k 
 |-  F/_ k F
3 clim2f2.z 
 |-  Z = ( ZZ>= ` M )
4 clim2f2.m 
 |-  ( ph -> M e. ZZ )
5 clim2f2.f 
 |-  ( ph -> F e. V )
6 clim2f2.b 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = B )
7 eqidd 
 |-  ( ( ph /\ k e. ZZ ) -> ( F ` k ) = ( F ` k ) )
8 1 2 5 7 climf2 
 |-  ( 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 ) ) ) )
9 nfv 
 |-  F/ k j e. Z
10 1 9 nfan 
 |-  F/ k ( ph /\ j e. Z )
11 3 uztrn2 
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
12 6 eleq1d 
 |-  ( ( ph /\ k e. Z ) -> ( ( F ` k ) e. CC <-> B e. CC ) )
13 6 fvoveq1d 
 |-  ( ( ph /\ k e. Z ) -> ( abs ` ( ( F ` k ) - A ) ) = ( abs ` ( B - A ) ) )
14 13 breq1d 
 |-  ( ( ph /\ k e. Z ) -> ( ( abs ` ( ( F ` k ) - A ) ) < x <-> ( abs ` ( B - A ) ) < x ) )
15 12 14 anbi12d 
 |-  ( ( ph /\ k e. Z ) -> ( ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) <-> ( B e. CC /\ ( abs ` ( B - A ) ) < x ) ) )
16 11 15 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 ) ) )
17 16 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 ) ) )
18 10 17 ralbida 
 |-  ( ( 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 ) ) )
19 18 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 ) ) )
20 3 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 ) ) )
21 4 20 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 ) ) )
22 19 21 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 ) ) )
23 22 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 ) ) )
24 23 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 ) ) ) )
25 8 24 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 ) ) ) )