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

Metamath Proof Explorer

Theorem nltmnf

Description: No extended real is less than minus infinity. (Contributed by NM, 15-Oct-2005)

Ref Expression
Assertion nltmnf ( 𝐴 ∈ ℝ* → ¬ 𝐴 < -∞ )

Proof

Step Hyp Ref Expression
1 mnfnre ⊢ -∞ ∉ ℝ
2 1 neli ⊢ ¬ -∞ ∈ ℝ
3 2 intnan ⊢ ¬ ( 𝐴 ∈ ℝ ∧ -∞ ∈ ℝ )
4 3 intnanr ⊢ ¬ ( ( 𝐴 ∈ ℝ ∧ -∞ ∈ ℝ ) ∧ 𝐴 <ℝ -∞ )
5 pnfnemnf ⊢ +∞ ≠ -∞
6 5 nesymi ⊢ ¬ -∞ = +∞
7 6 intnan ⊢ ¬ ( 𝐴 = -∞ ∧ -∞ = +∞ )
8 4 7 pm3.2ni ⊢ ¬ ( ( ( 𝐴 ∈ ℝ ∧ -∞ ∈ ℝ ) ∧ 𝐴 <ℝ -∞ ) ∨ ( 𝐴 = -∞ ∧ -∞ = +∞ ) )
9 6 intnan ⊢ ¬ ( 𝐴 ∈ ℝ ∧ -∞ = +∞ )
10 2 intnan ⊢ ¬ ( 𝐴 = -∞ ∧ -∞ ∈ ℝ )
11 9 10 pm3.2ni ⊢ ¬ ( ( 𝐴 ∈ ℝ ∧ -∞ = +∞ ) ∨ ( 𝐴 = -∞ ∧ -∞ ∈ ℝ ) )
12 8 11 pm3.2ni ⊢ ¬ ( ( ( ( 𝐴 ∈ ℝ ∧ -∞ ∈ ℝ ) ∧ 𝐴 <ℝ -∞ ) ∨ ( 𝐴 = -∞ ∧ -∞ = +∞ ) ) ∨ ( ( 𝐴 ∈ ℝ ∧ -∞ = +∞ ) ∨ ( 𝐴 = -∞ ∧ -∞ ∈ ℝ ) ) )
13 mnfxr ⊢ -∞ ∈ ℝ*
14 ltxr ⊢ ( ( 𝐴 ∈ ℝ* ∧ -∞ ∈ ℝ* ) → ( 𝐴 < -∞ ↔ ( ( ( ( 𝐴 ∈ ℝ ∧ -∞ ∈ ℝ ) ∧ 𝐴 <ℝ -∞ ) ∨ ( 𝐴 = -∞ ∧ -∞ = +∞ ) ) ∨ ( ( 𝐴 ∈ ℝ ∧ -∞ = +∞ ) ∨ ( 𝐴 = -∞ ∧ -∞ ∈ ℝ ) ) ) ) )
15 13 14 mpan2 ⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 < -∞ ↔ ( ( ( ( 𝐴 ∈ ℝ ∧ -∞ ∈ ℝ ) ∧ 𝐴 <ℝ -∞ ) ∨ ( 𝐴 = -∞ ∧ -∞ = +∞ ) ) ∨ ( ( 𝐴 ∈ ℝ ∧ -∞ = +∞ ) ∨ ( 𝐴 = -∞ ∧ -∞ ∈ ℝ ) ) ) ) )
16 12 15 mtbiri ⊢ ( 𝐴 ∈ ℝ* → ¬ 𝐴 < -∞ )