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