This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ Ⅎ 𝑥 ⊤
2 0ex ⊢ ∅ ∈ V
3 2 a1i ⊢ ( ⊤ → ∅ ∈ V )
4 0red ⊢ ( ⊤ → 0 ∈ ℝ )
5 noel ⊢ ¬ 𝑥 ∈ ∅
6 elinel1 ⊢ ( 𝑥 ∈ ( ∅ ∩ ( 0 [,) +∞ ) ) → 𝑥 ∈ ∅ )
7 6 con3i ⊢ ( ¬ 𝑥 ∈ ∅ → ¬ 𝑥 ∈ ( ∅ ∩ ( 0 [,) +∞ ) ) )
8 5 7 ax-mp ⊢ ¬ 𝑥 ∈ ( ∅ ∩ ( 0 [,) +∞ ) )
9 pm2.21 ⊢ ( ¬ 𝑥 ∈ ( ∅ ∩ ( 0 [,) +∞ ) ) → ( 𝑥 ∈ ( ∅ ∩ ( 0 [,) +∞ ) ) → ( ∅ ‘ 𝑥 ) ∈ ℝ* ) )
10 8 9 ax-mp ⊢ ( 𝑥 ∈ ( ∅ ∩ ( 0 [,) +∞ ) ) → ( ∅ ‘ 𝑥 ) ∈ ℝ* )
11 10 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( ∅ ∩ ( 0 [,) +∞ ) ) ) → ( ∅ ‘ 𝑥 ) ∈ ℝ* )
12 1 3 4 11 liminfval3 ⊢ ( ⊤ → ( lim inf ‘ ( 𝑥 ∈ ∅ ↦ ( ∅ ‘ 𝑥 ) ) ) = -𝑒 ( lim sup ‘ ( 𝑥 ∈ ∅ ↦ -𝑒 ( ∅ ‘ 𝑥 ) ) ) )
13 12 mptru ⊢ ( lim inf ‘ ( 𝑥 ∈ ∅ ↦ ( ∅ ‘ 𝑥 ) ) ) = -𝑒 ( lim sup ‘ ( 𝑥 ∈ ∅ ↦ -𝑒 ( ∅ ‘ 𝑥 ) ) )
14 mpt0 ⊢ ( 𝑥 ∈ ∅ ↦ ( ∅ ‘ 𝑥 ) ) = ∅
15 14 fveq2i ⊢ ( lim inf ‘ ( 𝑥 ∈ ∅ ↦ ( ∅ ‘ 𝑥 ) ) ) = ( lim inf ‘ ∅ )
16 mpt0 ⊢ ( 𝑥 ∈ ∅ ↦ -𝑒 ( ∅ ‘ 𝑥 ) ) = ∅
17 16 fveq2i ⊢ ( lim sup ‘ ( 𝑥 ∈ ∅ ↦ -𝑒 ( ∅ ‘ 𝑥 ) ) ) = ( lim sup ‘ ∅ )
18 limsup0 ⊢ ( lim sup ‘ ∅ ) = -∞
19 17 18 eqtri ⊢ ( lim sup ‘ ( 𝑥 ∈ ∅ ↦ -𝑒 ( ∅ ‘ 𝑥 ) ) ) = -∞
20 19 xnegeqi ⊢ -𝑒 ( lim sup ‘ ( 𝑥 ∈ ∅ ↦ -𝑒 ( ∅ ‘ 𝑥 ) ) ) = -𝑒 -∞
21 xnegmnf ⊢ -𝑒 -∞ = +∞
22 20 21 eqtri ⊢ -𝑒 ( lim sup ‘ ( 𝑥 ∈ ∅ ↦ -𝑒 ( ∅ ‘ 𝑥 ) ) ) = +∞
23 13 15 22 3eqtr3i ⊢ ( lim inf ‘ ∅ ) = +∞