Theorem zscut

Description: A cut expression for surreal integers. (Contributed by Scott Fenton, 20-Aug-2025)

	Ref	Expression
Assertion	zscut	$$⊢A\in {\mathbb{Z}}_s\to A=\left\{A{-}_s{1}_s\right\}{|}_s\left\{A{+}_s{1}_s\right\}$$

Proof

Step	Hyp	Ref	Expression
1		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)$$
2		n0scut	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to A=\left\{A{-}_s{1}_s\right\}{|}_s\varnothing$$
3		n0sno	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to A\in \mathrm{No}$$
4		1sno	$$⊢1_s\in \mathrm{No}$$
5	4	a1i	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to 1_s\in \mathrm{No}$$
6	3 5	subscld	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to A{-}_s{1}_s\in \mathrm{No}$$
7		snelpwi	$$⊢A{-}_s{1}_s\in \mathrm{No}\to \left\{A{-}_s{1}_s\right\}\in 𝒫\mathrm{No}$$
8		nulssgt	$$⊢\left\{A{-}_s{1}_s\right\}\in 𝒫\mathrm{No}\to \left\{A{-}_s{1}_s\right\}{\ll }_s\varnothing$$
9	6 7 8	3syl	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to \left\{A{-}_s{1}_s\right\}{\ll }_s\varnothing$$
10		slerflex	$$⊢A{-}_s{1}_s\in \mathrm{No}\to \left(A{-}_s{1}_s\right){\le }_s\left(A{-}_s{1}_s\right)$$
11	6 10	syl	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to \left(A{-}_s{1}_s\right){\le }_s\left(A{-}_s{1}_s\right)$$
12		ovex	$$⊢A{-}_s{1}_s\in \mathrm{V}$$
13		breq1	$$⊢x=A{-}_s{1}_s\to \left(x{\le }_{s}y\leftrightarrow \left(A{-}_s{1}_s\right){\le }_{s}y\right)$$
14	13	rexbidv	$$⊢x=A{-}_s{1}_s\to \left(\exists y\in \left\{A{-}_s{1}_s\right\}x{\le }_{s}y\leftrightarrow \exists y\in \left\{A{-}_s{1}_s\right\}\left(A{-}_s{1}_s\right){\le }_{s}y\right)$$
15	12 14	ralsn	$$⊢\forall x\in \left\{A{-}_s{1}_s\right\}\exists y\in \left\{A{-}_s{1}_s\right\}x{\le }_{s}y\leftrightarrow \exists y\in \left\{A{-}_s{1}_s\right\}\left(A{-}_s{1}_s\right){\le }_{s}y$$
16		breq2	$$⊢y=A{-}_s{1}_s\to \left(\left(A{-}_s{1}_s\right){\le }_{s}y\leftrightarrow \left(A{-}_s{1}_s\right){\le }_s\left(A{-}_s{1}_s\right)\right)$$
17	12 16	rexsn	$$⊢\exists y\in \left\{A{-}_s{1}_s\right\}\left(A{-}_s{1}_s\right){\le }_{s}y\leftrightarrow \left(A{-}_s{1}_s\right){\le }_s\left(A{-}_s{1}_s\right)$$
18	15 17	bitri	$$⊢\forall x\in \left\{A{-}_s{1}_s\right\}\exists y\in \left\{A{-}_s{1}_s\right\}x{\le }_{s}y\leftrightarrow \left(A{-}_s{1}_s\right){\le }_s\left(A{-}_s{1}_s\right)$$
19	11 18	sylibr	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to \forall x\in \left\{A{-}_s{1}_s\right\}\exists y\in \left\{A{-}_s{1}_s\right\}x{\le }_{s}y$$
20		ral0	$$⊢\forall x\in \varnothing \exists y\in \left\{A{+}_s{1}_s\right\}y{\le }_{s}x$$
21	20	a1i	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to \forall x\in \varnothing \exists y\in \left\{A{+}_s{1}_s\right\}y{\le }_{s}x$$
22	3	sltm1d	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to \left(A{-}_s{1}_s\right){<}_{s}A$$
23	6 3 22	ssltsn	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to \left\{A{-}_s{1}_s\right\}{\ll }_s\left\{A\right\}$$
24	2	sneqd	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to \left\{A\right\}=\left\{\left\{A{-}_s{1}_s\right\}{|}_s\varnothing \right\}$$
25	23 24	breqtrd	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to \left\{A{-}_s{1}_s\right\}{\ll }_s\left\{\left\{A{-}_s{1}_s\right\}{|}_s\varnothing \right\}$$
26	3 5	addscld	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to A{+}_s{1}_s\in \mathrm{No}$$
27	3	sltp1d	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to A{<}_s\left(A{+}_s{1}_s\right)$$
28	3 26 27	ssltsn	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to \left\{A\right\}{\ll }_s\left\{A{+}_s{1}_s\right\}$$
29	24 28	eqbrtrrd	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to \left\{\left\{A{-}_s{1}_s\right\}{|}_s\varnothing \right\}{\ll }_s\left\{A{+}_s{1}_s\right\}$$
30	9 19 21 25 29	cofcut1d	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to \left\{A{-}_s{1}_s\right\}{|}_s\varnothing =\left\{A{-}_s{1}_s\right\}{|}_s\left\{A{+}_s{1}_s\right\}$$
31	2 30	eqtrd	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to A=\left\{A{-}_s{1}_s\right\}{|}_s\left\{A{+}_s{1}_s\right\}$$
32	31	adantl	$$⊢\left(A\in \mathrm{No}\wedge A\in {\mathbb{N}}_{\mathrm{0s}}\right)\to A=\left\{A{-}_s{1}_s\right\}{|}_s\left\{A{+}_s{1}_s\right\}$$
33		negsfn	$$⊢{+}_{s}Fn\mathrm{No}$$
34		simpl	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to A\in \mathrm{No}$$
35	4	a1i	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to 1_s\in \mathrm{No}$$
36	34 35	addscld	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to A{+}_s{1}_s\in \mathrm{No}$$
37		fnsnfv	$$⊢\left({+}_{s}Fn\mathrm{No}\wedge A{+}_s{1}_s\in \mathrm{No}\right)\to \left\{{+}_s\left(A{+}_s{1}_s\right)\right\}={+}_s\left[\left\{A{+}_s{1}_s\right\}\right]$$
38	33 36 37	sylancr	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left\{{+}_s\left(A{+}_s{1}_s\right)\right\}={+}_s\left[\left\{A{+}_s{1}_s\right\}\right]$$
39		negsdi	$$⊢\left(A\in \mathrm{No}\wedge 1_s\in \mathrm{No}\right)\to {+}_s\left(A{+}_s{1}_s\right)={+}_s\left(A\right){+}_s{+}_s\left(1_s\right)$$
40	34 4 39	sylancl	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to {+}_s\left(A{+}_s{1}_s\right)={+}_s\left(A\right){+}_s{+}_s\left(1_s\right)$$
41		n0sno	$$⊢{+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\to {+}_s\left(A\right)\in \mathrm{No}$$
42	41	adantl	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to {+}_s\left(A\right)\in \mathrm{No}$$
43	42 35	subsvald	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to {+}_s\left(A\right){-}_s{1}_s={+}_s\left(A\right){+}_s{+}_s\left(1_s\right)$$
44	40 43	eqtr4d	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to {+}_s\left(A{+}_s{1}_s\right)={+}_s\left(A\right){-}_s{1}_s$$
45	44	sneqd	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left\{{+}_s\left(A{+}_s{1}_s\right)\right\}=\left\{{+}_s\left(A\right){-}_s{1}_s\right\}$$
46	38 45	eqtr3d	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to {+}_s\left[\left\{A{+}_s{1}_s\right\}\right]=\left\{{+}_s\left(A\right){-}_s{1}_s\right\}$$
47	34 35	subscld	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to A{-}_s{1}_s\in \mathrm{No}$$
48		fnsnfv	$$⊢\left({+}_{s}Fn\mathrm{No}\wedge A{-}_s{1}_s\in \mathrm{No}\right)\to \left\{{+}_s\left(A{-}_s{1}_s\right)\right\}={+}_s\left[\left\{A{-}_s{1}_s\right\}\right]$$
49	33 47 48	sylancr	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left\{{+}_s\left(A{-}_s{1}_s\right)\right\}={+}_s\left[\left\{A{-}_s{1}_s\right\}\right]$$
50	35 34	subsvald	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to 1_s{-}_{s}A=1_s{+}_s{+}_s\left(A\right)$$
51	34 35	negsubsdi2d	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to {+}_s\left(A{-}_s{1}_s\right)=1_s{-}_{s}A$$
52	42 35	addscomd	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to {+}_s\left(A\right){+}_s{1}_s=1_s{+}_s{+}_s\left(A\right)$$
53	50 51 52	3eqtr4d	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to {+}_s\left(A{-}_s{1}_s\right)={+}_s\left(A\right){+}_s{1}_s$$
54	53	sneqd	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left\{{+}_s\left(A{-}_s{1}_s\right)\right\}=\left\{{+}_s\left(A\right){+}_s{1}_s\right\}$$
55	49 54	eqtr3d	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to {+}_s\left[\left\{A{-}_s{1}_s\right\}\right]=\left\{{+}_s\left(A\right){+}_s{1}_s\right\}$$
56	46 55	oveq12d	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to {+}_s\left[\left\{A{+}_s{1}_s\right\}\right]{|}_s{+}_s\left[\left\{A{-}_s{1}_s\right\}\right]=\left\{{+}_s\left(A\right){-}_s{1}_s\right\}{|}_s\left\{{+}_s\left(A\right){+}_s{1}_s\right\}$$
57	34	sltm1d	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(A{-}_s{1}_s\right){<}_{s}A$$
58	34	sltp1d	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to A{<}_s\left(A{+}_s{1}_s\right)$$
59	47 34 36 57 58	slttrd	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(A{-}_s{1}_s\right){<}_s\left(A{+}_s{1}_s\right)$$
60	47 36 59	ssltsn	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left\{A{-}_s{1}_s\right\}{\ll }_s\left\{A{+}_s{1}_s\right\}$$
61		eqidd	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left\{A{-}_s{1}_s\right\}{|}_s\left\{A{+}_s{1}_s\right\}=\left\{A{-}_s{1}_s\right\}{|}_s\left\{A{+}_s{1}_s\right\}$$
62	60 61	negsunif	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to {+}_s\left(\left\{A{-}_s{1}_s\right\}{|}_s\left\{A{+}_s{1}_s\right\}\right)={+}_s\left[\left\{A{+}_s{1}_s\right\}\right]{|}_s{+}_s\left[\left\{A{-}_s{1}_s\right\}\right]$$
63		n0scut	$$⊢{+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\to {+}_s\left(A\right)=\left\{{+}_s\left(A\right){-}_s{1}_s\right\}{|}_s\varnothing$$
64	4	a1i	$$⊢{+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\to 1_s\in \mathrm{No}$$
65	41 64	subscld	$$⊢{+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\to {+}_s\left(A\right){-}_s{1}_s\in \mathrm{No}$$
66		snelpwi	$$⊢{+}_s\left(A\right){-}_s{1}_s\in \mathrm{No}\to \left\{{+}_s\left(A\right){-}_s{1}_s\right\}\in 𝒫\mathrm{No}$$
67		nulssgt	$$⊢\left\{{+}_s\left(A\right){-}_s{1}_s\right\}\in 𝒫\mathrm{No}\to \left\{{+}_s\left(A\right){-}_s{1}_s\right\}{\ll }_s\varnothing$$
68	65 66 67	3syl	$$⊢{+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\to \left\{{+}_s\left(A\right){-}_s{1}_s\right\}{\ll }_s\varnothing$$
69		slerflex	$$⊢{+}_s\left(A\right){-}_s{1}_s\in \mathrm{No}\to \left({+}_s\left(A\right){-}_s{1}_s\right){\le }_s\left({+}_s\left(A\right){-}_s{1}_s\right)$$
70	65 69	syl	$$⊢{+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\to \left({+}_s\left(A\right){-}_s{1}_s\right){\le }_s\left({+}_s\left(A\right){-}_s{1}_s\right)$$
71		ovex	$$⊢{+}_s\left(A\right){-}_s{1}_s\in \mathrm{V}$$
72		breq1	$$⊢x={+}_s\left(A\right){-}_s{1}_s\to \left(x{\le }_{s}y\leftrightarrow \left({+}_s\left(A\right){-}_s{1}_s\right){\le }_{s}y\right)$$
73	72	rexbidv	$$⊢x={+}_s\left(A\right){-}_s{1}_s\to \left(\exists y\in \left\{{+}_s\left(A\right){-}_s{1}_s\right\}x{\le }_{s}y\leftrightarrow \exists y\in \left\{{+}_s\left(A\right){-}_s{1}_s\right\}\left({+}_s\left(A\right){-}_s{1}_s\right){\le }_{s}y\right)$$
74	71 73	ralsn	$$⊢\forall x\in \left\{{+}_s\left(A\right){-}_s{1}_s\right\}\exists y\in \left\{{+}_s\left(A\right){-}_s{1}_s\right\}x{\le }_{s}y\leftrightarrow \exists y\in \left\{{+}_s\left(A\right){-}_s{1}_s\right\}\left({+}_s\left(A\right){-}_s{1}_s\right){\le }_{s}y$$
75		breq2	$$⊢y={+}_s\left(A\right){-}_s{1}_s\to \left(\left({+}_s\left(A\right){-}_s{1}_s\right){\le }_{s}y\leftrightarrow \left({+}_s\left(A\right){-}_s{1}_s\right){\le }_s\left({+}_s\left(A\right){-}_s{1}_s\right)\right)$$
76	71 75	rexsn	$$⊢\exists y\in \left\{{+}_s\left(A\right){-}_s{1}_s\right\}\left({+}_s\left(A\right){-}_s{1}_s\right){\le }_{s}y\leftrightarrow \left({+}_s\left(A\right){-}_s{1}_s\right){\le }_s\left({+}_s\left(A\right){-}_s{1}_s\right)$$
77	74 76	bitri	$$⊢\forall x\in \left\{{+}_s\left(A\right){-}_s{1}_s\right\}\exists y\in \left\{{+}_s\left(A\right){-}_s{1}_s\right\}x{\le }_{s}y\leftrightarrow \left({+}_s\left(A\right){-}_s{1}_s\right){\le }_s\left({+}_s\left(A\right){-}_s{1}_s\right)$$
78	70 77	sylibr	$$⊢{+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\to \forall x\in \left\{{+}_s\left(A\right){-}_s{1}_s\right\}\exists y\in \left\{{+}_s\left(A\right){-}_s{1}_s\right\}x{\le }_{s}y$$
79		ral0	$$⊢\forall x\in \varnothing \exists y\in \left\{{+}_s\left(A\right){+}_s{1}_s\right\}y{\le }_{s}x$$
80	79	a1i	$$⊢{+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\to \forall x\in \varnothing \exists y\in \left\{{+}_s\left(A\right){+}_s{1}_s\right\}y{\le }_{s}x$$
81	41	sltm1d	$$⊢{+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\to \left({+}_s\left(A\right){-}_s{1}_s\right){<}_s{+}_s\left(A\right)$$
82	65 41 81	ssltsn	$$⊢{+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\to \left\{{+}_s\left(A\right){-}_s{1}_s\right\}{\ll }_s\left\{{+}_s\left(A\right)\right\}$$
83	63	sneqd	$$⊢{+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\to \left\{{+}_s\left(A\right)\right\}=\left\{\left\{{+}_s\left(A\right){-}_s{1}_s\right\}{|}_s\varnothing \right\}$$
84	82 83	breqtrd	$$⊢{+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\to \left\{{+}_s\left(A\right){-}_s{1}_s\right\}{\ll }_s\left\{\left\{{+}_s\left(A\right){-}_s{1}_s\right\}{|}_s\varnothing \right\}$$
85	41 64	addscld	$$⊢{+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\to {+}_s\left(A\right){+}_s{1}_s\in \mathrm{No}$$
86	41	sltp1d	$$⊢{+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\to {+}_s\left(A\right){<}_s\left({+}_s\left(A\right){+}_s{1}_s\right)$$
87	41 85 86	ssltsn	$$⊢{+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\to \left\{{+}_s\left(A\right)\right\}{\ll }_s\left\{{+}_s\left(A\right){+}_s{1}_s\right\}$$
88	83 87	eqbrtrrd	$$⊢{+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\to \left\{\left\{{+}_s\left(A\right){-}_s{1}_s\right\}{|}_s\varnothing \right\}{\ll }_s\left\{{+}_s\left(A\right){+}_s{1}_s\right\}$$
89	68 78 80 84 88	cofcut1d	$$⊢{+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\to \left\{{+}_s\left(A\right){-}_s{1}_s\right\}{|}_s\varnothing =\left\{{+}_s\left(A\right){-}_s{1}_s\right\}{|}_s\left\{{+}_s\left(A\right){+}_s{1}_s\right\}$$
90	63 89	eqtrd	$$⊢{+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\to {+}_s\left(A\right)=\left\{{+}_s\left(A\right){-}_s{1}_s\right\}{|}_s\left\{{+}_s\left(A\right){+}_s{1}_s\right\}$$
91	90	adantl	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to {+}_s\left(A\right)=\left\{{+}_s\left(A\right){-}_s{1}_s\right\}{|}_s\left\{{+}_s\left(A\right){+}_s{1}_s\right\}$$
92	56 62 91	3eqtr4rd	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to {+}_s\left(A\right)={+}_s\left(\left\{A{-}_s{1}_s\right\}{|}_s\left\{A{+}_s{1}_s\right\}\right)$$
93	60	scutcld	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left\{A{-}_s{1}_s\right\}{|}_s\left\{A{+}_s{1}_s\right\}\in \mathrm{No}$$
94		negs11	$$⊢\left(A\in \mathrm{No}\wedge \left\{A{-}_s{1}_s\right\}{|}_s\left\{A{+}_s{1}_s\right\}\in \mathrm{No}\right)\to \left({+}_s\left(A\right)={+}_s\left(\left\{A{-}_s{1}_s\right\}{|}_s\left\{A{+}_s{1}_s\right\}\right)\leftrightarrow A=\left\{A{-}_s{1}_s\right\}{|}_s\left\{A{+}_s{1}_s\right\}\right)$$
95	93 94	syldan	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left({+}_s\left(A\right)={+}_s\left(\left\{A{-}_s{1}_s\right\}{|}_s\left\{A{+}_s{1}_s\right\}\right)\leftrightarrow A=\left\{A{-}_s{1}_s\right\}{|}_s\left\{A{+}_s{1}_s\right\}\right)$$
96	92 95	mpbid	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to A=\left\{A{-}_s{1}_s\right\}{|}_s\left\{A{+}_s{1}_s\right\}$$
97	32 96	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 A=\left\{A{-}_s{1}_s\right\}{|}_s\left\{A{+}_s{1}_s\right\}$$
98	1 97	sylbi	$$⊢A\in {\mathbb{Z}}_s\to A=\left\{A{-}_s{1}_s\right\}{|}_s\left\{A{+}_s{1}_s\right\}$$