Theorem eln0zs

Description: Non-negative surreal integer property expressed in terms of integers. (Contributed by Scott Fenton, 25-Jul-2025)

	Ref	Expression
Assertion	eln0zs	$$⊢N\in {\mathbb{N}}_{\mathrm{0s}}\leftrightarrow \left(N\in {\mathbb{Z}}_s\wedge 0_s{\le }_{s}N\right)$$

Proof

Step	Hyp	Ref	Expression
1		n0zs	$$⊢N\in {\mathbb{N}}_{\mathrm{0s}}\to N\in {\mathbb{Z}}_s$$
2		n0sge0	$$⊢N\in {\mathbb{N}}_{\mathrm{0s}}\to 0_s{\le }_{s}N$$
3	1 2	jca	$$⊢N\in {\mathbb{N}}_{\mathrm{0s}}\to \left(N\in {\mathbb{Z}}_s\wedge 0_s{\le }_{s}N\right)$$
4		elzs	$$⊢N\in {\mathbb{Z}}_s\leftrightarrow \exists x\in {\mathbb{N}}_s\exists y\in {\mathbb{N}}_{s}N=x{-}_{s}y$$
5		nnno	$$⊢x\in {\mathbb{N}}_s\to x\in \mathrm{No}$$
6	5	adantr	$$⊢\left(x\in {\mathbb{N}}_s\wedge y\in {\mathbb{N}}_s\right)\to x\in \mathrm{No}$$
7		nnno	$$⊢y\in {\mathbb{N}}_s\to y\in \mathrm{No}$$
8	7	adantl	$$⊢\left(x\in {\mathbb{N}}_s\wedge y\in {\mathbb{N}}_s\right)\to y\in \mathrm{No}$$
9	6 8	subsge0d	$$⊢\left(x\in {\mathbb{N}}_s\wedge y\in {\mathbb{N}}_s\right)\to \left(0_s{\le }_s\left(x{-}_{s}y\right)\leftrightarrow y{\le }_{s}x\right)$$
10		nnn0s	$$⊢y\in {\mathbb{N}}_s\to y\in {\mathbb{N}}_{\mathrm{0s}}$$
11		nnn0s	$$⊢x\in {\mathbb{N}}_s\to x\in {\mathbb{N}}_{\mathrm{0s}}$$
12		n0subs	$$⊢\left(y\in {\mathbb{N}}_{\mathrm{0s}}\wedge x\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(y{\le }_{s}x\leftrightarrow x{-}_{s}y\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
13	10 11 12	syl2anr	$$⊢\left(x\in {\mathbb{N}}_s\wedge y\in {\mathbb{N}}_s\right)\to \left(y{\le }_{s}x\leftrightarrow x{-}_{s}y\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
14	9 13	bitrd	$$⊢\left(x\in {\mathbb{N}}_s\wedge y\in {\mathbb{N}}_s\right)\to \left(0_s{\le }_s\left(x{-}_{s}y\right)\leftrightarrow x{-}_{s}y\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
15	14	biimpd	$$⊢\left(x\in {\mathbb{N}}_s\wedge y\in {\mathbb{N}}_s\right)\to \left(0_s{\le }_s\left(x{-}_{s}y\right)\to x{-}_{s}y\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
16		breq2	$$⊢N=x{-}_{s}y\to \left(0_s{\le }_{s}N\leftrightarrow 0_s{\le }_s\left(x{-}_{s}y\right)\right)$$
17		eleq1	$$⊢N=x{-}_{s}y\to \left(N\in {\mathbb{N}}_{\mathrm{0s}}\leftrightarrow x{-}_{s}y\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
18	16 17	imbi12d	$$⊢N=x{-}_{s}y\to \left(\left(0_s{\le }_{s}N\to N\in {\mathbb{N}}_{\mathrm{0s}}\right)\leftrightarrow \left(0_s{\le }_s\left(x{-}_{s}y\right)\to x{-}_{s}y\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$
19	15 18	syl5ibrcom	$$⊢\left(x\in {\mathbb{N}}_s\wedge y\in {\mathbb{N}}_s\right)\to \left(N=x{-}_{s}y\to \left(0_s{\le }_{s}N\to N\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$
20	19	rexlimivv	$$⊢\exists x\in {\mathbb{N}}_s\exists y\in {\mathbb{N}}_{s}N=x{-}_{s}y\to \left(0_s{\le }_{s}N\to N\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
21	4 20	sylbi	$$⊢N\in {\mathbb{Z}}_s\to \left(0_s{\le }_{s}N\to N\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
22	21	imp	$$⊢\left(N\in {\mathbb{Z}}_s\wedge 0_s{\le }_{s}N\right)\to N\in {\mathbb{N}}_{\mathrm{0s}}$$
23	3 22	impbii	$$⊢N\in {\mathbb{N}}_{\mathrm{0s}}\leftrightarrow \left(N\in {\mathbb{Z}}_s\wedge 0_s{\le }_{s}N\right)$$