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

Metamath Proof Explorer

Theorem climi0

Description: Convergence of a sequence of complex numbers to zero. (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 )
climi0.5 
|- ( ph -> F ~~> 0 )
Assertion climi0 
|- ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` B ) < 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 climi0.5 
 |-  ( ph -> F ~~> 0 )
6 1 2 3 4 5 climi 
 |-  ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - 0 ) ) < C ) )
7 subid1 
 |-  ( B e. CC -> ( B - 0 ) = B )
8 7 fveq2d 
 |-  ( B e. CC -> ( abs ` ( B - 0 ) ) = ( abs ` B ) )
9 8 breq1d 
 |-  ( B e. CC -> ( ( abs ` ( B - 0 ) ) < C <-> ( abs ` B ) < C ) )
10 9 biimpa 
 |-  ( ( B e. CC /\ ( abs ` ( B - 0 ) ) < C ) -> ( abs ` B ) < C )
11 10 ralimi 
 |-  ( A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - 0 ) ) < C ) -> A. k e. ( ZZ>= ` j ) ( abs ` B ) < C )
12 11 reximi 
 |-  ( E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - 0 ) ) < C ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` B ) < C )
13 6 12 syl 
 |-  ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` B ) < C )