Theorem nnzs

Description: A positive surreal integer is a surreal integer. (Contributed by Scott Fenton, 17-May-2025)

	Ref	Expression
Assertion	nnzs	$$⊢A\in {\mathbb{N}}_s\to A\in {\mathbb{Z}}_s$$

Proof

Step	Hyp	Ref	Expression
1		peano2nns	$$⊢A\in {\mathbb{N}}_s\to A{+}_s{1}_s\in {\mathbb{N}}_s$$
2		nnsno	$$⊢A\in {\mathbb{N}}_s\to A\in \mathrm{No}$$
3		1sno	$$⊢1_s\in \mathrm{No}$$
4		pncans	$$⊢\left(A\in \mathrm{No}\wedge 1_s\in \mathrm{No}\right)\to \left(A{+}_s{1}_s\right){-}_s{1}_s=A$$
5	2 3 4	sylancl	$$⊢A\in {\mathbb{N}}_s\to \left(A{+}_s{1}_s\right){-}_s{1}_s=A$$
6	5	eqcomd	$$⊢A\in {\mathbb{N}}_s\to A=\left(A{+}_s{1}_s\right){-}_s{1}_s$$
7		1nns	$$⊢1_s\in {\mathbb{N}}_s$$
8		rspceov	$$⊢\left(A{+}_s{1}_s\in {\mathbb{N}}_s\wedge 1_s\in {\mathbb{N}}_s\wedge A=\left(A{+}_s{1}_s\right){-}_s{1}_s\right)\to \exists x\in {\mathbb{N}}_s\exists y\in {\mathbb{N}}_{s}A=x{-}_{s}y$$
9	7 8	mp3an2	$$⊢\left(A{+}_s{1}_s\in {\mathbb{N}}_s\wedge A=\left(A{+}_s{1}_s\right){-}_s{1}_s\right)\to \exists x\in {\mathbb{N}}_s\exists y\in {\mathbb{N}}_{s}A=x{-}_{s}y$$
10	1 6 9	syl2anc	$$⊢A\in {\mathbb{N}}_s\to \exists x\in {\mathbb{N}}_s\exists y\in {\mathbb{N}}_{s}A=x{-}_{s}y$$
11		elzs	$$⊢A\in {\mathbb{Z}}_s\leftrightarrow \exists x\in {\mathbb{N}}_s\exists y\in {\mathbb{N}}_{s}A=x{-}_{s}y$$
12	10 11	sylibr	$$⊢A\in {\mathbb{N}}_s\to A\in {\mathbb{Z}}_s$$