limsupval4

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

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

Proof

Step	Hyp	Ref	Expression
1		limsupval4.x	$⊢ Ⅎ x φ$
2		limsupval4.a	$⊢ φ \to A \in V$
3		limsupval4.m	$⊢ φ \to M \in ℝ$
4		limsupval4.b	$⊢ (φ \land x \in (A \cap [M, +∞))) \to B \in ℝ^{*}$
5		ovex	$⊢ [M, +∞) \in V$
6	5	inex2	$⊢ A \cap [M, +∞) \in V$
7	6	mptex	$⊢ (x \in (A \cap [M, +∞)) ⟼ B) \in V$
8		limsupcl	$⊢ (x \in (A \cap [M, +∞)) ⟼ B) \in V \to lim sup ((x \in (A \cap [M, +∞)) ⟼ B)) \in ℝ^{*}$
9	7 8	ax-mp	$⊢ lim sup ((x \in (A \cap [M, +∞)) ⟼ B)) \in ℝ^{*}$
10	9	a1i	$⊢ φ \to lim sup ((x \in (A \cap [M, +∞)) ⟼ B)) \in ℝ^{*}$
11	10	xnegnegd	$⊢ φ \to - (- lim sup ((x \in (A \cap [M, +∞)) ⟼ B))) = lim sup ((x \in (A \cap [M, +∞)) ⟼ B))$
12	11	eqcomd	$⊢ φ \to lim sup ((x \in (A \cap [M, +∞)) ⟼ B)) = - (- lim sup ((x \in (A \cap [M, +∞)) ⟼ B)))$
13		eqid	$⊢ [M, +∞) = [M, +∞)$
14	2 3 13	limsupresicompt	$⊢ φ \to lim sup ((x \in A ⟼ B)) = lim sup ((x \in (A \cap [M, +∞)) ⟼ B))$
15	4	xnegcld	$⊢ (φ \land x \in (A \cap [M, +∞))) \to - B \in ℝ^{*}$
16	1 2 3 15	liminfval3	$⊢ φ \to lim inf ((x \in A ⟼ - B)) = - lim sup ((x \in A ⟼ - (- B)))$
17	2 3 13	limsupresicompt	$⊢ φ \to lim sup ((x \in A ⟼ - (- B))) = lim sup ((x \in (A \cap [M, +∞)) ⟼ - (- B)))$
18	4	xnegnegd	$⊢ (φ \land x \in (A \cap [M, +∞))) \to - (- B) = B$
19	1 18	mpteq2da	$⊢ φ \to (x \in (A \cap [M, +∞)) ⟼ - (- B)) = (x \in (A \cap [M, +∞)) ⟼ B)$
20	19	fveq2d	$⊢ φ \to lim sup ((x \in (A \cap [M, +∞)) ⟼ - (- B))) = lim sup ((x \in (A \cap [M, +∞)) ⟼ B))$
21	17 20	eqtrd	$⊢ φ \to lim sup ((x \in A ⟼ - (- B))) = lim sup ((x \in (A \cap [M, +∞)) ⟼ B))$
22	21	xnegeqd	$⊢ φ \to - lim sup ((x \in A ⟼ - (- B))) = - lim sup ((x \in (A \cap [M, +∞)) ⟼ B))$
23	16 22	eqtrd	$⊢ φ \to lim inf ((x \in A ⟼ - B)) = - lim sup ((x \in (A \cap [M, +∞)) ⟼ B))$
24	23	xnegeqd	$⊢ φ \to - lim inf ((x \in A ⟼ - B)) = - (- lim sup ((x \in (A \cap [M, +∞)) ⟼ B)))$
25	12 14 24	3eqtr4d	$⊢ φ \to lim sup ((x \in A ⟼ B)) = - lim inf ((x \in A ⟼ - B))$

Metamath Proof Explorer

Theorem limsupval4

Proof