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