Metamath Proof Explorer


Theorem limsupequzmpt

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 limsupequzmpt.j 𝑗 𝜑
limsupequzmpt.m ( 𝜑𝑀 ∈ ℤ )
limsupequzmpt.n ( 𝜑𝑁 ∈ ℤ )
limsupequzmpt.a 𝐴 = ( ℤ𝑀 )
limsupequzmpt.b 𝐵 = ( ℤ𝑁 )
limsupequzmpt.c ( ( 𝜑𝑗𝐴 ) → 𝐶𝑉 )
limsupequzmpt.d ( ( 𝜑𝑗𝐵 ) → 𝐶𝑊 )
Assertion limsupequzmpt ( 𝜑 → ( lim sup ‘ ( 𝑗𝐴𝐶 ) ) = ( lim sup ‘ ( 𝑗𝐵𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 limsupequzmpt.j 𝑗 𝜑
2 limsupequzmpt.m ( 𝜑𝑀 ∈ ℤ )
3 limsupequzmpt.n ( 𝜑𝑁 ∈ ℤ )
4 limsupequzmpt.a 𝐴 = ( ℤ𝑀 )
5 limsupequzmpt.b 𝐵 = ( ℤ𝑁 )
6 limsupequzmpt.c ( ( 𝜑𝑗𝐴 ) → 𝐶𝑉 )
7 limsupequzmpt.d ( ( 𝜑𝑗𝐵 ) → 𝐶𝑊 )
8 eqid if ( 𝑀𝑁 , 𝑁 , 𝑀 ) = if ( 𝑀𝑁 , 𝑁 , 𝑀 )
9 1 2 3 4 5 6 7 8 limsupequzmptlem ( 𝜑 → ( lim sup ‘ ( 𝑗𝐴𝐶 ) ) = ( lim sup ‘ ( 𝑗𝐵𝐶 ) ) )