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		0no	⊢ 0s ∈ No
2		1nns	⊢ 1s ∈ ℕs
3		0lt1s	⊢ 0s <s 1s
4		1no	⊢ 1s ∈ No
5	4	a1i	⊢ ( ⊤ → 1s ∈ No )
6	5	lt0negs2d	⊢ ( ⊤ → ( 0s <s 1s ↔ ( -us ‘ 1s ) <s 0s ) )
7	6	mptru	⊢ ( 0s <s 1s ↔ ( -us ‘ 1s ) <s 0s )
8	3 7	mpbi	⊢ ( -us ‘ 1s ) <s 0s
9	8 3	pm3.2i	⊢ ( ( -us ‘ 1s ) <s 0s ∧ 0s <s 1s )
10		fveq2	⊢ ( 𝑛 = 1s → ( -us ‘ 𝑛 ) = ( -us ‘ 1s ) )
11	10	breq1d	⊢ ( 𝑛 = 1s → ( ( -us ‘ 𝑛 ) <s 0s ↔ ( -us ‘ 1s ) <s 0s ) )
12		breq2	⊢ ( 𝑛 = 1s → ( 0s <s 𝑛 ↔ 0s <s 1s ) )
13	11 12	anbi12d	⊢ ( 𝑛 = 1s → ( ( ( -us ‘ 𝑛 ) <s 0s ∧ 0s <s 𝑛 ) ↔ ( ( -us ‘ 1s ) <s 0s ∧ 0s <s 1s ) ) )
14	13	rspcev	⊢ ( ( 1s ∈ ℕs ∧ ( ( -us ‘ 1s ) <s 0s ∧ 0s <s 1s ) ) → ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 0s ∧ 0s <s 𝑛 ) )
15	2 9 14	mp2an	⊢ ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 0s ∧ 0s <s 𝑛 )
16		ral0	⊢ ∀ 𝑥𝑂 ∈ ∅ ∃ 𝑛 ∈ ℕs ( 1s /su 𝑛 ) ≤s ( abss ‘ ( 0s -s 𝑥𝑂 ) )
17		left0s	⊢ ( L ‘ 0s ) = ∅
18		right0s	⊢ ( R ‘ 0s ) = ∅
19	17 18	uneq12i	⊢ ( ( L ‘ 0s ) ∪ ( R ‘ 0s ) ) = ( ∅ ∪ ∅ )
20		un0	⊢ ( ∅ ∪ ∅ ) = ∅
21	19 20	eqtri	⊢ ( ( L ‘ 0s ) ∪ ( R ‘ 0s ) ) = ∅
22	21	raleqi	⊢ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 0s ) ∪ ( R ‘ 0s ) ) ∃ 𝑛 ∈ ℕs ( 1s /su 𝑛 ) ≤s ( abss ‘ ( 0s -s 𝑥𝑂 ) ) ↔ ∀ 𝑥𝑂 ∈ ∅ ∃ 𝑛 ∈ ℕs ( 1s /su 𝑛 ) ≤s ( abss ‘ ( 0s -s 𝑥𝑂 ) ) )
23	16 22	mpbir	⊢ ∀ 𝑥𝑂 ∈ ( ( L ‘ 0s ) ∪ ( R ‘ 0s ) ) ∃ 𝑛 ∈ ℕs ( 1s /su 𝑛 ) ≤s ( abss ‘ ( 0s -s 𝑥𝑂 ) )
24	15 23	pm3.2i	⊢ ( ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 0s ∧ 0s <s 𝑛 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 0s ) ∪ ( R ‘ 0s ) ) ∃ 𝑛 ∈ ℕs ( 1s /su 𝑛 ) ≤s ( abss ‘ ( 0s -s 𝑥𝑂 ) ) )
25		elreno2	⊢ ( 0s ∈ ℝs ↔ ( 0s ∈ No ∧ ( ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 0s ∧ 0s <s 𝑛 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 0s ) ∪ ( R ‘ 0s ) ) ∃ 𝑛 ∈ ℕs ( 1s /su 𝑛 ) ≤s ( abss ‘ ( 0s -s 𝑥𝑂 ) ) ) ) )
26	1 24 25	mpbir2an	⊢ 0s ∈ ℝs