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

Proof

Step	Hyp	Ref	Expression
1		climlimsup.1	$⊢ φ \to M \in ℤ$
2		climlimsup.2	$⊢ Z = ℤ_{\geq M}$
3		climlimsup.3	$⊢ φ \to F : Z ⟶ ℝ$
4	3	adantr	$⊢ (φ \land F \in dom ⇝) \to F : Z ⟶ ℝ$
5	1	adantr	$⊢ (φ \land F \in dom ⇝) \to M \in ℤ$
6		simpr	$⊢ (φ \land F \in dom ⇝) \to F \in dom ⇝$
7	2	climcau	$⊢ (M \in ℤ \land F \in dom ⇝) \to \forall x \in ℝ^{+} \exists m \in Z \forall k \in ℤ_{\geq m} \|F (k) - F (m)\| < x$
8	5 6 7	syl2anc	$⊢ (φ \land F \in dom ⇝) \to \forall x \in ℝ^{+} \exists m \in Z \forall k \in ℤ_{\geq m} \|F (k) - F (m)\| < x$
9	2 4 8	caurcvg	$⊢ (φ \land F \in dom ⇝) \to F ⇝ lim sup (F)$
10		climrel	$⊢ Rel ⇝$
11		releldm	$⊢ (Rel ⇝ \land F ⇝ lim sup (F)) \to F \in dom ⇝$
12	10 11	mpan	$⊢ F ⇝ lim sup (F) \to F \in dom ⇝$
13	12	adantl	$⊢ (φ \land F ⇝ lim sup (F)) \to F \in dom ⇝$
14	9 13	impbida	$⊢ φ \to (F \in dom ⇝ \leftrightarrow F ⇝ lim sup (F))$