Metamath Proof Explorer

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 syl6bb 
 |-  ( 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 syl6bb 
 |-  ( 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 syl6bb 
 |-  ( 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 syl6bb 
 |-  ( 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 syl6bb 
 |-  ( 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 ) ) ) ) )