This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem limsupequz

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 limsupequz.1 ⊢ Ⅎ k φ
limsupequz.2 ⊢ Ⅎ _ k F
limsupequz.3 ⊢ Ⅎ _ k G
limsupequz.4 ⊢ φ → M ∈ ℤ
limsupequz.5 ⊢ φ → F Fn ℤ ≥ M
limsupequz.6 ⊢ φ → N ∈ ℤ
limsupequz.7 ⊢ φ → G Fn ℤ ≥ N
limsupequz.8 ⊢ φ → K ∈ ℤ
limsupequz.9 ⊢ φ ∧ k ∈ ℤ ≥ K → F ⁡ k = G ⁡ k
Assertion limsupequz ⊢ φ → lim sup ⁡ F = lim sup ⁡ G

Proof

Step Hyp Ref Expression
1 limsupequz.1 ⊢ Ⅎ k φ
2 limsupequz.2 ⊢ Ⅎ _ k F
3 limsupequz.3 ⊢ Ⅎ _ k G
4 limsupequz.4 ⊢ φ → M ∈ ℤ
5 limsupequz.5 ⊢ φ → F Fn ℤ ≥ M
6 limsupequz.6 ⊢ φ → N ∈ ℤ
7 limsupequz.7 ⊢ φ → G Fn ℤ ≥ N
8 limsupequz.8 ⊢ φ → K ∈ ℤ
9 limsupequz.9 ⊢ φ ∧ k ∈ ℤ ≥ K → F ⁡ k = G ⁡ k
10 nfv ⊢ Ⅎ j φ
11 nfv ⊢ Ⅎ k j ∈ ℤ ≥ K
12 1 11 nfan ⊢ Ⅎ k φ ∧ j ∈ ℤ ≥ K
13 nfcv ⊢ Ⅎ _ k j
14 2 13 nffv ⊢ Ⅎ _ k F ⁡ j
15 3 13 nffv ⊢ Ⅎ _ k G ⁡ j
16 14 15 nfeq ⊢ Ⅎ k F ⁡ j = G ⁡ j
17 12 16 nfim ⊢ Ⅎ k φ ∧ j ∈ ℤ ≥ K → F ⁡ j = G ⁡ j
18 eleq1w ⊢ k = j → k ∈ ℤ ≥ K ↔ j ∈ ℤ ≥ K
19 18 anbi2d ⊢ k = j → φ ∧ k ∈ ℤ ≥ K ↔ φ ∧ j ∈ ℤ ≥ K
20 fveq2 ⊢ k = j → F ⁡ k = F ⁡ j
21 fveq2 ⊢ k = j → G ⁡ k = G ⁡ j
22 20 21 eqeq12d ⊢ k = j → F ⁡ k = G ⁡ k ↔ F ⁡ j = G ⁡ j
23 19 22 imbi12d ⊢ k = j → φ ∧ k ∈ ℤ ≥ K → F ⁡ k = G ⁡ k ↔ φ ∧ j ∈ ℤ ≥ K → F ⁡ j = G ⁡ j
24 17 23 9 chvarfv ⊢ φ ∧ j ∈ ℤ ≥ K → F ⁡ j = G ⁡ j
25 10 4 5 6 7 8 24 limsupequzlem ⊢ φ → lim sup ⁡ F = lim sup ⁡ G