Theorem 0reno

Description: Surreal zero is a surreal real. (Contributed by Scott Fenton, 15-Apr-2025)

	Ref	Expression
Assertion	0reno	$$⊢0_s\in {ℝ}_s$$

Proof

Step	Hyp	Ref	Expression
1		0sno	$$⊢0_s\in \mathrm{No}$$
2		1nns	$$⊢1_s\in {\mathbb{N}}_s$$
3		0slt1s	$$⊢0_s{<}_s{1}_s$$
4		1sno	$$⊢1_s\in \mathrm{No}$$
5		sltneg	$$⊢\left(0_s\in \mathrm{No}\wedge 1_s\in \mathrm{No}\right)\to \left(0_s{<}_s{1}_s\leftrightarrow {+}_s\left(1_s\right){<}_s{+}_s\left(0_s\right)\right)$$
6	1 4 5	mp2an	$$⊢0_s{<}_s{1}_s\leftrightarrow {+}_s\left(1_s\right){<}_s{+}_s\left(0_s\right)$$
7	3 6	mpbi	$$⊢{+}_s\left(1_s\right){<}_s{+}_s\left(0_s\right)$$
8		negs0s	$$⊢{+}_s\left(0_s\right)=0_s$$
9	7 8	breqtri	$$⊢{+}_s\left(1_s\right){<}_s{0}_s$$
10	9 3	pm3.2i	$$⊢\left({+}_s\left(1_s\right){<}_s{0}_s\wedge 0_s{<}_s{1}_s\right)$$
11		fveq2	$$⊢n=1_s\to {+}_s\left(n\right)={+}_s\left(1_s\right)$$
12	11	breq1d	$$⊢n=1_s\to \left({+}_s\left(n\right){<}_s{0}_s\leftrightarrow {+}_s\left(1_s\right){<}_s{0}_s\right)$$
13		breq2	$$⊢n=1_s\to \left(0_s{<}_{s}n\leftrightarrow 0_s{<}_s{1}_s\right)$$
14	12 13	anbi12d	$$⊢n=1_s\to \left(\left({+}_s\left(n\right){<}_s{0}_s\wedge 0_s{<}_{s}n\right)\leftrightarrow \left({+}_s\left(1_s\right){<}_s{0}_s\wedge 0_s{<}_s{1}_s\right)\right)$$
15	14	rspcev	$$⊢\left(1_s\in {\mathbb{N}}_s\wedge \left({+}_s\left(1_s\right){<}_s{0}_s\wedge 0_s{<}_s{1}_s\right)\right)\to \exists n\in {\mathbb{N}}_s\left({+}_s\left(n\right){<}_s{0}_s\wedge 0_s{<}_{s}n\right)$$
16	2 10 15	mp2an	$$⊢\exists n\in {\mathbb{N}}_s\left({+}_s\left(n\right){<}_s{0}_s\wedge 0_s{<}_{s}n\right)$$
17	4	a1i	$$⊢n\in {\mathbb{N}}_s\to 1_s\in \mathrm{No}$$
18		nnsno	$$⊢n\in {\mathbb{N}}_s\to n\in \mathrm{No}$$
19		nnne0s	$$⊢n\in {\mathbb{N}}_s\to n\ne 0_s$$
20	17 18 19	divscld	$$⊢n\in {\mathbb{N}}_s\to 1_s{/}_{\mathrm{su}}n\in \mathrm{No}$$
21	20	negsval2d	$$⊢n\in {\mathbb{N}}_s\to {+}_s\left(1_s{/}_{\mathrm{su}}n\right)=0_s{-}_s\left(1_s{/}_{\mathrm{su}}n\right)$$
22	21	eqeq2d	$$⊢n\in {\mathbb{N}}_s\to \left(x={+}_s\left(1_s{/}_{\mathrm{su}}n\right)\leftrightarrow x=0_s{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)$$
23	22	bicomd	$$⊢n\in {\mathbb{N}}_s\to \left(x=0_s{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\leftrightarrow x={+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)$$
24	23	rexbiia	$$⊢\exists n\in {\mathbb{N}}_{s}x=0_s{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\leftrightarrow \exists n\in {\mathbb{N}}_{s}x={+}_s\left(1_s{/}_{\mathrm{su}}n\right)$$
25	24	abbii	$$⊢\left\{x|\exists n\in {\mathbb{N}}_{s}x=0_s{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}=\left\{x|\exists n\in {\mathbb{N}}_{s}x={+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}$$
26		addslid	$$⊢1_s{/}_{\mathrm{su}}n\in \mathrm{No}\to 0_s{+}_s\left(1_s{/}_{\mathrm{su}}n\right)=1_s{/}_{\mathrm{su}}n$$
27	20 26	syl	$$⊢n\in {\mathbb{N}}_s\to 0_s{+}_s\left(1_s{/}_{\mathrm{su}}n\right)=1_s{/}_{\mathrm{su}}n$$
28	27	eqeq2d	$$⊢n\in {\mathbb{N}}_s\to \left(x=0_s{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\leftrightarrow x=1_s{/}_{\mathrm{su}}n\right)$$
29	28	rexbiia	$$⊢\exists n\in {\mathbb{N}}_{s}x=0_s{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\leftrightarrow \exists n\in {\mathbb{N}}_{s}x=1_s{/}_{\mathrm{su}}n$$
30	29	abbii	$$⊢\left\{x|\exists n\in {\mathbb{N}}_{s}x=0_s{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}=\left\{x|\exists n\in {\mathbb{N}}_{s}x=1_s{/}_{\mathrm{su}}n\right\}$$
31	25 30	oveq12i	$$⊢\left\{x|\exists n\in {\mathbb{N}}_{s}x=0_s{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{|}_s\left\{x|\exists n\in {\mathbb{N}}_{s}x=0_s{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}=\left\{x|\exists n\in {\mathbb{N}}_{s}x={+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{|}_s\left\{x|\exists n\in {\mathbb{N}}_{s}x=1_s{/}_{\mathrm{su}}n\right\}$$
32		nnsex	$$⊢{\mathbb{N}}_s\in \mathrm{V}$$
33	32	abrexex	$$⊢\left\{x|\exists n\in {\mathbb{N}}_{s}x={+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\in \mathrm{V}$$
34	33	a1i	$$⊢\top \to \left\{x|\exists n\in {\mathbb{N}}_{s}x={+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\in \mathrm{V}$$
35		snex	$$⊢\left\{0_s\right\}\in \mathrm{V}$$
36	35	a1i	$$⊢\top \to \left\{0_s\right\}\in \mathrm{V}$$
37	20	negscld	$$⊢n\in {\mathbb{N}}_s\to {+}_s\left(1_s{/}_{\mathrm{su}}n\right)\in \mathrm{No}$$
38		eleq1	$$⊢x={+}_s\left(1_s{/}_{\mathrm{su}}n\right)\to \left(x\in \mathrm{No}\leftrightarrow {+}_s\left(1_s{/}_{\mathrm{su}}n\right)\in \mathrm{No}\right)$$
39	37 38	syl5ibrcom	$$⊢n\in {\mathbb{N}}_s\to \left(x={+}_s\left(1_s{/}_{\mathrm{su}}n\right)\to x\in \mathrm{No}\right)$$
40	39	rexlimiv	$$⊢\exists n\in {\mathbb{N}}_{s}x={+}_s\left(1_s{/}_{\mathrm{su}}n\right)\to x\in \mathrm{No}$$
41	40	a1i	$$⊢\top \to \left(\exists n\in {\mathbb{N}}_{s}x={+}_s\left(1_s{/}_{\mathrm{su}}n\right)\to x\in \mathrm{No}\right)$$
42	41	abssdv	$$⊢\top \to \left\{x|\exists n\in {\mathbb{N}}_{s}x={+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\subseteq \mathrm{No}$$
43	1	a1i	$$⊢\top \to 0_s\in \mathrm{No}$$
44	43	snssd	$$⊢\top \to \left\{0_s\right\}\subseteq \mathrm{No}$$
45		vex	$$⊢z\in \mathrm{V}$$
46		eqeq1	$$⊢x=z\to \left(x={+}_s\left(1_s{/}_{\mathrm{su}}n\right)\leftrightarrow z={+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)$$
47	46	rexbidv	$$⊢x=z\to \left(\exists n\in {\mathbb{N}}_{s}x={+}_s\left(1_s{/}_{\mathrm{su}}n\right)\leftrightarrow \exists n\in {\mathbb{N}}_{s}z={+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)$$
48	45 47	elab	$$⊢z\in \left\{x|\exists n\in {\mathbb{N}}_{s}x={+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\leftrightarrow \exists n\in {\mathbb{N}}_{s}z={+}_s\left(1_s{/}_{\mathrm{su}}n\right)$$
49		velsn	$$⊢y\in \left\{0_s\right\}\leftrightarrow y=0_s$$
50	48 49	anbi12i	$$⊢\left(z\in \left\{x|\exists n\in {\mathbb{N}}_{s}x={+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\wedge y\in \left\{0_s\right\}\right)\leftrightarrow \left(\exists n\in {\mathbb{N}}_{s}z={+}_s\left(1_s{/}_{\mathrm{su}}n\right)\wedge y=0_s\right)$$
51		r19.41v	$$⊢\exists n\in {\mathbb{N}}_s\left(z={+}_s\left(1_s{/}_{\mathrm{su}}n\right)\wedge y=0_s\right)\leftrightarrow \left(\exists n\in {\mathbb{N}}_{s}z={+}_s\left(1_s{/}_{\mathrm{su}}n\right)\wedge y=0_s\right)$$
52	50 51	bitr4i	$$⊢\left(z\in \left\{x|\exists n\in {\mathbb{N}}_{s}x={+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\wedge y\in \left\{0_s\right\}\right)\leftrightarrow \exists n\in {\mathbb{N}}_s\left(z={+}_s\left(1_s{/}_{\mathrm{su}}n\right)\wedge y=0_s\right)$$
53		muls02	$$⊢n\in \mathrm{No}\to 0_s{\cdot }_{s}n=0_s$$
54	18 53	syl	$$⊢n\in {\mathbb{N}}_s\to 0_s{\cdot }_{s}n=0_s$$
55	54 3	eqbrtrdi	$$⊢n\in {\mathbb{N}}_s\to \left(0_s{\cdot }_{s}n\right){<}_s{1}_s$$
56	1	a1i	$$⊢n\in {\mathbb{N}}_s\to 0_s\in \mathrm{No}$$
57		nnsgt0	$$⊢n\in {\mathbb{N}}_s\to 0_s{<}_{s}n$$
58	56 17 18 57	sltmuldivd	$$⊢n\in {\mathbb{N}}_s\to \left(\left(0_s{\cdot }_{s}n\right){<}_s{1}_s\leftrightarrow 0_s{<}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)$$
59	55 58	mpbid	$$⊢n\in {\mathbb{N}}_s\to 0_s{<}_s\left(1_s{/}_{\mathrm{su}}n\right)$$
60	20	slt0neg2d	$$⊢n\in {\mathbb{N}}_s\to \left(0_s{<}_s\left(1_s{/}_{\mathrm{su}}n\right)\leftrightarrow {+}_s\left(1_s{/}_{\mathrm{su}}n\right){<}_s{0}_s\right)$$
61	59 60	mpbid	$$⊢n\in {\mathbb{N}}_s\to {+}_s\left(1_s{/}_{\mathrm{su}}n\right){<}_s{0}_s$$
62		breq12	$$⊢\left(z={+}_s\left(1_s{/}_{\mathrm{su}}n\right)\wedge y=0_s\right)\to \left(z{<}_{s}y\leftrightarrow {+}_s\left(1_s{/}_{\mathrm{su}}n\right){<}_s{0}_s\right)$$
63	61 62	syl5ibrcom	$$⊢n\in {\mathbb{N}}_s\to \left(\left(z={+}_s\left(1_s{/}_{\mathrm{su}}n\right)\wedge y=0_s\right)\to z{<}_{s}y\right)$$
64	63	rexlimiv	$$⊢\exists n\in {\mathbb{N}}_s\left(z={+}_s\left(1_s{/}_{\mathrm{su}}n\right)\wedge y=0_s\right)\to z{<}_{s}y$$
65	52 64	sylbi	$$⊢\left(z\in \left\{x|\exists n\in {\mathbb{N}}_{s}x={+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\wedge y\in \left\{0_s\right\}\right)\to z{<}_{s}y$$
66	65	3adant1	$$⊢\left(\top \wedge z\in \left\{x|\exists n\in {\mathbb{N}}_{s}x={+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\wedge y\in \left\{0_s\right\}\right)\to z{<}_{s}y$$
67	34 36 42 44 66	ssltd	$$⊢\top \to \left\{x|\exists n\in {\mathbb{N}}_{s}x={+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{\ll }_s\left\{0_s\right\}$$
68	32	abrexex	$$⊢\left\{x|\exists n\in {\mathbb{N}}_{s}x=1_s{/}_{\mathrm{su}}n\right\}\in \mathrm{V}$$
69	68	a1i	$$⊢\top \to \left\{x|\exists n\in {\mathbb{N}}_{s}x=1_s{/}_{\mathrm{su}}n\right\}\in \mathrm{V}$$
70		eleq1	$$⊢x=1_s{/}_{\mathrm{su}}n\to \left(x\in \mathrm{No}\leftrightarrow 1_s{/}_{\mathrm{su}}n\in \mathrm{No}\right)$$
71	20 70	syl5ibrcom	$$⊢n\in {\mathbb{N}}_s\to \left(x=1_s{/}_{\mathrm{su}}n\to x\in \mathrm{No}\right)$$
72	71	rexlimiv	$$⊢\exists n\in {\mathbb{N}}_{s}x=1_s{/}_{\mathrm{su}}n\to x\in \mathrm{No}$$
73	72	a1i	$$⊢\top \to \left(\exists n\in {\mathbb{N}}_{s}x=1_s{/}_{\mathrm{su}}n\to x\in \mathrm{No}\right)$$
74	73	abssdv	$$⊢\top \to \left\{x|\exists n\in {\mathbb{N}}_{s}x=1_s{/}_{\mathrm{su}}n\right\}\subseteq \mathrm{No}$$
75		eqeq1	$$⊢x=z\to \left(x=1_s{/}_{\mathrm{su}}n\leftrightarrow z=1_s{/}_{\mathrm{su}}n\right)$$
76	75	rexbidv	$$⊢x=z\to \left(\exists n\in {\mathbb{N}}_{s}x=1_s{/}_{\mathrm{su}}n\leftrightarrow \exists n\in {\mathbb{N}}_{s}z=1_s{/}_{\mathrm{su}}n\right)$$
77	45 76	elab	$$⊢z\in \left\{x|\exists n\in {\mathbb{N}}_{s}x=1_s{/}_{\mathrm{su}}n\right\}\leftrightarrow \exists n\in {\mathbb{N}}_{s}z=1_s{/}_{\mathrm{su}}n$$
78	49 77	anbi12i	$$⊢\left(y\in \left\{0_s\right\}\wedge z\in \left\{x|\exists n\in {\mathbb{N}}_{s}x=1_s{/}_{\mathrm{su}}n\right\}\right)\leftrightarrow \left(y=0_s\wedge \exists n\in {\mathbb{N}}_{s}z=1_s{/}_{\mathrm{su}}n\right)$$
79		r19.42v	$$⊢\exists n\in {\mathbb{N}}_s\left(y=0_s\wedge z=1_s{/}_{\mathrm{su}}n\right)\leftrightarrow \left(y=0_s\wedge \exists n\in {\mathbb{N}}_{s}z=1_s{/}_{\mathrm{su}}n\right)$$
80	78 79	bitr4i	$$⊢\left(y\in \left\{0_s\right\}\wedge z\in \left\{x|\exists n\in {\mathbb{N}}_{s}x=1_s{/}_{\mathrm{su}}n\right\}\right)\leftrightarrow \exists n\in {\mathbb{N}}_s\left(y=0_s\wedge z=1_s{/}_{\mathrm{su}}n\right)$$
81		breq12	$$⊢\left(y=0_s\wedge z=1_s{/}_{\mathrm{su}}n\right)\to \left(y{<}_{s}z\leftrightarrow 0_s{<}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)$$
82	59 81	syl5ibrcom	$$⊢n\in {\mathbb{N}}_s\to \left(\left(y=0_s\wedge z=1_s{/}_{\mathrm{su}}n\right)\to y{<}_{s}z\right)$$
83	82	rexlimiv	$$⊢\exists n\in {\mathbb{N}}_s\left(y=0_s\wedge z=1_s{/}_{\mathrm{su}}n\right)\to y{<}_{s}z$$
84	83	a1i	$$⊢\top \to \left(\exists n\in {\mathbb{N}}_s\left(y=0_s\wedge z=1_s{/}_{\mathrm{su}}n\right)\to y{<}_{s}z\right)$$
85	80 84	biimtrid	$$⊢\top \to \left(\left(y\in \left\{0_s\right\}\wedge z\in \left\{x|\exists n\in {\mathbb{N}}_{s}x=1_s{/}_{\mathrm{su}}n\right\}\right)\to y{<}_{s}z\right)$$
86	85	3impib	$$⊢\left(\top \wedge y\in \left\{0_s\right\}\wedge z\in \left\{x|\exists n\in {\mathbb{N}}_{s}x=1_s{/}_{\mathrm{su}}n\right\}\right)\to y{<}_{s}z$$
87	36 69 44 74 86	ssltd	$$⊢\top \to \left\{0_s\right\}{\ll }_s\left\{x|\exists n\in {\mathbb{N}}_{s}x=1_s{/}_{\mathrm{su}}n\right\}$$
88	67 87	cuteq0	$$⊢\top \to \left\{x|\exists n\in {\mathbb{N}}_{s}x={+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{|}_s\left\{x|\exists n\in {\mathbb{N}}_{s}x=1_s{/}_{\mathrm{su}}n\right\}=0_s$$
89	88	mptru	$$⊢\left\{x|\exists n\in {\mathbb{N}}_{s}x={+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{|}_s\left\{x|\exists n\in {\mathbb{N}}_{s}x=1_s{/}_{\mathrm{su}}n\right\}=0_s$$
90	31 89	eqtr2i	$$⊢0_s=\left\{x|\exists n\in {\mathbb{N}}_{s}x=0_s{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{|}_s\left\{x|\exists n\in {\mathbb{N}}_{s}x=0_s{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}$$
91	16 90	pm3.2i	$$⊢\left(\exists n\in {\mathbb{N}}_s\left({+}_s\left(n\right){<}_s{0}_s\wedge 0_s{<}_{s}n\right)\wedge 0_s=\left\{x|\exists n\in {\mathbb{N}}_{s}x=0_s{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{|}_s\left\{x|\exists n\in {\mathbb{N}}_{s}x=0_s{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\right)$$
92		elreno	$$⊢0_s\in {ℝ}_s\leftrightarrow \left(0_s\in \mathrm{No}\wedge \left(\exists n\in {\mathbb{N}}_s\left({+}_s\left(n\right){<}_s{0}_s\wedge 0_s{<}_{s}n\right)\wedge 0_s=\left\{x|\exists n\in {\mathbb{N}}_{s}x=0_s{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{|}_s\left\{x|\exists n\in {\mathbb{N}}_{s}x=0_s{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\right)\right)$$
93	1 91 92	mpbir2an	$$⊢0_s\in {ℝ}_s$$