Metamath Proof Explorer

Theorem liminfval3

Description: Alternate definition of liminf when the given function is eventually extended real-valued. (Contributed by Glauco Siliprandi, 2-Jan-2022)

		Ref	Expression
	Hypotheses	liminfval3.x	$⊢ Ⅎ x φ$
		liminfval3.a	$⊢ φ \to A \in V$
		liminfval3.m	$⊢ φ \to M \in ℝ$
		liminfval3.b	$⊢ (φ \land x \in (A \cap [M, +∞))) \to B \in ℝ^{*}$
	Assertion	liminfval3	$⊢ φ \to lim inf ((x \in A ⟼ B)) = - lim sup ((x \in A ⟼ - B))$

Proof

Step	Hyp	Ref	Expression
1		liminfval3.x	$⊢ Ⅎ x φ$
2		liminfval3.a	$⊢ φ \to A \in V$
3		liminfval3.m	$⊢ φ \to M \in ℝ$
4		liminfval3.b	$⊢ (φ \land x \in (A \cap [M, +∞))) \to B \in ℝ^{*}$
5		inss1	$⊢ A \cap [M, +∞) \subseteq A$
6	5	a1i	$⊢ φ \to A \cap [M, +∞) \subseteq A$
7	2 6	ssexd	$⊢ φ \to A \cap [M, +∞) \in V$
8	1 7 4	liminfvalxrmpt	$⊢ φ \to lim inf ((x \in (A \cap [M, +∞)) ⟼ B)) = - lim sup ((x \in (A \cap [M, +∞)) ⟼ - B))$
9		eqid	$⊢ [M, +∞) = [M, +∞)$
10	3 9 2	liminfresicompt	$⊢ φ \to lim inf ((x \in (A \cap [M, +∞)) ⟼ B)) = lim inf ((x \in A ⟼ B))$
11	10	eqcomd	$⊢ φ \to lim inf ((x \in A ⟼ B)) = lim inf ((x \in (A \cap [M, +∞)) ⟼ B))$
12	2 3 9	limsupresicompt	$⊢ φ \to lim sup ((x \in A ⟼ - B)) = lim sup ((x \in (A \cap [M, +∞)) ⟼ - B))$
13	12	xnegeqd	$⊢ φ \to - lim sup ((x \in A ⟼ - B)) = - lim sup ((x \in (A \cap [M, +∞)) ⟼ - B))$
14	8 11 13	3eqtr4d	$⊢ φ \to lim inf ((x \in A ⟼ B)) = - lim sup ((x \in A ⟼ - B))$