Theorem zseo

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

	Ref	Expression
Assertion	zseo	⊢ ( 𝑁 ∈ ℤs → ( ∃ 𝑥 ∈ ℤs 𝑁 = ( 2s ·s 𝑥 ) ∨ ∃ 𝑥 ∈ ℤs 𝑁 = ( ( 2s ·s 𝑥 ) +s 1s ) ) )

Proof

Step	Hyp	Ref	Expression
1		elzs	⊢ ( 𝑁 ∈ ℤs ↔ ∃ 𝑦 ∈ ℕs ∃ 𝑧 ∈ ℕs 𝑁 = ( 𝑦 -s 𝑧 ) )
2		nnn0s	⊢ ( 𝑦 ∈ ℕs → 𝑦 ∈ ℕ0s )
3		n0seo	⊢ ( 𝑦 ∈ ℕ0s → ( ∃ 𝑤 ∈ ℕ0s 𝑦 = ( 2s ·s 𝑤 ) ∨ ∃ 𝑤 ∈ ℕ0s 𝑦 = ( ( 2s ·s 𝑤 ) +s 1s ) ) )
4	2 3	syl	⊢ ( 𝑦 ∈ ℕs → ( ∃ 𝑤 ∈ ℕ0s 𝑦 = ( 2s ·s 𝑤 ) ∨ ∃ 𝑤 ∈ ℕ0s 𝑦 = ( ( 2s ·s 𝑤 ) +s 1s ) ) )
5		nnn0s	⊢ ( 𝑧 ∈ ℕs → 𝑧 ∈ ℕ0s )
6		n0seo	⊢ ( 𝑧 ∈ ℕ0s → ( ∃ 𝑡 ∈ ℕ0s 𝑧 = ( 2s ·s 𝑡 ) ∨ ∃ 𝑡 ∈ ℕ0s 𝑧 = ( ( 2s ·s 𝑡 ) +s 1s ) ) )
7	5 6	syl	⊢ ( 𝑧 ∈ ℕs → ( ∃ 𝑡 ∈ ℕ0s 𝑧 = ( 2s ·s 𝑡 ) ∨ ∃ 𝑡 ∈ ℕ0s 𝑧 = ( ( 2s ·s 𝑡 ) +s 1s ) ) )
8		reeanv	⊢ ( ∃ 𝑤 ∈ ℕ0s ∃ 𝑡 ∈ ℕ0s ( 𝑦 = ( 2s ·s 𝑤 ) ∧ 𝑧 = ( 2s ·s 𝑡 ) ) ↔ ( ∃ 𝑤 ∈ ℕ0s 𝑦 = ( 2s ·s 𝑤 ) ∧ ∃ 𝑡 ∈ ℕ0s 𝑧 = ( 2s ·s 𝑡 ) ) )
9		n0zs	⊢ ( 𝑤 ∈ ℕ0s → 𝑤 ∈ ℤs )
10	9	adantr	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → 𝑤 ∈ ℤs )
11		n0zs	⊢ ( 𝑡 ∈ ℕ0s → 𝑡 ∈ ℤs )
12	11	adantl	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → 𝑡 ∈ ℤs )
13	10 12	zsubscld	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → ( 𝑤 -s 𝑡 ) ∈ ℤs )
14		2sno	⊢ 2s ∈ No
15	14	a1i	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → 2s ∈ No )
16		n0sno	⊢ ( 𝑤 ∈ ℕ0s → 𝑤 ∈ No )
17	16	adantr	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → 𝑤 ∈ No )
18		n0sno	⊢ ( 𝑡 ∈ ℕ0s → 𝑡 ∈ No )
19	18	adantl	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → 𝑡 ∈ No )
20	15 17 19	subsdid	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → ( 2s ·s ( 𝑤 -s 𝑡 ) ) = ( ( 2s ·s 𝑤 ) -s ( 2s ·s 𝑡 ) ) )
21	20	eqcomd	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → ( ( 2s ·s 𝑤 ) -s ( 2s ·s 𝑡 ) ) = ( 2s ·s ( 𝑤 -s 𝑡 ) ) )
22		oveq2	⊢ ( 𝑥 = ( 𝑤 -s 𝑡 ) → ( 2s ·s 𝑥 ) = ( 2s ·s ( 𝑤 -s 𝑡 ) ) )
23	22	rspceeqv	⊢ ( ( ( 𝑤 -s 𝑡 ) ∈ ℤs ∧ ( ( 2s ·s 𝑤 ) -s ( 2s ·s 𝑡 ) ) = ( 2s ·s ( 𝑤 -s 𝑡 ) ) ) → ∃ 𝑥 ∈ ℤs ( ( 2s ·s 𝑤 ) -s ( 2s ·s 𝑡 ) ) = ( 2s ·s 𝑥 ) )
24	13 21 23	syl2anc	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → ∃ 𝑥 ∈ ℤs ( ( 2s ·s 𝑤 ) -s ( 2s ·s 𝑡 ) ) = ( 2s ·s 𝑥 ) )
25		oveq12	⊢ ( ( 𝑦 = ( 2s ·s 𝑤 ) ∧ 𝑧 = ( 2s ·s 𝑡 ) ) → ( 𝑦 -s 𝑧 ) = ( ( 2s ·s 𝑤 ) -s ( 2s ·s 𝑡 ) ) )
26	25	eqeq1d	⊢ ( ( 𝑦 = ( 2s ·s 𝑤 ) ∧ 𝑧 = ( 2s ·s 𝑡 ) ) → ( ( 𝑦 -s 𝑧 ) = ( 2s ·s 𝑥 ) ↔ ( ( 2s ·s 𝑤 ) -s ( 2s ·s 𝑡 ) ) = ( 2s ·s 𝑥 ) ) )
27	26	rexbidv	⊢ ( ( 𝑦 = ( 2s ·s 𝑤 ) ∧ 𝑧 = ( 2s ·s 𝑡 ) ) → ( ∃ 𝑥 ∈ ℤs ( 𝑦 -s 𝑧 ) = ( 2s ·s 𝑥 ) ↔ ∃ 𝑥 ∈ ℤs ( ( 2s ·s 𝑤 ) -s ( 2s ·s 𝑡 ) ) = ( 2s ·s 𝑥 ) ) )
28	24 27	syl5ibrcom	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → ( ( 𝑦 = ( 2s ·s 𝑤 ) ∧ 𝑧 = ( 2s ·s 𝑡 ) ) → ∃ 𝑥 ∈ ℤs ( 𝑦 -s 𝑧 ) = ( 2s ·s 𝑥 ) ) )
29	28	rexlimivv	⊢ ( ∃ 𝑤 ∈ ℕ0s ∃ 𝑡 ∈ ℕ0s ( 𝑦 = ( 2s ·s 𝑤 ) ∧ 𝑧 = ( 2s ·s 𝑡 ) ) → ∃ 𝑥 ∈ ℤs ( 𝑦 -s 𝑧 ) = ( 2s ·s 𝑥 ) )
30	8 29	sylbir	⊢ ( ( ∃ 𝑤 ∈ ℕ0s 𝑦 = ( 2s ·s 𝑤 ) ∧ ∃ 𝑡 ∈ ℕ0s 𝑧 = ( 2s ·s 𝑡 ) ) → ∃ 𝑥 ∈ ℤs ( 𝑦 -s 𝑧 ) = ( 2s ·s 𝑥 ) )
31	30	orcd	⊢ ( ( ∃ 𝑤 ∈ ℕ0s 𝑦 = ( 2s ·s 𝑤 ) ∧ ∃ 𝑡 ∈ ℕ0s 𝑧 = ( 2s ·s 𝑡 ) ) → ( ∃ 𝑥 ∈ ℤs ( 𝑦 -s 𝑧 ) = ( 2s ·s 𝑥 ) ∨ ∃ 𝑥 ∈ ℤs ( 𝑦 -s 𝑧 ) = ( ( 2s ·s 𝑥 ) +s 1s ) ) )
32		reeanv	⊢ ( ∃ 𝑤 ∈ ℕ0s ∃ 𝑡 ∈ ℕ0s ( 𝑦 = ( ( 2s ·s 𝑤 ) +s 1s ) ∧ 𝑧 = ( 2s ·s 𝑡 ) ) ↔ ( ∃ 𝑤 ∈ ℕ0s 𝑦 = ( ( 2s ·s 𝑤 ) +s 1s ) ∧ ∃ 𝑡 ∈ ℕ0s 𝑧 = ( 2s ·s 𝑡 ) ) )
33	15 17	mulscld	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → ( 2s ·s 𝑤 ) ∈ No )
34		1sno	⊢ 1s ∈ No
35	34	a1i	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → 1s ∈ No )
36	15 19	mulscld	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → ( 2s ·s 𝑡 ) ∈ No )
37	33 35 36	addsubsd	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → ( ( ( 2s ·s 𝑤 ) +s 1s ) -s ( 2s ·s 𝑡 ) ) = ( ( ( 2s ·s 𝑤 ) -s ( 2s ·s 𝑡 ) ) +s 1s ) )
38	21	oveq1d	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → ( ( ( 2s ·s 𝑤 ) -s ( 2s ·s 𝑡 ) ) +s 1s ) = ( ( 2s ·s ( 𝑤 -s 𝑡 ) ) +s 1s ) )
39	37 38	eqtrd	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → ( ( ( 2s ·s 𝑤 ) +s 1s ) -s ( 2s ·s 𝑡 ) ) = ( ( 2s ·s ( 𝑤 -s 𝑡 ) ) +s 1s ) )
40	22	oveq1d	⊢ ( 𝑥 = ( 𝑤 -s 𝑡 ) → ( ( 2s ·s 𝑥 ) +s 1s ) = ( ( 2s ·s ( 𝑤 -s 𝑡 ) ) +s 1s ) )
41	40	rspceeqv	⊢ ( ( ( 𝑤 -s 𝑡 ) ∈ ℤs ∧ ( ( ( 2s ·s 𝑤 ) +s 1s ) -s ( 2s ·s 𝑡 ) ) = ( ( 2s ·s ( 𝑤 -s 𝑡 ) ) +s 1s ) ) → ∃ 𝑥 ∈ ℤs ( ( ( 2s ·s 𝑤 ) +s 1s ) -s ( 2s ·s 𝑡 ) ) = ( ( 2s ·s 𝑥 ) +s 1s ) )
42	13 39 41	syl2anc	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → ∃ 𝑥 ∈ ℤs ( ( ( 2s ·s 𝑤 ) +s 1s ) -s ( 2s ·s 𝑡 ) ) = ( ( 2s ·s 𝑥 ) +s 1s ) )
43		oveq12	⊢ ( ( 𝑦 = ( ( 2s ·s 𝑤 ) +s 1s ) ∧ 𝑧 = ( 2s ·s 𝑡 ) ) → ( 𝑦 -s 𝑧 ) = ( ( ( 2s ·s 𝑤 ) +s 1s ) -s ( 2s ·s 𝑡 ) ) )
44	43	eqeq1d	⊢ ( ( 𝑦 = ( ( 2s ·s 𝑤 ) +s 1s ) ∧ 𝑧 = ( 2s ·s 𝑡 ) ) → ( ( 𝑦 -s 𝑧 ) = ( ( 2s ·s 𝑥 ) +s 1s ) ↔ ( ( ( 2s ·s 𝑤 ) +s 1s ) -s ( 2s ·s 𝑡 ) ) = ( ( 2s ·s 𝑥 ) +s 1s ) ) )
45	44	rexbidv	⊢ ( ( 𝑦 = ( ( 2s ·s 𝑤 ) +s 1s ) ∧ 𝑧 = ( 2s ·s 𝑡 ) ) → ( ∃ 𝑥 ∈ ℤs ( 𝑦 -s 𝑧 ) = ( ( 2s ·s 𝑥 ) +s 1s ) ↔ ∃ 𝑥 ∈ ℤs ( ( ( 2s ·s 𝑤 ) +s 1s ) -s ( 2s ·s 𝑡 ) ) = ( ( 2s ·s 𝑥 ) +s 1s ) ) )
46	42 45	syl5ibrcom	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → ( ( 𝑦 = ( ( 2s ·s 𝑤 ) +s 1s ) ∧ 𝑧 = ( 2s ·s 𝑡 ) ) → ∃ 𝑥 ∈ ℤs ( 𝑦 -s 𝑧 ) = ( ( 2s ·s 𝑥 ) +s 1s ) ) )
47	46	rexlimivv	⊢ ( ∃ 𝑤 ∈ ℕ0s ∃ 𝑡 ∈ ℕ0s ( 𝑦 = ( ( 2s ·s 𝑤 ) +s 1s ) ∧ 𝑧 = ( 2s ·s 𝑡 ) ) → ∃ 𝑥 ∈ ℤs ( 𝑦 -s 𝑧 ) = ( ( 2s ·s 𝑥 ) +s 1s ) )
48	32 47	sylbir	⊢ ( ( ∃ 𝑤 ∈ ℕ0s 𝑦 = ( ( 2s ·s 𝑤 ) +s 1s ) ∧ ∃ 𝑡 ∈ ℕ0s 𝑧 = ( 2s ·s 𝑡 ) ) → ∃ 𝑥 ∈ ℤs ( 𝑦 -s 𝑧 ) = ( ( 2s ·s 𝑥 ) +s 1s ) )
49	48	olcd	⊢ ( ( ∃ 𝑤 ∈ ℕ0s 𝑦 = ( ( 2s ·s 𝑤 ) +s 1s ) ∧ ∃ 𝑡 ∈ ℕ0s 𝑧 = ( 2s ·s 𝑡 ) ) → ( ∃ 𝑥 ∈ ℤs ( 𝑦 -s 𝑧 ) = ( 2s ·s 𝑥 ) ∨ ∃ 𝑥 ∈ ℤs ( 𝑦 -s 𝑧 ) = ( ( 2s ·s 𝑥 ) +s 1s ) ) )
50		reeanv	⊢ ( ∃ 𝑤 ∈ ℕ0s ∃ 𝑡 ∈ ℕ0s ( 𝑦 = ( 2s ·s 𝑤 ) ∧ 𝑧 = ( ( 2s ·s 𝑡 ) +s 1s ) ) ↔ ( ∃ 𝑤 ∈ ℕ0s 𝑦 = ( 2s ·s 𝑤 ) ∧ ∃ 𝑡 ∈ ℕ0s 𝑧 = ( ( 2s ·s 𝑡 ) +s 1s ) ) )
51		1zs	⊢ 1s ∈ ℤs
52	51	a1i	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → 1s ∈ ℤs )
53	13 52	zsubscld	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → ( ( 𝑤 -s 𝑡 ) -s 1s ) ∈ ℤs )
54	13	znod	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → ( 𝑤 -s 𝑡 ) ∈ No )
55	15 54 35	subsdid	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → ( 2s ·s ( ( 𝑤 -s 𝑡 ) -s 1s ) ) = ( ( 2s ·s ( 𝑤 -s 𝑡 ) ) -s ( 2s ·s 1s ) ) )
56	55	oveq1d	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → ( ( 2s ·s ( ( 𝑤 -s 𝑡 ) -s 1s ) ) +s 1s ) = ( ( ( 2s ·s ( 𝑤 -s 𝑡 ) ) -s ( 2s ·s 1s ) ) +s 1s ) )
57		mulsrid	⊢ ( 2s ∈ No → ( 2s ·s 1s ) = 2s )
58	14 57	ax-mp	⊢ ( 2s ·s 1s ) = 2s
59	58	oveq2i	⊢ ( ( 2s ·s ( 𝑤 -s 𝑡 ) ) -s ( 2s ·s 1s ) ) = ( ( 2s ·s ( 𝑤 -s 𝑡 ) ) -s 2s )
60	59	oveq1i	⊢ ( ( ( 2s ·s ( 𝑤 -s 𝑡 ) ) -s ( 2s ·s 1s ) ) +s 1s ) = ( ( ( 2s ·s ( 𝑤 -s 𝑡 ) ) -s 2s ) +s 1s )
61	15 54	mulscld	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → ( 2s ·s ( 𝑤 -s 𝑡 ) ) ∈ No )
62	61 35 15	addsubsd	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → ( ( ( 2s ·s ( 𝑤 -s 𝑡 ) ) +s 1s ) -s 2s ) = ( ( ( 2s ·s ( 𝑤 -s 𝑡 ) ) -s 2s ) +s 1s ) )
63	61 35 15	addsubsassd	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → ( ( ( 2s ·s ( 𝑤 -s 𝑡 ) ) +s 1s ) -s 2s ) = ( ( 2s ·s ( 𝑤 -s 𝑡 ) ) +s ( 1s -s 2s ) ) )
64	62 63	eqtr3d	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → ( ( ( 2s ·s ( 𝑤 -s 𝑡 ) ) -s 2s ) +s 1s ) = ( ( 2s ·s ( 𝑤 -s 𝑡 ) ) +s ( 1s -s 2s ) ) )
65	60 64	eqtrid	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → ( ( ( 2s ·s ( 𝑤 -s 𝑡 ) ) -s ( 2s ·s 1s ) ) +s 1s ) = ( ( 2s ·s ( 𝑤 -s 𝑡 ) ) +s ( 1s -s 2s ) ) )
66	56 65	eqtrd	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → ( ( 2s ·s ( ( 𝑤 -s 𝑡 ) -s 1s ) ) +s 1s ) = ( ( 2s ·s ( 𝑤 -s 𝑡 ) ) +s ( 1s -s 2s ) ) )
67		subscl	⊢ ( ( 1s ∈ No ∧ 2s ∈ No ) → ( 1s -s 2s ) ∈ No )
68	34 14 67	mp2an	⊢ ( 1s -s 2s ) ∈ No
69		negnegs	⊢ ( ( 1s -s 2s ) ∈ No → ( -us ‘ ( -us ‘ ( 1s -s 2s ) ) ) = ( 1s -s 2s ) )
70	68 69	ax-mp	⊢ ( -us ‘ ( -us ‘ ( 1s -s 2s ) ) ) = ( 1s -s 2s )
71	34	a1i	⊢ ( ⊤ → 1s ∈ No )
72	14	a1i	⊢ ( ⊤ → 2s ∈ No )
73	71 72	negsubsdi2d	⊢ ( ⊤ → ( -us ‘ ( 1s -s 2s ) ) = ( 2s -s 1s ) )
74	73	mptru	⊢ ( -us ‘ ( 1s -s 2s ) ) = ( 2s -s 1s )
75		1p1e2s	⊢ ( 1s +s 1s ) = 2s
76		subadds	⊢ ( ( 2s ∈ No ∧ 1s ∈ No ∧ 1s ∈ No ) → ( ( 2s -s 1s ) = 1s ↔ ( 1s +s 1s ) = 2s ) )
77	14 34 34 76	mp3an	⊢ ( ( 2s -s 1s ) = 1s ↔ ( 1s +s 1s ) = 2s )
78	75 77	mpbir	⊢ ( 2s -s 1s ) = 1s
79	74 78	eqtri	⊢ ( -us ‘ ( 1s -s 2s ) ) = 1s
80	79	fveq2i	⊢ ( -us ‘ ( -us ‘ ( 1s -s 2s ) ) ) = ( -us ‘ 1s )
81	70 80	eqtr3i	⊢ ( 1s -s 2s ) = ( -us ‘ 1s )
82	81	oveq2i	⊢ ( ( 2s ·s ( 𝑤 -s 𝑡 ) ) +s ( 1s -s 2s ) ) = ( ( 2s ·s ( 𝑤 -s 𝑡 ) ) +s ( -us ‘ 1s ) )
83	61 35	subsvald	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → ( ( 2s ·s ( 𝑤 -s 𝑡 ) ) -s 1s ) = ( ( 2s ·s ( 𝑤 -s 𝑡 ) ) +s ( -us ‘ 1s ) ) )
84	82 83	eqtr4id	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → ( ( 2s ·s ( 𝑤 -s 𝑡 ) ) +s ( 1s -s 2s ) ) = ( ( 2s ·s ( 𝑤 -s 𝑡 ) ) -s 1s ) )
85	20	oveq1d	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → ( ( 2s ·s ( 𝑤 -s 𝑡 ) ) -s 1s ) = ( ( ( 2s ·s 𝑤 ) -s ( 2s ·s 𝑡 ) ) -s 1s ) )
86	84 85	eqtrd	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → ( ( 2s ·s ( 𝑤 -s 𝑡 ) ) +s ( 1s -s 2s ) ) = ( ( ( 2s ·s 𝑤 ) -s ( 2s ·s 𝑡 ) ) -s 1s ) )
87	33 36 35	subsubs4d	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → ( ( ( 2s ·s 𝑤 ) -s ( 2s ·s 𝑡 ) ) -s 1s ) = ( ( 2s ·s 𝑤 ) -s ( ( 2s ·s 𝑡 ) +s 1s ) ) )
88	66 86 87	3eqtrrd	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → ( ( 2s ·s 𝑤 ) -s ( ( 2s ·s 𝑡 ) +s 1s ) ) = ( ( 2s ·s ( ( 𝑤 -s 𝑡 ) -s 1s ) ) +s 1s ) )
89		oveq2	⊢ ( 𝑥 = ( ( 𝑤 -s 𝑡 ) -s 1s ) → ( 2s ·s 𝑥 ) = ( 2s ·s ( ( 𝑤 -s 𝑡 ) -s 1s ) ) )
90	89	oveq1d	⊢ ( 𝑥 = ( ( 𝑤 -s 𝑡 ) -s 1s ) → ( ( 2s ·s 𝑥 ) +s 1s ) = ( ( 2s ·s ( ( 𝑤 -s 𝑡 ) -s 1s ) ) +s 1s ) )
91	90	rspceeqv	⊢ ( ( ( ( 𝑤 -s 𝑡 ) -s 1s ) ∈ ℤs ∧ ( ( 2s ·s 𝑤 ) -s ( ( 2s ·s 𝑡 ) +s 1s ) ) = ( ( 2s ·s ( ( 𝑤 -s 𝑡 ) -s 1s ) ) +s 1s ) ) → ∃ 𝑥 ∈ ℤs ( ( 2s ·s 𝑤 ) -s ( ( 2s ·s 𝑡 ) +s 1s ) ) = ( ( 2s ·s 𝑥 ) +s 1s ) )
92	53 88 91	syl2anc	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → ∃ 𝑥 ∈ ℤs ( ( 2s ·s 𝑤 ) -s ( ( 2s ·s 𝑡 ) +s 1s ) ) = ( ( 2s ·s 𝑥 ) +s 1s ) )
93		oveq12	⊢ ( ( 𝑦 = ( 2s ·s 𝑤 ) ∧ 𝑧 = ( ( 2s ·s 𝑡 ) +s 1s ) ) → ( 𝑦 -s 𝑧 ) = ( ( 2s ·s 𝑤 ) -s ( ( 2s ·s 𝑡 ) +s 1s ) ) )
94	93	eqeq1d	⊢ ( ( 𝑦 = ( 2s ·s 𝑤 ) ∧ 𝑧 = ( ( 2s ·s 𝑡 ) +s 1s ) ) → ( ( 𝑦 -s 𝑧 ) = ( ( 2s ·s 𝑥 ) +s 1s ) ↔ ( ( 2s ·s 𝑤 ) -s ( ( 2s ·s 𝑡 ) +s 1s ) ) = ( ( 2s ·s 𝑥 ) +s 1s ) ) )
95	94	rexbidv	⊢ ( ( 𝑦 = ( 2s ·s 𝑤 ) ∧ 𝑧 = ( ( 2s ·s 𝑡 ) +s 1s ) ) → ( ∃ 𝑥 ∈ ℤs ( 𝑦 -s 𝑧 ) = ( ( 2s ·s 𝑥 ) +s 1s ) ↔ ∃ 𝑥 ∈ ℤs ( ( 2s ·s 𝑤 ) -s ( ( 2s ·s 𝑡 ) +s 1s ) ) = ( ( 2s ·s 𝑥 ) +s 1s ) ) )
96	92 95	syl5ibrcom	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → ( ( 𝑦 = ( 2s ·s 𝑤 ) ∧ 𝑧 = ( ( 2s ·s 𝑡 ) +s 1s ) ) → ∃ 𝑥 ∈ ℤs ( 𝑦 -s 𝑧 ) = ( ( 2s ·s 𝑥 ) +s 1s ) ) )
97	96	rexlimivv	⊢ ( ∃ 𝑤 ∈ ℕ0s ∃ 𝑡 ∈ ℕ0s ( 𝑦 = ( 2s ·s 𝑤 ) ∧ 𝑧 = ( ( 2s ·s 𝑡 ) +s 1s ) ) → ∃ 𝑥 ∈ ℤs ( 𝑦 -s 𝑧 ) = ( ( 2s ·s 𝑥 ) +s 1s ) )
98	50 97	sylbir	⊢ ( ( ∃ 𝑤 ∈ ℕ0s 𝑦 = ( 2s ·s 𝑤 ) ∧ ∃ 𝑡 ∈ ℕ0s 𝑧 = ( ( 2s ·s 𝑡 ) +s 1s ) ) → ∃ 𝑥 ∈ ℤs ( 𝑦 -s 𝑧 ) = ( ( 2s ·s 𝑥 ) +s 1s ) )
99	98	olcd	⊢ ( ( ∃ 𝑤 ∈ ℕ0s 𝑦 = ( 2s ·s 𝑤 ) ∧ ∃ 𝑡 ∈ ℕ0s 𝑧 = ( ( 2s ·s 𝑡 ) +s 1s ) ) → ( ∃ 𝑥 ∈ ℤs ( 𝑦 -s 𝑧 ) = ( 2s ·s 𝑥 ) ∨ ∃ 𝑥 ∈ ℤs ( 𝑦 -s 𝑧 ) = ( ( 2s ·s 𝑥 ) +s 1s ) ) )
100		reeanv	⊢ ( ∃ 𝑤 ∈ ℕ0s ∃ 𝑡 ∈ ℕ0s ( 𝑦 = ( ( 2s ·s 𝑤 ) +s 1s ) ∧ 𝑧 = ( ( 2s ·s 𝑡 ) +s 1s ) ) ↔ ( ∃ 𝑤 ∈ ℕ0s 𝑦 = ( ( 2s ·s 𝑤 ) +s 1s ) ∧ ∃ 𝑡 ∈ ℕ0s 𝑧 = ( ( 2s ·s 𝑡 ) +s 1s ) ) )
101	33 35 36 35	addsubs4d	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → ( ( ( 2s ·s 𝑤 ) +s 1s ) -s ( ( 2s ·s 𝑡 ) +s 1s ) ) = ( ( ( 2s ·s 𝑤 ) -s ( 2s ·s 𝑡 ) ) +s ( 1s -s 1s ) ) )
102		subsid	⊢ ( 1s ∈ No → ( 1s -s 1s ) = 0s )
103	34 102	ax-mp	⊢ ( 1s -s 1s ) = 0s
104	103	oveq2i	⊢ ( ( ( 2s ·s 𝑤 ) -s ( 2s ·s 𝑡 ) ) +s ( 1s -s 1s ) ) = ( ( ( 2s ·s 𝑤 ) -s ( 2s ·s 𝑡 ) ) +s 0s )
105	33 36	subscld	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → ( ( 2s ·s 𝑤 ) -s ( 2s ·s 𝑡 ) ) ∈ No )
106	105	addsridd	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → ( ( ( 2s ·s 𝑤 ) -s ( 2s ·s 𝑡 ) ) +s 0s ) = ( ( 2s ·s 𝑤 ) -s ( 2s ·s 𝑡 ) ) )
107	106 21	eqtrd	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → ( ( ( 2s ·s 𝑤 ) -s ( 2s ·s 𝑡 ) ) +s 0s ) = ( 2s ·s ( 𝑤 -s 𝑡 ) ) )
108	104 107	eqtrid	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → ( ( ( 2s ·s 𝑤 ) -s ( 2s ·s 𝑡 ) ) +s ( 1s -s 1s ) ) = ( 2s ·s ( 𝑤 -s 𝑡 ) ) )
109	101 108	eqtrd	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → ( ( ( 2s ·s 𝑤 ) +s 1s ) -s ( ( 2s ·s 𝑡 ) +s 1s ) ) = ( 2s ·s ( 𝑤 -s 𝑡 ) ) )
110	22	rspceeqv	⊢ ( ( ( 𝑤 -s 𝑡 ) ∈ ℤs ∧ ( ( ( 2s ·s 𝑤 ) +s 1s ) -s ( ( 2s ·s 𝑡 ) +s 1s ) ) = ( 2s ·s ( 𝑤 -s 𝑡 ) ) ) → ∃ 𝑥 ∈ ℤs ( ( ( 2s ·s 𝑤 ) +s 1s ) -s ( ( 2s ·s 𝑡 ) +s 1s ) ) = ( 2s ·s 𝑥 ) )
111	13 109 110	syl2anc	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → ∃ 𝑥 ∈ ℤs ( ( ( 2s ·s 𝑤 ) +s 1s ) -s ( ( 2s ·s 𝑡 ) +s 1s ) ) = ( 2s ·s 𝑥 ) )
112		oveq12	⊢ ( ( 𝑦 = ( ( 2s ·s 𝑤 ) +s 1s ) ∧ 𝑧 = ( ( 2s ·s 𝑡 ) +s 1s ) ) → ( 𝑦 -s 𝑧 ) = ( ( ( 2s ·s 𝑤 ) +s 1s ) -s ( ( 2s ·s 𝑡 ) +s 1s ) ) )
113	112	eqeq1d	⊢ ( ( 𝑦 = ( ( 2s ·s 𝑤 ) +s 1s ) ∧ 𝑧 = ( ( 2s ·s 𝑡 ) +s 1s ) ) → ( ( 𝑦 -s 𝑧 ) = ( 2s ·s 𝑥 ) ↔ ( ( ( 2s ·s 𝑤 ) +s 1s ) -s ( ( 2s ·s 𝑡 ) +s 1s ) ) = ( 2s ·s 𝑥 ) ) )
114	113	rexbidv	⊢ ( ( 𝑦 = ( ( 2s ·s 𝑤 ) +s 1s ) ∧ 𝑧 = ( ( 2s ·s 𝑡 ) +s 1s ) ) → ( ∃ 𝑥 ∈ ℤs ( 𝑦 -s 𝑧 ) = ( 2s ·s 𝑥 ) ↔ ∃ 𝑥 ∈ ℤs ( ( ( 2s ·s 𝑤 ) +s 1s ) -s ( ( 2s ·s 𝑡 ) +s 1s ) ) = ( 2s ·s 𝑥 ) ) )
115	111 114	syl5ibrcom	⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑡 ∈ ℕ0s ) → ( ( 𝑦 = ( ( 2s ·s 𝑤 ) +s 1s ) ∧ 𝑧 = ( ( 2s ·s 𝑡 ) +s 1s ) ) → ∃ 𝑥 ∈ ℤs ( 𝑦 -s 𝑧 ) = ( 2s ·s 𝑥 ) ) )
116	115	rexlimivv	⊢ ( ∃ 𝑤 ∈ ℕ0s ∃ 𝑡 ∈ ℕ0s ( 𝑦 = ( ( 2s ·s 𝑤 ) +s 1s ) ∧ 𝑧 = ( ( 2s ·s 𝑡 ) +s 1s ) ) → ∃ 𝑥 ∈ ℤs ( 𝑦 -s 𝑧 ) = ( 2s ·s 𝑥 ) )
117	100 116	sylbir	⊢ ( ( ∃ 𝑤 ∈ ℕ0s 𝑦 = ( ( 2s ·s 𝑤 ) +s 1s ) ∧ ∃ 𝑡 ∈ ℕ0s 𝑧 = ( ( 2s ·s 𝑡 ) +s 1s ) ) → ∃ 𝑥 ∈ ℤs ( 𝑦 -s 𝑧 ) = ( 2s ·s 𝑥 ) )
118	117	orcd	⊢ ( ( ∃ 𝑤 ∈ ℕ0s 𝑦 = ( ( 2s ·s 𝑤 ) +s 1s ) ∧ ∃ 𝑡 ∈ ℕ0s 𝑧 = ( ( 2s ·s 𝑡 ) +s 1s ) ) → ( ∃ 𝑥 ∈ ℤs ( 𝑦 -s 𝑧 ) = ( 2s ·s 𝑥 ) ∨ ∃ 𝑥 ∈ ℤs ( 𝑦 -s 𝑧 ) = ( ( 2s ·s 𝑥 ) +s 1s ) ) )
119	31 49 99 118	ccase	⊢ ( ( ( ∃ 𝑤 ∈ ℕ0s 𝑦 = ( 2s ·s 𝑤 ) ∨ ∃ 𝑤 ∈ ℕ0s 𝑦 = ( ( 2s ·s 𝑤 ) +s 1s ) ) ∧ ( ∃ 𝑡 ∈ ℕ0s 𝑧 = ( 2s ·s 𝑡 ) ∨ ∃ 𝑡 ∈ ℕ0s 𝑧 = ( ( 2s ·s 𝑡 ) +s 1s ) ) ) → ( ∃ 𝑥 ∈ ℤs ( 𝑦 -s 𝑧 ) = ( 2s ·s 𝑥 ) ∨ ∃ 𝑥 ∈ ℤs ( 𝑦 -s 𝑧 ) = ( ( 2s ·s 𝑥 ) +s 1s ) ) )
120	4 7 119	syl2an	⊢ ( ( 𝑦 ∈ ℕs ∧ 𝑧 ∈ ℕs ) → ( ∃ 𝑥 ∈ ℤs ( 𝑦 -s 𝑧 ) = ( 2s ·s 𝑥 ) ∨ ∃ 𝑥 ∈ ℤs ( 𝑦 -s 𝑧 ) = ( ( 2s ·s 𝑥 ) +s 1s ) ) )
121		eqeq1	⊢ ( 𝑁 = ( 𝑦 -s 𝑧 ) → ( 𝑁 = ( 2s ·s 𝑥 ) ↔ ( 𝑦 -s 𝑧 ) = ( 2s ·s 𝑥 ) ) )
122	121	rexbidv	⊢ ( 𝑁 = ( 𝑦 -s 𝑧 ) → ( ∃ 𝑥 ∈ ℤs 𝑁 = ( 2s ·s 𝑥 ) ↔ ∃ 𝑥 ∈ ℤs ( 𝑦 -s 𝑧 ) = ( 2s ·s 𝑥 ) ) )
123		eqeq1	⊢ ( 𝑁 = ( 𝑦 -s 𝑧 ) → ( 𝑁 = ( ( 2s ·s 𝑥 ) +s 1s ) ↔ ( 𝑦 -s 𝑧 ) = ( ( 2s ·s 𝑥 ) +s 1s ) ) )
124	123	rexbidv	⊢ ( 𝑁 = ( 𝑦 -s 𝑧 ) → ( ∃ 𝑥 ∈ ℤs 𝑁 = ( ( 2s ·s 𝑥 ) +s 1s ) ↔ ∃ 𝑥 ∈ ℤs ( 𝑦 -s 𝑧 ) = ( ( 2s ·s 𝑥 ) +s 1s ) ) )
125	122 124	orbi12d	⊢ ( 𝑁 = ( 𝑦 -s 𝑧 ) → ( ( ∃ 𝑥 ∈ ℤs 𝑁 = ( 2s ·s 𝑥 ) ∨ ∃ 𝑥 ∈ ℤs 𝑁 = ( ( 2s ·s 𝑥 ) +s 1s ) ) ↔ ( ∃ 𝑥 ∈ ℤs ( 𝑦 -s 𝑧 ) = ( 2s ·s 𝑥 ) ∨ ∃ 𝑥 ∈ ℤs ( 𝑦 -s 𝑧 ) = ( ( 2s ·s 𝑥 ) +s 1s ) ) ) )
126	120 125	syl5ibrcom	⊢ ( ( 𝑦 ∈ ℕs ∧ 𝑧 ∈ ℕs ) → ( 𝑁 = ( 𝑦 -s 𝑧 ) → ( ∃ 𝑥 ∈ ℤs 𝑁 = ( 2s ·s 𝑥 ) ∨ ∃ 𝑥 ∈ ℤs 𝑁 = ( ( 2s ·s 𝑥 ) +s 1s ) ) ) )
127	126	rexlimivv	⊢ ( ∃ 𝑦 ∈ ℕs ∃ 𝑧 ∈ ℕs 𝑁 = ( 𝑦 -s 𝑧 ) → ( ∃ 𝑥 ∈ ℤs 𝑁 = ( 2s ·s 𝑥 ) ∨ ∃ 𝑥 ∈ ℤs 𝑁 = ( ( 2s ·s 𝑥 ) +s 1s ) ) )
128	1 127	sylbi	⊢ ( 𝑁 ∈ ℤs → ( ∃ 𝑥 ∈ ℤs 𝑁 = ( 2s ·s 𝑥 ) ∨ ∃ 𝑥 ∈ ℤs 𝑁 = ( ( 2s ·s 𝑥 ) +s 1s ) ) )