Theorem climd

Description: Express the predicate: The limit of complex number sequence F is A , or F converges to A . (Contributed by Glauco Siliprandi, 26-Jun-2021)

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

Proof

Step	Hyp	Ref	Expression
1		climd.1	|- F/ k ph
2		climd.2	|- F/_ k F
3		climd.3	|- Z = ( ZZ>= ` M )
4		climd.4	|- ( ph -> M e. ZZ )
5		climd.5	|- ( ph -> F ~~> A )
6		climd.6	|- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )
7		climd.7	|- ( ph -> X e. RR+ )
8		climrel	|- Rel ~~>
9	8	brrelex1i	|- ( F ~~> A -> F e. _V )
10	5 9	syl	|- ( ph -> F e. _V )
11	1 2 3 4 10 6	clim2f2	|- ( 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 ) ) ) )
12	5 11	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 ) ) )
13	12	simprd	|- ( ph -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - A ) ) < x ) )
14		breq2	|- ( x = X -> ( ( abs ` ( B - A ) ) < x <-> ( abs ` ( B - A ) ) < X ) )
15	14	anbi2d	|- ( x = X -> ( ( B e. CC /\ ( abs ` ( B - A ) ) < x ) <-> ( B e. CC /\ ( abs ` ( B - A ) ) < X ) ) )
16	15	rexralbidv	|- ( x = X -> ( 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 ) ) < X ) ) )
17	16	rspcva	|- ( ( X e. RR+ /\ A. x e. RR+ 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 ) ) < X ) )
18	7 13 17	syl2anc	|- ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - A ) ) < X ) )