Theorem climlimsup

Description: A sequence of real numbers converges if and only if it converges to its superior limit. The first hypothesis is needed (see climlimsupcex for a counterexample). (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	climlimsup.1	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	climlimsup.2	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	climlimsup.3	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
Assertion	climlimsup	⊢ ( 𝜑 → ( 𝐹 ∈ dom ⇝ ↔ 𝐹 ⇝ ( lim sup ‘ 𝐹 ) ) )

Proof

Step	Hyp	Ref	Expression
1		climlimsup.1	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2		climlimsup.2	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3		climlimsup.3	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
4	3	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐹 : 𝑍 ⟶ ℝ )
5	1	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝑀 ∈ ℤ )
6		simpr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐹 ∈ dom ⇝ )
7	2	climcau	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑚 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 )
8	5 6 7	syl2anc	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑚 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑚 ) ) ) < 𝑥 )
9	2 4 8	caurcvg	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐹 ⇝ ( lim sup ‘ 𝐹 ) )
10		climrel	⊢ Rel ⇝
11		releldm	⊢ ( ( Rel ⇝ ∧ 𝐹 ⇝ ( lim sup ‘ 𝐹 ) ) → 𝐹 ∈ dom ⇝ )
12	10 11	mpan	⊢ ( 𝐹 ⇝ ( lim sup ‘ 𝐹 ) → 𝐹 ∈ dom ⇝ )
13	12	adantl	⊢ ( ( 𝜑 ∧ 𝐹 ⇝ ( lim sup ‘ 𝐹 ) ) → 𝐹 ∈ dom ⇝ )
14	9 13	impbida	⊢ ( 𝜑 → ( 𝐹 ∈ dom ⇝ ↔ 𝐹 ⇝ ( lim sup ‘ 𝐹 ) ) )