Theorem nnsgt0

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

	Ref	Expression
Assertion	nnsgt0	⊢ ( 𝐴 ∈ ℕs → 0s <s 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		nnssn0s	⊢ ℕs ⊆ ℕ0s
2	1	sseli	⊢ ( 𝐴 ∈ ℕs → 𝐴 ∈ ℕ0s )
3		n0sge0	⊢ ( 𝐴 ∈ ℕ0s → 0s ≤s 𝐴 )
4	2 3	syl	⊢ ( 𝐴 ∈ ℕs → 0s ≤s 𝐴 )
5		nnne0s	⊢ ( 𝐴 ∈ ℕs → 𝐴 ≠ 0s )
6		0sno	⊢ 0s ∈ No
7	6	a1i	⊢ ( 𝐴 ∈ ℕs → 0s ∈ No )
8		nnsno	⊢ ( 𝐴 ∈ ℕs → 𝐴 ∈ No )
9	7 8	sltlend	⊢ ( 𝐴 ∈ ℕs → ( 0s <s 𝐴 ↔ ( 0s ≤s 𝐴 ∧ 𝐴 ≠ 0s ) ) )
10	4 5 9	mpbir2and	⊢ ( 𝐴 ∈ ℕs → 0s <s 𝐴 )