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 ‘ ( 𝑗 ∈ 𝐵 ↦ 𝐶 ) ) ) |
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 ‘ ( 𝑗 ∈ 𝐵 ↦ 𝐶 ) ) ) |