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

Metamath Proof Explorer

Theorem xnn0nnn0pnf

Description: An extended nonnegative integer which is not a standard nonnegative integer is positive infinity. (Contributed by AV, 10-Dec-2020)

		Ref	Expression
	Assertion	xnn0nnn0pnf	$⊢ (N \in ℕ_{0}^{*} \land \neg N \in ℕ_{0}) \to N = +∞$

Step	Hyp	Ref	Expression
1		elxnn0	$⊢ N \in ℕ_{0}^{*} \leftrightarrow (N \in ℕ_{0} \lor N = +∞)$
2		pm2.53	$⊢ (N \in ℕ_{0} \lor N = +∞) \to (\neg N \in ℕ_{0} \to N = +∞)$
3	1 2	sylbi	$⊢ N \in ℕ_{0}^{*} \to (\neg N \in ℕ_{0} \to N = +∞)$
4	3	imp	$⊢ (N \in ℕ_{0}^{*} \land \neg N \in ℕ_{0}) \to N = +∞$