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	ffvelrnd	\|- ( ( 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 ) ) )

Metamath Proof Explorer

Theorem limsupreuz

Proof