Metamath Proof Explorer


Theorem clim2d

Description: The limit of complex number sequence F is eventually approximated. (Contributed by Glauco Siliprandi, 26-Jun-2021)

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

Proof

Step Hyp Ref Expression
1 clim2d.k
 |-  F/ k ph
2 clim2d.f
 |-  F/_ k F
3 clim2d.m
 |-  ( ph -> M e. ZZ )
4 clim2d.z
 |-  Z = ( ZZ>= ` M )
5 clim2d.c
 |-  ( ph -> F ~~> A )
6 clim2d.b
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = B )
7 clim2d.x
 |-  ( ph -> X e. RR+ )
8 climrel
 |-  Rel ~~>
9 8 a1i
 |-  ( ph -> Rel ~~> )
10 brrelex1
 |-  ( ( Rel ~~> /\ F ~~> A ) -> F e. _V )
11 9 5 10 syl2anc
 |-  ( ph -> F e. _V )
12 1 2 4 3 11 6 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 ) ) ) )
13 5 12 mpbid
 |-  ( ph -> ( A e. CC /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - A ) ) < x ) ) )
14 13 simprd
 |-  ( ph -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - A ) ) < x ) )
15 breq2
 |-  ( x = X -> ( ( abs ` ( B - A ) ) < x <-> ( abs ` ( B - A ) ) < X ) )
16 15 anbi2d
 |-  ( x = X -> ( ( B e. CC /\ ( abs ` ( B - A ) ) < x ) <-> ( B e. CC /\ ( abs ` ( B - A ) ) < X ) ) )
17 16 ralbidv
 |-  ( x = X -> ( A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - A ) ) < x ) <-> A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - A ) ) < X ) ) )
18 17 rexbidv
 |-  ( x = X -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - A ) ) < x ) <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - A ) ) < X ) ) )
19 18 rspcva
 |-  ( ( X e. RR+ /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - A ) ) < x ) ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - A ) ) < X ) )
20 7 14 19 syl2anc
 |-  ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - A ) ) < X ) )