Description: Given a function on the reals, defined on a set of upper integers, its supremum limit is real if and only if two condition holds: 1. there is a real number that is less than or equal to the function, infinitely often; 2. there is a real number that is greater than or equal to the function. (Contributed by Glauco Siliprandi, 23-Oct-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | limsupreuzmpt.j | |
|
limsupreuzmpt.m | |
||
limsupreuzmpt.z | |
||
limsupreuzmpt.b | |
||
Assertion | limsupreuzmpt | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | limsupreuzmpt.j | |
|
2 | limsupreuzmpt.m | |
|
3 | limsupreuzmpt.z | |
|
4 | limsupreuzmpt.b | |
|
5 | nfmpt1 | |
|
6 | 1 4 | fmptd2f | |
7 | 5 2 3 6 | limsupreuz | |
8 | nfv | |
|
9 | 1 8 | nfan | |
10 | simpll | |
|
11 | 3 | uztrn2 | |
12 | 11 | adantll | |
13 | eqid | |
|
14 | 13 | a1i | |
15 | 14 4 | fvmpt2d | |
16 | 10 12 15 | syl2anc | |
17 | 16 | breq2d | |
18 | 9 17 | rexbida | |
19 | 18 | ralbidva | |
20 | 19 | rexbidv | |
21 | breq1 | |
|
22 | 21 | rexbidv | |
23 | 22 | ralbidv | |
24 | fveq2 | |
|
25 | 24 | rexeqdv | |
26 | 25 | cbvralvw | |
27 | 26 | a1i | |
28 | 23 27 | bitrd | |
29 | 28 | cbvrexvw | |
30 | 29 | a1i | |
31 | 20 30 | bitrd | |
32 | 15 | breq1d | |
33 | 1 32 | ralbida | |
34 | 33 | rexbidv | |
35 | breq2 | |
|
36 | 35 | ralbidv | |
37 | 36 | cbvrexvw | |
38 | 37 | a1i | |
39 | 34 38 | bitrd | |
40 | 31 39 | anbi12d | |
41 | 7 40 | bitrd | |