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 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
climliminf.2 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
climliminf.3 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
Assertion climliminf ( 𝜑 → ( 𝐹 ∈ dom ⇝ ↔ 𝐹 ⇝ ( lim inf ‘ 𝐹 ) ) )

Proof

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