Metamath Proof Explorer

Theorem limsupequzmptlem

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 limsupequzmptlem.j ⊢ Ⅎ 𝑗 𝜑
limsupequzmptlem.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
limsupequzmptlem.n ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
limsupequzmptlem.a ⊢ 𝐴 = ( ℤ≥ ‘ 𝑀 )
limsupequzmptlem.b ⊢ 𝐵 = ( ℤ≥ ‘ 𝑁 )
limsupequzmptlem.c ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
limsupequzmptlem.d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐵 ) → 𝐶 ∈ 𝑊 )
limsupequzmptlem.k ⊢ 𝐾 = if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 )
Assertion limsupequzmptlem ( 𝜑 → ( lim sup ‘ ( 𝑗 ∈ 𝐴 ↦ 𝐶 ) ) = ( lim sup ‘ ( 𝑗 ∈ 𝐵 ↦ 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 limsupequzmptlem.j ⊢ Ⅎ 𝑗 𝜑
2 limsupequzmptlem.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 limsupequzmptlem.n ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
4 limsupequzmptlem.a ⊢ 𝐴 = ( ℤ≥ ‘ 𝑀 )
5 limsupequzmptlem.b ⊢ 𝐵 = ( ℤ≥ ‘ 𝑁 )
6 limsupequzmptlem.c ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
7 limsupequzmptlem.d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐵 ) → 𝐶 ∈ 𝑊 )
8 limsupequzmptlem.k ⊢ 𝐾 = if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 )
9 nfmpt1 ⊢ Ⅎ 𝑗 ( 𝑗 ∈ 𝐴 ↦ 𝐶 )
10 nfmpt1 ⊢ Ⅎ 𝑗 ( 𝑗 ∈ 𝐵 ↦ 𝐶 )
11 4 eqcomi ⊢ ( ℤ≥ ‘ 𝑀 ) = 𝐴
12 11 eleq2i ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ 𝑗 ∈ 𝐴 )
13 12 biimpi ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑗 ∈ 𝐴 )
14 13 6 sylan2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝐶 ∈ 𝑉 )
15 4 mpteq1i ⊢ ( 𝑗 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ 𝐶 )
16 1 14 15 fnmptd ⊢ ( 𝜑 → ( 𝑗 ∈ 𝐴 ↦ 𝐶 ) Fn ( ℤ≥ ‘ 𝑀 ) )
17 5 eleq2i ⊢ ( 𝑗 ∈ 𝐵 ↔ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) )
18 17 bicomi ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ↔ 𝑗 ∈ 𝐵 )
19 18 biimpi ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑗 ∈ 𝐵 )
20 19 7 sylan2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝐶 ∈ 𝑊 )
21 5 mpteq1i ⊢ ( 𝑗 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ↦ 𝐶 )
22 1 20 21 fnmptd ⊢ ( 𝜑 → ( 𝑗 ∈ 𝐵 ↦ 𝐶 ) Fn ( ℤ≥ ‘ 𝑁 ) )
23 3 2 ifcld ⊢ ( 𝜑 → if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∈ ℤ )
24 8 23 eqeltrid ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
25 eqid ⊢ ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑀 )
26 2 zred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
27 3 zred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
28 max1 ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → 𝑀 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) )
29 26 27 28 syl2anc ⊢ ( 𝜑 → 𝑀 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) )
30 29 8 breqtrrdi ⊢ ( 𝜑 → 𝑀 ≤ 𝐾 )
31 25 2 24 30 eluzd ⊢ ( 𝜑 → 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) )
32 31 uzssd ⊢ ( 𝜑 → ( ℤ≥ ‘ 𝐾 ) ⊆ ( ℤ≥ ‘ 𝑀 ) )
33 11 a1i ⊢ ( 𝜑 → ( ℤ≥ ‘ 𝑀 ) = 𝐴 )
34 32 33 sseqtrd ⊢ ( 𝜑 → ( ℤ≥ ‘ 𝐾 ) ⊆ 𝐴 )
35 34 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ℤ≥ ‘ 𝐾 ) ⊆ 𝐴 )
36 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) )
37 35 36 sseldd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝑗 ∈ 𝐴 )
38 37 6 syldan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝐶 ∈ 𝑉 )
39 eqid ⊢ ( 𝑗 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑗 ∈ 𝐴 ↦ 𝐶 )
40 39 fvmpt2 ⊢ ( ( 𝑗 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉 ) → ( ( 𝑗 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑗 ) = 𝐶 )
41 37 38 40 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ( 𝑗 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑗 ) = 𝐶 )
42 eqid ⊢ ( ℤ≥ ‘ 𝑁 ) = ( ℤ≥ ‘ 𝑁 )
43 max2 ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → 𝑁 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) )
44 26 27 43 syl2anc ⊢ ( 𝜑 → 𝑁 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) )
45 44 8 breqtrrdi ⊢ ( 𝜑 → 𝑁 ≤ 𝐾 )
46 42 3 24 45 eluzd ⊢ ( 𝜑 → 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) )
47 46 uzssd ⊢ ( 𝜑 → ( ℤ≥ ‘ 𝐾 ) ⊆ ( ℤ≥ ‘ 𝑁 ) )
48 5 eqcomi ⊢ ( ℤ≥ ‘ 𝑁 ) = 𝐵
49 48 a1i ⊢ ( 𝜑 → ( ℤ≥ ‘ 𝑁 ) = 𝐵 )
50 47 49 sseqtrd ⊢ ( 𝜑 → ( ℤ≥ ‘ 𝐾 ) ⊆ 𝐵 )
51 50 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ℤ≥ ‘ 𝐾 ) ⊆ 𝐵 )
52 51 36 sseldd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝑗 ∈ 𝐵 )
53 eqid ⊢ ( 𝑗 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑗 ∈ 𝐵 ↦ 𝐶 )
54 53 fvmpt2 ⊢ ( ( 𝑗 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ) → ( ( 𝑗 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑗 ) = 𝐶 )
55 52 38 54 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ( 𝑗 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑗 ) = 𝐶 )
56 41 55 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ( 𝑗 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑗 ) = ( ( 𝑗 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑗 ) )
57 1 9 10 2 16 3 22 24 56 limsupequz ⊢ ( 𝜑 → ( lim sup ‘ ( 𝑗 ∈ 𝐴 ↦ 𝐶 ) ) = ( lim sup ‘ ( 𝑗 ∈ 𝐵 ↦ 𝐶 ) ) )