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 _kF
dfxlim2.m φM
dfxlim2.z Z=M
dfxlim2.f φF:Z*
Assertion dfxlim2 φF*AFAA=−∞xjZkjFkxA=+∞xjZkjxFk

Proof

Step Hyp Ref Expression
1 dfxlim2.k _kF
2 dfxlim2.m φM
3 dfxlim2.z Z=M
4 dfxlim2.f φF:Z*
5 2 3 4 dfxlim2v φF*AFAA=−∞yiZliFlyA=+∞yiZliyFl
6 biid FAFA
7 breq2 y=xFlyFlx
8 7 rexralbidv y=xiZliFlyiZliFlx
9 fveq2 i=ji=j
10 9 raleqdv i=jliFlxljFlx
11 nfcv _kl
12 1 11 nffv _kFl
13 nfcv _k
14 nfcv _kx
15 12 13 14 nfbr kFlx
16 nfv lFkx
17 fveq2 l=kFl=Fk
18 17 breq1d l=kFlxFkx
19 15 16 18 cbvralw ljFlxkjFkx
20 10 19 bitrdi i=jliFlxkjFkx
21 20 cbvrexvw iZliFlxjZkjFkx
22 8 21 bitrdi y=xiZliFlyjZkjFkx
23 22 cbvralvw yiZliFlyxjZkjFkx
24 23 anbi2i A=−∞yiZliFlyA=−∞xjZkjFkx
25 breq1 y=xyFlxFl
26 25 rexralbidv y=xiZliyFliZlixFl
27 9 raleqdv i=jlixFlljxFl
28 14 13 12 nfbr kxFl
29 nfv lxFk
30 17 breq2d l=kxFlxFk
31 28 29 30 cbvralw ljxFlkjxFk
32 27 31 bitrdi i=jlixFlkjxFk
33 32 cbvrexvw iZlixFljZkjxFk
34 26 33 bitrdi y=xiZliyFljZkjxFk
35 34 cbvralvw yiZliyFlxjZkjxFk
36 35 anbi2i A=+∞yiZliyFlA=+∞xjZkjxFk
37 6 24 36 3orbi123i FAA=−∞yiZliFlyA=+∞yiZliyFlFAA=−∞xjZkjFkxA=+∞xjZkjxFk
38 5 37 bitrdi φF*AFAA=−∞xjZkjFkxA=+∞xjZkjxFk