Metamath Proof Explorer

Theorem liminfvaluz

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

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

Proof

Step	Hyp	Ref	Expression
1		liminfvaluz.k	$⊢ Ⅎ k φ$
2		liminfvaluz.m	$⊢ φ \to M \in ℤ$
3		liminfvaluz.z	$⊢ Z = ℤ_{\geq M}$
4		liminfvaluz.b	$⊢ (φ \land k \in Z) \to B \in ℝ^{*}$
5	3	fvexi	$⊢ Z \in V$
6	5	a1i	$⊢ φ \to Z \in V$
7	2	zred	$⊢ φ \to M \in ℝ$
8		simpr	$⊢ (φ \land k \in (Z \cap [M, +∞))) \to k \in (Z \cap [M, +∞))$
9	2 3	uzinico3	$⊢ φ \to Z = Z \cap [M, +∞)$
10	9	eqcomd	$⊢ φ \to Z \cap [M, +∞) = Z$
11	10	adantr	$⊢ (φ \land k \in (Z \cap [M, +∞))) \to Z \cap [M, +∞) = Z$
12	8 11	eleqtrd	$⊢ (φ \land k \in (Z \cap [M, +∞))) \to k \in Z$
13	12 4	syldan	$⊢ (φ \land k \in (Z \cap [M, +∞))) \to B \in ℝ^{*}$
14	1 6 7 13	liminfval3	$⊢ φ \to lim inf ((k \in Z ⟼ B)) = - lim sup ((k \in Z ⟼ - B))$