# Metamath Proof Explorer

## Theorem 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}\phantom{\rule{.4em}{0ex}}{\phi }$
limsupval4.a ${⊢}{\phi }\to {A}\in {V}$
limsupval4.m ${⊢}{\phi }\to {M}\in ℝ$
limsupval4.b ${⊢}\left({\phi }\wedge {x}\in \left({A}\cap \left[{M},\mathrm{+\infty }\right)\right)\right)\to {B}\in {ℝ}^{*}$
Assertion limsupval4 ${⊢}{\phi }\to \mathrm{lim sup}\left(\left({x}\in {A}⟼{B}\right)\right)=-\mathrm{lim inf}\left(\left({x}\in {A}⟼-{B}\right)\right)$

### Proof

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