This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem limsupreuz

Description: Given a function on the reals, 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 limsupreuz.1 
|- F/_ j F
limsupreuz.2 
|- ( ph -> M e. ZZ )
limsupreuz.3 
|- Z = ( ZZ>= ` M )
limsupreuz.4 
|- ( ph -> F : Z --> RR )
Assertion limsupreuz 
|- ( ph -> ( ( limsup ` F ) e. RR <-> ( E. x e. RR A. k e. Z E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) /\ E. x e. RR A. j e. Z ( F ` j ) <_ x ) ) )

Proof

Step Hyp Ref Expression
1 limsupreuz.1 
 |-  F/_ j F
2 limsupreuz.2 
 |-  ( ph -> M e. ZZ )
3 limsupreuz.3 
 |-  Z = ( ZZ>= ` M )
4 limsupreuz.4 
 |-  ( ph -> F : Z --> RR )
5 nfcv 
 |-  F/_ l F
6 4 frexr 
 |-  ( ph -> F : Z --> RR* )
7 5 2 3 6 limsupre3uzlem 
 |-  ( ph -> ( ( limsup ` F ) e. RR <-> ( E. y e. RR A. i e. Z E. l e. ( ZZ>= ` i ) y <_ ( F ` l ) /\ E. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ y ) ) )
8 breq1 
 |-  ( y = x -> ( y <_ ( F ` l ) <-> x <_ ( F ` l ) ) )
9 8 rexbidv 
 |-  ( y = x -> ( E. l e. ( ZZ>= ` i ) y <_ ( F ` l ) <-> E. l e. ( ZZ>= ` i ) x <_ ( F ` l ) ) )
10 9 ralbidv 
 |-  ( y = x -> ( A. i e. Z E. l e. ( ZZ>= ` i ) y <_ ( F ` l ) <-> A. i e. Z E. l e. ( ZZ>= ` i ) x <_ ( F ` l ) ) )
11 fveq2 
 |-  ( i = k -> ( ZZ>= ` i ) = ( ZZ>= ` k ) )
12 11 rexeqdv 
 |-  ( i = k -> ( E. l e. ( ZZ>= ` i ) x <_ ( F ` l ) <-> E. l e. ( ZZ>= ` k ) x <_ ( F ` l ) ) )
13 nfcv 
 |-  F/_ j x
14 nfcv 
 |-  F/_ j <_
15 nfcv 
 |-  F/_ j l
16 1 15 nffv 
 |-  F/_ j ( F ` l )
17 13 14 16 nfbr 
 |-  F/ j x <_ ( F ` l )
18 nfv 
 |-  F/ l x <_ ( F ` j )
19 fveq2 
 |-  ( l = j -> ( F ` l ) = ( F ` j ) )
20 19 breq2d 
 |-  ( l = j -> ( x <_ ( F ` l ) <-> x <_ ( F ` j ) ) )
21 17 18 20 cbvrexw 
 |-  ( E. l e. ( ZZ>= ` k ) x <_ ( F ` l ) <-> E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) )
22 21 a1i 
 |-  ( i = k -> ( E. l e. ( ZZ>= ` k ) x <_ ( F ` l ) <-> E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) ) )
23 12 22 bitrd 
 |-  ( i = k -> ( E. l e. ( ZZ>= ` i ) x <_ ( F ` l ) <-> E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) ) )
24 23 cbvralvw 
 |-  ( A. i e. Z E. l e. ( ZZ>= ` i ) x <_ ( F ` l ) <-> A. k e. Z E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) )
25 24 a1i 
 |-  ( y = x -> ( A. i e. Z E. l e. ( ZZ>= ` i ) x <_ ( F ` l ) <-> A. k e. Z E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) ) )
26 10 25 bitrd 
 |-  ( y = x -> ( A. i e. Z E. l e. ( ZZ>= ` i ) y <_ ( F ` l ) <-> A. k e. Z E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) ) )
27 26 cbvrexvw 
 |-  ( E. y e. RR A. i e. Z E. l e. ( ZZ>= ` i ) y <_ ( F ` l ) <-> E. x e. RR A. k e. Z E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) )
28 breq2 
 |-  ( y = x -> ( ( F ` l ) <_ y <-> ( F ` l ) <_ x ) )
29 28 ralbidv 
 |-  ( y = x -> ( A. l e. ( ZZ>= ` i ) ( F ` l ) <_ y <-> A. l e. ( ZZ>= ` i ) ( F ` l ) <_ x ) )
30 29 rexbidv 
 |-  ( y = x -> ( E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ y <-> E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ x ) )
31 11 raleqdv 
 |-  ( i = k -> ( A. l e. ( ZZ>= ` i ) ( F ` l ) <_ x <-> A. l e. ( ZZ>= ` k ) ( F ` l ) <_ x ) )
32 16 14 13 nfbr 
 |-  F/ j ( F ` l ) <_ x
33 nfv 
 |-  F/ l ( F ` j ) <_ x
34 19 breq1d 
 |-  ( l = j -> ( ( F ` l ) <_ x <-> ( F ` j ) <_ x ) )
35 32 33 34 cbvralw 
 |-  ( A. l e. ( ZZ>= ` k ) ( F ` l ) <_ x <-> A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x )
36 35 a1i 
 |-  ( i = k -> ( A. l e. ( ZZ>= ` k ) ( F ` l ) <_ x <-> A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) )
37 31 36 bitrd 
 |-  ( i = k -> ( A. l e. ( ZZ>= ` i ) ( F ` l ) <_ x <-> A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) )
38 37 cbvrexvw 
 |-  ( E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ x <-> E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x )
39 38 a1i 
 |-  ( y = x -> ( E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ x <-> E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) )
40 30 39 bitrd 
 |-  ( y = x -> ( E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ y <-> E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) )
41 40 cbvrexvw 
 |-  ( E. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ y <-> E. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x )
42 27 41 anbi12i 
 |-  ( ( E. y e. RR A. i e. Z E. l e. ( ZZ>= ` i ) y <_ ( F ` l ) /\ E. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ y ) <-> ( E. x e. RR A. k e. Z E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) /\ E. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) )
43 42 a1i 
 |-  ( ph -> ( ( E. y e. RR A. i e. Z E. l e. ( ZZ>= ` i ) y <_ ( F ` l ) /\ E. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ y ) <-> ( E. x e. RR A. k e. Z E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) /\ E. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) ) )
44 7 43 bitrd 
 |-  ( ph -> ( ( limsup ` F ) e. RR <-> ( E. x e. RR A. k e. Z E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) /\ E. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) ) )
45 nfv 
 |-  F/ i ( F ` j ) <_ x
46 nfcv 
 |-  F/_ j i
47 1 46 nffv 
 |-  F/_ j ( F ` i )
48 47 14 13 nfbr 
 |-  F/ j ( F ` i ) <_ x
49 fveq2 
 |-  ( j = i -> ( F ` j ) = ( F ` i ) )
50 49 breq1d 
 |-  ( j = i -> ( ( F ` j ) <_ x <-> ( F ` i ) <_ x ) )
51 45 48 50 cbvralw 
 |-  ( A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x <-> A. i e. ( ZZ>= ` k ) ( F ` i ) <_ x )
52 51 rexbii 
 |-  ( E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x <-> E. k e. Z A. i e. ( ZZ>= ` k ) ( F ` i ) <_ x )
53 52 rexbii 
 |-  ( E. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x <-> E. x e. RR E. k e. Z A. i e. ( ZZ>= ` k ) ( F ` i ) <_ x )
54 53 a1i 
 |-  ( ph -> ( E. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x <-> E. x e. RR E. k e. Z A. i e. ( ZZ>= ` k ) ( F ` i ) <_ x ) )
55 nfv 
 |-  F/ i ph
56 4 adantr 
 |-  ( ( ph /\ i e. Z ) -> F : Z --> RR )
57 simpr 
 |-  ( ( ph /\ i e. Z ) -> i e. Z )
58 56 57 ffvelcdmd 
 |-  ( ( ph /\ i e. Z ) -> ( F ` i ) e. RR )
59 55 2 3 58 uzub 
 |-  ( ph -> ( E. x e. RR E. k e. Z A. i e. ( ZZ>= ` k ) ( F ` i ) <_ x <-> E. x e. RR A. i e. Z ( F ` i ) <_ x ) )
60 eqcom 
 |-  ( j = i <-> i = j )
61 60 imbi1i 
 |-  ( ( j = i -> ( ( F ` j ) <_ x <-> ( F ` i ) <_ x ) ) <-> ( i = j -> ( ( F ` j ) <_ x <-> ( F ` i ) <_ x ) ) )
62 bicom 
 |-  ( ( ( F ` j ) <_ x <-> ( F ` i ) <_ x ) <-> ( ( F ` i ) <_ x <-> ( F ` j ) <_ x ) )
63 62 imbi2i 
 |-  ( ( i = j -> ( ( F ` j ) <_ x <-> ( F ` i ) <_ x ) ) <-> ( i = j -> ( ( F ` i ) <_ x <-> ( F ` j ) <_ x ) ) )
64 61 63 bitri 
 |-  ( ( j = i -> ( ( F ` j ) <_ x <-> ( F ` i ) <_ x ) ) <-> ( i = j -> ( ( F ` i ) <_ x <-> ( F ` j ) <_ x ) ) )
65 50 64 mpbi 
 |-  ( i = j -> ( ( F ` i ) <_ x <-> ( F ` j ) <_ x ) )
66 48 45 65 cbvralw 
 |-  ( A. i e. Z ( F ` i ) <_ x <-> A. j e. Z ( F ` j ) <_ x )
67 66 rexbii 
 |-  ( E. x e. RR A. i e. Z ( F ` i ) <_ x <-> E. x e. RR A. j e. Z ( F ` j ) <_ x )
68 67 a1i 
 |-  ( ph -> ( E. x e. RR A. i e. Z ( F ` i ) <_ x <-> E. x e. RR A. j e. Z ( F ` j ) <_ x ) )
69 54 59 68 3bitrd 
 |-  ( ph -> ( E. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x <-> E. x e. RR A. j e. Z ( F ` j ) <_ x ) )
70 69 anbi2d 
 |-  ( ph -> ( ( E. x e. RR A. k e. Z E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) /\ E. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) <-> ( E. x e. RR A. k e. Z E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) /\ E. x e. RR A. j e. Z ( F ` j ) <_ x ) ) )
71 44 70 bitrd 
 |-  ( ph -> ( ( limsup ` F ) e. RR <-> ( E. x e. RR A. k e. Z E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) /\ E. x e. RR A. j e. Z ( F ` j ) <_ x ) ) )