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	$$⊢Ⅎk\phi$$
	limsupequz.2	$$⊢\underset{\_}{Ⅎ}kF$$
	limsupequz.3	$$⊢\underset{\_}{Ⅎ}kG$$
	limsupequz.4	$$⊢\phi \to M\in \mathbb{Z}$$
	limsupequz.5	$$⊢\phi \to FFn{\mathbb{Z}}_{\ge M}$$
	limsupequz.6	$$⊢\phi \to N\in \mathbb{Z}$$
	limsupequz.7	$$⊢\phi \to GFn{\mathbb{Z}}_{\ge N}$$
	limsupequz.8	$$⊢\phi \to K\in \mathbb{Z}$$
	limsupequz.9	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge K}\right)\to F\left(k\right)=G\left(k\right)$$
Assertion	limsupequz	$$⊢\phi \to \mathrm{lim\; sup}\left(F\right)=\mathrm{lim\; sup}\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		limsupequz.1	$$⊢Ⅎk\phi$$
2		limsupequz.2	$$⊢\underset{\_}{Ⅎ}kF$$
3		limsupequz.3	$$⊢\underset{\_}{Ⅎ}kG$$
4		limsupequz.4	$$⊢\phi \to M\in \mathbb{Z}$$
5		limsupequz.5	$$⊢\phi \to FFn{\mathbb{Z}}_{\ge M}$$
6		limsupequz.6	$$⊢\phi \to N\in \mathbb{Z}$$
7		limsupequz.7	$$⊢\phi \to GFn{\mathbb{Z}}_{\ge N}$$
8		limsupequz.8	$$⊢\phi \to K\in \mathbb{Z}$$
9		limsupequz.9	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge K}\right)\to F\left(k\right)=G\left(k\right)$$
10		nfv	$$⊢Ⅎj\phi$$
11		nfv	$$⊢Ⅎkj\in {\mathbb{Z}}_{\ge K}$$
12	1 11	nfan	$$⊢Ⅎk\left(\phi \wedge j\in {\mathbb{Z}}_{\ge K}\right)$$
13		nfcv	$$⊢\underset{\_}{Ⅎ}kj$$
14	2 13	nffv	$$⊢\underset{\_}{Ⅎ}kF\left(j\right)$$
15	3 13	nffv	$$⊢\underset{\_}{Ⅎ}kG\left(j\right)$$
16	14 15	nfeq	$$⊢ℲkF\left(j\right)=G\left(j\right)$$
17	12 16	nfim	$$⊢Ⅎk\left(\left(\phi \wedge j\in {\mathbb{Z}}_{\ge K}\right)\to F\left(j\right)=G\left(j\right)\right)$$
18		eleq1w	$$⊢k=j\to \left(k\in {\mathbb{Z}}_{\ge K}\leftrightarrow j\in {\mathbb{Z}}_{\ge K}\right)$$
19	18	anbi2d	$$⊢k=j\to \left(\left(\phi \wedge k\in {\mathbb{Z}}_{\ge K}\right)\leftrightarrow \left(\phi \wedge j\in {\mathbb{Z}}_{\ge K}\right)\right)$$
20		fveq2	$$⊢k=j\to F\left(k\right)=F\left(j\right)$$
21		fveq2	$$⊢k=j\to G\left(k\right)=G\left(j\right)$$
22	20 21	eqeq12d	$$⊢k=j\to \left(F\left(k\right)=G\left(k\right)\leftrightarrow F\left(j\right)=G\left(j\right)\right)$$
23	19 22	imbi12d	$$⊢k=j\to \left(\left(\left(\phi \wedge k\in {\mathbb{Z}}_{\ge K}\right)\to F\left(k\right)=G\left(k\right)\right)\leftrightarrow \left(\left(\phi \wedge j\in {\mathbb{Z}}_{\ge K}\right)\to F\left(j\right)=G\left(j\right)\right)\right)$$
24	17 23 9	chvarfv	$$⊢\left(\phi \wedge j\in {\mathbb{Z}}_{\ge K}\right)\to F\left(j\right)=G\left(j\right)$$
25	10 4 5 6 7 8 24	limsupequzlem	$$⊢\phi \to \mathrm{lim\; sup}\left(F\right)=\mathrm{lim\; sup}\left(G\right)$$