xnn0nemnf

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

		Ref	Expression
	Assertion	xnn0nemnf	$⊢ A \in ℕ_{0}^{*} \to A \neq −∞$

Step	Hyp	Ref	Expression
1		elxnn0	$⊢ A \in ℕ_{0}^{*} \leftrightarrow (A \in ℕ_{0} \lor A = +∞)$
2		nn0re	$⊢ A \in ℕ_{0} \to A \in ℝ$
3	2	renemnfd	$⊢ A \in ℕ_{0} \to A \neq −∞$
4		pnfnemnf	$⊢ +∞ \neq −∞$
5		neeq1	$⊢ A = +∞ \to (A \neq −∞ \leftrightarrow +∞ \neq −∞)$
6	4 5	mpbiri	$⊢ A = +∞ \to A \neq −∞$
7	3 6	jaoi	$⊢ (A \in ℕ_{0} \lor A = +∞) \to A \neq −∞$
8	1 7	sylbi	$⊢ A \in ℕ_{0}^{*} \to A \neq −∞$

Metamath Proof Explorer