Theorem nnsgt0

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

	Ref	Expression
Assertion	nnsgt0	|- ( A e. NN_s -> 0s

Proof

Step	Hyp	Ref	Expression
1		nnssn0s	|- NN_s C_ NN0_s
2	1	sseli	|- ( A e. NN_s -> A e. NN0_s )
3		n0sge0	|- ( A e. NN0_s -> 0s <_s A )
4	2 3	syl	|- ( A e. NN_s -> 0s <_s A )
5		nnne0s	|- ( A e. NN_s -> A =/= 0s )
6		0sno	|- 0s e. No
7	6	a1i	|- ( A e. NN_s -> 0s e. No )
8		nnsno	|- ( A e. NN_s -> A e. No )
9	7 8	sltlend	|- ( A e. NN_s -> ( 0s ( 0s <_s A /\ A =/= 0s ) ) )
10	4 5 9	mpbir2and	|- ( A e. NN_s -> 0s