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 )