Theorem nnsgt0

Description: A positive integer is greater than zero. (Contributed by Scott Fenton, 15-Apr-2025)

	Ref	Expression
Assertion	nnsgt0	$$⊢A\in {\mathbb{N}}_s\to 0_s{<}_{s}A$$

Proof

Step	Hyp	Ref	Expression
1		nnssn0s	$$⊢{\mathbb{N}}_s\subseteq {\mathbb{N}}_{\mathrm{0s}}$$
2	1	sseli	$$⊢A\in {\mathbb{N}}_s\to A\in {\mathbb{N}}_{\mathrm{0s}}$$
3		n0sge0	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to 0_s{\le }_{s}A$$
4	2 3	syl	$$⊢A\in {\mathbb{N}}_s\to 0_s{\le }_{s}A$$
5		nnne0s	$$⊢A\in {\mathbb{N}}_s\to A\ne 0_s$$
6		0no	$$⊢0_s\in \mathrm{No}$$
7	6	a1i	$$⊢A\in {\mathbb{N}}_s\to 0_s\in \mathrm{No}$$
8		nnno	$$⊢A\in {\mathbb{N}}_s\to A\in \mathrm{No}$$
9	7 8	ltlesnd	$$⊢A\in {\mathbb{N}}_s\to \left(0_s{<}_{s}A\leftrightarrow \left(0_s{\le }_{s}A\wedge A\ne 0_s\right)\right)$$
10	4 5 9	mpbir2and	$$⊢A\in {\mathbb{N}}_s\to 0_s{<}_{s}A$$