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	⊢ ( 𝜑 → 𝐴 ∈ No )
	cutneg.2	⊢ ( 𝜑 → 𝐴 <s 0s )
Assertion	cutneg	⊢ ( 𝜑 → ( { 𝐴 } |s ∅ ) = 0s )

Proof

Step	Hyp	Ref	Expression
1		cutneg.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		cutneg.2	⊢ ( 𝜑 → 𝐴 <s 0s )
3		0no	⊢ 0s ∈ No
4	3	a1i	⊢ ( 𝜑 → 0s ∈ No )
5	1 4 2	sltssn	⊢ ( 𝜑 → { 𝐴 } <<s { 0s } )
6		snelpwi	⊢ ( 0s ∈ No → { 0s } ∈ 𝒫 No )
7	3 6	ax-mp	⊢ { 0s } ∈ 𝒫 No
8		nulsgts	⊢ ( { 0s } ∈ 𝒫 No → { 0s } <<s ∅ )
9	7 8	mp1i	⊢ ( 𝜑 → { 0s } <<s ∅ )
10	5 9	cuteq0	⊢ ( 𝜑 → ( { 𝐴 } |s ∅ ) = 0s )