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

Metamath Proof Explorer

Theorem climd

Description: Express the predicate: The limit of complex number sequence F is A , or F converges to A . (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses climd.1 
|- F/ k ph
climd.2 
|- F/_ k F
climd.3 
|- Z = ( ZZ>= ` M )
climd.4 
|- ( ph -> M e. ZZ )
climd.5 
|- ( ph -> F ~~> A )
climd.6 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )
climd.7 
|- ( ph -> X e. RR+ )
Assertion climd 
|- ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - A ) ) < X ) )

Proof

Step Hyp Ref Expression
1 climd.1 
 |-  F/ k ph
2 climd.2 
 |-  F/_ k F
3 climd.3 
 |-  Z = ( ZZ>= ` M )
4 climd.4 
 |-  ( ph -> M e. ZZ )
5 climd.5 
 |-  ( ph -> F ~~> A )
6 climd.6 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = B )
7 climd.7 
 |-  ( ph -> X e. RR+ )
8 climrel 
 |-  Rel ~~>
9 8 brrelex1i 
 |-  ( F ~~> A -> F e. _V )
10 5 9 syl 
 |-  ( ph -> F e. _V )
11 1 2 3 4 10 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 ) ) ) )
12 5 11 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 ) ) )
13 12 simprd 
 |-  ( ph -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - A ) ) < x ) )
14 breq2 
 |-  ( x = X -> ( ( abs ` ( B - A ) ) < x <-> ( abs ` ( B - A ) ) < X ) )
15 14 anbi2d 
 |-  ( x = X -> ( ( B e. CC /\ ( abs ` ( B - A ) ) < x ) <-> ( B e. CC /\ ( abs ` ( B - A ) ) < X ) ) )
16 15 rexralbidv 
 |-  ( 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 ) ) )
17 16 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 ) )
18 7 13 17 syl2anc 
 |-  ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - A ) ) < X ) )