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	|- ( A e. NN0_s -> ( A A = 0s ) )

Proof

Step	Hyp	Ref	Expression
1		n0sno	|- ( A e. NN0_s -> A e. No )
2		0sno	|- 0s e. No
3		sletri3	|- ( ( A e. No /\ 0s e. No ) -> ( A = 0s <-> ( A <_s 0s /\ 0s <_s A ) ) )
4	1 2 3	sylancl	|- ( A e. NN0_s -> ( A = 0s <-> ( A <_s 0s /\ 0s <_s A ) ) )
5		n0sge0	|- ( A e. NN0_s -> 0s <_s A )
6	5	biantrud	|- ( A e. NN0_s -> ( A <_s 0s <-> ( A <_s 0s /\ 0s <_s A ) ) )
7		0n0s	|- 0s e. NN0_s
8		n0sleltp1	|- ( ( A e. NN0_s /\ 0s e. NN0_s ) -> ( A <_s 0s <-> A
9	7 8	mpan2	|- ( A e. NN0_s -> ( A <_s 0s <-> A
10		1sno	|- 1s e. No
11		addslid	|- ( 1s e. No -> ( 0s +s 1s ) = 1s )
12	10 11	ax-mp	|- ( 0s +s 1s ) = 1s
13	12	breq2i	|- ( A A
14	9 13	bitrdi	|- ( A e. NN0_s -> ( A <_s 0s <-> A
15	4 6 14	3bitr2rd	|- ( A e. NN0_s -> ( A A = 0s ) )