Theorem n0lts1e0

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

	Ref	Expression
Assertion	n0lts1e0	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to \left(A{<}_s{1}_s\leftrightarrow A=0_s\right)$$

Proof

Step	Hyp	Ref	Expression
1		n0no	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to A\in \mathrm{No}$$
2		0no	$$⊢0_s\in \mathrm{No}$$
3		lestri3	$$⊢\left(A\in \mathrm{No}\wedge 0_s\in \mathrm{No}\right)\to \left(A=0_s\leftrightarrow \left(A{\le }_s{0}_s\wedge 0_s{\le }_{s}A\right)\right)$$
4	1 2 3	sylancl	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to \left(A=0_s\leftrightarrow \left(A{\le }_s{0}_s\wedge 0_s{\le }_{s}A\right)\right)$$
5		n0sge0	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to 0_s{\le }_{s}A$$
6	5	biantrud	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to \left(A{\le }_s{0}_s\leftrightarrow \left(A{\le }_s{0}_s\wedge 0_s{\le }_{s}A\right)\right)$$
7		0n0s	$$⊢0_s\in {\mathbb{N}}_{\mathrm{0s}}$$
8		n0lesltp1	$$⊢\left(A\in {\mathbb{N}}_{\mathrm{0s}}\wedge 0_s\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(A{\le }_s{0}_s\leftrightarrow A{<}_s\left(0_s{+}_s{1}_s\right)\right)$$
9	7 8	mpan2	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to \left(A{\le }_s{0}_s\leftrightarrow A{<}_s\left(0_s{+}_s{1}_s\right)\right)$$
10		1no	$$⊢1_s\in \mathrm{No}$$
11		addslid	$$⊢1_s\in \mathrm{No}\to 0_s{+}_s{1}_s=1_s$$
12	10 11	ax-mp	$$⊢0_s{+}_s{1}_s=1_s$$
13	12	breq2i	$$⊢A{<}_s\left(0_s{+}_s{1}_s\right)\leftrightarrow A{<}_s{1}_s$$
14	9 13	bitrdi	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to \left(A{\le }_s{0}_s\leftrightarrow A{<}_s{1}_s\right)$$
15	4 6 14	3bitr2rd	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to \left(A{<}_s{1}_s\leftrightarrow A=0_s\right)$$