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

Metamath Proof Explorer

Theorem climliminf

Description: A sequence of real numbers converges if and only if it converges to its inferior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses climliminf.1 ⊢ φ → M ∈ ℤ
climliminf.2 ⊢ Z = ℤ ≥ M
climliminf.3 ⊢ φ → F : Z ⟶ ℝ
Assertion climliminf ⊢ φ → F ∈ dom ⁡ ⇝ ↔ F ⇝ lim inf ⁡ F

Proof

Step Hyp Ref Expression
1 climliminf.1 ⊢ φ → M ∈ ℤ
2 climliminf.2 ⊢ Z = ℤ ≥ M
3 climliminf.3 ⊢ φ → F : Z ⟶ ℝ
4 1 2 3 climlimsup ⊢ φ → F ∈ dom ⁡ ⇝ ↔ F ⇝ lim sup ⁡ F
5 4 biimpd ⊢ φ → F ∈ dom ⁡ ⇝ → F ⇝ lim sup ⁡ F
6 5 imp ⊢ φ ∧ F ∈ dom ⁡ ⇝ → F ⇝ lim sup ⁡ F
7 1 adantr ⊢ φ ∧ F ∈ dom ⁡ ⇝ → M ∈ ℤ
8 3 adantr ⊢ φ ∧ F ∈ dom ⁡ ⇝ → F : Z ⟶ ℝ
9 simpr ⊢ φ ∧ F ∈ dom ⁡ ⇝ → F ∈ dom ⁡ ⇝
10 7 2 8 9 climliminflimsupd ⊢ φ ∧ F ∈ dom ⁡ ⇝ → lim inf ⁡ F = lim sup ⁡ F
11 6 10 breqtrrd ⊢ φ ∧ F ∈ dom ⁡ ⇝ → F ⇝ lim inf ⁡ F
12 climrel ⊢ Rel ⁡ ⇝
13 12 releldmi ⊢ F ⇝ lim inf ⁡ F → F ∈ dom ⁡ ⇝
14 13 adantl ⊢ φ ∧ F ⇝ lim inf ⁡ F → F ∈ dom ⁡ ⇝
15 11 14 impbida ⊢ φ → F ∈ dom ⁡ ⇝ ↔ F ⇝ lim inf ⁡ F