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	⊢ ( 𝐴 ∈ ℝ* → ¬ 𝐴 < -∞ )