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

Metamath Proof Explorer

Theorem nn0nepnf

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

		Ref	Expression
	Assertion	nn0nepnf	$⊢ A \in ℕ_{0} \to A \neq +∞$

Step	Hyp	Ref	Expression
1		pnfnre	$⊢ +∞ \notin ℝ$
2	1	neli	$⊢ \neg +∞ \in ℝ$
3		nn0re	$⊢ +∞ \in ℕ_{0} \to +∞ \in ℝ$
4	2 3	mto	$⊢ \neg +∞ \in ℕ_{0}$
5		eleq1	$⊢ A = +∞ \to (A \in ℕ_{0} \leftrightarrow +∞ \in ℕ_{0})$
6	4 5	mtbiri	$⊢ A = +∞ \to \neg A \in ℕ_{0}$
7	6	necon2ai	$⊢ A \in ℕ_{0} \to A \neq +∞$