Theorem n0slt1e0

Description: A non-negative surreal integer is less than one iff it is zero. (Contributed by Scott Fenton, 23-Feb-2026)

	Ref	Expression
Assertion	n0slt1e0	⊢ ( 𝐴 ∈ ℕ0s → ( 𝐴 <s 1s ↔ 𝐴 = 0s ) )

Proof

Step	Hyp	Ref	Expression
1		n0sno	⊢ ( 𝐴 ∈ ℕ0s → 𝐴 ∈ No )
2		0sno	⊢ 0s ∈ No
3		sletri3	⊢ ( ( 𝐴 ∈ No ∧ 0s ∈ No ) → ( 𝐴 = 0s ↔ ( 𝐴 ≤s 0s ∧ 0s ≤s 𝐴 ) ) )
4	1 2 3	sylancl	⊢ ( 𝐴 ∈ ℕ0s → ( 𝐴 = 0s ↔ ( 𝐴 ≤s 0s ∧ 0s ≤s 𝐴 ) ) )
5		n0sge0	⊢ ( 𝐴 ∈ ℕ0s → 0s ≤s 𝐴 )
6	5	biantrud	⊢ ( 𝐴 ∈ ℕ0s → ( 𝐴 ≤s 0s ↔ ( 𝐴 ≤s 0s ∧ 0s ≤s 𝐴 ) ) )
7		0n0s	⊢ 0s ∈ ℕ0s
8		n0sleltp1	⊢ ( ( 𝐴 ∈ ℕ0s ∧ 0s ∈ ℕ0s ) → ( 𝐴 ≤s 0s ↔ 𝐴 <s ( 0s +s 1s ) ) )
9	7 8	mpan2	⊢ ( 𝐴 ∈ ℕ0s → ( 𝐴 ≤s 0s ↔ 𝐴 <s ( 0s +s 1s ) ) )
10		1sno	⊢ 1s ∈ No
11		addslid	⊢ ( 1s ∈ No → ( 0s +s 1s ) = 1s )
12	10 11	ax-mp	⊢ ( 0s +s 1s ) = 1s
13	12	breq2i	⊢ ( 𝐴 <s ( 0s +s 1s ) ↔ 𝐴 <s 1s )
14	9 13	bitrdi	⊢ ( 𝐴 ∈ ℕ0s → ( 𝐴 ≤s 0s ↔ 𝐴 <s 1s ) )
15	4 6 14	3bitr2rd	⊢ ( 𝐴 ∈ ℕ0s → ( 𝐴 <s 1s ↔ 𝐴 = 0s ) )