Theorem 0zs

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

	Ref	Expression
Assertion	0zs	$$⊢0_s\in {\mathbb{Z}}_s$$

Proof

Step	Hyp	Ref	Expression
1		1nns	$$⊢1_s\in {\mathbb{N}}_s$$
2		1sno	$$⊢1_s\in \mathrm{No}$$
3		subsid	$$⊢1_s\in \mathrm{No}\to 1_s{-}_s{1}_s=0_s$$
4	2 3	ax-mp	$$⊢1_s{-}_s{1}_s=0_s$$
5	4	eqcomi	$$⊢0_s=1_s{-}_s{1}_s$$
6		rspceov	$$⊢\left(1_s\in {\mathbb{N}}_s\wedge 1_s\in {\mathbb{N}}_s\wedge 0_s=1_s{-}_s{1}_s\right)\to \exists n\in {\mathbb{N}}_s\exists m\in {\mathbb{N}}_s{0}_s=n{-}_{s}m$$
7	1 1 5 6	mp3an	$$⊢\exists n\in {\mathbb{N}}_s\exists m\in {\mathbb{N}}_s{0}_s=n{-}_{s}m$$
8		elzs	$$⊢0_s\in {\mathbb{Z}}_s\leftrightarrow \exists n\in {\mathbb{N}}_s\exists m\in {\mathbb{N}}_s{0}_s=n{-}_{s}m$$
9	7 8	mpbir	$$⊢0_s\in {\mathbb{Z}}_s$$