Theorem clim0

Description: Express the predicate F converges to 0 . (Contributed by NM, 24-Feb-2008) (Revised by Mario Carneiro, 31-Jan-2014)

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

Proof

Step	Hyp	Ref	Expression
1		clim0.1	|- Z = ( ZZ>= ` M )
2		clim0.2	|- ( ph -> M e. ZZ )
3		clim0.3	|- ( ph -> F e. V )
4		clim0.4	|- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )
5	1 2 3 4	clim2	|- ( ph -> ( F ~~> 0 <-> ( 0 e. CC /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - 0 ) ) < x ) ) ) )
6		0cn	|- 0 e. CC
7	6	biantrur	|- ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - 0 ) ) < x ) <-> ( 0 e. CC /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - 0 ) ) < x ) ) )
8		subid1	|- ( B e. CC -> ( B - 0 ) = B )
9	8	fveq2d	|- ( B e. CC -> ( abs ` ( B - 0 ) ) = ( abs ` B ) )
10	9	breq1d	|- ( B e. CC -> ( ( abs ` ( B - 0 ) ) < x <-> ( abs ` B ) < x ) )
11	10	pm5.32i	|- ( ( B e. CC /\ ( abs ` ( B - 0 ) ) < x ) <-> ( B e. CC /\ ( abs ` B ) < x ) )
12	11	ralbii	|- ( A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - 0 ) ) < x ) <-> A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` B ) < x ) )
13	12	rexbii	|- ( E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - 0 ) ) < x ) <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` B ) < x ) )
14	13	ralbii	|- ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - 0 ) ) < x ) <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` B ) < x ) )
15	7 14	bitr3i	|- ( ( 0 e. CC /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - 0 ) ) < x ) ) <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` B ) < x ) )
16	5 15	bitrdi	|- ( ph -> ( F ~~> 0 <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` B ) < x ) ) )