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

Metamath Proof Explorer

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 ‘ 𝐹 ) ) )