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	4	a1i	$$⊢\top \to 1_s\in \mathrm{No}$$
6	5	slt0neg2d	$$⊢\top \to \left(0_s{<}_s{1}_s\leftrightarrow {+}_s\left(1_s\right){<}_s{0}_s\right)$$
7	6	mptru	$$⊢0_s{<}_s{1}_s\leftrightarrow {+}_s\left(1_s\right){<}_s{0}_s$$
8	3 7	mpbi	$$⊢{+}_s\left(1_s\right){<}_s{0}_s$$
9	8 3	pm3.2i	$$⊢\left({+}_s\left(1_s\right){<}_s{0}_s\wedge 0_s{<}_s{1}_s\right)$$
10		fveq2	$$⊢n=1_s\to {+}_s\left(n\right)={+}_s\left(1_s\right)$$
11	10	breq1d	$$⊢n=1_s\to \left({+}_s\left(n\right){<}_s{0}_s\leftrightarrow {+}_s\left(1_s\right){<}_s{0}_s\right)$$
12		breq2	$$⊢n=1_s\to \left(0_s{<}_{s}n\leftrightarrow 0_s{<}_s{1}_s\right)$$
13	11 12	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)$$
14	13	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)$$
15	2 9 14	mp2an	$$⊢\exists n\in {\mathbb{N}}_s\left({+}_s\left(n\right){<}_s{0}_s\wedge 0_s{<}_{s}n\right)$$
16		ral0	Could not format A. xO e. (/) E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( 0s -s xO ) ) : No typesetting found for |- A. xO e. (/) E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( 0s -s xO ) ) with typecode |-
17		left0s	$$⊢L\left(0_s\right)=\varnothing$$
18		right0s	$$⊢R\left(0_s\right)=\varnothing$$
19	17 18	uneq12i	$$⊢L\left(0_s\right)\cup R\left(0_s\right)=\varnothing \cup \varnothing$$
20		un0	$$⊢\varnothing \cup \varnothing =\varnothing$$
21	19 20	eqtri	$$⊢L\left(0_s\right)\cup R\left(0_s\right)=\varnothing$$
22	21	raleqi	Could not format ( A. xO e. ( ( _Left ` 0s ) u. ( _Right ` 0s ) ) E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( 0s -s xO ) ) <-> A. xO e. (/) E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( 0s -s xO ) ) ) : No typesetting found for |- ( A. xO e. ( ( _Left ` 0s ) u. ( _Right ` 0s ) ) E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( 0s -s xO ) ) <-> A. xO e. (/) E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( 0s -s xO ) ) ) with typecode |-
23	16 22	mpbir	Could not format A. xO e. ( ( _Left ` 0s ) u. ( _Right ` 0s ) ) E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( 0s -s xO ) ) : No typesetting found for |- A. xO e. ( ( _Left ` 0s ) u. ( _Right ` 0s ) ) E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( 0s -s xO ) ) with typecode |-
24	15 23	pm3.2i	Could not format ( E. n e. NN_s ( ( -us ` n )
25		elreno2	Could not format ( 0s e. RR_s <-> ( 0s e. No /\ ( E. n e. NN_s ( ( -us ` n ) ( 0s e. No /\ ( E. n e. NN_s ( ( -us ` n )
26	1 24 25	mpbir2an	$$⊢0_s\in {ℝ}_s$$