Theorem znegscl

Description: The surreal integers are closed under negation. (Contributed by Scott Fenton, 26-May-2025)

	Ref	Expression
Assertion	znegscl	$$⊢A\in {\mathbb{Z}}_s\to {+}_s\left(A\right)\in {\mathbb{Z}}_s$$

Proof

Step	Hyp	Ref	Expression
1		nnsno	$$⊢n\in {\mathbb{N}}_s\to n\in \mathrm{No}$$
2	1	adantr	$$⊢\left(n\in {\mathbb{N}}_s\wedge m\in {\mathbb{N}}_s\right)\to n\in \mathrm{No}$$
3		nnsno	$$⊢m\in {\mathbb{N}}_s\to m\in \mathrm{No}$$
4	3	adantl	$$⊢\left(n\in {\mathbb{N}}_s\wedge m\in {\mathbb{N}}_s\right)\to m\in \mathrm{No}$$
5	2 4	negsubsdi2d	$$⊢\left(n\in {\mathbb{N}}_s\wedge m\in {\mathbb{N}}_s\right)\to {+}_s\left(n{-}_{s}m\right)=m{-}_{s}n$$
6		fveqeq2	$$⊢A=n{-}_{s}m\to \left({+}_s\left(A\right)=m{-}_{s}n\leftrightarrow {+}_s\left(n{-}_{s}m\right)=m{-}_{s}n\right)$$
7	5 6	syl5ibrcom	$$⊢\left(n\in {\mathbb{N}}_s\wedge m\in {\mathbb{N}}_s\right)\to \left(A=n{-}_{s}m\to {+}_s\left(A\right)=m{-}_{s}n\right)$$
8	7	reximdva	$$⊢n\in {\mathbb{N}}_s\to \left(\exists m\in {\mathbb{N}}_{s}A=n{-}_{s}m\to \exists m\in {\mathbb{N}}_s{+}_s\left(A\right)=m{-}_{s}n\right)$$
9	8	reximia	$$⊢\exists n\in {\mathbb{N}}_s\exists m\in {\mathbb{N}}_{s}A=n{-}_{s}m\to \exists n\in {\mathbb{N}}_s\exists m\in {\mathbb{N}}_s{+}_s\left(A\right)=m{-}_{s}n$$
10		elzs	$$⊢A\in {\mathbb{Z}}_s\leftrightarrow \exists n\in {\mathbb{N}}_s\exists m\in {\mathbb{N}}_{s}A=n{-}_{s}m$$
11		elzs	$$⊢{+}_s\left(A\right)\in {\mathbb{Z}}_s\leftrightarrow \exists m\in {\mathbb{N}}_s\exists n\in {\mathbb{N}}_s{+}_s\left(A\right)=m{-}_{s}n$$
12		rexcom	$$⊢\exists m\in {\mathbb{N}}_s\exists n\in {\mathbb{N}}_s{+}_s\left(A\right)=m{-}_{s}n\leftrightarrow \exists n\in {\mathbb{N}}_s\exists m\in {\mathbb{N}}_s{+}_s\left(A\right)=m{-}_{s}n$$
13	11 12	bitri	$$⊢{+}_s\left(A\right)\in {\mathbb{Z}}_s\leftrightarrow \exists n\in {\mathbb{N}}_s\exists m\in {\mathbb{N}}_s{+}_s\left(A\right)=m{-}_{s}n$$
14	9 10 13	3imtr4i	$$⊢A\in {\mathbb{Z}}_s\to {+}_s\left(A\right)\in {\mathbb{Z}}_s$$