Metamath Proof Explorer

Theorem liminf0

Description: The inferior limit of the empty set. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Assertion liminf0 ⊢lim inf⁡∅=+∞

Proof

Step Hyp Ref Expression
1 nftru ⊢Ⅎx⊤
2 0ex ⊢∅∈V
3 2 a1i ⊢⊤→∅∈V
4 0red ⊢⊤→0∈ℝ
5 noel ⊢¬x∈∅
6 elinel1 ⊢x∈∅∩0+∞→x∈∅
7 6 con3i ⊢¬x∈∅→¬x∈∅∩0+∞
8 5 7 ax-mp ⊢¬x∈∅∩0+∞
9 pm2.21 ⊢¬x∈∅∩0+∞→x∈∅∩0+∞→∅⁡x∈ℝ*
10 8 9 ax-mp ⊢x∈∅∩0+∞→∅⁡x∈ℝ*
11 10 adantl ⊢⊤∧x∈∅∩0+∞→∅⁡x∈ℝ*
12 1 3 4 11 liminfval3 ⊢⊤→lim inf⁡x∈∅⟼∅⁡x=−lim sup⁡x∈∅⟼−∅⁡x
13 12 mptru ⊢lim inf⁡x∈∅⟼∅⁡x=−lim sup⁡x∈∅⟼−∅⁡x
14 mpt0 ⊢x∈∅⟼∅⁡x=∅
15 14 fveq2i ⊢lim inf⁡x∈∅⟼∅⁡x=lim inf⁡∅
16 mpt0 ⊢x∈∅⟼−∅⁡x=∅
17 16 fveq2i ⊢lim sup⁡x∈∅⟼−∅⁡x=lim sup⁡∅
18 limsup0 ⊢lim sup⁡∅=−∞
19 17 18 eqtri ⊢lim sup⁡x∈∅⟼−∅⁡x=−∞
20 19 xnegeqi ⊢−lim sup⁡x∈∅⟼−∅⁡x=−−∞
21 xnegmnf ⊢−−∞=+∞
22 20 21 eqtri ⊢−lim sup⁡x∈∅⟼−∅⁡x=+∞
23 13 15 22 3eqtr3i ⊢lim inf⁡∅=+∞