Theorem cutneg

Description: The simplest number greater than a negative number is zero. (Contributed by Scott Fenton, 4-Sep-2025)

	Ref	Expression
Hypotheses	cutneg.1	|- ( ph -> A e. No )
	cutneg.2	|- ( ph -> A
Assertion	cutneg	|- ( ph -> ( { A } |s (/) ) = 0s )

Proof

Step	Hyp	Ref	Expression
1		cutneg.1	|- ( ph -> A e. No )
2		cutneg.2	|- ( ph -> A
3		0sno	|- 0s e. No
4	3	a1i	|- ( ph -> 0s e. No )
5	1 4 2	ssltsn	|- ( ph -> { A } <
6		snelpwi	|- ( 0s e. No -> { 0s } e. ~P No )
7	3 6	ax-mp	|- { 0s } e. ~P No
8		nulssgt	|- ( { 0s } e. ~P No -> { 0s } <
9	7 8	mp1i	|- ( ph -> { 0s } <
10	5 9	cuteq0	|- ( ph -> ( { A } |s (/) ) = 0s )