Theorem xnn0nemnf

Description: No extended nonnegative integer equals negative infinity. (Contributed by AV, 10-Dec-2020)

	Ref	Expression
Assertion	xnn0nemnf	⊢ ( 𝐴 ∈ ℕ0* → 𝐴 ≠ -∞ )

Proof

Step	Hyp	Ref	Expression
1		elxnn0	⊢ ( 𝐴 ∈ ℕ0* ↔ ( 𝐴 ∈ ℕ0 ∨ 𝐴 = +∞ ) )
2		nn0re	⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℝ )
3	2	renemnfd	⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ≠ -∞ )
4		pnfnemnf	⊢ +∞ ≠ -∞
5		neeq1	⊢ ( 𝐴 = +∞ → ( 𝐴 ≠ -∞ ↔ +∞ ≠ -∞ ) )
6	4 5	mpbiri	⊢ ( 𝐴 = +∞ → 𝐴 ≠ -∞ )
7	3 6	jaoi	⊢ ( ( 𝐴 ∈ ℕ0 ∨ 𝐴 = +∞ ) → 𝐴 ≠ -∞ )
8	1 7	sylbi	⊢ ( 𝐴 ∈ ℕ0* → 𝐴 ≠ -∞ )