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

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 ) )