Metamath Proof Explorer


Theorem limsupreuzmpt

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 jφ
limsupreuzmpt.m φM
limsupreuzmpt.z Z=M
limsupreuzmpt.b φjZB
Assertion limsupreuzmpt φlim supjZBxkZjkxBxjZBx

Proof

Step Hyp Ref Expression
1 limsupreuzmpt.j jφ
2 limsupreuzmpt.m φM
3 limsupreuzmpt.z Z=M
4 limsupreuzmpt.b φjZB
5 nfmpt1 _jjZB
6 1 4 fmptd2f φjZB:Z
7 5 2 3 6 limsupreuz φlim supjZByiZjiyjZBjyjZjZBjy
8 nfv jiZ
9 1 8 nfan jφiZ
10 simpll φiZjiφ
11 3 uztrn2 iZjijZ
12 11 adantll φiZjijZ
13 eqid jZB=jZB
14 13 a1i φjZB=jZB
15 14 4 fvmpt2d φjZjZBj=B
16 10 12 15 syl2anc φiZjijZBj=B
17 16 breq2d φiZjiyjZBjyB
18 9 17 rexbida φiZjiyjZBjjiyB
19 18 ralbidva φiZjiyjZBjiZjiyB
20 19 rexbidv φyiZjiyjZBjyiZjiyB
21 breq1 y=xyBxB
22 21 rexbidv y=xjiyBjixB
23 22 ralbidv y=xiZjiyBiZjixB
24 fveq2 i=ki=k
25 24 rexeqdv i=kjixBjkxB
26 25 cbvralvw iZjixBkZjkxB
27 26 a1i y=xiZjixBkZjkxB
28 23 27 bitrd y=xiZjiyBkZjkxB
29 28 cbvrexvw yiZjiyBxkZjkxB
30 29 a1i φyiZjiyBxkZjkxB
31 20 30 bitrd φyiZjiyjZBjxkZjkxB
32 15 breq1d φjZjZBjyBy
33 1 32 ralbida φjZjZBjyjZBy
34 33 rexbidv φyjZjZBjyyjZBy
35 breq2 y=xByBx
36 35 ralbidv y=xjZByjZBx
37 36 cbvrexvw yjZByxjZBx
38 37 a1i φyjZByxjZBx
39 34 38 bitrd φyjZjZBjyxjZBx
40 31 39 anbi12d φyiZjiyjZBjyjZjZBjyxkZjkxBxjZBx
41 7 40 bitrd φlim supjZBxkZjkxBxjZBx