supcnvlimsup

Description: If a function on a set of upper integers has a real superior limit, the supremum of the rightmost parts of the function, converges to that superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	supcnvlimsup.m	\|- ( ph -> M e. ZZ )
	supcnvlimsup.z	\|- Z = ( ZZ>= ` M )
	supcnvlimsup.f	\|- ( ph -> F : Z --> RR )
	supcnvlimsup.r	\|- ( ph -> ( limsup ` F ) e. RR )
Assertion	supcnvlimsup	\|- ( ph -> ( k e. Z \|-> sup ( ran ( F \|` ( ZZ>= ` k ) ) , RR* , < ) ) ~~> ( limsup ` F ) )

Proof

Step	Hyp	Ref	Expression
1		supcnvlimsup.m	\|- ( ph -> M e. ZZ )
2		supcnvlimsup.z	\|- Z = ( ZZ>= ` M )
3		supcnvlimsup.f	\|- ( ph -> F : Z --> RR )
4		supcnvlimsup.r	\|- ( ph -> ( limsup ` F ) e. RR )
5	3	adantr	\|- ( ( ph /\ n e. Z ) -> F : Z --> RR )
6		id	\|- ( n e. Z -> n e. Z )
7	2 6	uzssd2	\|- ( n e. Z -> ( ZZ>= ` n ) C_ Z )
8	7	adantl	\|- ( ( ph /\ n e. Z ) -> ( ZZ>= ` n ) C_ Z )
9	5 8	feqresmpt	\|- ( ( ph /\ n e. Z ) -> ( F \|` ( ZZ>= ` n ) ) = ( m e. ( ZZ>= ` n ) \|-> ( F ` m ) ) )
10	9	rneqd	\|- ( ( ph /\ n e. Z ) -> ran ( F \|` ( ZZ>= ` n ) ) = ran ( m e. ( ZZ>= ` n ) \|-> ( F ` m ) ) )
11	10	supeq1d	\|- ( ( ph /\ n e. Z ) -> sup ( ran ( F \|` ( ZZ>= ` n ) ) , RR* , < ) = sup ( ran ( m e. ( ZZ>= ` n ) \|-> ( F ` m ) ) , RR* , < ) )
12		nfcv	\|- F/_ m F
13	4	renepnfd	\|- ( ph -> ( limsup ` F ) =/= +oo )
14	12 2 3 13	limsupubuz	\|- ( ph -> E. x e. RR A. m e. Z ( F ` m ) <_ x )
15	14	adantr	\|- ( ( ph /\ n e. Z ) -> E. x e. RR A. m e. Z ( F ` m ) <_ x )
16		ssralv	\|- ( ( ZZ>= ` n ) C_ Z -> ( A. m e. Z ( F ` m ) <_ x -> A. m e. ( ZZ>= ` n ) ( F ` m ) <_ x ) )
17	7 16	syl	\|- ( n e. Z -> ( A. m e. Z ( F ` m ) <_ x -> A. m e. ( ZZ>= ` n ) ( F ` m ) <_ x ) )
18	17	adantl	\|- ( ( ph /\ n e. Z ) -> ( A. m e. Z ( F ` m ) <_ x -> A. m e. ( ZZ>= ` n ) ( F ` m ) <_ x ) )
19	18	reximdv	\|- ( ( ph /\ n e. Z ) -> ( E. x e. RR A. m e. Z ( F ` m ) <_ x -> E. x e. RR A. m e. ( ZZ>= ` n ) ( F ` m ) <_ x ) )
20	15 19	mpd	\|- ( ( ph /\ n e. Z ) -> E. x e. RR A. m e. ( ZZ>= ` n ) ( F ` m ) <_ x )
21		nfv	\|- F/ m ( ph /\ n e. Z )
22	2	eluzelz2	\|- ( n e. Z -> n e. ZZ )
23		uzid	\|- ( n e. ZZ -> n e. ( ZZ>= ` n ) )
24		ne0i	\|- ( n e. ( ZZ>= ` n ) -> ( ZZ>= ` n ) =/= (/) )
25	22 23 24	3syl	\|- ( n e. Z -> ( ZZ>= ` n ) =/= (/) )
26	25	adantl	\|- ( ( ph /\ n e. Z ) -> ( ZZ>= ` n ) =/= (/) )
27	5	adantr	\|- ( ( ( ph /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) -> F : Z --> RR )
28	8	sselda	\|- ( ( ( ph /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) -> m e. Z )
29	27 28	ffvelcdmd	\|- ( ( ( ph /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) -> ( F ` m ) e. RR )
30	21 26 29	supxrre3rnmpt	\|- ( ( ph /\ n e. Z ) -> ( sup ( ran ( m e. ( ZZ>= ` n ) \|-> ( F ` m ) ) , RR* , < ) e. RR <-> E. x e. RR A. m e. ( ZZ>= ` n ) ( F ` m ) <_ x ) )
31	20 30	mpbird	\|- ( ( ph /\ n e. Z ) -> sup ( ran ( m e. ( ZZ>= ` n ) \|-> ( F ` m ) ) , RR* , < ) e. RR )
32	11 31	eqeltrd	\|- ( ( ph /\ n e. Z ) -> sup ( ran ( F \|` ( ZZ>= ` n ) ) , RR* , < ) e. RR )
33	32	fmpttd	\|- ( ph -> ( n e. Z \|-> sup ( ran ( F \|` ( ZZ>= ` n ) ) , RR* , < ) ) : Z --> RR )
34		eqid	\|- ( ZZ>= ` i ) = ( ZZ>= ` i )
35	2	eluzelz2	\|- ( i e. Z -> i e. ZZ )
36	35	peano2zd	\|- ( i e. Z -> ( i + 1 ) e. ZZ )
37	35	zred	\|- ( i e. Z -> i e. RR )
38		lep1	\|- ( i e. RR -> i <_ ( i + 1 ) )
39	37 38	syl	\|- ( i e. Z -> i <_ ( i + 1 ) )
40	34 35 36 39	eluzd	\|- ( i e. Z -> ( i + 1 ) e. ( ZZ>= ` i ) )
41		uzss	\|- ( ( i + 1 ) e. ( ZZ>= ` i ) -> ( ZZ>= ` ( i + 1 ) ) C_ ( ZZ>= ` i ) )
42		ssres2	\|- ( ( ZZ>= ` ( i + 1 ) ) C_ ( ZZ>= ` i ) -> ( F \|` ( ZZ>= ` ( i + 1 ) ) ) C_ ( F \|` ( ZZ>= ` i ) ) )
43		rnss	\|- ( ( F \|` ( ZZ>= ` ( i + 1 ) ) ) C_ ( F \|` ( ZZ>= ` i ) ) -> ran ( F \|` ( ZZ>= ` ( i + 1 ) ) ) C_ ran ( F \|` ( ZZ>= ` i ) ) )
44	40 41 42 43	4syl	\|- ( i e. Z -> ran ( F \|` ( ZZ>= ` ( i + 1 ) ) ) C_ ran ( F \|` ( ZZ>= ` i ) ) )
45	44	adantl	\|- ( ( ph /\ i e. Z ) -> ran ( F \|` ( ZZ>= ` ( i + 1 ) ) ) C_ ran ( F \|` ( ZZ>= ` i ) ) )
46		rnresss	\|- ran ( F \|` ( ZZ>= ` i ) ) C_ ran F
47	46	a1i	\|- ( ( ph /\ i e. Z ) -> ran ( F \|` ( ZZ>= ` i ) ) C_ ran F )
48	3	frnd	\|- ( ph -> ran F C_ RR )
49	48	adantr	\|- ( ( ph /\ i e. Z ) -> ran F C_ RR )
50	47 49	sstrd	\|- ( ( ph /\ i e. Z ) -> ran ( F \|` ( ZZ>= ` i ) ) C_ RR )
51		ressxr	\|- RR C_ RR*
52	51	a1i	\|- ( ( ph /\ i e. Z ) -> RR C_ RR* )
53	50 52	sstrd	\|- ( ( ph /\ i e. Z ) -> ran ( F \|` ( ZZ>= ` i ) ) C_ RR* )
54		supxrss	\|- ( ( ran ( F \|` ( ZZ>= ` ( i + 1 ) ) ) C_ ran ( F \|` ( ZZ>= ` i ) ) /\ ran ( F \|` ( ZZ>= ` i ) ) C_ RR* ) -> sup ( ran ( F \|` ( ZZ>= ` ( i + 1 ) ) ) , RR* , < ) <_ sup ( ran ( F \|` ( ZZ>= ` i ) ) , RR* , < ) )
55	45 53 54	syl2anc	\|- ( ( ph /\ i e. Z ) -> sup ( ran ( F \|` ( ZZ>= ` ( i + 1 ) ) ) , RR* , < ) <_ sup ( ran ( F \|` ( ZZ>= ` i ) ) , RR* , < ) )
56		eqidd	\|- ( i e. Z -> ( n e. Z \|-> sup ( ran ( F \|` ( ZZ>= ` n ) ) , RR* , < ) ) = ( n e. Z \|-> sup ( ran ( F \|` ( ZZ>= ` n ) ) , RR* , < ) ) )
57		fveq2	\|- ( n = ( i + 1 ) -> ( ZZ>= ` n ) = ( ZZ>= ` ( i + 1 ) ) )
58	57	reseq2d	\|- ( n = ( i + 1 ) -> ( F \|` ( ZZ>= ` n ) ) = ( F \|` ( ZZ>= ` ( i + 1 ) ) ) )
59	58	rneqd	\|- ( n = ( i + 1 ) -> ran ( F \|` ( ZZ>= ` n ) ) = ran ( F \|` ( ZZ>= ` ( i + 1 ) ) ) )
60	59	supeq1d	\|- ( n = ( i + 1 ) -> sup ( ran ( F \|` ( ZZ>= ` n ) ) , RR* , < ) = sup ( ran ( F \|` ( ZZ>= ` ( i + 1 ) ) ) , RR* , < ) )
61	60	adantl	\|- ( ( i e. Z /\ n = ( i + 1 ) ) -> sup ( ran ( F \|` ( ZZ>= ` n ) ) , RR* , < ) = sup ( ran ( F \|` ( ZZ>= ` ( i + 1 ) ) ) , RR* , < ) )
62	2	peano2uzs	\|- ( i e. Z -> ( i + 1 ) e. Z )
63		xrltso	\|- < Or RR*
64	63	supex	\|- sup ( ran ( F \|` ( ZZ>= ` ( i + 1 ) ) ) , RR* , < ) e. _V
65	64	a1i	\|- ( i e. Z -> sup ( ran ( F \|` ( ZZ>= ` ( i + 1 ) ) ) , RR* , < ) e. _V )
66	56 61 62 65	fvmptd	\|- ( i e. Z -> ( ( n e. Z \|-> sup ( ran ( F \|` ( ZZ>= ` n ) ) , RR* , < ) ) ` ( i + 1 ) ) = sup ( ran ( F \|` ( ZZ>= ` ( i + 1 ) ) ) , RR* , < ) )
67	66	adantl	\|- ( ( ph /\ i e. Z ) -> ( ( n e. Z \|-> sup ( ran ( F \|` ( ZZ>= ` n ) ) , RR* , < ) ) ` ( i + 1 ) ) = sup ( ran ( F \|` ( ZZ>= ` ( i + 1 ) ) ) , RR* , < ) )
68		fveq2	\|- ( n = i -> ( ZZ>= ` n ) = ( ZZ>= ` i ) )
69	68	reseq2d	\|- ( n = i -> ( F \|` ( ZZ>= ` n ) ) = ( F \|` ( ZZ>= ` i ) ) )
70	69	rneqd	\|- ( n = i -> ran ( F \|` ( ZZ>= ` n ) ) = ran ( F \|` ( ZZ>= ` i ) ) )
71	70	supeq1d	\|- ( n = i -> sup ( ran ( F \|` ( ZZ>= ` n ) ) , RR* , < ) = sup ( ran ( F \|` ( ZZ>= ` i ) ) , RR* , < ) )
72	71	adantl	\|- ( ( i e. Z /\ n = i ) -> sup ( ran ( F \|` ( ZZ>= ` n ) ) , RR* , < ) = sup ( ran ( F \|` ( ZZ>= ` i ) ) , RR* , < ) )
73		id	\|- ( i e. Z -> i e. Z )
74	63	supex	\|- sup ( ran ( F \|` ( ZZ>= ` i ) ) , RR* , < ) e. _V
75	74	a1i	\|- ( i e. Z -> sup ( ran ( F \|` ( ZZ>= ` i ) ) , RR* , < ) e. _V )
76	56 72 73 75	fvmptd	\|- ( i e. Z -> ( ( n e. Z \|-> sup ( ran ( F \|` ( ZZ>= ` n ) ) , RR* , < ) ) ` i ) = sup ( ran ( F \|` ( ZZ>= ` i ) ) , RR* , < ) )
77	76	adantl	\|- ( ( ph /\ i e. Z ) -> ( ( n e. Z \|-> sup ( ran ( F \|` ( ZZ>= ` n ) ) , RR* , < ) ) ` i ) = sup ( ran ( F \|` ( ZZ>= ` i ) ) , RR* , < ) )
78	67 77	breq12d	\|- ( ( ph /\ i e. Z ) -> ( ( ( n e. Z \|-> sup ( ran ( F \|` ( ZZ>= ` n ) ) , RR* , < ) ) ` ( i + 1 ) ) <_ ( ( n e. Z \|-> sup ( ran ( F \|` ( ZZ>= ` n ) ) , RR* , < ) ) ` i ) <-> sup ( ran ( F \|` ( ZZ>= ` ( i + 1 ) ) ) , RR* , < ) <_ sup ( ran ( F \|` ( ZZ>= ` i ) ) , RR* , < ) ) )
79	55 78	mpbird	\|- ( ( ph /\ i e. Z ) -> ( ( n e. Z \|-> sup ( ran ( F \|` ( ZZ>= ` n ) ) , RR* , < ) ) ` ( i + 1 ) ) <_ ( ( n e. Z \|-> sup ( ran ( F \|` ( ZZ>= ` n ) ) , RR* , < ) ) ` i ) )
80		nfcv	\|- F/_ j F
81	3	frexr	\|- ( ph -> F : Z --> RR* )
82	80 1 2 81	limsupre3uz	\|- ( ph -> ( ( limsup ` F ) e. RR <-> ( E. x e. RR A. i e. Z E. j e. ( ZZ>= ` i ) x <_ ( F ` j ) /\ E. x e. RR E. i e. Z A. j e. ( ZZ>= ` i ) ( F ` j ) <_ x ) ) )
83	4 82	mpbid	\|- ( ph -> ( E. x e. RR A. i e. Z E. j e. ( ZZ>= ` i ) x <_ ( F ` j ) /\ E. x e. RR E. i e. Z A. j e. ( ZZ>= ` i ) ( F ` j ) <_ x ) )
84	83	simpld	\|- ( ph -> E. x e. RR A. i e. Z E. j e. ( ZZ>= ` i ) x <_ ( F ` j ) )
85		simp-4r	\|- ( ( ( ( ( ph /\ x e. RR ) /\ i e. Z ) /\ j e. ( ZZ>= ` i ) ) /\ x <_ ( F ` j ) ) -> x e. RR )
86	85	rexrd	\|- ( ( ( ( ( ph /\ x e. RR ) /\ i e. Z ) /\ j e. ( ZZ>= ` i ) ) /\ x <_ ( F ` j ) ) -> x e. RR* )
87	81	3ad2ant1	\|- ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> F : Z --> RR* )
88	2	uztrn2	\|- ( ( i e. Z /\ j e. ( ZZ>= ` i ) ) -> j e. Z )
89	88	3adant1	\|- ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> j e. Z )
90	87 89	ffvelcdmd	\|- ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> ( F ` j ) e. RR* )
91	90	ad5ant134	\|- ( ( ( ( ( ph /\ x e. RR ) /\ i e. Z ) /\ j e. ( ZZ>= ` i ) ) /\ x <_ ( F ` j ) ) -> ( F ` j ) e. RR* )
92	53	supxrcld	\|- ( ( ph /\ i e. Z ) -> sup ( ran ( F \|` ( ZZ>= ` i ) ) , RR* , < ) e. RR* )
93	92	ad5ant13	\|- ( ( ( ( ( ph /\ x e. RR ) /\ i e. Z ) /\ j e. ( ZZ>= ` i ) ) /\ x <_ ( F ` j ) ) -> sup ( ran ( F \|` ( ZZ>= ` i ) ) , RR* , < ) e. RR* )
94		simpr	\|- ( ( ( ( ( ph /\ x e. RR ) /\ i e. Z ) /\ j e. ( ZZ>= ` i ) ) /\ x <_ ( F ` j ) ) -> x <_ ( F ` j ) )
95	53	3adant3	\|- ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> ran ( F \|` ( ZZ>= ` i ) ) C_ RR* )
96		fvres	\|- ( j e. ( ZZ>= ` i ) -> ( ( F \|` ( ZZ>= ` i ) ) ` j ) = ( F ` j ) )
97	96	eqcomd	\|- ( j e. ( ZZ>= ` i ) -> ( F ` j ) = ( ( F \|` ( ZZ>= ` i ) ) ` j ) )
98	97	3ad2ant3	\|- ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> ( F ` j ) = ( ( F \|` ( ZZ>= ` i ) ) ` j ) )
99	3	ffnd	\|- ( ph -> F Fn Z )
100	99	adantr	\|- ( ( ph /\ i e. Z ) -> F Fn Z )
101	2 73	uzssd2	\|- ( i e. Z -> ( ZZ>= ` i ) C_ Z )
102	101	adantl	\|- ( ( ph /\ i e. Z ) -> ( ZZ>= ` i ) C_ Z )
103		fnssres	\|- ( ( F Fn Z /\ ( ZZ>= ` i ) C_ Z ) -> ( F \|` ( ZZ>= ` i ) ) Fn ( ZZ>= ` i ) )
104	100 102 103	syl2anc	\|- ( ( ph /\ i e. Z ) -> ( F \|` ( ZZ>= ` i ) ) Fn ( ZZ>= ` i ) )
105	104	3adant3	\|- ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> ( F \|` ( ZZ>= ` i ) ) Fn ( ZZ>= ` i ) )
106		simp3	\|- ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> j e. ( ZZ>= ` i ) )
107		fnfvelrn	\|- ( ( ( F \|` ( ZZ>= ` i ) ) Fn ( ZZ>= ` i ) /\ j e. ( ZZ>= ` i ) ) -> ( ( F \|` ( ZZ>= ` i ) ) ` j ) e. ran ( F \|` ( ZZ>= ` i ) ) )
108	105 106 107	syl2anc	\|- ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> ( ( F \|` ( ZZ>= ` i ) ) ` j ) e. ran ( F \|` ( ZZ>= ` i ) ) )
109	98 108	eqeltrd	\|- ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> ( F ` j ) e. ran ( F \|` ( ZZ>= ` i ) ) )
110		eqid	\|- sup ( ran ( F \|` ( ZZ>= ` i ) ) , RR* , < ) = sup ( ran ( F \|` ( ZZ>= ` i ) ) , RR* , < )
111	95 109 110	supxrubd	\|- ( ( ph /\ i e. Z /\ j e. ( ZZ>= ` i ) ) -> ( F ` j ) <_ sup ( ran ( F \|` ( ZZ>= ` i ) ) , RR* , < ) )
112	111	ad5ant134	\|- ( ( ( ( ( ph /\ x e. RR ) /\ i e. Z ) /\ j e. ( ZZ>= ` i ) ) /\ x <_ ( F ` j ) ) -> ( F ` j ) <_ sup ( ran ( F \|` ( ZZ>= ` i ) ) , RR* , < ) )
113	86 91 93 94 112	xrletrd	\|- ( ( ( ( ( ph /\ x e. RR ) /\ i e. Z ) /\ j e. ( ZZ>= ` i ) ) /\ x <_ ( F ` j ) ) -> x <_ sup ( ran ( F \|` ( ZZ>= ` i ) ) , RR* , < ) )
114	113	rexlimdva2	\|- ( ( ( ph /\ x e. RR ) /\ i e. Z ) -> ( E. j e. ( ZZ>= ` i ) x <_ ( F ` j ) -> x <_ sup ( ran ( F \|` ( ZZ>= ` i ) ) , RR* , < ) ) )
115	114	ralimdva	\|- ( ( ph /\ x e. RR ) -> ( A. i e. Z E. j e. ( ZZ>= ` i ) x <_ ( F ` j ) -> A. i e. Z x <_ sup ( ran ( F \|` ( ZZ>= ` i ) ) , RR* , < ) ) )
116	115	reximdva	\|- ( ph -> ( E. x e. RR A. i e. Z E. j e. ( ZZ>= ` i ) x <_ ( F ` j ) -> E. x e. RR A. i e. Z x <_ sup ( ran ( F \|` ( ZZ>= ` i ) ) , RR* , < ) ) )
117	84 116	mpd	\|- ( ph -> E. x e. RR A. i e. Z x <_ sup ( ran ( F \|` ( ZZ>= ` i ) ) , RR* , < ) )
118		simpl	\|- ( ( y = x /\ i e. Z ) -> y = x )
119	76	adantl	\|- ( ( y = x /\ i e. Z ) -> ( ( n e. Z \|-> sup ( ran ( F \|` ( ZZ>= ` n ) ) , RR* , < ) ) ` i ) = sup ( ran ( F \|` ( ZZ>= ` i ) ) , RR* , < ) )
120	118 119	breq12d	\|- ( ( y = x /\ i e. Z ) -> ( y <_ ( ( n e. Z \|-> sup ( ran ( F \|` ( ZZ>= ` n ) ) , RR* , < ) ) ` i ) <-> x <_ sup ( ran ( F \|` ( ZZ>= ` i ) ) , RR* , < ) ) )
121	120	ralbidva	\|- ( y = x -> ( A. i e. Z y <_ ( ( n e. Z \|-> sup ( ran ( F \|` ( ZZ>= ` n ) ) , RR* , < ) ) ` i ) <-> A. i e. Z x <_ sup ( ran ( F \|` ( ZZ>= ` i ) ) , RR* , < ) ) )
122	121	cbvrexvw	\|- ( E. y e. RR A. i e. Z y <_ ( ( n e. Z \|-> sup ( ran ( F \|` ( ZZ>= ` n ) ) , RR* , < ) ) ` i ) <-> E. x e. RR A. i e. Z x <_ sup ( ran ( F \|` ( ZZ>= ` i ) ) , RR* , < ) )
123	117 122	sylibr	\|- ( ph -> E. y e. RR A. i e. Z y <_ ( ( n e. Z \|-> sup ( ran ( F \|` ( ZZ>= ` n ) ) , RR* , < ) ) ` i ) )
124	2 1 33 79 123	climinf	\|- ( ph -> ( n e. Z \|-> sup ( ran ( F \|` ( ZZ>= ` n ) ) , RR* , < ) ) ~~> inf ( ran ( n e. Z \|-> sup ( ran ( F \|` ( ZZ>= ` n ) ) , RR* , < ) ) , RR , < ) )
125		fveq2	\|- ( n = k -> ( ZZ>= ` n ) = ( ZZ>= ` k ) )
126	125	reseq2d	\|- ( n = k -> ( F \|` ( ZZ>= ` n ) ) = ( F \|` ( ZZ>= ` k ) ) )
127	126	rneqd	\|- ( n = k -> ran ( F \|` ( ZZ>= ` n ) ) = ran ( F \|` ( ZZ>= ` k ) ) )
128	127	supeq1d	\|- ( n = k -> sup ( ran ( F \|` ( ZZ>= ` n ) ) , RR* , < ) = sup ( ran ( F \|` ( ZZ>= ` k ) ) , RR* , < ) )
129	128	cbvmptv	\|- ( n e. Z \|-> sup ( ran ( F \|` ( ZZ>= ` n ) ) , RR* , < ) ) = ( k e. Z \|-> sup ( ran ( F \|` ( ZZ>= ` k ) ) , RR* , < ) )
130	129	a1i	\|- ( ph -> ( n e. Z \|-> sup ( ran ( F \|` ( ZZ>= ` n ) ) , RR* , < ) ) = ( k e. Z \|-> sup ( ran ( F \|` ( ZZ>= ` k ) ) , RR* , < ) ) )
131	1 2 3 4	limsupvaluz2	\|- ( ph -> ( limsup ` F ) = inf ( ran ( n e. Z \|-> sup ( ran ( F \|` ( ZZ>= ` n ) ) , RR* , < ) ) , RR , < ) )
132	131	eqcomd	\|- ( ph -> inf ( ran ( n e. Z \|-> sup ( ran ( F \|` ( ZZ>= ` n ) ) , RR* , < ) ) , RR , < ) = ( limsup ` F ) )
133	130 132	breq12d	\|- ( ph -> ( ( n e. Z \|-> sup ( ran ( F \|` ( ZZ>= ` n ) ) , RR* , < ) ) ~~> inf ( ran ( n e. Z \|-> sup ( ran ( F \|` ( ZZ>= ` n ) ) , RR* , < ) ) , RR , < ) <-> ( k e. Z \|-> sup ( ran ( F \|` ( ZZ>= ` k ) ) , RR* , < ) ) ~~> ( limsup ` F ) ) )
134	124 133	mpbid	\|- ( ph -> ( k e. Z \|-> sup ( ran ( F \|` ( ZZ>= ` k ) ) , RR* , < ) ) ~~> ( limsup ` F ) )

Metamath Proof Explorer

Theorem supcnvlimsup

Proof