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	$⊢ φ \to M \in ℤ$
		climliminf.2	$⊢ Z = ℤ_{\geq M}$
		climliminf.3	$⊢ φ \to F : Z ⟶ ℝ$
	Assertion	climliminf	$⊢ φ \to (F \in dom ⇝ \leftrightarrow F ⇝ lim inf (F))$

Proof

Step	Hyp	Ref	Expression
1		climliminf.1	$⊢ φ \to M \in ℤ$
2		climliminf.2	$⊢ Z = ℤ_{\geq M}$
3		climliminf.3	$⊢ φ \to F : Z ⟶ ℝ$
4	1 2 3	climlimsup	$⊢ φ \to (F \in dom ⇝ \leftrightarrow F ⇝ lim sup (F))$
5	4	biimpd	$⊢ φ \to (F \in dom ⇝ \to F ⇝ lim sup (F))$
6	5	imp	$⊢ (φ \land F \in dom ⇝) \to F ⇝ lim sup (F)$
7	1	adantr	$⊢ (φ \land F \in dom ⇝) \to M \in ℤ$
8	3	adantr	$⊢ (φ \land F \in dom ⇝) \to F : Z ⟶ ℝ$
9		simpr	$⊢ (φ \land F \in dom ⇝) \to F \in dom ⇝$
10	7 2 8 9	climliminflimsupd	$⊢ (φ \land F \in dom ⇝) \to lim inf (F) = lim sup (F)$
11	6 10	breqtrrd	$⊢ (φ \land F \in dom ⇝) \to F ⇝ lim inf (F)$
12		climrel	$⊢ Rel ⇝$
13	12	releldmi	$⊢ F ⇝ lim inf (F) \to F \in dom ⇝$
14	13	adantl	$⊢ (φ \land F ⇝ lim inf (F)) \to F \in dom ⇝$
15	11 14	impbida	$⊢ φ \to (F \in dom ⇝ \leftrightarrow F ⇝ lim inf (F))$