Theorem limsupequz

Description: Two functions that are eventually equal to one another have the same superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	limsupequz.1	|- F/ k ph
	limsupequz.2	|- F/_ k F
	limsupequz.3	|- F/_ k G
	limsupequz.4	|- ( ph -> M e. ZZ )
	limsupequz.5	|- ( ph -> F Fn ( ZZ>= ` M ) )
	limsupequz.6	|- ( ph -> N e. ZZ )
	limsupequz.7	|- ( ph -> G Fn ( ZZ>= ` N ) )
	limsupequz.8	|- ( ph -> K e. ZZ )
	limsupequz.9	|- ( ( ph /\ k e. ( ZZ>= ` K ) ) -> ( F ` k ) = ( G ` k ) )
Assertion	limsupequz	|- ( ph -> ( limsup ` F ) = ( limsup ` G ) )

Proof

Step	Hyp	Ref	Expression
1		limsupequz.1	|- F/ k ph
2		limsupequz.2	|- F/_ k F
3		limsupequz.3	|- F/_ k G
4		limsupequz.4	|- ( ph -> M e. ZZ )
5		limsupequz.5	|- ( ph -> F Fn ( ZZ>= ` M ) )
6		limsupequz.6	|- ( ph -> N e. ZZ )
7		limsupequz.7	|- ( ph -> G Fn ( ZZ>= ` N ) )
8		limsupequz.8	|- ( ph -> K e. ZZ )
9		limsupequz.9	|- ( ( ph /\ k e. ( ZZ>= ` K ) ) -> ( F ` k ) = ( G ` k ) )
10		nfv	|- F/ j ph
11		nfv	|- F/ k j e. ( ZZ>= ` K )
12	1 11	nfan	|- F/ k ( ph /\ j e. ( ZZ>= ` K ) )
13		nfcv	|- F/_ k j
14	2 13	nffv	|- F/_ k ( F ` j )
15	3 13	nffv	|- F/_ k ( G ` j )
16	14 15	nfeq	|- F/ k ( F ` j ) = ( G ` j )
17	12 16	nfim	|- F/ k ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( F ` j ) = ( G ` j ) )
18		eleq1w	|- ( k = j -> ( k e. ( ZZ>= ` K ) <-> j e. ( ZZ>= ` K ) ) )
19	18	anbi2d	|- ( k = j -> ( ( ph /\ k e. ( ZZ>= ` K ) ) <-> ( ph /\ j e. ( ZZ>= ` K ) ) ) )
20		fveq2	|- ( k = j -> ( F ` k ) = ( F ` j ) )
21		fveq2	|- ( k = j -> ( G ` k ) = ( G ` j ) )
22	20 21	eqeq12d	|- ( k = j -> ( ( F ` k ) = ( G ` k ) <-> ( F ` j ) = ( G ` j ) ) )
23	19 22	imbi12d	|- ( k = j -> ( ( ( ph /\ k e. ( ZZ>= ` K ) ) -> ( F ` k ) = ( G ` k ) ) <-> ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( F ` j ) = ( G ` j ) ) ) )
24	17 23 9	chvarfv	|- ( ( ph /\ j e. ( ZZ>= ` K ) ) -> ( F ` j ) = ( G ` j ) )
25	10 4 5 6 7 8 24	limsupequzlem	|- ( ph -> ( limsup ` F ) = ( limsup ` G ) )