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	⊢ Ⅎ 𝑘 𝜑
	limsupequz.2	⊢ Ⅎ 𝑘 𝐹
	limsupequz.3	⊢ Ⅎ 𝑘 𝐺
	limsupequz.4	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	limsupequz.5	⊢ ( 𝜑 → 𝐹 Fn ( ℤ≥ ‘ 𝑀 ) )
	limsupequz.6	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
	limsupequz.7	⊢ ( 𝜑 → 𝐺 Fn ( ℤ≥ ‘ 𝑁 ) )
	limsupequz.8	⊢ ( 𝜑 → 𝐾 ∈ ℤ )
	limsupequz.9	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
Assertion	limsupequz	⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) = ( lim sup ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		limsupequz.1	⊢ Ⅎ 𝑘 𝜑
2		limsupequz.2	⊢ Ⅎ 𝑘 𝐹
3		limsupequz.3	⊢ Ⅎ 𝑘 𝐺
4		limsupequz.4	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
5		limsupequz.5	⊢ ( 𝜑 → 𝐹 Fn ( ℤ≥ ‘ 𝑀 ) )
6		limsupequz.6	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
7		limsupequz.7	⊢ ( 𝜑 → 𝐺 Fn ( ℤ≥ ‘ 𝑁 ) )
8		limsupequz.8	⊢ ( 𝜑 → 𝐾 ∈ ℤ )
9		limsupequz.9	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
10		nfv	⊢ Ⅎ 𝑗 𝜑
11		nfv	⊢ Ⅎ 𝑘 𝑗 ∈ ( ℤ≥ ‘ 𝐾 )
12	1 11	nfan	⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) )
13		nfcv	⊢ Ⅎ 𝑘 𝑗
14	2 13	nffv	⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑗 )
15	3 13	nffv	⊢ Ⅎ 𝑘 ( 𝐺 ‘ 𝑗 )
16	14 15	nfeq	⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑗 ) = ( 𝐺 ‘ 𝑗 )
17	12 16	nfim	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝐹 ‘ 𝑗 ) = ( 𝐺 ‘ 𝑗 ) )
18		eleq1w	⊢ ( 𝑘 = 𝑗 → ( 𝑘 ∈ ( ℤ≥ ‘ 𝐾 ) ↔ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) )
19	18	anbi2d	⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝐾 ) ) ↔ ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) ) )
20		fveq2	⊢ ( 𝑘 = 𝑗 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑗 ) )
21		fveq2	⊢ ( 𝑘 = 𝑗 → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑗 ) )
22	20 21	eqeq12d	⊢ ( 𝑘 = 𝑗 → ( ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) ↔ ( 𝐹 ‘ 𝑗 ) = ( 𝐺 ‘ 𝑗 ) ) )
23	19 22	imbi12d	⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝐹 ‘ 𝑗 ) = ( 𝐺 ‘ 𝑗 ) ) ) )
24	17 23 9	chvarfv	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝐹 ‘ 𝑗 ) = ( 𝐺 ‘ 𝑗 ) )
25	10 4 5 6 7 8 24	limsupequzlem	⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) = ( lim sup ‘ 𝐺 ) )