Theorem addhalfcut

Description: The cut of a surreal non-negative integer and its successor is the original number plus one half. Part of theorem 4.2 of Gonshor p. 30. (Contributed by Scott Fenton, 13-Aug-2025)

	Ref	Expression
Hypothesis	addhalfcut.1	⊢ ( 𝜑 → 𝐴 ∈ ℕ0s )
Assertion	addhalfcut	⊢ ( 𝜑 → ( { 𝐴 } |s { ( 𝐴 +s 1s ) } ) = ( 𝐴 +s ( 1s /su 2s ) ) )

Proof

Step	Hyp	Ref	Expression
1		addhalfcut.1	⊢ ( 𝜑 → 𝐴 ∈ ℕ0s )
2	1	n0nod	⊢ ( 𝜑 → 𝐴 ∈ No )
3		1no	⊢ 1s ∈ No
4	3	a1i	⊢ ( 𝜑 → 1s ∈ No )
5	2 4	addscld	⊢ ( 𝜑 → ( 𝐴 +s 1s ) ∈ No )
6	2	ltsp1d	⊢ ( 𝜑 → 𝐴 <s ( 𝐴 +s 1s ) )
7		no2times	⊢ ( 𝐴 ∈ No → ( 2s ·s 𝐴 ) = ( 𝐴 +s 𝐴 ) )
8	2 7	syl	⊢ ( 𝜑 → ( 2s ·s 𝐴 ) = ( 𝐴 +s 𝐴 ) )
9	8	oveq1d	⊢ ( 𝜑 → ( ( 2s ·s 𝐴 ) +s 1s ) = ( ( 𝐴 +s 𝐴 ) +s 1s ) )
10	2 2 4	addsassd	⊢ ( 𝜑 → ( ( 𝐴 +s 𝐴 ) +s 1s ) = ( 𝐴 +s ( 𝐴 +s 1s ) ) )
11	9 10	eqtr2d	⊢ ( 𝜑 → ( 𝐴 +s ( 𝐴 +s 1s ) ) = ( ( 2s ·s 𝐴 ) +s 1s ) )
12		2nns	⊢ 2s ∈ ℕs
13		nnn0s	⊢ ( 2s ∈ ℕs → 2s ∈ ℕ0s )
14	12 13	ax-mp	⊢ 2s ∈ ℕ0s
15	14	a1i	⊢ ( 𝜑 → 2s ∈ ℕ0s )
16		n0mulscl	⊢ ( ( 2s ∈ ℕ0s ∧ 𝐴 ∈ ℕ0s ) → ( 2s ·s 𝐴 ) ∈ ℕ0s )
17	15 1 16	syl2anc	⊢ ( 𝜑 → ( 2s ·s 𝐴 ) ∈ ℕ0s )
18		1n0s	⊢ 1s ∈ ℕ0s
19	18	a1i	⊢ ( 𝜑 → 1s ∈ ℕ0s )
20		n0addscl	⊢ ( ( ( 2s ·s 𝐴 ) ∈ ℕ0s ∧ 1s ∈ ℕ0s ) → ( ( 2s ·s 𝐴 ) +s 1s ) ∈ ℕ0s )
21	17 19 20	syl2anc	⊢ ( 𝜑 → ( ( 2s ·s 𝐴 ) +s 1s ) ∈ ℕ0s )
22		n0cut	⊢ ( ( ( 2s ·s 𝐴 ) +s 1s ) ∈ ℕ0s → ( ( 2s ·s 𝐴 ) +s 1s ) = ( { ( ( ( 2s ·s 𝐴 ) +s 1s ) −s 1s ) } |s ∅ ) )
23	21 22	syl	⊢ ( 𝜑 → ( ( 2s ·s 𝐴 ) +s 1s ) = ( { ( ( ( 2s ·s 𝐴 ) +s 1s ) −s 1s ) } |s ∅ ) )
24		2no	⊢ 2s ∈ No
25	24	a1i	⊢ ( 𝜑 → 2s ∈ No )
26	25 2	mulscld	⊢ ( 𝜑 → ( 2s ·s 𝐴 ) ∈ No )
27		pncans	⊢ ( ( ( 2s ·s 𝐴 ) ∈ No ∧ 1s ∈ No ) → ( ( ( 2s ·s 𝐴 ) +s 1s ) −s 1s ) = ( 2s ·s 𝐴 ) )
28	26 4 27	syl2anc	⊢ ( 𝜑 → ( ( ( 2s ·s 𝐴 ) +s 1s ) −s 1s ) = ( 2s ·s 𝐴 ) )
29	28	sneqd	⊢ ( 𝜑 → { ( ( ( 2s ·s 𝐴 ) +s 1s ) −s 1s ) } = { ( 2s ·s 𝐴 ) } )
30	29	oveq1d	⊢ ( 𝜑 → ( { ( ( ( 2s ·s 𝐴 ) +s 1s ) −s 1s ) } |s ∅ ) = ( { ( 2s ·s 𝐴 ) } |s ∅ ) )
31	23 30	eqtrd	⊢ ( 𝜑 → ( ( 2s ·s 𝐴 ) +s 1s ) = ( { ( 2s ·s 𝐴 ) } |s ∅ ) )
32		snelpwi	⊢ ( ( 2s ·s 𝐴 ) ∈ No → { ( 2s ·s 𝐴 ) } ∈ 𝒫 No )
33		nulsgts	⊢ ( { ( 2s ·s 𝐴 ) } ∈ 𝒫 No → { ( 2s ·s 𝐴 ) } <<s ∅ )
34	26 32 33	3syl	⊢ ( 𝜑 → { ( 2s ·s 𝐴 ) } <<s ∅ )
35		lesid	⊢ ( ( 2s ·s 𝐴 ) ∈ No → ( 2s ·s 𝐴 ) ≤s ( 2s ·s 𝐴 ) )
36	26 35	syl	⊢ ( 𝜑 → ( 2s ·s 𝐴 ) ≤s ( 2s ·s 𝐴 ) )
37		ovex	⊢ ( 2s ·s 𝐴 ) ∈ V
38		breq2	⊢ ( 𝑦 = ( 2s ·s 𝐴 ) → ( 𝑥 ≤s 𝑦 ↔ 𝑥 ≤s ( 2s ·s 𝐴 ) ) )
39	37 38	rexsn	⊢ ( ∃ 𝑦 ∈ { ( 2s ·s 𝐴 ) } 𝑥 ≤s 𝑦 ↔ 𝑥 ≤s ( 2s ·s 𝐴 ) )
40	39	ralbii	⊢ ( ∀ 𝑥 ∈ { ( 2s ·s 𝐴 ) } ∃ 𝑦 ∈ { ( 2s ·s 𝐴 ) } 𝑥 ≤s 𝑦 ↔ ∀ 𝑥 ∈ { ( 2s ·s 𝐴 ) } 𝑥 ≤s ( 2s ·s 𝐴 ) )
41		breq1	⊢ ( 𝑥 = ( 2s ·s 𝐴 ) → ( 𝑥 ≤s ( 2s ·s 𝐴 ) ↔ ( 2s ·s 𝐴 ) ≤s ( 2s ·s 𝐴 ) ) )
42	37 41	ralsn	⊢ ( ∀ 𝑥 ∈ { ( 2s ·s 𝐴 ) } 𝑥 ≤s ( 2s ·s 𝐴 ) ↔ ( 2s ·s 𝐴 ) ≤s ( 2s ·s 𝐴 ) )
43	40 42	bitri	⊢ ( ∀ 𝑥 ∈ { ( 2s ·s 𝐴 ) } ∃ 𝑦 ∈ { ( 2s ·s 𝐴 ) } 𝑥 ≤s 𝑦 ↔ ( 2s ·s 𝐴 ) ≤s ( 2s ·s 𝐴 ) )
44	36 43	sylibr	⊢ ( 𝜑 → ∀ 𝑥 ∈ { ( 2s ·s 𝐴 ) } ∃ 𝑦 ∈ { ( 2s ·s 𝐴 ) } 𝑥 ≤s 𝑦 )
45		ral0	⊢ ∀ 𝑥 ∈ ∅ ∃ 𝑦 ∈ { ( 2s ·s ( 𝐴 +s 1s ) ) } 𝑦 ≤s 𝑥
46	45	a1i	⊢ ( 𝜑 → ∀ 𝑥 ∈ ∅ ∃ 𝑦 ∈ { ( 2s ·s ( 𝐴 +s 1s ) ) } 𝑦 ≤s 𝑥 )
47	26 4	addscld	⊢ ( 𝜑 → ( ( 2s ·s 𝐴 ) +s 1s ) ∈ No )
48	26	ltsp1d	⊢ ( 𝜑 → ( 2s ·s 𝐴 ) <s ( ( 2s ·s 𝐴 ) +s 1s ) )
49	26 47 48	sltssn	⊢ ( 𝜑 → { ( 2s ·s 𝐴 ) } <<s { ( ( 2s ·s 𝐴 ) +s 1s ) } )
50	31	sneqd	⊢ ( 𝜑 → { ( ( 2s ·s 𝐴 ) +s 1s ) } = { ( { ( 2s ·s 𝐴 ) } |s ∅ ) } )
51	49 50	breqtrd	⊢ ( 𝜑 → { ( 2s ·s 𝐴 ) } <<s { ( { ( 2s ·s 𝐴 ) } |s ∅ ) } )
52	25 5	mulscld	⊢ ( 𝜑 → ( 2s ·s ( 𝐴 +s 1s ) ) ∈ No )
53	4	ltsp1d	⊢ ( 𝜑 → 1s <s ( 1s +s 1s ) )
54		1p1e2s	⊢ ( 1s +s 1s ) = 2s
55	53 54	breqtrdi	⊢ ( 𝜑 → 1s <s 2s )
56	4 25 26	ltadds2d	⊢ ( 𝜑 → ( 1s <s 2s ↔ ( ( 2s ·s 𝐴 ) +s 1s ) <s ( ( 2s ·s 𝐴 ) +s 2s ) ) )
57	55 56	mpbid	⊢ ( 𝜑 → ( ( 2s ·s 𝐴 ) +s 1s ) <s ( ( 2s ·s 𝐴 ) +s 2s ) )
58	25 2 4	addsdid	⊢ ( 𝜑 → ( 2s ·s ( 𝐴 +s 1s ) ) = ( ( 2s ·s 𝐴 ) +s ( 2s ·s 1s ) ) )
59		mulsrid	⊢ ( 2s ∈ No → ( 2s ·s 1s ) = 2s )
60	24 59	ax-mp	⊢ ( 2s ·s 1s ) = 2s
61	60	oveq2i	⊢ ( ( 2s ·s 𝐴 ) +s ( 2s ·s 1s ) ) = ( ( 2s ·s 𝐴 ) +s 2s )
62	58 61	eqtrdi	⊢ ( 𝜑 → ( 2s ·s ( 𝐴 +s 1s ) ) = ( ( 2s ·s 𝐴 ) +s 2s ) )
63	57 62	breqtrrd	⊢ ( 𝜑 → ( ( 2s ·s 𝐴 ) +s 1s ) <s ( 2s ·s ( 𝐴 +s 1s ) ) )
64	47 52 63	sltssn	⊢ ( 𝜑 → { ( ( 2s ·s 𝐴 ) +s 1s ) } <<s { ( 2s ·s ( 𝐴 +s 1s ) ) } )
65	50 64	eqbrtrrd	⊢ ( 𝜑 → { ( { ( 2s ·s 𝐴 ) } |s ∅ ) } <<s { ( 2s ·s ( 𝐴 +s 1s ) ) } )
66	34 44 46 51 65	cofcut1d	⊢ ( 𝜑 → ( { ( 2s ·s 𝐴 ) } |s ∅ ) = ( { ( 2s ·s 𝐴 ) } |s { ( 2s ·s ( 𝐴 +s 1s ) ) } ) )
67	11 31 66	3eqtrrd	⊢ ( 𝜑 → ( { ( 2s ·s 𝐴 ) } |s { ( 2s ·s ( 𝐴 +s 1s ) ) } ) = ( 𝐴 +s ( 𝐴 +s 1s ) ) )
68		eqid	⊢ ( { 𝐴 } |s { ( 𝐴 +s 1s ) } ) = ( { 𝐴 } |s { ( 𝐴 +s 1s ) } )
69	2 5 6 67 68	halfcut	⊢ ( 𝜑 → ( { 𝐴 } |s { ( 𝐴 +s 1s ) } ) = ( ( 𝐴 +s ( 𝐴 +s 1s ) ) /su 2s ) )
70	11	oveq1d	⊢ ( 𝜑 → ( ( 𝐴 +s ( 𝐴 +s 1s ) ) /su 2s ) = ( ( ( 2s ·s 𝐴 ) +s 1s ) /su 2s ) )
71		2ne0s	⊢ 2s ≠ 0s
72	71	a1i	⊢ ( 𝜑 → 2s ≠ 0s )
73	26 4 25 72	divsdird	⊢ ( 𝜑 → ( ( ( 2s ·s 𝐴 ) +s 1s ) /su 2s ) = ( ( ( 2s ·s 𝐴 ) /su 2s ) +s ( 1s /su 2s ) ) )
74	2 25 72	divscan3d	⊢ ( 𝜑 → ( ( 2s ·s 𝐴 ) /su 2s ) = 𝐴 )
75	74	oveq1d	⊢ ( 𝜑 → ( ( ( 2s ·s 𝐴 ) /su 2s ) +s ( 1s /su 2s ) ) = ( 𝐴 +s ( 1s /su 2s ) ) )
76	73 75	eqtrd	⊢ ( 𝜑 → ( ( ( 2s ·s 𝐴 ) +s 1s ) /su 2s ) = ( 𝐴 +s ( 1s /su 2s ) ) )
77	69 70 76	3eqtrd	⊢ ( 𝜑 → ( { 𝐴 } |s { ( 𝐴 +s 1s ) } ) = ( 𝐴 +s ( 1s /su 2s ) ) )