Metamath Proof Explorer

Theorem limsupvaluz4

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	limsupvaluz4.k	$⊢ Ⅎ k φ$
		limsupvaluz4.m	$⊢ φ \to M \in ℤ$
		limsupvaluz4.z	$⊢ Z = ℤ_{\geq M}$
		limsupvaluz4.b	$⊢ (φ \land k \in Z) \to B \in ℝ$
	Assertion	limsupvaluz4	$⊢ φ \to lim sup ((k \in Z ⟼ B)) = - lim inf ((k \in Z ⟼ - B))$

Proof

Step	Hyp	Ref	Expression
1		limsupvaluz4.k	$⊢ Ⅎ k φ$
2		limsupvaluz4.m	$⊢ φ \to M \in ℤ$
3		limsupvaluz4.z	$⊢ Z = ℤ_{\geq M}$
4		limsupvaluz4.b	$⊢ (φ \land k \in Z) \to B \in ℝ$
5	4	rexrd	$⊢ (φ \land k \in Z) \to B \in ℝ^{*}$
6	1 2 3 5	limsupvaluz3	$⊢ φ \to lim sup ((k \in Z ⟼ B)) = - lim inf ((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 inf ((k \in Z ⟼ - B)) = lim inf ((k \in Z ⟼ - B))$
10	9	xnegeqd	$⊢ φ \to - lim inf ((k \in Z ⟼ - B)) = - lim inf ((k \in Z ⟼ - B))$
11	6 10	eqtrd	$⊢ φ \to lim sup ((k \in Z ⟼ B)) = - lim inf ((k \in Z ⟼ - B))$