Theorem nngt0

Description: A positive integer is positive. (Contributed by NM, 26-Sep-1999)

	Ref	Expression
Assertion	nngt0	$$⊢A\in \mathbb{N}\to 0<A$$

Proof

Step	Hyp	Ref	Expression
1		nnre	$$⊢A\in \mathbb{N}\to A\in ℝ$$
2		nnge1	$$⊢A\in \mathbb{N}\to 1\le A$$
3		0lt1	$$⊢0<1$$
4		0re	$$⊢0\in ℝ$$
5		1re	$$⊢1\in ℝ$$
6		ltletr	$$⊢\left(0\in ℝ\wedge 1\in ℝ\wedge A\in ℝ\right)\to \left(\left(0<1\wedge 1\le A\right)\to 0<A\right)$$
7	4 5 6	mp3an12	$$⊢A\in ℝ\to \left(\left(0<1\wedge 1\le A\right)\to 0<A\right)$$
8	3 7	mpani	$$⊢A\in ℝ\to \left(1\le A\to 0<A\right)$$
9	1 2 8	sylc	$$⊢A\in \mathbb{N}\to 0<A$$