Theorem 0reno

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

	Ref	Expression
Assertion	0reno	|- 0s e. RR_s

Proof

Step	Hyp	Ref	Expression
1		0no	|- 0s e. No
2		1nns	|- 1s e. NN_s
3		0lt1s	|- 0s
4		1no	|- 1s e. No
5	4	a1i	|- ( T. -> 1s e. No )
6	5	lt0negs2d	|- ( T. -> ( 0s ( -us ` 1s )
7	6	mptru	|- ( 0s ( -us ` 1s )
8	3 7	mpbi	|- ( -us ` 1s )
9	8 3	pm3.2i	|- ( ( -us ` 1s )
10		fveq2	|- ( n = 1s -> ( -us ` n ) = ( -us ` 1s ) )
11	10	breq1d	|- ( n = 1s -> ( ( -us ` n ) ( -us ` 1s )
12		breq2	|- ( n = 1s -> ( 0s 0s
13	11 12	anbi12d	|- ( n = 1s -> ( ( ( -us ` n ) ( ( -us ` 1s )
14	13	rspcev	|- ( ( 1s e. NN_s /\ ( ( -us ` 1s ) E. n e. NN_s ( ( -us ` n )
15	2 9 14	mp2an	|- E. n e. NN_s ( ( -us ` n )
16		ral0	|- A. xO e. (/) E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( 0s -s xO ) )
17		left0s	|- ( _Left ` 0s ) = (/)
18		right0s	|- ( _Right ` 0s ) = (/)
19	17 18	uneq12i	|- ( ( _Left ` 0s ) u. ( _Right ` 0s ) ) = ( (/) u. (/) )
20		un0	|- ( (/) u. (/) ) = (/)
21	19 20	eqtri	|- ( ( _Left ` 0s ) u. ( _Right ` 0s ) ) = (/)
22	21	raleqi	|- ( 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 ) ) )
23	16 22	mpbir	|- A. xO e. ( ( _Left ` 0s ) u. ( _Right ` 0s ) ) E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( 0s -s xO ) )
24	15 23	pm3.2i	|- ( E. n e. NN_s ( ( -us ` n )
25		elreno2	|- ( 0s e. RR_s <-> ( 0s e. No /\ ( E. n e. NN_s ( ( -us ` n )
26	1 24 25	mpbir2an	|- 0s e. RR_s