Metamath Proof Explorer

Theorem liminfvaluz2

Description: Alternate definition of liminf for a real-valued function, defined on a set of upper integers. (Contributed by Glauco Siliprandi, 2-Jan-2022)

		Ref	Expression
	Hypotheses	liminfvaluz2.k	$⊢ Ⅎ k φ$
		liminfvaluz2.m	$⊢ φ \to M \in ℤ$
		liminfvaluz2.z	$⊢ Z = ℤ_{\geq M}$
		liminfvaluz2.b	$⊢ (φ \land k \in Z) \to B \in ℝ$
	Assertion	liminfvaluz2	$⊢ φ \to lim inf ((k \in Z ⟼ B)) = - lim sup ((k \in Z ⟼ - B))$

Proof

Step	Hyp	Ref	Expression
1		liminfvaluz2.k	$⊢ Ⅎ k φ$
2		liminfvaluz2.m	$⊢ φ \to M \in ℤ$
3		liminfvaluz2.z	$⊢ Z = ℤ_{\geq M}$
4		liminfvaluz2.b	$⊢ (φ \land k \in Z) \to B \in ℝ$
5	4	rexrd	$⊢ (φ \land k \in Z) \to B \in ℝ^{*}$
6	1 2 3 5	liminfvaluz	$⊢ φ \to lim inf ((k \in Z ⟼ B)) = - lim sup ((k \in Z ⟼ - B))$
7	4	rexnegd	$⊢ (φ \land k \in Z) \to - B = - B$
8	1 7	mpteq2da	$⊢ φ \to (k \in Z ⟼ - B) = (k \in Z ⟼ - B)$
9	8	fveq2d	$⊢ φ \to lim sup ((k \in Z ⟼ - B)) = lim sup ((k \in Z ⟼ - B))$
10	9	xnegeqd	$⊢ φ \to - lim sup ((k \in Z ⟼ - B)) = - lim sup ((k \in Z ⟼ - B))$
11	6 10	eqtrd	$⊢ φ \to lim inf ((k \in Z ⟼ B)) = - lim sup ((k \in Z ⟼ - B))$