Theorem n0zs

Description: A non-negative surreal integer is a surreal integer. (Contributed by Scott Fenton, 26-May-2025)

	Ref	Expression
Assertion	n0zs	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to A\in {\mathbb{Z}}_s$$

Proof

Step	Hyp	Ref	Expression
1		eln0s	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\leftrightarrow \left(A\in {\mathbb{N}}_s\vee A=0_s\right)$$
2		nnzs	$$⊢A\in {\mathbb{N}}_s\to A\in {\mathbb{Z}}_s$$
3		id	$$⊢A=0_s\to A=0_s$$
4		0zs	$$⊢0_s\in {\mathbb{Z}}_s$$
5	3 4	eqeltrdi	$$⊢A=0_s\to A\in {\mathbb{Z}}_s$$
6	2 5	jaoi	$$⊢\left(A\in {\mathbb{N}}_s\vee A=0_s\right)\to A\in {\mathbb{Z}}_s$$
7	1 6	sylbi	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to A\in {\mathbb{Z}}_s$$