Metamath Proof Explorer

Theorem dfxlim2v

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 dfxlim2v.1 
|- ( ph -> M e. ZZ )
dfxlim2v.2 
|- Z = ( ZZ>= ` M )
dfxlim2v.3 
|- ( ph -> F : Z --> RR* )
Assertion dfxlim2v 
|- ( 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 dfxlim2v.1 
 |-  ( ph -> M e. ZZ )
2 dfxlim2v.2 
 |-  Z = ( ZZ>= ` M )
3 dfxlim2v.3 
 |-  ( ph -> F : Z --> RR* )
4 simplr 
 |-  ( ( ( ph /\ F ~~>* A ) /\ A e. RR ) -> F ~~>* A )
5 1 adantr 
 |-  ( ( ph /\ A e. RR ) -> M e. ZZ )
6 3 adantr 
 |-  ( ( ph /\ A e. RR ) -> F : Z --> RR* )
7 simpr 
 |-  ( ( ph /\ A e. RR ) -> A e. RR )
8 5 2 6 7 xlimclim2 
 |-  ( ( ph /\ A e. RR ) -> ( F ~~>* A <-> F ~~> A ) )
9 8 adantlr 
 |-  ( ( ( ph /\ F ~~>* A ) /\ A e. RR ) -> ( F ~~>* A <-> F ~~> A ) )
10 4 9 mpbid 
 |-  ( ( ( ph /\ F ~~>* A ) /\ A e. RR ) -> F ~~> A )
11 10 3mix1d 
 |-  ( ( ( ph /\ F ~~>* A ) /\ A e. RR ) -> ( 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 ) ) ) )
12 simpr 
 |-  ( ( ( ph /\ F ~~>* A ) /\ A = -oo ) -> A = -oo )
13 simpl 
 |-  ( ( F ~~>* A /\ A = -oo ) -> F ~~>* A )
14 simpr 
 |-  ( ( F ~~>* A /\ A = -oo ) -> A = -oo )
15 13 14 breqtrd 
 |-  ( ( F ~~>* A /\ A = -oo ) -> F ~~>* -oo )
16 15 adantll 
 |-  ( ( ( ph /\ F ~~>* A ) /\ A = -oo ) -> F ~~>* -oo )
17 nfcv 
 |-  F/_ k F
18 17 1 2 3 xlimmnf 
 |-  ( ph -> ( F ~~>* -oo <-> A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) <_ x ) )
19 18 ad2antrr 
 |-  ( ( ( ph /\ F ~~>* A ) /\ A = -oo ) -> ( F ~~>* -oo <-> A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) <_ x ) )
20 16 19 mpbid 
 |-  ( ( ( ph /\ F ~~>* A ) /\ A = -oo ) -> A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) <_ x )
21 3mix2 
 |-  ( ( A = -oo /\ A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) <_ x ) -> ( 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 ) ) ) )
22 12 20 21 syl2anc 
 |-  ( ( ( ph /\ F ~~>* A ) /\ A = -oo ) -> ( 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 ) ) ) )
23 22 adantlr 
 |-  ( ( ( ( ph /\ F ~~>* A ) /\ -. A e. RR ) /\ A = -oo ) -> ( 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 ) ) ) )
24 simpll 
 |-  ( ( ( ( ph /\ F ~~>* A ) /\ -. A e. RR ) /\ -. A = -oo ) -> ( ph /\ F ~~>* A ) )
25 xlimcl 
 |-  ( F ~~>* A -> A e. RR* )
26 25 ad3antlr 
 |-  ( ( ( ( ph /\ F ~~>* A ) /\ -. A e. RR ) /\ -. A = -oo ) -> A e. RR* )
27 simplr 
 |-  ( ( ( ( ph /\ F ~~>* A ) /\ -. A e. RR ) /\ -. A = -oo ) -> -. A e. RR )
28 neqne 
 |-  ( -. A = -oo -> A =/= -oo )
29 28 adantl 
 |-  ( ( ( ( ph /\ F ~~>* A ) /\ -. A e. RR ) /\ -. A = -oo ) -> A =/= -oo )
30 26 27 29 xrnmnfpnf 
 |-  ( ( ( ( ph /\ F ~~>* A ) /\ -. A e. RR ) /\ -. A = -oo ) -> A = +oo )
31 simpr 
 |-  ( ( ( ph /\ F ~~>* A ) /\ A = +oo ) -> A = +oo )
32 simpl 
 |-  ( ( F ~~>* A /\ A = +oo ) -> F ~~>* A )
33 simpr 
 |-  ( ( F ~~>* A /\ A = +oo ) -> A = +oo )
34 32 33 breqtrd 
 |-  ( ( F ~~>* A /\ A = +oo ) -> F ~~>* +oo )
35 34 adantll 
 |-  ( ( ( ph /\ F ~~>* A ) /\ A = +oo ) -> F ~~>* +oo )
36 17 1 2 3 xlimpnf 
 |-  ( ph -> ( F ~~>* +oo <-> A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) x <_ ( F ` k ) ) )
37 36 ad2antrr 
 |-  ( ( ( ph /\ F ~~>* A ) /\ A = +oo ) -> ( F ~~>* +oo <-> A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) x <_ ( F ` k ) ) )
38 35 37 mpbid 
 |-  ( ( ( ph /\ F ~~>* A ) /\ A = +oo ) -> A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) x <_ ( F ` k ) )
39 3mix3 
 |-  ( ( A = +oo /\ A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) x <_ ( F ` k ) ) -> ( 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 ) ) ) )
40 31 38 39 syl2anc 
 |-  ( ( ( ph /\ F ~~>* A ) /\ A = +oo ) -> ( 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 ) ) ) )
41 24 30 40 syl2anc 
 |-  ( ( ( ( ph /\ F ~~>* A ) /\ -. A e. RR ) /\ -. A = -oo ) -> ( 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 ) ) ) )
42 23 41 pm2.61dan 
 |-  ( ( ( ph /\ F ~~>* A ) /\ -. A e. RR ) -> ( 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 ) ) ) )
43 11 42 pm2.61dan 
 |-  ( ( 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 ) ) ) )
44 1 adantr 
 |-  ( ( ph /\ F ~~> A ) -> M e. ZZ )
45 3 adantr 
 |-  ( ( ph /\ F ~~> A ) -> F : Z --> RR* )
46 simpr 
 |-  ( ( ph /\ F ~~> A ) -> F ~~> A )
47 44 2 45 46 climxlim2 
 |-  ( ( ph /\ F ~~> A ) -> F ~~>* A )
48 18 biimpar 
 |-  ( ( ph /\ A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) <_ x ) -> F ~~>* -oo )
49 48 adantrl 
 |-  ( ( ph /\ ( A = -oo /\ A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) <_ x ) ) -> F ~~>* -oo )
50 simprl 
 |-  ( ( ph /\ ( A = -oo /\ A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) <_ x ) ) -> A = -oo )
51 49 50 breqtrrd 
 |-  ( ( ph /\ ( A = -oo /\ A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) <_ x ) ) -> F ~~>* A )
52 36 biimpar 
 |-  ( ( ph /\ A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) x <_ ( F ` k ) ) -> F ~~>* +oo )
53 52 adantrl 
 |-  ( ( ph /\ ( A = +oo /\ A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) x <_ ( F ` k ) ) ) -> F ~~>* +oo )
54 simprl 
 |-  ( ( ph /\ ( A = +oo /\ A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) x <_ ( F ` k ) ) ) -> A = +oo )
55 53 54 breqtrrd 
 |-  ( ( ph /\ ( A = +oo /\ A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) x <_ ( F ` k ) ) ) -> F ~~>* A )
56 47 51 55 3jaodan 
 |-  ( ( ph /\ ( 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 ) ) ) ) -> F ~~>* A )
57 43 56 impbida 
 |-  ( 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 ) ) ) ) )