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 ⊢ φ → M ∈ ℤ
climlimsup.2 ⊢ Z = ℤ ≥ M
climlimsup.3 ⊢ φ → F : Z ⟶ ℝ
Assertion climlimsup ⊢ φ → F ∈ dom ⁡ ⇝ ↔ F ⇝ lim sup ⁡ F

Proof

Step Hyp Ref Expression
1 climlimsup.1 ⊢ φ → M ∈ ℤ
2 climlimsup.2 ⊢ Z = ℤ ≥ M
3 climlimsup.3 ⊢ φ → F : Z ⟶ ℝ
4 3 adantr ⊢ φ ∧ F ∈ dom ⁡ ⇝ → F : Z ⟶ ℝ
5 1 adantr ⊢ φ ∧ F ∈ dom ⁡ ⇝ → M ∈ ℤ
6 simpr ⊢ φ ∧ F ∈ dom ⁡ ⇝ → F ∈ dom ⁡ ⇝
7 2 climcau ⊢ M ∈ ℤ ∧ F ∈ dom ⁡ ⇝ → ∀ x ∈ ℝ + ∃ m ∈ Z ∀ k ∈ ℤ ≥ m F ⁡ k − F ⁡ m < x
8 5 6 7 syl2anc ⊢ φ ∧ F ∈ dom ⁡ ⇝ → ∀ x ∈ ℝ + ∃ m ∈ Z ∀ k ∈ ℤ ≥ m F ⁡ k − F ⁡ m < x
9 2 4 8 caurcvg ⊢ φ ∧ F ∈ dom ⁡ ⇝ → F ⇝ lim sup ⁡ F
10 climrel ⊢ Rel ⁡ ⇝
11 releldm ⊢ Rel ⁡ ⇝ ∧ F ⇝ lim sup ⁡ F → F ∈ dom ⁡ ⇝
12 10 11 mpan ⊢ F ⇝ lim sup ⁡ F → F ∈ dom ⁡ ⇝
13 12 adantl ⊢ φ ∧ F ⇝ lim sup ⁡ F → F ∈ dom ⁡ ⇝
14 9 13 impbida ⊢ φ → F ∈ dom ⁡ ⇝ ↔ F ⇝ lim sup ⁡ F