Metamath Proof Explorer

Theorem limsupequzlem

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

Proof

Step Hyp Ref Expression
1 limsupequzlem.1 ⊢ Ⅎ 𝑘 𝜑
2 limsupequzlem.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 limsupequzlem.4 ⊢ ( 𝜑 → 𝐹 Fn ( ℤ≥ ‘ 𝑀 ) )
4 limsupequzlem.5 ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
5 limsupequzlem.6 ⊢ ( 𝜑 → 𝐺 Fn ( ℤ≥ ‘ 𝑁 ) )
6 limsupequzlem.7 ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
7 limsupequzlem.8 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
8 eqid ⊢ ( ℤ≥ ‘ 𝐾 ) = ( ℤ≥ ‘ 𝐾 )
9 6 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ) ) → 𝐾 ∈ ℤ )
10 eluzelz ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ) → 𝑘 ∈ ℤ )
11 10 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ) ) → 𝑘 ∈ ℤ )
12 6 zred ⊢ ( 𝜑 → 𝐾 ∈ ℝ )
13 12 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ) ) → 𝐾 ∈ ℝ )
14 13 rexrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ) ) → 𝐾 ∈ ℝ* )
15 zssxr ⊢ ℤ ⊆ ℝ*
16 tpssi ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → { 𝑀 , 𝑁 , 𝐾 } ⊆ ℤ )
17 2 4 6 16 syl3anc ⊢ ( 𝜑 → { 𝑀 , 𝑁 , 𝐾 } ⊆ ℤ )
18 xrltso ⊢ < Or ℝ*
19 18 a1i ⊢ ( 𝜑 → < Or ℝ* )
20 tpfi ⊢ { 𝑀 , 𝑁 , 𝐾 } ∈ Fin
21 20 a1i ⊢ ( 𝜑 → { 𝑀 , 𝑁 , 𝐾 } ∈ Fin )
22 2 tpnzd ⊢ ( 𝜑 → { 𝑀 , 𝑁 , 𝐾 } ≠ ∅ )
23 15 a1i ⊢ ( 𝜑 → ℤ ⊆ ℝ* )
24 17 23 sstrd ⊢ ( 𝜑 → { 𝑀 , 𝑁 , 𝐾 } ⊆ ℝ* )
25 fisupcl ⊢ ( ( < Or ℝ* ∧ ( { 𝑀 , 𝑁 , 𝐾 } ∈ Fin ∧ { 𝑀 , 𝑁 , 𝐾 } ≠ ∅ ∧ { 𝑀 , 𝑁 , 𝐾 } ⊆ ℝ* ) ) → sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ∈ { 𝑀 , 𝑁 , 𝐾 } )
26 19 21 22 24 25 syl13anc ⊢ ( 𝜑 → sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ∈ { 𝑀 , 𝑁 , 𝐾 } )
27 17 26 sseldd ⊢ ( 𝜑 → sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ∈ ℤ )
28 15 27 sseldi ⊢ ( 𝜑 → sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ∈ ℝ* )
29 28 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ) ) → sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ∈ ℝ* )
30 eluzelre ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ) → 𝑘 ∈ ℝ )
31 30 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ) ) → 𝑘 ∈ ℝ )
32 31 rexrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ) ) → 𝑘 ∈ ℝ* )
33 tpid3g ⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ { 𝑀 , 𝑁 , 𝐾 } )
34 6 33 syl ⊢ ( 𝜑 → 𝐾 ∈ { 𝑀 , 𝑁 , 𝐾 } )
35 eqid ⊢ sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) = sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < )
36 24 34 35 supxrubd ⊢ ( 𝜑 → 𝐾 ≤ sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) )
37 36 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ) ) → 𝐾 ≤ sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) )
38 eluzle ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ) → sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ≤ 𝑘 )
39 38 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ) ) → sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ≤ 𝑘 )
40 14 29 32 37 39 xrletrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ) ) → 𝐾 ≤ 𝑘 )
41 8 9 11 40 eluzd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝐾 ) )
42 41 7 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
43 1 42 ralrimia ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( ℤ≥ ‘ sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ) ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
44 eqid ⊢ ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑀 )
45 tpid1g ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ { 𝑀 , 𝑁 , 𝐾 } )
46 2 45 syl ⊢ ( 𝜑 → 𝑀 ∈ { 𝑀 , 𝑁 , 𝐾 } )
47 24 46 35 supxrubd ⊢ ( 𝜑 → 𝑀 ≤ sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) )
48 44 2 27 47 eluzd ⊢ ( 𝜑 → sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ∈ ( ℤ≥ ‘ 𝑀 ) )
49 uzss ⊢ ( sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( ℤ≥ ‘ sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ) ⊆ ( ℤ≥ ‘ 𝑀 ) )
50 48 49 syl ⊢ ( 𝜑 → ( ℤ≥ ‘ sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ) ⊆ ( ℤ≥ ‘ 𝑀 ) )
51 eqid ⊢ ( ℤ≥ ‘ 𝑁 ) = ( ℤ≥ ‘ 𝑁 )
52 tpid2g ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ { 𝑀 , 𝑁 , 𝐾 } )
53 4 52 syl ⊢ ( 𝜑 → 𝑁 ∈ { 𝑀 , 𝑁 , 𝐾 } )
54 24 53 35 supxrubd ⊢ ( 𝜑 → 𝑁 ≤ sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) )
55 51 4 27 54 eluzd ⊢ ( 𝜑 → sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ∈ ( ℤ≥ ‘ 𝑁 ) )
56 uzss ⊢ ( sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ∈ ( ℤ≥ ‘ 𝑁 ) → ( ℤ≥ ‘ sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ) ⊆ ( ℤ≥ ‘ 𝑁 ) )
57 55 56 syl ⊢ ( 𝜑 → ( ℤ≥ ‘ sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ) ⊆ ( ℤ≥ ‘ 𝑁 ) )
58 fvreseq0 ⊢ ( ( ( 𝐹 Fn ( ℤ≥ ‘ 𝑀 ) ∧ 𝐺 Fn ( ℤ≥ ‘ 𝑁 ) ) ∧ ( ( ℤ≥ ‘ sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ) ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ ( ℤ≥ ‘ sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ) ⊆ ( ℤ≥ ‘ 𝑁 ) ) ) → ( ( 𝐹 ↾ ( ℤ≥ ‘ sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ) ) = ( 𝐺 ↾ ( ℤ≥ ‘ sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ) ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ) ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) ) )
59 3 5 50 57 58 syl22anc ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( ℤ≥ ‘ sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ) ) = ( 𝐺 ↾ ( ℤ≥ ‘ sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ) ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ) ( 𝐹 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) ) )
60 43 59 mpbird ⊢ ( 𝜑 → ( 𝐹 ↾ ( ℤ≥ ‘ sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ) ) = ( 𝐺 ↾ ( ℤ≥ ‘ sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ) ) )
61 60 fveq2d ⊢ ( 𝜑 → ( lim sup ‘ ( 𝐹 ↾ ( ℤ≥ ‘ sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ) ) ) = ( lim sup ‘ ( 𝐺 ↾ ( ℤ≥ ‘ sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ) ) ) )
62 eqid ⊢ ( ℤ≥ ‘ sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ) = ( ℤ≥ ‘ sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) )
63 fvexd ⊢ ( 𝜑 → ( ℤ≥ ‘ 𝑀 ) ∈ V )
64 3 63 fnexd ⊢ ( 𝜑 → 𝐹 ∈ V )
65 3 fndmd ⊢ ( 𝜑 → dom 𝐹 = ( ℤ≥ ‘ 𝑀 ) )
66 uzssz ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
67 65 66 eqsstrdi ⊢ ( 𝜑 → dom 𝐹 ⊆ ℤ )
68 27 62 64 67 limsupresuz2 ⊢ ( 𝜑 → ( lim sup ‘ ( 𝐹 ↾ ( ℤ≥ ‘ sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ) ) ) = ( lim sup ‘ 𝐹 ) )
69 fvexd ⊢ ( 𝜑 → ( ℤ≥ ‘ 𝑁 ) ∈ V )
70 5 69 fnexd ⊢ ( 𝜑 → 𝐺 ∈ V )
71 5 fndmd ⊢ ( 𝜑 → dom 𝐺 = ( ℤ≥ ‘ 𝑁 ) )
72 uzssz ⊢ ( ℤ≥ ‘ 𝑁 ) ⊆ ℤ
73 71 72 eqsstrdi ⊢ ( 𝜑 → dom 𝐺 ⊆ ℤ )
74 27 62 70 73 limsupresuz2 ⊢ ( 𝜑 → ( lim sup ‘ ( 𝐺 ↾ ( ℤ≥ ‘ sup ( { 𝑀 , 𝑁 , 𝐾 } , ℝ* , < ) ) ) ) = ( lim sup ‘ 𝐺 ) )
75 61 68 74 3eqtr3d ⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) = ( lim sup ‘ 𝐺 ) )