Theorem dfxlim2

Description: An alternative definition for the convergence relation in the extended real numbers. This resembles what's found in most textbooks: three distinct definitions for the same symbol (limit of a sequence). (Contributed by Glauco Siliprandi, 5-Feb-2022)

	Ref	Expression
Hypotheses	dfxlim2.k	|- F/_ k F
	dfxlim2.m	|- ( ph -> M e. ZZ )
	dfxlim2.z	|- Z = ( ZZ>= ` M )
	dfxlim2.f	|- ( ph -> F : Z --> RR* )
Assertion	dfxlim2	|- ( ph -> ( F ~~>* A <-> ( F ~~> A \/ ( A = -oo /\ A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) <_ x ) \/ ( A = +oo /\ A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) x <_ ( F ` k ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfxlim2.k	|- F/_ k F
2		dfxlim2.m	|- ( ph -> M e. ZZ )
3		dfxlim2.z	|- Z = ( ZZ>= ` M )
4		dfxlim2.f	|- ( ph -> F : Z --> RR* )
5	2 3 4	dfxlim2v	|- ( ph -> ( F ~~>* A <-> ( F ~~> A \/ ( A = -oo /\ A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ y ) \/ ( A = +oo /\ A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) ) ) ) )
6		biid	|- ( F ~~> A <-> F ~~> A )
7		breq2	|- ( y = x -> ( ( F ` l ) <_ y <-> ( F ` l ) <_ x ) )
8	7	rexralbidv	|- ( y = x -> ( E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ y <-> E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ x ) )
9		fveq2	|- ( i = j -> ( ZZ>= ` i ) = ( ZZ>= ` j ) )
10	9	raleqdv	|- ( i = j -> ( A. l e. ( ZZ>= ` i ) ( F ` l ) <_ x <-> A. l e. ( ZZ>= ` j ) ( F ` l ) <_ x ) )
11		nfcv	|- F/_ k l
12	1 11	nffv	|- F/_ k ( F ` l )
13		nfcv	|- F/_ k <_
14		nfcv	|- F/_ k x
15	12 13 14	nfbr	|- F/ k ( F ` l ) <_ x
16		nfv	|- F/ l ( F ` k ) <_ x
17		fveq2	|- ( l = k -> ( F ` l ) = ( F ` k ) )
18	17	breq1d	|- ( l = k -> ( ( F ` l ) <_ x <-> ( F ` k ) <_ x ) )
19	15 16 18	cbvralw	|- ( A. l e. ( ZZ>= ` j ) ( F ` l ) <_ x <-> A. k e. ( ZZ>= ` j ) ( F ` k ) <_ x )
20	10 19	bitrdi	|- ( i = j -> ( A. l e. ( ZZ>= ` i ) ( F ` l ) <_ x <-> A. k e. ( ZZ>= ` j ) ( F ` k ) <_ x ) )
21	20	cbvrexvw	|- ( E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ x <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) <_ x )
22	8 21	bitrdi	|- ( y = x -> ( E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ y <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) <_ x ) )
23	22	cbvralvw	|- ( A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ y <-> A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) <_ x )
24	23	anbi2i	|- ( ( A = -oo /\ A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ y ) <-> ( A = -oo /\ A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) <_ x ) )
25		breq1	|- ( y = x -> ( y <_ ( F ` l ) <-> x <_ ( F ` l ) ) )
26	25	rexralbidv	|- ( y = x -> ( E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) <-> E. i e. Z A. l e. ( ZZ>= ` i ) x <_ ( F ` l ) ) )
27	9	raleqdv	|- ( i = j -> ( A. l e. ( ZZ>= ` i ) x <_ ( F ` l ) <-> A. l e. ( ZZ>= ` j ) x <_ ( F ` l ) ) )
28	14 13 12	nfbr	|- F/ k x <_ ( F ` l )
29		nfv	|- F/ l x <_ ( F ` k )
30	17	breq2d	|- ( l = k -> ( x <_ ( F ` l ) <-> x <_ ( F ` k ) ) )
31	28 29 30	cbvralw	|- ( A. l e. ( ZZ>= ` j ) x <_ ( F ` l ) <-> A. k e. ( ZZ>= ` j ) x <_ ( F ` k ) )
32	27 31	bitrdi	|- ( i = j -> ( A. l e. ( ZZ>= ` i ) x <_ ( F ` l ) <-> A. k e. ( ZZ>= ` j ) x <_ ( F ` k ) ) )
33	32	cbvrexvw	|- ( E. i e. Z A. l e. ( ZZ>= ` i ) x <_ ( F ` l ) <-> E. j e. Z A. k e. ( ZZ>= ` j ) x <_ ( F ` k ) )
34	26 33	bitrdi	|- ( y = x -> ( E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) <-> E. j e. Z A. k e. ( ZZ>= ` j ) x <_ ( F ` k ) ) )
35	34	cbvralvw	|- ( A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) <-> A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) x <_ ( F ` k ) )
36	35	anbi2i	|- ( ( A = +oo /\ A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) ) <-> ( A = +oo /\ A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) x <_ ( F ` k ) ) )
37	6 24 36	3orbi123i	|- ( ( F ~~> A \/ ( A = -oo /\ A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ y ) \/ ( A = +oo /\ A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) ) ) <-> ( F ~~> A \/ ( A = -oo /\ A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) <_ x ) \/ ( A = +oo /\ A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) x <_ ( F ` k ) ) ) )
38	5 37	bitrdi	|- ( ph -> ( F ~~>* A <-> ( F ~~> A \/ ( A = -oo /\ A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) <_ x ) \/ ( A = +oo /\ A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) x <_ ( F ` k ) ) ) ) )