Theorem n0seo

Description: A non-negative surreal integer is either even or odd. (Contributed by Scott Fenton, 19-Aug-2025)

	Ref	Expression
Assertion	n0seo	⊢ ( 𝑁 ∈ ℕ0s → ( ∃ 𝑥 ∈ ℕ0s 𝑁 = ( 2s ·s 𝑥 ) ∨ ∃ 𝑥 ∈ ℕ0s 𝑁 = ( ( 2s ·s 𝑥 ) +s 1s ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqeq1	⊢ ( 𝑚 = 0s → ( 𝑚 = ( 2s ·s 𝑥 ) ↔ 0s = ( 2s ·s 𝑥 ) ) )
2	1	rexbidv	⊢ ( 𝑚 = 0s → ( ∃ 𝑥 ∈ ℕ0s 𝑚 = ( 2s ·s 𝑥 ) ↔ ∃ 𝑥 ∈ ℕ0s 0s = ( 2s ·s 𝑥 ) ) )
3		eqeq1	⊢ ( 𝑚 = 0s → ( 𝑚 = ( ( 2s ·s 𝑥 ) +s 1s ) ↔ 0s = ( ( 2s ·s 𝑥 ) +s 1s ) ) )
4	3	rexbidv	⊢ ( 𝑚 = 0s → ( ∃ 𝑥 ∈ ℕ0s 𝑚 = ( ( 2s ·s 𝑥 ) +s 1s ) ↔ ∃ 𝑥 ∈ ℕ0s 0s = ( ( 2s ·s 𝑥 ) +s 1s ) ) )
5	2 4	orbi12d	⊢ ( 𝑚 = 0s → ( ( ∃ 𝑥 ∈ ℕ0s 𝑚 = ( 2s ·s 𝑥 ) ∨ ∃ 𝑥 ∈ ℕ0s 𝑚 = ( ( 2s ·s 𝑥 ) +s 1s ) ) ↔ ( ∃ 𝑥 ∈ ℕ0s 0s = ( 2s ·s 𝑥 ) ∨ ∃ 𝑥 ∈ ℕ0s 0s = ( ( 2s ·s 𝑥 ) +s 1s ) ) ) )
6		eqeq1	⊢ ( 𝑚 = 𝑛 → ( 𝑚 = ( 2s ·s 𝑥 ) ↔ 𝑛 = ( 2s ·s 𝑥 ) ) )
7	6	rexbidv	⊢ ( 𝑚 = 𝑛 → ( ∃ 𝑥 ∈ ℕ0s 𝑚 = ( 2s ·s 𝑥 ) ↔ ∃ 𝑥 ∈ ℕ0s 𝑛 = ( 2s ·s 𝑥 ) ) )
8		eqeq1	⊢ ( 𝑚 = 𝑛 → ( 𝑚 = ( ( 2s ·s 𝑥 ) +s 1s ) ↔ 𝑛 = ( ( 2s ·s 𝑥 ) +s 1s ) ) )
9	8	rexbidv	⊢ ( 𝑚 = 𝑛 → ( ∃ 𝑥 ∈ ℕ0s 𝑚 = ( ( 2s ·s 𝑥 ) +s 1s ) ↔ ∃ 𝑥 ∈ ℕ0s 𝑛 = ( ( 2s ·s 𝑥 ) +s 1s ) ) )
10	7 9	orbi12d	⊢ ( 𝑚 = 𝑛 → ( ( ∃ 𝑥 ∈ ℕ0s 𝑚 = ( 2s ·s 𝑥 ) ∨ ∃ 𝑥 ∈ ℕ0s 𝑚 = ( ( 2s ·s 𝑥 ) +s 1s ) ) ↔ ( ∃ 𝑥 ∈ ℕ0s 𝑛 = ( 2s ·s 𝑥 ) ∨ ∃ 𝑥 ∈ ℕ0s 𝑛 = ( ( 2s ·s 𝑥 ) +s 1s ) ) ) )
11		eqeq1	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( 𝑚 = ( 2s ·s 𝑥 ) ↔ ( 𝑛 +s 1s ) = ( 2s ·s 𝑥 ) ) )
12	11	rexbidv	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( ∃ 𝑥 ∈ ℕ0s 𝑚 = ( 2s ·s 𝑥 ) ↔ ∃ 𝑥 ∈ ℕ0s ( 𝑛 +s 1s ) = ( 2s ·s 𝑥 ) ) )
13		oveq2	⊢ ( 𝑥 = 𝑦 → ( 2s ·s 𝑥 ) = ( 2s ·s 𝑦 ) )
14	13	eqeq2d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑛 +s 1s ) = ( 2s ·s 𝑥 ) ↔ ( 𝑛 +s 1s ) = ( 2s ·s 𝑦 ) ) )
15	14	cbvrexvw	⊢ ( ∃ 𝑥 ∈ ℕ0s ( 𝑛 +s 1s ) = ( 2s ·s 𝑥 ) ↔ ∃ 𝑦 ∈ ℕ0s ( 𝑛 +s 1s ) = ( 2s ·s 𝑦 ) )
16	12 15	bitrdi	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( ∃ 𝑥 ∈ ℕ0s 𝑚 = ( 2s ·s 𝑥 ) ↔ ∃ 𝑦 ∈ ℕ0s ( 𝑛 +s 1s ) = ( 2s ·s 𝑦 ) ) )
17		eqeq1	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( 𝑚 = ( ( 2s ·s 𝑥 ) +s 1s ) ↔ ( 𝑛 +s 1s ) = ( ( 2s ·s 𝑥 ) +s 1s ) ) )
18	17	rexbidv	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( ∃ 𝑥 ∈ ℕ0s 𝑚 = ( ( 2s ·s 𝑥 ) +s 1s ) ↔ ∃ 𝑥 ∈ ℕ0s ( 𝑛 +s 1s ) = ( ( 2s ·s 𝑥 ) +s 1s ) ) )
19	13	oveq1d	⊢ ( 𝑥 = 𝑦 → ( ( 2s ·s 𝑥 ) +s 1s ) = ( ( 2s ·s 𝑦 ) +s 1s ) )
20	19	eqeq2d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑛 +s 1s ) = ( ( 2s ·s 𝑥 ) +s 1s ) ↔ ( 𝑛 +s 1s ) = ( ( 2s ·s 𝑦 ) +s 1s ) ) )
21	20	cbvrexvw	⊢ ( ∃ 𝑥 ∈ ℕ0s ( 𝑛 +s 1s ) = ( ( 2s ·s 𝑥 ) +s 1s ) ↔ ∃ 𝑦 ∈ ℕ0s ( 𝑛 +s 1s ) = ( ( 2s ·s 𝑦 ) +s 1s ) )
22	18 21	bitrdi	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( ∃ 𝑥 ∈ ℕ0s 𝑚 = ( ( 2s ·s 𝑥 ) +s 1s ) ↔ ∃ 𝑦 ∈ ℕ0s ( 𝑛 +s 1s ) = ( ( 2s ·s 𝑦 ) +s 1s ) ) )
23	16 22	orbi12d	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( ( ∃ 𝑥 ∈ ℕ0s 𝑚 = ( 2s ·s 𝑥 ) ∨ ∃ 𝑥 ∈ ℕ0s 𝑚 = ( ( 2s ·s 𝑥 ) +s 1s ) ) ↔ ( ∃ 𝑦 ∈ ℕ0s ( 𝑛 +s 1s ) = ( 2s ·s 𝑦 ) ∨ ∃ 𝑦 ∈ ℕ0s ( 𝑛 +s 1s ) = ( ( 2s ·s 𝑦 ) +s 1s ) ) ) )
24		eqeq1	⊢ ( 𝑚 = 𝑁 → ( 𝑚 = ( 2s ·s 𝑥 ) ↔ 𝑁 = ( 2s ·s 𝑥 ) ) )
25	24	rexbidv	⊢ ( 𝑚 = 𝑁 → ( ∃ 𝑥 ∈ ℕ0s 𝑚 = ( 2s ·s 𝑥 ) ↔ ∃ 𝑥 ∈ ℕ0s 𝑁 = ( 2s ·s 𝑥 ) ) )
26		eqeq1	⊢ ( 𝑚 = 𝑁 → ( 𝑚 = ( ( 2s ·s 𝑥 ) +s 1s ) ↔ 𝑁 = ( ( 2s ·s 𝑥 ) +s 1s ) ) )
27	26	rexbidv	⊢ ( 𝑚 = 𝑁 → ( ∃ 𝑥 ∈ ℕ0s 𝑚 = ( ( 2s ·s 𝑥 ) +s 1s ) ↔ ∃ 𝑥 ∈ ℕ0s 𝑁 = ( ( 2s ·s 𝑥 ) +s 1s ) ) )
28	25 27	orbi12d	⊢ ( 𝑚 = 𝑁 → ( ( ∃ 𝑥 ∈ ℕ0s 𝑚 = ( 2s ·s 𝑥 ) ∨ ∃ 𝑥 ∈ ℕ0s 𝑚 = ( ( 2s ·s 𝑥 ) +s 1s ) ) ↔ ( ∃ 𝑥 ∈ ℕ0s 𝑁 = ( 2s ·s 𝑥 ) ∨ ∃ 𝑥 ∈ ℕ0s 𝑁 = ( ( 2s ·s 𝑥 ) +s 1s ) ) ) )
29		0n0s	⊢ 0s ∈ ℕ0s
30		2sno	⊢ 2s ∈ No
31		muls01	⊢ ( 2s ∈ No → ( 2s ·s 0s ) = 0s )
32	30 31	ax-mp	⊢ ( 2s ·s 0s ) = 0s
33	32	eqcomi	⊢ 0s = ( 2s ·s 0s )
34		oveq2	⊢ ( 𝑥 = 0s → ( 2s ·s 𝑥 ) = ( 2s ·s 0s ) )
35	34	rspceeqv	⊢ ( ( 0s ∈ ℕ0s ∧ 0s = ( 2s ·s 0s ) ) → ∃ 𝑥 ∈ ℕ0s 0s = ( 2s ·s 𝑥 ) )
36	29 33 35	mp2an	⊢ ∃ 𝑥 ∈ ℕ0s 0s = ( 2s ·s 𝑥 )
37	36	orci	⊢ ( ∃ 𝑥 ∈ ℕ0s 0s = ( 2s ·s 𝑥 ) ∨ ∃ 𝑥 ∈ ℕ0s 0s = ( ( 2s ·s 𝑥 ) +s 1s ) )
38		eqid	⊢ ( ( 2s ·s 𝑥 ) +s 1s ) = ( ( 2s ·s 𝑥 ) +s 1s )
39		oveq2	⊢ ( 𝑦 = 𝑥 → ( 2s ·s 𝑦 ) = ( 2s ·s 𝑥 ) )
40	39	oveq1d	⊢ ( 𝑦 = 𝑥 → ( ( 2s ·s 𝑦 ) +s 1s ) = ( ( 2s ·s 𝑥 ) +s 1s ) )
41	40	rspceeqv	⊢ ( ( 𝑥 ∈ ℕ0s ∧ ( ( 2s ·s 𝑥 ) +s 1s ) = ( ( 2s ·s 𝑥 ) +s 1s ) ) → ∃ 𝑦 ∈ ℕ0s ( ( 2s ·s 𝑥 ) +s 1s ) = ( ( 2s ·s 𝑦 ) +s 1s ) )
42	38 41	mpan2	⊢ ( 𝑥 ∈ ℕ0s → ∃ 𝑦 ∈ ℕ0s ( ( 2s ·s 𝑥 ) +s 1s ) = ( ( 2s ·s 𝑦 ) +s 1s ) )
43		oveq1	⊢ ( 𝑛 = ( 2s ·s 𝑥 ) → ( 𝑛 +s 1s ) = ( ( 2s ·s 𝑥 ) +s 1s ) )
44	43	eqeq1d	⊢ ( 𝑛 = ( 2s ·s 𝑥 ) → ( ( 𝑛 +s 1s ) = ( ( 2s ·s 𝑦 ) +s 1s ) ↔ ( ( 2s ·s 𝑥 ) +s 1s ) = ( ( 2s ·s 𝑦 ) +s 1s ) ) )
45	44	rexbidv	⊢ ( 𝑛 = ( 2s ·s 𝑥 ) → ( ∃ 𝑦 ∈ ℕ0s ( 𝑛 +s 1s ) = ( ( 2s ·s 𝑦 ) +s 1s ) ↔ ∃ 𝑦 ∈ ℕ0s ( ( 2s ·s 𝑥 ) +s 1s ) = ( ( 2s ·s 𝑦 ) +s 1s ) ) )
46	42 45	syl5ibrcom	⊢ ( 𝑥 ∈ ℕ0s → ( 𝑛 = ( 2s ·s 𝑥 ) → ∃ 𝑦 ∈ ℕ0s ( 𝑛 +s 1s ) = ( ( 2s ·s 𝑦 ) +s 1s ) ) )
47	46	rexlimiv	⊢ ( ∃ 𝑥 ∈ ℕ0s 𝑛 = ( 2s ·s 𝑥 ) → ∃ 𝑦 ∈ ℕ0s ( 𝑛 +s 1s ) = ( ( 2s ·s 𝑦 ) +s 1s ) )
48		peano2n0s	⊢ ( 𝑥 ∈ ℕ0s → ( 𝑥 +s 1s ) ∈ ℕ0s )
49		1p1e2s	⊢ ( 1s +s 1s ) = 2s
50		mulsrid	⊢ ( 2s ∈ No → ( 2s ·s 1s ) = 2s )
51	30 50	ax-mp	⊢ ( 2s ·s 1s ) = 2s
52	49 51	eqtr4i	⊢ ( 1s +s 1s ) = ( 2s ·s 1s )
53	52	oveq2i	⊢ ( ( 2s ·s 𝑥 ) +s ( 1s +s 1s ) ) = ( ( 2s ·s 𝑥 ) +s ( 2s ·s 1s ) )
54	30	a1i	⊢ ( 𝑥 ∈ ℕ0s → 2s ∈ No )
55		n0sno	⊢ ( 𝑥 ∈ ℕ0s → 𝑥 ∈ No )
56	54 55	mulscld	⊢ ( 𝑥 ∈ ℕ0s → ( 2s ·s 𝑥 ) ∈ No )
57		1sno	⊢ 1s ∈ No
58	57	a1i	⊢ ( 𝑥 ∈ ℕ0s → 1s ∈ No )
59	56 58 58	addsassd	⊢ ( 𝑥 ∈ ℕ0s → ( ( ( 2s ·s 𝑥 ) +s 1s ) +s 1s ) = ( ( 2s ·s 𝑥 ) +s ( 1s +s 1s ) ) )
60	54 55 58	addsdid	⊢ ( 𝑥 ∈ ℕ0s → ( 2s ·s ( 𝑥 +s 1s ) ) = ( ( 2s ·s 𝑥 ) +s ( 2s ·s 1s ) ) )
61	53 59 60	3eqtr4a	⊢ ( 𝑥 ∈ ℕ0s → ( ( ( 2s ·s 𝑥 ) +s 1s ) +s 1s ) = ( 2s ·s ( 𝑥 +s 1s ) ) )
62		oveq2	⊢ ( 𝑦 = ( 𝑥 +s 1s ) → ( 2s ·s 𝑦 ) = ( 2s ·s ( 𝑥 +s 1s ) ) )
63	62	rspceeqv	⊢ ( ( ( 𝑥 +s 1s ) ∈ ℕ0s ∧ ( ( ( 2s ·s 𝑥 ) +s 1s ) +s 1s ) = ( 2s ·s ( 𝑥 +s 1s ) ) ) → ∃ 𝑦 ∈ ℕ0s ( ( ( 2s ·s 𝑥 ) +s 1s ) +s 1s ) = ( 2s ·s 𝑦 ) )
64	48 61 63	syl2anc	⊢ ( 𝑥 ∈ ℕ0s → ∃ 𝑦 ∈ ℕ0s ( ( ( 2s ·s 𝑥 ) +s 1s ) +s 1s ) = ( 2s ·s 𝑦 ) )
65		oveq1	⊢ ( 𝑛 = ( ( 2s ·s 𝑥 ) +s 1s ) → ( 𝑛 +s 1s ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) +s 1s ) )
66	65	eqeq1d	⊢ ( 𝑛 = ( ( 2s ·s 𝑥 ) +s 1s ) → ( ( 𝑛 +s 1s ) = ( 2s ·s 𝑦 ) ↔ ( ( ( 2s ·s 𝑥 ) +s 1s ) +s 1s ) = ( 2s ·s 𝑦 ) ) )
67	66	rexbidv	⊢ ( 𝑛 = ( ( 2s ·s 𝑥 ) +s 1s ) → ( ∃ 𝑦 ∈ ℕ0s ( 𝑛 +s 1s ) = ( 2s ·s 𝑦 ) ↔ ∃ 𝑦 ∈ ℕ0s ( ( ( 2s ·s 𝑥 ) +s 1s ) +s 1s ) = ( 2s ·s 𝑦 ) ) )
68	64 67	syl5ibrcom	⊢ ( 𝑥 ∈ ℕ0s → ( 𝑛 = ( ( 2s ·s 𝑥 ) +s 1s ) → ∃ 𝑦 ∈ ℕ0s ( 𝑛 +s 1s ) = ( 2s ·s 𝑦 ) ) )
69	68	rexlimiv	⊢ ( ∃ 𝑥 ∈ ℕ0s 𝑛 = ( ( 2s ·s 𝑥 ) +s 1s ) → ∃ 𝑦 ∈ ℕ0s ( 𝑛 +s 1s ) = ( 2s ·s 𝑦 ) )
70	47 69	orim12i	⊢ ( ( ∃ 𝑥 ∈ ℕ0s 𝑛 = ( 2s ·s 𝑥 ) ∨ ∃ 𝑥 ∈ ℕ0s 𝑛 = ( ( 2s ·s 𝑥 ) +s 1s ) ) → ( ∃ 𝑦 ∈ ℕ0s ( 𝑛 +s 1s ) = ( ( 2s ·s 𝑦 ) +s 1s ) ∨ ∃ 𝑦 ∈ ℕ0s ( 𝑛 +s 1s ) = ( 2s ·s 𝑦 ) ) )
71	70	orcomd	⊢ ( ( ∃ 𝑥 ∈ ℕ0s 𝑛 = ( 2s ·s 𝑥 ) ∨ ∃ 𝑥 ∈ ℕ0s 𝑛 = ( ( 2s ·s 𝑥 ) +s 1s ) ) → ( ∃ 𝑦 ∈ ℕ0s ( 𝑛 +s 1s ) = ( 2s ·s 𝑦 ) ∨ ∃ 𝑦 ∈ ℕ0s ( 𝑛 +s 1s ) = ( ( 2s ·s 𝑦 ) +s 1s ) ) )
72	71	a1i	⊢ ( 𝑛 ∈ ℕ0s → ( ( ∃ 𝑥 ∈ ℕ0s 𝑛 = ( 2s ·s 𝑥 ) ∨ ∃ 𝑥 ∈ ℕ0s 𝑛 = ( ( 2s ·s 𝑥 ) +s 1s ) ) → ( ∃ 𝑦 ∈ ℕ0s ( 𝑛 +s 1s ) = ( 2s ·s 𝑦 ) ∨ ∃ 𝑦 ∈ ℕ0s ( 𝑛 +s 1s ) = ( ( 2s ·s 𝑦 ) +s 1s ) ) ) )
73	5 10 23 28 37 72	n0sind	⊢ ( 𝑁 ∈ ℕ0s → ( ∃ 𝑥 ∈ ℕ0s 𝑁 = ( 2s ·s 𝑥 ) ∨ ∃ 𝑥 ∈ ℕ0s 𝑁 = ( ( 2s ·s 𝑥 ) +s 1s ) ) )