Metamath Proof Explorer


Theorem limsupvaluz2

Description: The superior limit, when the domain of a real-valued function is a set of upper integers, and the superior limit is real. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses limsupvaluz2.m ( 𝜑𝑀 ∈ ℤ )
limsupvaluz2.z 𝑍 = ( ℤ𝑀 )
limsupvaluz2.f ( 𝜑𝐹 : 𝑍 ⟶ ℝ )
limsupvaluz2.r ( 𝜑 → ( lim sup ‘ 𝐹 ) ∈ ℝ )
Assertion limsupvaluz2 ( 𝜑 → ( lim sup ‘ 𝐹 ) = inf ( ran ( 𝑘𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑘 ) ) , ℝ* , < ) ) , ℝ , < ) )

Proof

Step Hyp Ref Expression
1 limsupvaluz2.m ( 𝜑𝑀 ∈ ℤ )
2 limsupvaluz2.z 𝑍 = ( ℤ𝑀 )
3 limsupvaluz2.f ( 𝜑𝐹 : 𝑍 ⟶ ℝ )
4 limsupvaluz2.r ( 𝜑 → ( lim sup ‘ 𝐹 ) ∈ ℝ )
5 3 frexr ( 𝜑𝐹 : 𝑍 ⟶ ℝ* )
6 1 2 5 limsupvaluz ( 𝜑 → ( lim sup ‘ 𝐹 ) = inf ( ran ( 𝑛𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ) , ℝ* , < ) )
7 3 adantr ( ( 𝜑𝑛𝑍 ) → 𝐹 : 𝑍 ⟶ ℝ )
8 2 uzssd3 ( 𝑛𝑍 → ( ℤ𝑛 ) ⊆ 𝑍 )
9 8 adantl ( ( 𝜑𝑛𝑍 ) → ( ℤ𝑛 ) ⊆ 𝑍 )
10 7 9 feqresmpt ( ( 𝜑𝑛𝑍 ) → ( 𝐹 ↾ ( ℤ𝑛 ) ) = ( 𝑚 ∈ ( ℤ𝑛 ) ↦ ( 𝐹𝑚 ) ) )
11 10 rneqd ( ( 𝜑𝑛𝑍 ) → ran ( 𝐹 ↾ ( ℤ𝑛 ) ) = ran ( 𝑚 ∈ ( ℤ𝑛 ) ↦ ( 𝐹𝑚 ) ) )
12 11 supeq1d ( ( 𝜑𝑛𝑍 ) → sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) = sup ( ran ( 𝑚 ∈ ( ℤ𝑛 ) ↦ ( 𝐹𝑚 ) ) , ℝ* , < ) )
13 nfcv 𝑚 𝐹
14 4 renepnfd ( 𝜑 → ( lim sup ‘ 𝐹 ) ≠ +∞ )
15 13 2 3 14 limsupubuz ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑚𝑍 ( 𝐹𝑚 ) ≤ 𝑥 )
16 15 adantr ( ( 𝜑𝑛𝑍 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑚𝑍 ( 𝐹𝑚 ) ≤ 𝑥 )
17 ssralv ( ( ℤ𝑛 ) ⊆ 𝑍 → ( ∀ 𝑚𝑍 ( 𝐹𝑚 ) ≤ 𝑥 → ∀ 𝑚 ∈ ( ℤ𝑛 ) ( 𝐹𝑚 ) ≤ 𝑥 ) )
18 8 17 syl ( 𝑛𝑍 → ( ∀ 𝑚𝑍 ( 𝐹𝑚 ) ≤ 𝑥 → ∀ 𝑚 ∈ ( ℤ𝑛 ) ( 𝐹𝑚 ) ≤ 𝑥 ) )
19 18 adantl ( ( 𝜑𝑛𝑍 ) → ( ∀ 𝑚𝑍 ( 𝐹𝑚 ) ≤ 𝑥 → ∀ 𝑚 ∈ ( ℤ𝑛 ) ( 𝐹𝑚 ) ≤ 𝑥 ) )
20 19 reximdv ( ( 𝜑𝑛𝑍 ) → ( ∃ 𝑥 ∈ ℝ ∀ 𝑚𝑍 ( 𝐹𝑚 ) ≤ 𝑥 → ∃ 𝑥 ∈ ℝ ∀ 𝑚 ∈ ( ℤ𝑛 ) ( 𝐹𝑚 ) ≤ 𝑥 ) )
21 16 20 mpd ( ( 𝜑𝑛𝑍 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑚 ∈ ( ℤ𝑛 ) ( 𝐹𝑚 ) ≤ 𝑥 )
22 nfv 𝑚 ( 𝜑𝑛𝑍 )
23 2 eluzelz2 ( 𝑛𝑍𝑛 ∈ ℤ )
24 uzid ( 𝑛 ∈ ℤ → 𝑛 ∈ ( ℤ𝑛 ) )
25 ne0i ( 𝑛 ∈ ( ℤ𝑛 ) → ( ℤ𝑛 ) ≠ ∅ )
26 23 24 25 3syl ( 𝑛𝑍 → ( ℤ𝑛 ) ≠ ∅ )
27 26 adantl ( ( 𝜑𝑛𝑍 ) → ( ℤ𝑛 ) ≠ ∅ )
28 7 adantr ( ( ( 𝜑𝑛𝑍 ) ∧ 𝑚 ∈ ( ℤ𝑛 ) ) → 𝐹 : 𝑍 ⟶ ℝ )
29 9 sselda ( ( ( 𝜑𝑛𝑍 ) ∧ 𝑚 ∈ ( ℤ𝑛 ) ) → 𝑚𝑍 )
30 28 29 ffvelcdmd ( ( ( 𝜑𝑛𝑍 ) ∧ 𝑚 ∈ ( ℤ𝑛 ) ) → ( 𝐹𝑚 ) ∈ ℝ )
31 22 27 30 supxrre3rnmpt ( ( 𝜑𝑛𝑍 ) → ( sup ( ran ( 𝑚 ∈ ( ℤ𝑛 ) ↦ ( 𝐹𝑚 ) ) , ℝ* , < ) ∈ ℝ ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑚 ∈ ( ℤ𝑛 ) ( 𝐹𝑚 ) ≤ 𝑥 ) )
32 21 31 mpbird ( ( 𝜑𝑛𝑍 ) → sup ( ran ( 𝑚 ∈ ( ℤ𝑛 ) ↦ ( 𝐹𝑚 ) ) , ℝ* , < ) ∈ ℝ )
33 12 32 eqeltrd ( ( 𝜑𝑛𝑍 ) → sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ∈ ℝ )
34 33 fmpttd ( 𝜑 → ( 𝑛𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ) : 𝑍 ⟶ ℝ )
35 34 frnd ( 𝜑 → ran ( 𝑛𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ) ⊆ ℝ )
36 nfv 𝑛 𝜑
37 eqid ( 𝑛𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ) = ( 𝑛𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) )
38 1 2 uzn0d ( 𝜑𝑍 ≠ ∅ )
39 36 33 37 38 rnmptn0 ( 𝜑 → ran ( 𝑛𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ) ≠ ∅ )
40 nfcv 𝑗 𝐹
41 40 1 2 5 limsupre3uz ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ∈ ℝ ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑖𝑍𝑗 ∈ ( ℤ𝑖 ) 𝑥 ≤ ( 𝐹𝑗 ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑖𝑍𝑗 ∈ ( ℤ𝑖 ) ( 𝐹𝑗 ) ≤ 𝑥 ) ) )
42 4 41 mpbid ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑖𝑍𝑗 ∈ ( ℤ𝑖 ) 𝑥 ≤ ( 𝐹𝑗 ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑖𝑍𝑗 ∈ ( ℤ𝑖 ) ( 𝐹𝑗 ) ≤ 𝑥 ) )
43 42 simpld ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑖𝑍𝑗 ∈ ( ℤ𝑖 ) 𝑥 ≤ ( 𝐹𝑗 ) )
44 simp-4r ( ( ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑖𝑍 ) ∧ 𝑗 ∈ ( ℤ𝑖 ) ) ∧ 𝑥 ≤ ( 𝐹𝑗 ) ) → 𝑥 ∈ ℝ )
45 44 rexrd ( ( ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑖𝑍 ) ∧ 𝑗 ∈ ( ℤ𝑖 ) ) ∧ 𝑥 ≤ ( 𝐹𝑗 ) ) → 𝑥 ∈ ℝ* )
46 5 3ad2ant1 ( ( 𝜑𝑖𝑍𝑗 ∈ ( ℤ𝑖 ) ) → 𝐹 : 𝑍 ⟶ ℝ* )
47 2 uztrn2 ( ( 𝑖𝑍𝑗 ∈ ( ℤ𝑖 ) ) → 𝑗𝑍 )
48 47 3adant1 ( ( 𝜑𝑖𝑍𝑗 ∈ ( ℤ𝑖 ) ) → 𝑗𝑍 )
49 46 48 ffvelcdmd ( ( 𝜑𝑖𝑍𝑗 ∈ ( ℤ𝑖 ) ) → ( 𝐹𝑗 ) ∈ ℝ* )
50 49 ad5ant134 ( ( ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑖𝑍 ) ∧ 𝑗 ∈ ( ℤ𝑖 ) ) ∧ 𝑥 ≤ ( 𝐹𝑗 ) ) → ( 𝐹𝑗 ) ∈ ℝ* )
51 rnresss ran ( 𝐹 ↾ ( ℤ𝑖 ) ) ⊆ ran 𝐹
52 3 frnd ( 𝜑 → ran 𝐹 ⊆ ℝ )
53 52 adantr ( ( 𝜑𝑖𝑍 ) → ran 𝐹 ⊆ ℝ )
54 51 53 sstrid ( ( 𝜑𝑖𝑍 ) → ran ( 𝐹 ↾ ( ℤ𝑖 ) ) ⊆ ℝ )
55 54 ssrexr ( ( 𝜑𝑖𝑍 ) → ran ( 𝐹 ↾ ( ℤ𝑖 ) ) ⊆ ℝ* )
56 55 supxrcld ( ( 𝜑𝑖𝑍 ) → sup ( ran ( 𝐹 ↾ ( ℤ𝑖 ) ) , ℝ* , < ) ∈ ℝ* )
57 56 ad5ant13 ( ( ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑖𝑍 ) ∧ 𝑗 ∈ ( ℤ𝑖 ) ) ∧ 𝑥 ≤ ( 𝐹𝑗 ) ) → sup ( ran ( 𝐹 ↾ ( ℤ𝑖 ) ) , ℝ* , < ) ∈ ℝ* )
58 simpr ( ( ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑖𝑍 ) ∧ 𝑗 ∈ ( ℤ𝑖 ) ) ∧ 𝑥 ≤ ( 𝐹𝑗 ) ) → 𝑥 ≤ ( 𝐹𝑗 ) )
59 55 3adant3 ( ( 𝜑𝑖𝑍𝑗 ∈ ( ℤ𝑖 ) ) → ran ( 𝐹 ↾ ( ℤ𝑖 ) ) ⊆ ℝ* )
60 fvres ( 𝑗 ∈ ( ℤ𝑖 ) → ( ( 𝐹 ↾ ( ℤ𝑖 ) ) ‘ 𝑗 ) = ( 𝐹𝑗 ) )
61 60 eqcomd ( 𝑗 ∈ ( ℤ𝑖 ) → ( 𝐹𝑗 ) = ( ( 𝐹 ↾ ( ℤ𝑖 ) ) ‘ 𝑗 ) )
62 61 3ad2ant3 ( ( 𝜑𝑖𝑍𝑗 ∈ ( ℤ𝑖 ) ) → ( 𝐹𝑗 ) = ( ( 𝐹 ↾ ( ℤ𝑖 ) ) ‘ 𝑗 ) )
63 3 ffnd ( 𝜑𝐹 Fn 𝑍 )
64 2 uzssd3 ( 𝑖𝑍 → ( ℤ𝑖 ) ⊆ 𝑍 )
65 fnssres ( ( 𝐹 Fn 𝑍 ∧ ( ℤ𝑖 ) ⊆ 𝑍 ) → ( 𝐹 ↾ ( ℤ𝑖 ) ) Fn ( ℤ𝑖 ) )
66 63 64 65 syl2an ( ( 𝜑𝑖𝑍 ) → ( 𝐹 ↾ ( ℤ𝑖 ) ) Fn ( ℤ𝑖 ) )
67 fnfvelrn ( ( ( 𝐹 ↾ ( ℤ𝑖 ) ) Fn ( ℤ𝑖 ) ∧ 𝑗 ∈ ( ℤ𝑖 ) ) → ( ( 𝐹 ↾ ( ℤ𝑖 ) ) ‘ 𝑗 ) ∈ ran ( 𝐹 ↾ ( ℤ𝑖 ) ) )
68 66 67 stoic3 ( ( 𝜑𝑖𝑍𝑗 ∈ ( ℤ𝑖 ) ) → ( ( 𝐹 ↾ ( ℤ𝑖 ) ) ‘ 𝑗 ) ∈ ran ( 𝐹 ↾ ( ℤ𝑖 ) ) )
69 62 68 eqeltrd ( ( 𝜑𝑖𝑍𝑗 ∈ ( ℤ𝑖 ) ) → ( 𝐹𝑗 ) ∈ ran ( 𝐹 ↾ ( ℤ𝑖 ) ) )
70 eqid sup ( ran ( 𝐹 ↾ ( ℤ𝑖 ) ) , ℝ* , < ) = sup ( ran ( 𝐹 ↾ ( ℤ𝑖 ) ) , ℝ* , < )
71 59 69 70 supxrubd ( ( 𝜑𝑖𝑍𝑗 ∈ ( ℤ𝑖 ) ) → ( 𝐹𝑗 ) ≤ sup ( ran ( 𝐹 ↾ ( ℤ𝑖 ) ) , ℝ* , < ) )
72 71 ad5ant134 ( ( ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑖𝑍 ) ∧ 𝑗 ∈ ( ℤ𝑖 ) ) ∧ 𝑥 ≤ ( 𝐹𝑗 ) ) → ( 𝐹𝑗 ) ≤ sup ( ran ( 𝐹 ↾ ( ℤ𝑖 ) ) , ℝ* , < ) )
73 45 50 57 58 72 xrletrd ( ( ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑖𝑍 ) ∧ 𝑗 ∈ ( ℤ𝑖 ) ) ∧ 𝑥 ≤ ( 𝐹𝑗 ) ) → 𝑥 ≤ sup ( ran ( 𝐹 ↾ ( ℤ𝑖 ) ) , ℝ* , < ) )
74 73 rexlimdva2 ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑖𝑍 ) → ( ∃ 𝑗 ∈ ( ℤ𝑖 ) 𝑥 ≤ ( 𝐹𝑗 ) → 𝑥 ≤ sup ( ran ( 𝐹 ↾ ( ℤ𝑖 ) ) , ℝ* , < ) ) )
75 74 ralimdva ( ( 𝜑𝑥 ∈ ℝ ) → ( ∀ 𝑖𝑍𝑗 ∈ ( ℤ𝑖 ) 𝑥 ≤ ( 𝐹𝑗 ) → ∀ 𝑖𝑍 𝑥 ≤ sup ( ran ( 𝐹 ↾ ( ℤ𝑖 ) ) , ℝ* , < ) ) )
76 75 reximdva ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑖𝑍𝑗 ∈ ( ℤ𝑖 ) 𝑥 ≤ ( 𝐹𝑗 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑖𝑍 𝑥 ≤ sup ( ran ( 𝐹 ↾ ( ℤ𝑖 ) ) , ℝ* , < ) ) )
77 43 76 mpd ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑖𝑍 𝑥 ≤ sup ( ran ( 𝐹 ↾ ( ℤ𝑖 ) ) , ℝ* , < ) )
78 fveq2 ( 𝑛 = 𝑖 → ( ℤ𝑛 ) = ( ℤ𝑖 ) )
79 78 reseq2d ( 𝑛 = 𝑖 → ( 𝐹 ↾ ( ℤ𝑛 ) ) = ( 𝐹 ↾ ( ℤ𝑖 ) ) )
80 79 rneqd ( 𝑛 = 𝑖 → ran ( 𝐹 ↾ ( ℤ𝑛 ) ) = ran ( 𝐹 ↾ ( ℤ𝑖 ) ) )
81 80 supeq1d ( 𝑛 = 𝑖 → sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) = sup ( ran ( 𝐹 ↾ ( ℤ𝑖 ) ) , ℝ* , < ) )
82 eqcom ( 𝑛 = 𝑖𝑖 = 𝑛 )
83 eqcom ( sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) = sup ( ran ( 𝐹 ↾ ( ℤ𝑖 ) ) , ℝ* , < ) ↔ sup ( ran ( 𝐹 ↾ ( ℤ𝑖 ) ) , ℝ* , < ) = sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) )
84 81 82 83 3imtr3i ( 𝑖 = 𝑛 → sup ( ran ( 𝐹 ↾ ( ℤ𝑖 ) ) , ℝ* , < ) = sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) )
85 84 breq2d ( 𝑖 = 𝑛 → ( 𝑥 ≤ sup ( ran ( 𝐹 ↾ ( ℤ𝑖 ) ) , ℝ* , < ) ↔ 𝑥 ≤ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ) )
86 85 cbvralvw ( ∀ 𝑖𝑍 𝑥 ≤ sup ( ran ( 𝐹 ↾ ( ℤ𝑖 ) ) , ℝ* , < ) ↔ ∀ 𝑛𝑍 𝑥 ≤ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) )
87 86 rexbii ( ∃ 𝑥 ∈ ℝ ∀ 𝑖𝑍 𝑥 ≤ sup ( ran ( 𝐹 ↾ ( ℤ𝑖 ) ) , ℝ* , < ) ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑛𝑍 𝑥 ≤ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) )
88 77 87 sylib ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑛𝑍 𝑥 ≤ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) )
89 36 33 rnmptbd2 ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑛𝑍 𝑥 ≤ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran ( 𝑛𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ) 𝑥𝑦 ) )
90 88 89 mpbid ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran ( 𝑛𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ) 𝑥𝑦 )
91 infxrre ( ( ran ( 𝑛𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ) ⊆ ℝ ∧ ran ( 𝑛𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ) ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran ( 𝑛𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ) 𝑥𝑦 ) → inf ( ran ( 𝑛𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ) , ℝ* , < ) = inf ( ran ( 𝑛𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ) , ℝ , < ) )
92 35 39 90 91 syl3anc ( 𝜑 → inf ( ran ( 𝑛𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ) , ℝ* , < ) = inf ( ran ( 𝑛𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ) , ℝ , < ) )
93 fveq2 ( 𝑛 = 𝑘 → ( ℤ𝑛 ) = ( ℤ𝑘 ) )
94 93 reseq2d ( 𝑛 = 𝑘 → ( 𝐹 ↾ ( ℤ𝑛 ) ) = ( 𝐹 ↾ ( ℤ𝑘 ) ) )
95 94 rneqd ( 𝑛 = 𝑘 → ran ( 𝐹 ↾ ( ℤ𝑛 ) ) = ran ( 𝐹 ↾ ( ℤ𝑘 ) ) )
96 95 supeq1d ( 𝑛 = 𝑘 → sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) = sup ( ran ( 𝐹 ↾ ( ℤ𝑘 ) ) , ℝ* , < ) )
97 96 cbvmptv ( 𝑛𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ) = ( 𝑘𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑘 ) ) , ℝ* , < ) )
98 97 rneqi ran ( 𝑛𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ) = ran ( 𝑘𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑘 ) ) , ℝ* , < ) )
99 98 infeq1i inf ( ran ( 𝑛𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ) , ℝ , < ) = inf ( ran ( 𝑘𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑘 ) ) , ℝ* , < ) ) , ℝ , < )
100 99 a1i ( 𝜑 → inf ( ran ( 𝑛𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑛 ) ) , ℝ* , < ) ) , ℝ , < ) = inf ( ran ( 𝑘𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑘 ) ) , ℝ* , < ) ) , ℝ , < ) )
101 6 92 100 3eqtrd ( 𝜑 → ( lim sup ‘ 𝐹 ) = inf ( ran ( 𝑘𝑍 ↦ sup ( ran ( 𝐹 ↾ ( ℤ𝑘 ) ) , ℝ* , < ) ) , ℝ , < ) )