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 
|- F/ j ph
limsupreuzmpt.m 
|- ( ph -> M e. ZZ )
limsupreuzmpt.z 
|- Z = ( ZZ>= ` M )
limsupreuzmpt.b 
|- ( ( ph /\ j e. Z ) -> B e. RR )
Assertion limsupreuzmpt 
|- ( ph -> ( ( limsup ` ( j e. Z |-> B ) ) e. RR <-> ( E. x e. RR A. k e. Z E. j e. ( ZZ>= ` k ) x <_ B /\ E. x e. RR A. j e. Z B <_ x ) ) )

Proof

Step Hyp Ref Expression
1 limsupreuzmpt.j 
 |-  F/ j ph
2 limsupreuzmpt.m 
 |-  ( ph -> M e. ZZ )
3 limsupreuzmpt.z 
 |-  Z = ( ZZ>= ` M )
4 limsupreuzmpt.b 
 |-  ( ( ph /\ j e. Z ) -> B e. RR )
5 nfmpt1 
 |-  F/_ j ( j e. Z |-> B )
6 1 4 fmptd2f 
 |-  ( ph -> ( j e. Z |-> B ) : Z --> RR )
7 5 2 3 6 limsupreuz 
 |-  ( ph -> ( ( limsup ` ( j e. Z |-> B ) ) e. RR <-> ( E. y e. RR A. i e. Z E. j e. ( ZZ>= ` i ) y <_ ( ( j e. Z |-> B ) ` j ) /\ E. y e. RR A. j e. Z ( ( j e. Z |-> B ) ` j ) <_ y ) ) )
8 nfv 
 |-  F/ j i e. Z
9 1 8 nfan 
 |-  F/ j ( ph /\ i e. Z )
10 simpll 
 |-  ( ( ( ph /\ i e. Z ) /\ j e. ( ZZ>= ` i ) ) -> ph )
11 3 uztrn2 
 |-  ( ( i e. Z /\ j e. ( ZZ>= ` i ) ) -> j e. Z )
12 11 adantll 
 |-  ( ( ( ph /\ i e. Z ) /\ j e. ( ZZ>= ` i ) ) -> j e. Z )
13 eqid 
 |-  ( j e. Z |-> B ) = ( j e. Z |-> B )
14 13 a1i 
 |-  ( ph -> ( j e. Z |-> B ) = ( j e. Z |-> B ) )
15 14 4 fvmpt2d 
 |-  ( ( ph /\ j e. Z ) -> ( ( j e. Z |-> B ) ` j ) = B )
16 10 12 15 syl2anc 
 |-  ( ( ( ph /\ i e. Z ) /\ j e. ( ZZ>= ` i ) ) -> ( ( j e. Z |-> B ) ` j ) = B )
17 16 breq2d 
 |-  ( ( ( ph /\ i e. Z ) /\ j e. ( ZZ>= ` i ) ) -> ( y <_ ( ( j e. Z |-> B ) ` j ) <-> y <_ B ) )
18 9 17 rexbida 
 |-  ( ( ph /\ i e. Z ) -> ( E. j e. ( ZZ>= ` i ) y <_ ( ( j e. Z |-> B ) ` j ) <-> E. j e. ( ZZ>= ` i ) y <_ B ) )
19 18 ralbidva 
 |-  ( ph -> ( A. i e. Z E. j e. ( ZZ>= ` i ) y <_ ( ( j e. Z |-> B ) ` j ) <-> A. i e. Z E. j e. ( ZZ>= ` i ) y <_ B ) )
20 19 rexbidv 
 |-  ( ph -> ( E. y e. RR A. i e. Z E. j e. ( ZZ>= ` i ) y <_ ( ( j e. Z |-> B ) ` j ) <-> E. y e. RR A. i e. Z E. j e. ( ZZ>= ` i ) y <_ B ) )
21 breq1 
 |-  ( y = x -> ( y <_ B <-> x <_ B ) )
22 21 rexbidv 
 |-  ( y = x -> ( E. j e. ( ZZ>= ` i ) y <_ B <-> E. j e. ( ZZ>= ` i ) x <_ B ) )
23 22 ralbidv 
 |-  ( y = x -> ( A. i e. Z E. j e. ( ZZ>= ` i ) y <_ B <-> A. i e. Z E. j e. ( ZZ>= ` i ) x <_ B ) )
24 fveq2 
 |-  ( i = k -> ( ZZ>= ` i ) = ( ZZ>= ` k ) )
25 24 rexeqdv 
 |-  ( i = k -> ( E. j e. ( ZZ>= ` i ) x <_ B <-> E. j e. ( ZZ>= ` k ) x <_ B ) )
26 25 cbvralvw 
 |-  ( A. i e. Z E. j e. ( ZZ>= ` i ) x <_ B <-> A. k e. Z E. j e. ( ZZ>= ` k ) x <_ B )
27 26 a1i 
 |-  ( y = x -> ( A. i e. Z E. j e. ( ZZ>= ` i ) x <_ B <-> A. k e. Z E. j e. ( ZZ>= ` k ) x <_ B ) )
28 23 27 bitrd 
 |-  ( y = x -> ( A. i e. Z E. j e. ( ZZ>= ` i ) y <_ B <-> A. k e. Z E. j e. ( ZZ>= ` k ) x <_ B ) )
29 28 cbvrexvw 
 |-  ( E. y e. RR A. i e. Z E. j e. ( ZZ>= ` i ) y <_ B <-> E. x e. RR A. k e. Z E. j e. ( ZZ>= ` k ) x <_ B )
30 29 a1i 
 |-  ( ph -> ( E. y e. RR A. i e. Z E. j e. ( ZZ>= ` i ) y <_ B <-> E. x e. RR A. k e. Z E. j e. ( ZZ>= ` k ) x <_ B ) )
31 20 30 bitrd 
 |-  ( ph -> ( E. y e. RR A. i e. Z E. j e. ( ZZ>= ` i ) y <_ ( ( j e. Z |-> B ) ` j ) <-> E. x e. RR A. k e. Z E. j e. ( ZZ>= ` k ) x <_ B ) )
32 15 breq1d 
 |-  ( ( ph /\ j e. Z ) -> ( ( ( j e. Z |-> B ) ` j ) <_ y <-> B <_ y ) )
33 1 32 ralbida 
 |-  ( ph -> ( A. j e. Z ( ( j e. Z |-> B ) ` j ) <_ y <-> A. j e. Z B <_ y ) )
34 33 rexbidv 
 |-  ( ph -> ( E. y e. RR A. j e. Z ( ( j e. Z |-> B ) ` j ) <_ y <-> E. y e. RR A. j e. Z B <_ y ) )
35 breq2 
 |-  ( y = x -> ( B <_ y <-> B <_ x ) )
36 35 ralbidv 
 |-  ( y = x -> ( A. j e. Z B <_ y <-> A. j e. Z B <_ x ) )
37 36 cbvrexvw 
 |-  ( E. y e. RR A. j e. Z B <_ y <-> E. x e. RR A. j e. Z B <_ x )
38 37 a1i 
 |-  ( ph -> ( E. y e. RR A. j e. Z B <_ y <-> E. x e. RR A. j e. Z B <_ x ) )
39 34 38 bitrd 
 |-  ( ph -> ( E. y e. RR A. j e. Z ( ( j e. Z |-> B ) ` j ) <_ y <-> E. x e. RR A. j e. Z B <_ x ) )
40 31 39 anbi12d 
 |-  ( ph -> ( ( E. y e. RR A. i e. Z E. j e. ( ZZ>= ` i ) y <_ ( ( j e. Z |-> B ) ` j ) /\ E. y e. RR A. j e. Z ( ( j e. Z |-> B ) ` j ) <_ y ) <-> ( E. x e. RR A. k e. Z E. j e. ( ZZ>= ` k ) x <_ B /\ E. x e. RR A. j e. Z B <_ x ) ) )
41 7 40 bitrd 
 |-  ( ph -> ( ( limsup ` ( j e. Z |-> B ) ) e. RR <-> ( E. x e. RR A. k e. Z E. j e. ( ZZ>= ` k ) x <_ B /\ E. x e. RR A. j e. Z B <_ x ) ) )