Theorem elzn0s

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

	Ref	Expression
Assertion	elzn0s	$$⊢A\in {\mathbb{Z}}_s\leftrightarrow \left(A\in \mathrm{No}\wedge \left(A\in {\mathbb{N}}_{\mathrm{0s}}\vee {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		elzs	$$⊢A\in {\mathbb{Z}}_s\leftrightarrow \exists n\in {\mathbb{N}}_s\exists m\in {\mathbb{N}}_{s}A=n{-}_{s}m$$
2		nnno	$$⊢n\in {\mathbb{N}}_s\to n\in \mathrm{No}$$
3		nnno	$$⊢m\in {\mathbb{N}}_s\to m\in \mathrm{No}$$
4		subscl	$$⊢\left(n\in \mathrm{No}\wedge m\in \mathrm{No}\right)\to n{-}_{s}m\in \mathrm{No}$$
5	2 3 4	syl2an	$$⊢\left(n\in {\mathbb{N}}_s\wedge m\in {\mathbb{N}}_s\right)\to n{-}_{s}m\in \mathrm{No}$$
6		lestric	$$⊢\left(m\in \mathrm{No}\wedge n\in \mathrm{No}\right)\to \left(m{\le }_{s}n\vee n{\le }_{s}m\right)$$
7	3 2 6	syl2anr	$$⊢\left(n\in {\mathbb{N}}_s\wedge m\in {\mathbb{N}}_s\right)\to \left(m{\le }_{s}n\vee n{\le }_{s}m\right)$$
8		nnn0s	$$⊢m\in {\mathbb{N}}_s\to m\in {\mathbb{N}}_{\mathrm{0s}}$$
9		nnn0s	$$⊢n\in {\mathbb{N}}_s\to n\in {\mathbb{N}}_{\mathrm{0s}}$$
10		n0subs	$$⊢\left(m\in {\mathbb{N}}_{\mathrm{0s}}\wedge n\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(m{\le }_{s}n\leftrightarrow n{-}_{s}m\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
11	8 9 10	syl2anr	$$⊢\left(n\in {\mathbb{N}}_s\wedge m\in {\mathbb{N}}_s\right)\to \left(m{\le }_{s}n\leftrightarrow n{-}_{s}m\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
12		n0subs	$$⊢\left(n\in {\mathbb{N}}_{\mathrm{0s}}\wedge m\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(n{\le }_{s}m\leftrightarrow m{-}_{s}n\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
13	9 8 12	syl2an	$$⊢\left(n\in {\mathbb{N}}_s\wedge m\in {\mathbb{N}}_s\right)\to \left(n{\le }_{s}m\leftrightarrow m{-}_{s}n\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
14	2	adantr	$$⊢\left(n\in {\mathbb{N}}_s\wedge m\in {\mathbb{N}}_s\right)\to n\in \mathrm{No}$$
15	3	adantl	$$⊢\left(n\in {\mathbb{N}}_s\wedge m\in {\mathbb{N}}_s\right)\to m\in \mathrm{No}$$
16	14 15	negsubsdi2d	$$⊢\left(n\in {\mathbb{N}}_s\wedge m\in {\mathbb{N}}_s\right)\to {+}_s\left(n{-}_{s}m\right)=m{-}_{s}n$$
17	16	eleq1d	$$⊢\left(n\in {\mathbb{N}}_s\wedge m\in {\mathbb{N}}_s\right)\to \left({+}_s\left(n{-}_{s}m\right)\in {\mathbb{N}}_{\mathrm{0s}}\leftrightarrow m{-}_{s}n\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
18	13 17	bitr4d	$$⊢\left(n\in {\mathbb{N}}_s\wedge m\in {\mathbb{N}}_s\right)\to \left(n{\le }_{s}m\leftrightarrow {+}_s\left(n{-}_{s}m\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
19	11 18	orbi12d	$$⊢\left(n\in {\mathbb{N}}_s\wedge m\in {\mathbb{N}}_s\right)\to \left(\left(m{\le }_{s}n\vee n{\le }_{s}m\right)\leftrightarrow \left(n{-}_{s}m\in {\mathbb{N}}_{\mathrm{0s}}\vee {+}_s\left(n{-}_{s}m\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$
20	7 19	mpbid	$$⊢\left(n\in {\mathbb{N}}_s\wedge m\in {\mathbb{N}}_s\right)\to \left(n{-}_{s}m\in {\mathbb{N}}_{\mathrm{0s}}\vee {+}_s\left(n{-}_{s}m\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
21	5 20	jca	$$⊢\left(n\in {\mathbb{N}}_s\wedge m\in {\mathbb{N}}_s\right)\to \left(n{-}_{s}m\in \mathrm{No}\wedge \left(n{-}_{s}m\in {\mathbb{N}}_{\mathrm{0s}}\vee {+}_s\left(n{-}_{s}m\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$
22		eleq1	$$⊢A=n{-}_{s}m\to \left(A\in \mathrm{No}\leftrightarrow n{-}_{s}m\in \mathrm{No}\right)$$
23		eleq1	$$⊢A=n{-}_{s}m\to \left(A\in {\mathbb{N}}_{\mathrm{0s}}\leftrightarrow n{-}_{s}m\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
24		fveq2	$$⊢A=n{-}_{s}m\to {+}_s\left(A\right)={+}_s\left(n{-}_{s}m\right)$$
25	24	eleq1d	$$⊢A=n{-}_{s}m\to \left({+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\leftrightarrow {+}_s\left(n{-}_{s}m\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
26	23 25	orbi12d	$$⊢A=n{-}_{s}m\to \left(\left(A\in {\mathbb{N}}_{\mathrm{0s}}\vee {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\leftrightarrow \left(n{-}_{s}m\in {\mathbb{N}}_{\mathrm{0s}}\vee {+}_s\left(n{-}_{s}m\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$
27	22 26	anbi12d	$$⊢A=n{-}_{s}m\to \left(\left(A\in \mathrm{No}\wedge \left(A\in {\mathbb{N}}_{\mathrm{0s}}\vee {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\leftrightarrow \left(n{-}_{s}m\in \mathrm{No}\wedge \left(n{-}_{s}m\in {\mathbb{N}}_{\mathrm{0s}}\vee {+}_s\left(n{-}_{s}m\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\right)$$
28	21 27	syl5ibrcom	$$⊢\left(n\in {\mathbb{N}}_s\wedge m\in {\mathbb{N}}_s\right)\to \left(A=n{-}_{s}m\to \left(A\in \mathrm{No}\wedge \left(A\in {\mathbb{N}}_{\mathrm{0s}}\vee {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\right)$$
29	28	rexlimivv	$$⊢\exists n\in {\mathbb{N}}_s\exists m\in {\mathbb{N}}_{s}A=n{-}_{s}m\to \left(A\in \mathrm{No}\wedge \left(A\in {\mathbb{N}}_{\mathrm{0s}}\vee {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$
30		n0p1nns	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to A{+}_s{1}_s\in {\mathbb{N}}_s$$
31		1nns	$$⊢1_s\in {\mathbb{N}}_s$$
32	31	a1i	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to 1_s\in {\mathbb{N}}_s$$
33		n0no	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to A\in \mathrm{No}$$
34		1no	$$⊢1_s\in \mathrm{No}$$
35		pncans	$$⊢\left(A\in \mathrm{No}\wedge 1_s\in \mathrm{No}\right)\to \left(A{+}_s{1}_s\right){-}_s{1}_s=A$$
36	33 34 35	sylancl	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to \left(A{+}_s{1}_s\right){-}_s{1}_s=A$$
37	36	eqcomd	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to A=\left(A{+}_s{1}_s\right){-}_s{1}_s$$
38		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 n\in {\mathbb{N}}_s\exists m\in {\mathbb{N}}_{s}A=n{-}_{s}m$$
39	30 32 37 38	syl3anc	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to \exists n\in {\mathbb{N}}_s\exists m\in {\mathbb{N}}_{s}A=n{-}_{s}m$$
40	39	adantl	$$⊢\left(A\in \mathrm{No}\wedge A\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \exists n\in {\mathbb{N}}_s\exists m\in {\mathbb{N}}_{s}A=n{-}_{s}m$$
41	31	a1i	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to 1_s\in {\mathbb{N}}_s$$
42	34	a1i	$$⊢A\in \mathrm{No}\to 1_s\in \mathrm{No}$$
43		id	$$⊢A\in \mathrm{No}\to A\in \mathrm{No}$$
44	42 43	subsvald	$$⊢A\in \mathrm{No}\to 1_s{-}_{s}A=1_s{+}_s{+}_s\left(A\right)$$
45		negscl	$$⊢A\in \mathrm{No}\to {+}_s\left(A\right)\in \mathrm{No}$$
46	42 45	addscomd	$$⊢A\in \mathrm{No}\to 1_s{+}_s{+}_s\left(A\right)={+}_s\left(A\right){+}_s{1}_s$$
47	44 46	eqtrd	$$⊢A\in \mathrm{No}\to 1_s{-}_{s}A={+}_s\left(A\right){+}_s{1}_s$$
48	47	adantr	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to 1_s{-}_{s}A={+}_s\left(A\right){+}_s{1}_s$$
49		n0p1nns	$$⊢{+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\to {+}_s\left(A\right){+}_s{1}_s\in {\mathbb{N}}_s$$
50	49	adantl	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to {+}_s\left(A\right){+}_s{1}_s\in {\mathbb{N}}_s$$
51	48 50	eqeltrd	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to 1_s{-}_{s}A\in {\mathbb{N}}_s$$
52	42 43	nncansd	$$⊢A\in \mathrm{No}\to 1_s{-}_s\left(1_s{-}_{s}A\right)=A$$
53	52	eqcomd	$$⊢A\in \mathrm{No}\to A=1_s{-}_s\left(1_s{-}_{s}A\right)$$
54	53	adantr	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to A=1_s{-}_s\left(1_s{-}_{s}A\right)$$
55		rspceov	$$⊢\left(1_s\in {\mathbb{N}}_s\wedge 1_s{-}_{s}A\in {\mathbb{N}}_s\wedge A=1_s{-}_s\left(1_s{-}_{s}A\right)\right)\to \exists n\in {\mathbb{N}}_s\exists m\in {\mathbb{N}}_{s}A=n{-}_{s}m$$
56	41 51 54 55	syl3anc	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \exists n\in {\mathbb{N}}_s\exists m\in {\mathbb{N}}_{s}A=n{-}_{s}m$$
57	40 56	jaodan	$$⊢\left(A\in \mathrm{No}\wedge \left(A\in {\mathbb{N}}_{\mathrm{0s}}\vee {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to \exists n\in {\mathbb{N}}_s\exists m\in {\mathbb{N}}_{s}A=n{-}_{s}m$$
58	29 57	impbii	$$⊢\exists n\in {\mathbb{N}}_s\exists m\in {\mathbb{N}}_{s}A=n{-}_{s}m\leftrightarrow \left(A\in \mathrm{No}\wedge \left(A\in {\mathbb{N}}_{\mathrm{0s}}\vee {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$
59	1 58	bitri	$$⊢A\in {\mathbb{Z}}_s\leftrightarrow \left(A\in \mathrm{No}\wedge \left(A\in {\mathbb{N}}_{\mathrm{0s}}\vee {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$