Metamath Proof Explorer

Theorem climi

Description: Convergence of a sequence of complex numbers. (Contributed by NM, 11-Jan-2007) (Revised by Mario Carneiro, 31-Jan-2014)

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

Proof

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