Metamath Proof Explorer


Theorem limsup0

Description: The superior limit of the empty set (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Assertion limsup0 lim sup = −∞

Proof

Step Hyp Ref Expression
1 0ex V
2 eqid x sup x +∞ * * < = x sup x +∞ * * <
3 2 limsupval V lim sup = sup ran x sup x +∞ * * < * <
4 1 3 ax-mp lim sup = sup ran x sup x +∞ * * < * <
5 0ima x +∞ =
6 5 ineq1i x +∞ * = *
7 0in * =
8 6 7 eqtri x +∞ * =
9 8 supeq1i sup x +∞ * * < = sup * <
10 xrsup0 sup * < = −∞
11 9 10 eqtri sup x +∞ * * < = −∞
12 11 mpteq2i x sup x +∞ * * < = x −∞
13 ren0
14 13 a1i
15 12 14 rnmptc ran x sup x +∞ * * < = −∞
16 15 mptru ran x sup x +∞ * * < = −∞
17 16 infeq1i sup ran x sup x +∞ * * < * < = sup −∞ * <
18 xrltso < Or *
19 mnfxr −∞ *
20 infsn < Or * −∞ * sup −∞ * < = −∞
21 18 19 20 mp2an sup −∞ * < = −∞
22 4 17 21 3eqtri lim sup = −∞