xnn0gt0

Description: Nonzero extended nonnegative integers are strictly greater than zero. (Contributed by Thierry Arnoux, 30-Jul-2023)

		Ref	Expression
	Assertion	xnn0gt0	$⊢ (N \in ℕ_{0}^{*} \land N \neq 0) \to 0 < N$

Step	Hyp	Ref	Expression
1		elxnn0	$⊢ N \in ℕ_{0}^{*} \leftrightarrow (N \in ℕ_{0} \lor N = +∞)$
2		elnnne0	$⊢ N \in ℕ \leftrightarrow (N \in ℕ_{0} \land N \neq 0)$
3		nngt0	$⊢ N \in ℕ \to 0 < N$
4	2 3	sylbir	$⊢ (N \in ℕ_{0} \land N \neq 0) \to 0 < N$
5	4	ancoms	$⊢ (N \neq 0 \land N \in ℕ_{0}) \to 0 < N$
6	5	adantll	$⊢ (((N \in ℕ_{0} \lor N = +∞) \land N \neq 0) \land N \in ℕ_{0}) \to 0 < N$
7		0ltpnf	$⊢ 0 < +∞$
8		breq2	$⊢ N = +∞ \to (0 < N \leftrightarrow 0 < +∞)$
9	7 8	mpbiri	$⊢ N = +∞ \to 0 < N$
10	9	adantl	$⊢ (((N \in ℕ_{0} \lor N = +∞) \land N \neq 0) \land N = +∞) \to 0 < N$
11		simpl	$⊢ ((N \in ℕ_{0} \lor N = +∞) \land N \neq 0) \to (N \in ℕ_{0} \lor N = +∞)$
12	6 10 11	mpjaodan	$⊢ ((N \in ℕ_{0} \lor N = +∞) \land N \neq 0) \to 0 < N$
13	1 12	sylanb	$⊢ (N \in ℕ_{0}^{*} \land N \neq 0) \to 0 < N$

Metamath Proof Explorer