Theorem 0reno

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

	Ref	Expression
Assertion	0reno	⊢ 0s ∈ ℝs

Proof

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