Metamath Proof Explorer

Theorem limsupbnd1f

Description: If a sequence is eventually at most A , then the limsup is also at most A . (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses limsupbnd1f.1 ⊢ Ⅎ _ j F
limsupbnd1f.2 ⊢ φ → B ⊆ ℝ
limsupbnd1f.3 ⊢ φ → F : B ⟶ ℝ *
limsupbnd1f.4 ⊢ φ → A ∈ ℝ *
limsupbnd1f.5 ⊢ φ → ∃ k ∈ ℝ ∀ j ∈ B k ≤ j → F ⁡ j ≤ A
Assertion limsupbnd1f ⊢ φ → lim sup ⁡ F ≤ A

Proof

Step Hyp Ref Expression
1 limsupbnd1f.1 ⊢ Ⅎ _ j F
2 limsupbnd1f.2 ⊢ φ → B ⊆ ℝ
3 limsupbnd1f.3 ⊢ φ → F : B ⟶ ℝ *
4 limsupbnd1f.4 ⊢ φ → A ∈ ℝ *
5 limsupbnd1f.5 ⊢ φ → ∃ k ∈ ℝ ∀ j ∈ B k ≤ j → F ⁡ j ≤ A
6 breq1 ⊢ k = i → k ≤ j ↔ i ≤ j
7 6 imbi1d ⊢ k = i → k ≤ j → F ⁡ j ≤ A ↔ i ≤ j → F ⁡ j ≤ A
8 7 ralbidv ⊢ k = i → ∀ j ∈ B k ≤ j → F ⁡ j ≤ A ↔ ∀ j ∈ B i ≤ j → F ⁡ j ≤ A
9 nfv ⊢ Ⅎ l i ≤ j → F ⁡ j ≤ A
10 nfv ⊢ Ⅎ j i ≤ l
11 nfcv ⊢ Ⅎ _ j l
12 1 11 nffv ⊢ Ⅎ _ j F ⁡ l
13 nfcv ⊢ Ⅎ _ j ≤
14 nfcv ⊢ Ⅎ _ j A
15 12 13 14 nfbr ⊢ Ⅎ j F ⁡ l ≤ A
16 10 15 nfim ⊢ Ⅎ j i ≤ l → F ⁡ l ≤ A
17 breq2 ⊢ j = l → i ≤ j ↔ i ≤ l
18 fveq2 ⊢ j = l → F ⁡ j = F ⁡ l
19 18 breq1d ⊢ j = l → F ⁡ j ≤ A ↔ F ⁡ l ≤ A
20 17 19 imbi12d ⊢ j = l → i ≤ j → F ⁡ j ≤ A ↔ i ≤ l → F ⁡ l ≤ A
21 9 16 20 cbvralw ⊢ ∀ j ∈ B i ≤ j → F ⁡ j ≤ A ↔ ∀ l ∈ B i ≤ l → F ⁡ l ≤ A
22 21 a1i ⊢ k = i → ∀ j ∈ B i ≤ j → F ⁡ j ≤ A ↔ ∀ l ∈ B i ≤ l → F ⁡ l ≤ A
23 8 22 bitrd ⊢ k = i → ∀ j ∈ B k ≤ j → F ⁡ j ≤ A ↔ ∀ l ∈ B i ≤ l → F ⁡ l ≤ A
24 23 cbvrexvw ⊢ ∃ k ∈ ℝ ∀ j ∈ B k ≤ j → F ⁡ j ≤ A ↔ ∃ i ∈ ℝ ∀ l ∈ B i ≤ l → F ⁡ l ≤ A
25 5 24 sylib ⊢ φ → ∃ i ∈ ℝ ∀ l ∈ B i ≤ l → F ⁡ l ≤ A
26 2 3 4 25 limsupbnd1 ⊢ φ → lim sup ⁡ F ≤ A