liminfval4

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

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

Proof

Step	Hyp	Ref	Expression
1		liminfval4.x	$⊢ Ⅎ x φ$
2		liminfval4.a	$⊢ φ \to A \in V$
3		liminfval4.m	$⊢ φ \to M \in ℝ$
4		liminfval4.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	4	rexrd	$⊢ (φ \land x \in (A \cap [M, +∞))) \to B \in ℝ^{*}$
9	1 7 8	liminfvalxrmpt	$⊢ φ \to lim inf ((x \in (A \cap [M, +∞)) ⟼ B)) = - lim sup ((x \in (A \cap [M, +∞)) ⟼ - B))$
10	4	rexnegd	$⊢ (φ \land x \in (A \cap [M, +∞))) \to - B = - B$
11	1 10	mpteq2da	$⊢ φ \to (x \in (A \cap [M, +∞)) ⟼ - B) = (x \in (A \cap [M, +∞)) ⟼ - B)$
12	11	fveq2d	$⊢ φ \to lim sup ((x \in (A \cap [M, +∞)) ⟼ - B)) = lim sup ((x \in (A \cap [M, +∞)) ⟼ - B))$
13	12	xnegeqd	$⊢ φ \to - lim sup ((x \in (A \cap [M, +∞)) ⟼ - B)) = - lim sup ((x \in (A \cap [M, +∞)) ⟼ - B))$
14	9 13	eqtrd	$⊢ φ \to lim inf ((x \in (A \cap [M, +∞)) ⟼ B)) = - lim sup ((x \in (A \cap [M, +∞)) ⟼ - B))$
15		eqid	$⊢ [M, +∞) = [M, +∞)$
16	3 15 2	liminfresicompt	$⊢ φ \to lim inf ((x \in (A \cap [M, +∞)) ⟼ B)) = lim inf ((x \in A ⟼ B))$
17	16	eqcomd	$⊢ φ \to lim inf ((x \in A ⟼ B)) = lim inf ((x \in (A \cap [M, +∞)) ⟼ B))$
18	2 3 15	limsupresicompt	$⊢ φ \to lim sup ((x \in A ⟼ - B)) = lim sup ((x \in (A \cap [M, +∞)) ⟼ - B))$
19	18	xnegeqd	$⊢ φ \to - lim sup ((x \in A ⟼ - B)) = - lim sup ((x \in (A \cap [M, +∞)) ⟼ - B))$
20	14 17 19	3eqtr4d	$⊢ φ \to lim inf ((x \in A ⟼ B)) = - lim sup ((x \in A ⟼ - B))$

Metamath Proof Explorer

Theorem liminfval4

Proof