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

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 ⊢ Ⅎ 𝑗 𝐹
limsupbnd1f.2 ⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
limsupbnd1f.3 ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ℝ* )
limsupbnd1f.4 ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
limsupbnd1f.5 ⊢ ( 𝜑 → ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 ) )
Assertion limsupbnd1f ( 𝜑 → ( lim sup ‘ 𝐹 ) ≤ 𝐴 )

Proof

Step Hyp Ref Expression
1 limsupbnd1f.1 ⊢ Ⅎ 𝑗 𝐹
2 limsupbnd1f.2 ⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
3 limsupbnd1f.3 ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ℝ* )
4 limsupbnd1f.4 ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
5 limsupbnd1f.5 ⊢ ( 𝜑 → ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 ) )
6 breq1 ⊢ ( 𝑘 = 𝑖 → ( 𝑘 ≤ 𝑗 ↔ 𝑖 ≤ 𝑗 ) )
7 6 imbi1d ⊢ ( 𝑘 = 𝑖 → ( ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 ) ↔ ( 𝑖 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 ) ) )
8 7 ralbidv ⊢ ( 𝑘 = 𝑖 → ( ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 ) ↔ ∀ 𝑗 ∈ 𝐵 ( 𝑖 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 ) ) )
9 nfv ⊢ Ⅎ 𝑙 ( 𝑖 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 )
10 nfv ⊢ Ⅎ 𝑗 𝑖 ≤ 𝑙
11 nfcv ⊢ Ⅎ 𝑗 𝑙
12 1 11 nffv ⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑙 )
13 nfcv ⊢ Ⅎ 𝑗 ≤
14 nfcv ⊢ Ⅎ 𝑗 𝐴
15 12 13 14 nfbr ⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑙 ) ≤ 𝐴
16 10 15 nfim ⊢ Ⅎ 𝑗 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝐴 )
17 breq2 ⊢ ( 𝑗 = 𝑙 → ( 𝑖 ≤ 𝑗 ↔ 𝑖 ≤ 𝑙 ) )
18 fveq2 ⊢ ( 𝑗 = 𝑙 → ( 𝐹 ‘ 𝑗 ) = ( 𝐹 ‘ 𝑙 ) )
19 18 breq1d ⊢ ( 𝑗 = 𝑙 → ( ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 ↔ ( 𝐹 ‘ 𝑙 ) ≤ 𝐴 ) )
20 17 19 imbi12d ⊢ ( 𝑗 = 𝑙 → ( ( 𝑖 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 ) ↔ ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝐴 ) ) )
21 9 16 20 cbvralw ⊢ ( ∀ 𝑗 ∈ 𝐵 ( 𝑖 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 ) ↔ ∀ 𝑙 ∈ 𝐵 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝐴 ) )
22 21 a1i ⊢ ( 𝑘 = 𝑖 → ( ∀ 𝑗 ∈ 𝐵 ( 𝑖 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 ) ↔ ∀ 𝑙 ∈ 𝐵 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝐴 ) ) )
23 8 22 bitrd ⊢ ( 𝑘 = 𝑖 → ( ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 ) ↔ ∀ 𝑙 ∈ 𝐵 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝐴 ) ) )
24 23 cbvrexvw ⊢ ( ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 ) ↔ ∃ 𝑖 ∈ ℝ ∀ 𝑙 ∈ 𝐵 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝐴 ) )
25 5 24 sylib ⊢ ( 𝜑 → ∃ 𝑖 ∈ ℝ ∀ 𝑙 ∈ 𝐵 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝐴 ) )
26 2 3 4 25 limsupbnd1 ⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ≤ 𝐴 )