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 | |
|
dfxlim2.m | |
||
dfxlim2.z | |
||
dfxlim2.f | |
||
Assertion | dfxlim2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfxlim2.k | |
|
2 | dfxlim2.m | |
|
3 | dfxlim2.z | |
|
4 | dfxlim2.f | |
|
5 | 2 3 4 | dfxlim2v | |
6 | biid | |
|
7 | breq2 | |
|
8 | 7 | rexralbidv | |
9 | fveq2 | |
|
10 | 9 | raleqdv | |
11 | nfcv | |
|
12 | 1 11 | nffv | |
13 | nfcv | |
|
14 | nfcv | |
|
15 | 12 13 14 | nfbr | |
16 | nfv | |
|
17 | fveq2 | |
|
18 | 17 | breq1d | |
19 | 15 16 18 | cbvralw | |
20 | 10 19 | bitrdi | |
21 | 20 | cbvrexvw | |
22 | 8 21 | bitrdi | |
23 | 22 | cbvralvw | |
24 | 23 | anbi2i | |
25 | breq1 | |
|
26 | 25 | rexralbidv | |
27 | 9 | raleqdv | |
28 | 14 13 12 | nfbr | |
29 | nfv | |
|
30 | 17 | breq2d | |
31 | 28 29 30 | cbvralw | |
32 | 27 31 | bitrdi | |
33 | 32 | cbvrexvw | |
34 | 26 33 | bitrdi | |
35 | 34 | cbvralvw | |
36 | 35 | anbi2i | |
37 | 6 24 36 | 3orbi123i | |
38 | 5 37 | bitrdi | |