Theorem limsupbnd1

Description: If a sequence is eventually at most A , then the limsup is also at most A . (The converse is only true if the less or equal is replaced by strictly less than; consider the sequence 1 / n which is never less or equal to zero even though the limsup is.) (Contributed by Mario Carneiro, 7-Sep-2014) (Revised by AV, 12-Sep-2020)

	Ref	Expression
Hypotheses	limsupbnd.1	⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
	limsupbnd.2	⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ℝ* )
	limsupbnd.3	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
	limsupbnd1.4	⊢ ( 𝜑 → ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 ) )
Assertion	limsupbnd1	⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ≤ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		limsupbnd.1	⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
2		limsupbnd.2	⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ℝ* )
3		limsupbnd.3	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
4		limsupbnd1.4	⊢ ( 𝜑 → ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 ) )
5	1	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) → 𝐵 ⊆ ℝ )
6	2	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) → 𝐹 : 𝐵 ⟶ ℝ* )
7		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) → 𝑘 ∈ ℝ )
8	3	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) → 𝐴 ∈ ℝ* )
9		eqid	⊢ ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
10	9	limsupgle	⊢ ( ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ) ∧ 𝑘 ∈ ℝ ∧ 𝐴 ∈ ℝ* ) → ( ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑘 ) ≤ 𝐴 ↔ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 ) ) )
11	5 6 7 8 10	syl211anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) → ( ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑘 ) ≤ 𝐴 ↔ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 ) ) )
12		reex	⊢ ℝ ∈ V
13	12	ssex	⊢ ( 𝐵 ⊆ ℝ → 𝐵 ∈ V )
14	1 13	syl	⊢ ( 𝜑 → 𝐵 ∈ V )
15		xrex	⊢ ℝ* ∈ V
16	15	a1i	⊢ ( 𝜑 → ℝ* ∈ V )
17		fex2	⊢ ( ( 𝐹 : 𝐵 ⟶ ℝ* ∧ 𝐵 ∈ V ∧ ℝ* ∈ V ) → 𝐹 ∈ V )
18	2 14 16 17	syl3anc	⊢ ( 𝜑 → 𝐹 ∈ V )
19		limsupcl	⊢ ( 𝐹 ∈ V → ( lim sup ‘ 𝐹 ) ∈ ℝ* )
20	18 19	syl	⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ∈ ℝ* )
21	20	xrleidd	⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ≤ ( lim sup ‘ 𝐹 ) )
22	9	limsuple	⊢ ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ∧ ( lim sup ‘ 𝐹 ) ∈ ℝ* ) → ( ( lim sup ‘ 𝐹 ) ≤ ( lim sup ‘ 𝐹 ) ↔ ∀ 𝑘 ∈ ℝ ( lim sup ‘ 𝐹 ) ≤ ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑘 ) ) )
23	1 2 20 22	syl3anc	⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ≤ ( lim sup ‘ 𝐹 ) ↔ ∀ 𝑘 ∈ ℝ ( lim sup ‘ 𝐹 ) ≤ ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑘 ) ) )
24	21 23	mpbid	⊢ ( 𝜑 → ∀ 𝑘 ∈ ℝ ( lim sup ‘ 𝐹 ) ≤ ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑘 ) )
25	24	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) → ( lim sup ‘ 𝐹 ) ≤ ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑘 ) )
26	20	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) → ( lim sup ‘ 𝐹 ) ∈ ℝ* )
27	9	limsupgf	⊢ ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) : ℝ ⟶ ℝ*
28	27	a1i	⊢ ( 𝜑 → ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) : ℝ ⟶ ℝ* )
29	28	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) → ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑘 ) ∈ ℝ* )
30		xrletr	⊢ ( ( ( lim sup ‘ 𝐹 ) ∈ ℝ* ∧ ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑘 ) ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( ( ( lim sup ‘ 𝐹 ) ≤ ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑘 ) ∧ ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑘 ) ≤ 𝐴 ) → ( lim sup ‘ 𝐹 ) ≤ 𝐴 ) )
31	26 29 8 30	syl3anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) → ( ( ( lim sup ‘ 𝐹 ) ≤ ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑘 ) ∧ ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑘 ) ≤ 𝐴 ) → ( lim sup ‘ 𝐹 ) ≤ 𝐴 ) )
32	25 31	mpand	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) → ( ( ( 𝑛 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑘 ) ≤ 𝐴 → ( lim sup ‘ 𝐹 ) ≤ 𝐴 ) )
33	11 32	sylbird	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) → ( ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 ) → ( lim sup ‘ 𝐹 ) ≤ 𝐴 ) )
34	33	rexlimdva	⊢ ( 𝜑 → ( ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 ) → ( lim sup ‘ 𝐹 ) ≤ 𝐴 ) )
35	4 34	mpd	⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ≤ 𝐴 )