Theorem zscut0

Description: Either the left or right set of a surreal integer is empty. (Contributed by Scott Fenton, 21-Feb-2026)

	Ref	Expression
Assertion	zscut0	$$⊢A\in {\mathbb{Z}}_s\to \left(L\left(A\right)=\varnothing \vee R\left(A\right)=\varnothing \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		n0ons	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to A\in {On}_s$$
3		elons	$$⊢A\in {On}_s\leftrightarrow \left(A\in \mathrm{No}\wedge R\left(A\right)=\varnothing \right)$$
4	3	simprbi	$$⊢A\in {On}_s\to R\left(A\right)=\varnothing$$
5	2 4	syl	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to R\left(A\right)=\varnothing$$
6	5	a1i	$$⊢A\in \mathrm{No}\to \left(A\in {\mathbb{N}}_{\mathrm{0s}}\to R\left(A\right)=\varnothing \right)$$
7		simpl	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to A\in \mathrm{No}$$
8	7	negscld	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to {+}_s\left(A\right)\in \mathrm{No}$$
9		negsleft	$$⊢{+}_s\left(A\right)\in \mathrm{No}\to L\left({+}_s\left({+}_s\left(A\right)\right)\right)={+}_s\left[R\left({+}_s\left(A\right)\right)\right]$$
10	8 9	syl	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to L\left({+}_s\left({+}_s\left(A\right)\right)\right)={+}_s\left[R\left({+}_s\left(A\right)\right)\right]$$
11		negnegs	$$⊢A\in \mathrm{No}\to {+}_s\left({+}_s\left(A\right)\right)=A$$
12	11	fveq2d	$$⊢A\in \mathrm{No}\to L\left({+}_s\left({+}_s\left(A\right)\right)\right)=L\left(A\right)$$
13	12	adantr	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to L\left({+}_s\left({+}_s\left(A\right)\right)\right)=L\left(A\right)$$
14		n0ons	$$⊢{+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\to {+}_s\left(A\right)\in {On}_s$$
15		elons	$$⊢{+}_s\left(A\right)\in {On}_s\leftrightarrow \left({+}_s\left(A\right)\in \mathrm{No}\wedge R\left({+}_s\left(A\right)\right)=\varnothing \right)$$
16	15	simprbi	$$⊢{+}_s\left(A\right)\in {On}_s\to R\left({+}_s\left(A\right)\right)=\varnothing$$
17	14 16	syl	$$⊢{+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\to R\left({+}_s\left(A\right)\right)=\varnothing$$
18	17	adantl	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to R\left({+}_s\left(A\right)\right)=\varnothing$$
19	18	imaeq2d	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to {+}_s\left[R\left({+}_s\left(A\right)\right)\right]={+}_s\left[\varnothing \right]$$
20		ima0	$$⊢{+}_s\left[\varnothing \right]=\varnothing$$
21	19 20	eqtrdi	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to {+}_s\left[R\left({+}_s\left(A\right)\right)\right]=\varnothing$$
22	10 13 21	3eqtr3d	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to L\left(A\right)=\varnothing$$
23	22	ex	$$⊢A\in \mathrm{No}\to \left({+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\to L\left(A\right)=\varnothing \right)$$
24	6 23	orim12d	$$⊢A\in \mathrm{No}\to \left(\left(A\in {\mathbb{N}}_{\mathrm{0s}}\vee {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(R\left(A\right)=\varnothing \vee L\left(A\right)=\varnothing \right)\right)$$
25	24	imp	$$⊢\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 \left(R\left(A\right)=\varnothing \vee L\left(A\right)=\varnothing \right)$$
26	25	orcomd	$$⊢\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 \left(L\left(A\right)=\varnothing \vee R\left(A\right)=\varnothing \right)$$
27	1 26	sylbi	$$⊢A\in {\mathbb{Z}}_s\to \left(L\left(A\right)=\varnothing \vee R\left(A\right)=\varnothing \right)$$