Metamath Proof Explorer

Theorem clim0cf

Description: Express the predicate F converges to 0 . Similar to clim , but without the disjoint var constraint F k . (Contributed by Glauco Siliprandi, 11-Dec-2019)

		Ref	Expression
	Hypotheses	clim0cf.nf	\|- F/_ k F
		clim0cf.z	\|- Z = ( ZZ>= ` M )
		clim0cf.m	\|- ( ph -> M e. ZZ )
		clim0cf.f	\|- ( ph -> F e. V )
		clim0cf.fv	\|- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )
		clim0cf.b	\|- ( ( ph /\ k e. Z ) -> B e. CC )
	Assertion	clim0cf	\|- ( ph -> ( F ~~> 0 <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` B ) < x ) )

Proof

Step	Hyp	Ref	Expression
1		clim0cf.nf	\|- F/_ k F
2		clim0cf.z	\|- Z = ( ZZ>= ` M )
3		clim0cf.m	\|- ( ph -> M e. ZZ )
4		clim0cf.f	\|- ( ph -> F e. V )
5		clim0cf.fv	\|- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )
6		clim0cf.b	\|- ( ( ph /\ k e. Z ) -> B e. CC )
7		0cnd	\|- ( ph -> 0 e. CC )
8	1 2 3 4 5 7 6	clim2cf	\|- ( ph -> ( F ~~> 0 <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( B - 0 ) ) < x ) )
9	2	uztrn2	\|- ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
10	6	subid1d	\|- ( ( ph /\ k e. Z ) -> ( B - 0 ) = B )
11	10	fveq2d	\|- ( ( ph /\ k e. Z ) -> ( abs ` ( B - 0 ) ) = ( abs ` B ) )
12	11	breq1d	\|- ( ( ph /\ k e. Z ) -> ( ( abs ` ( B - 0 ) ) < x <-> ( abs ` B ) < x ) )
13	9 12	sylan2	\|- ( ( ph /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( ( abs ` ( B - 0 ) ) < x <-> ( abs ` B ) < x ) )
14	13	anassrs	\|- ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( ( abs ` ( B - 0 ) ) < x <-> ( abs ` B ) < x ) )
15	14	ralbidva	\|- ( ( ph /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( abs ` ( B - 0 ) ) < x <-> A. k e. ( ZZ>= ` j ) ( abs ` B ) < x ) )
16	15	rexbidva	\|- ( ph -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( B - 0 ) ) < x <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` B ) < x ) )
17	16	ralbidv	\|- ( ph -> ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( B - 0 ) ) < x <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` B ) < x ) )
18	8 17	bitrd	\|- ( ph -> ( F ~~> 0 <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` B ) < x ) )