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	$$⊢\phi \to A\in {\mathbb{N}}_{\mathrm{0s}}$$
Assertion	addhalfcut	Could not format assertion : No typesetting found for |- ( ph -> ( { A } |s { ( A +s 1s ) } ) = ( A +s ( 1s /su 2s ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		addhalfcut.1	$$⊢\phi \to A\in {\mathbb{N}}_{\mathrm{0s}}$$
2	1	n0snod	$$⊢\phi \to A\in \mathrm{No}$$
3		1sno	$$⊢1_s\in \mathrm{No}$$
4	3	a1i	$$⊢\phi \to 1_s\in \mathrm{No}$$
5	2 4	addscld	$$⊢\phi \to A{+}_s{1}_s\in \mathrm{No}$$
6	2	sltp1d	$$⊢\phi \to A{<}_s\left(A{+}_s{1}_s\right)$$
7		no2times	Could not format ( A e. No -> ( 2s x.s A ) = ( A +s A ) ) : No typesetting found for |- ( A e. No -> ( 2s x.s A ) = ( A +s A ) ) with typecode |-
8	2 7	syl	Could not format ( ph -> ( 2s x.s A ) = ( A +s A ) ) : No typesetting found for |- ( ph -> ( 2s x.s A ) = ( A +s A ) ) with typecode |-
9	8	oveq1d	Could not format ( ph -> ( ( 2s x.s A ) +s 1s ) = ( ( A +s A ) +s 1s ) ) : No typesetting found for |- ( ph -> ( ( 2s x.s A ) +s 1s ) = ( ( A +s A ) +s 1s ) ) with typecode |-
10	2 2 4	addsassd	$$⊢\phi \to \left(A{+}_{s}A\right){+}_s{1}_s=A{+}_s\left(A{+}_s{1}_s\right)$$
11	9 10	eqtr2d	Could not format ( ph -> ( A +s ( A +s 1s ) ) = ( ( 2s x.s A ) +s 1s ) ) : No typesetting found for |- ( ph -> ( A +s ( A +s 1s ) ) = ( ( 2s x.s A ) +s 1s ) ) with typecode |-
12		2nns	Could not format 2s e. NN_s : No typesetting found for |- 2s e. NN_s with typecode |-
13		nnn0s	Could not format ( 2s e. NN_s -> 2s e. NN0_s ) : No typesetting found for |- ( 2s e. NN_s -> 2s e. NN0_s ) with typecode |-
14	12 13	ax-mp	Could not format 2s e. NN0_s : No typesetting found for |- 2s e. NN0_s with typecode |-
15	14	a1i	Could not format ( ph -> 2s e. NN0_s ) : No typesetting found for |- ( ph -> 2s e. NN0_s ) with typecode |-
16		n0mulscl	Could not format ( ( 2s e. NN0_s /\ A e. NN0_s ) -> ( 2s x.s A ) e. NN0_s ) : No typesetting found for |- ( ( 2s e. NN0_s /\ A e. NN0_s ) -> ( 2s x.s A ) e. NN0_s ) with typecode |-
17	15 1 16	syl2anc	Could not format ( ph -> ( 2s x.s A ) e. NN0_s ) : No typesetting found for |- ( ph -> ( 2s x.s A ) e. NN0_s ) with typecode |-
18		1n0s	$$⊢1_s\in {\mathbb{N}}_{\mathrm{0s}}$$
19	18	a1i	$$⊢\phi \to 1_s\in {\mathbb{N}}_{\mathrm{0s}}$$
20		n0addscl	Could not format ( ( ( 2s x.s A ) e. NN0_s /\ 1s e. NN0_s ) -> ( ( 2s x.s A ) +s 1s ) e. NN0_s ) : No typesetting found for |- ( ( ( 2s x.s A ) e. NN0_s /\ 1s e. NN0_s ) -> ( ( 2s x.s A ) +s 1s ) e. NN0_s ) with typecode |-
21	17 19 20	syl2anc	Could not format ( ph -> ( ( 2s x.s A ) +s 1s ) e. NN0_s ) : No typesetting found for |- ( ph -> ( ( 2s x.s A ) +s 1s ) e. NN0_s ) with typecode |-
22		n0scut	Could not format ( ( ( 2s x.s A ) +s 1s ) e. NN0_s -> ( ( 2s x.s A ) +s 1s ) = ( { ( ( ( 2s x.s A ) +s 1s ) -s 1s ) } |s (/) ) ) : No typesetting found for |- ( ( ( 2s x.s A ) +s 1s ) e. NN0_s -> ( ( 2s x.s A ) +s 1s ) = ( { ( ( ( 2s x.s A ) +s 1s ) -s 1s ) } |s (/) ) ) with typecode |-
23	21 22	syl	Could not format ( ph -> ( ( 2s x.s A ) +s 1s ) = ( { ( ( ( 2s x.s A ) +s 1s ) -s 1s ) } |s (/) ) ) : No typesetting found for |- ( ph -> ( ( 2s x.s A ) +s 1s ) = ( { ( ( ( 2s x.s A ) +s 1s ) -s 1s ) } |s (/) ) ) with typecode |-
24		2sno	Could not format 2s e. No : No typesetting found for |- 2s e. No with typecode |-
25	24	a1i	Could not format ( ph -> 2s e. No ) : No typesetting found for |- ( ph -> 2s e. No ) with typecode |-
26	25 2	mulscld	Could not format ( ph -> ( 2s x.s A ) e. No ) : No typesetting found for |- ( ph -> ( 2s x.s A ) e. No ) with typecode |-
27		pncans	Could not format ( ( ( 2s x.s A ) e. No /\ 1s e. No ) -> ( ( ( 2s x.s A ) +s 1s ) -s 1s ) = ( 2s x.s A ) ) : No typesetting found for |- ( ( ( 2s x.s A ) e. No /\ 1s e. No ) -> ( ( ( 2s x.s A ) +s 1s ) -s 1s ) = ( 2s x.s A ) ) with typecode |-
28	26 4 27	syl2anc	Could not format ( ph -> ( ( ( 2s x.s A ) +s 1s ) -s 1s ) = ( 2s x.s A ) ) : No typesetting found for |- ( ph -> ( ( ( 2s x.s A ) +s 1s ) -s 1s ) = ( 2s x.s A ) ) with typecode |-
29	28	sneqd	Could not format ( ph -> { ( ( ( 2s x.s A ) +s 1s ) -s 1s ) } = { ( 2s x.s A ) } ) : No typesetting found for |- ( ph -> { ( ( ( 2s x.s A ) +s 1s ) -s 1s ) } = { ( 2s x.s A ) } ) with typecode |-
30	29	oveq1d	Could not format ( ph -> ( { ( ( ( 2s x.s A ) +s 1s ) -s 1s ) } |s (/) ) = ( { ( 2s x.s A ) } |s (/) ) ) : No typesetting found for |- ( ph -> ( { ( ( ( 2s x.s A ) +s 1s ) -s 1s ) } |s (/) ) = ( { ( 2s x.s A ) } |s (/) ) ) with typecode |-
31	23 30	eqtrd	Could not format ( ph -> ( ( 2s x.s A ) +s 1s ) = ( { ( 2s x.s A ) } |s (/) ) ) : No typesetting found for |- ( ph -> ( ( 2s x.s A ) +s 1s ) = ( { ( 2s x.s A ) } |s (/) ) ) with typecode |-
32		snelpwi	Could not format ( ( 2s x.s A ) e. No -> { ( 2s x.s A ) } e. ~P No ) : No typesetting found for |- ( ( 2s x.s A ) e. No -> { ( 2s x.s A ) } e. ~P No ) with typecode |-
33		nulssgt	Could not format ( { ( 2s x.s A ) } e. ~P No -> { ( 2s x.s A ) } < { ( 2s x.s A ) } <
34	26 32 33	3syl	Could not format ( ph -> { ( 2s x.s A ) } < { ( 2s x.s A ) } <
35		slerflex	Could not format ( ( 2s x.s A ) e. No -> ( 2s x.s A ) <_s ( 2s x.s A ) ) : No typesetting found for |- ( ( 2s x.s A ) e. No -> ( 2s x.s A ) <_s ( 2s x.s A ) ) with typecode |-
36	26 35	syl	Could not format ( ph -> ( 2s x.s A ) <_s ( 2s x.s A ) ) : No typesetting found for |- ( ph -> ( 2s x.s A ) <_s ( 2s x.s A ) ) with typecode |-
37		ovex	Could not format ( 2s x.s A ) e. _V : No typesetting found for |- ( 2s x.s A ) e. _V with typecode |-
38		breq2	Could not format ( y = ( 2s x.s A ) -> ( x <_s y <-> x <_s ( 2s x.s A ) ) ) : No typesetting found for |- ( y = ( 2s x.s A ) -> ( x <_s y <-> x <_s ( 2s x.s A ) ) ) with typecode |-
39	37 38	rexsn	Could not format ( E. y e. { ( 2s x.s A ) } x <_s y <-> x <_s ( 2s x.s A ) ) : No typesetting found for |- ( E. y e. { ( 2s x.s A ) } x <_s y <-> x <_s ( 2s x.s A ) ) with typecode |-
40	39	ralbii	Could not format ( A. x e. { ( 2s x.s A ) } E. y e. { ( 2s x.s A ) } x <_s y <-> A. x e. { ( 2s x.s A ) } x <_s ( 2s x.s A ) ) : No typesetting found for |- ( A. x e. { ( 2s x.s A ) } E. y e. { ( 2s x.s A ) } x <_s y <-> A. x e. { ( 2s x.s A ) } x <_s ( 2s x.s A ) ) with typecode |-
41		breq1	Could not format ( x = ( 2s x.s A ) -> ( x <_s ( 2s x.s A ) <-> ( 2s x.s A ) <_s ( 2s x.s A ) ) ) : No typesetting found for |- ( x = ( 2s x.s A ) -> ( x <_s ( 2s x.s A ) <-> ( 2s x.s A ) <_s ( 2s x.s A ) ) ) with typecode |-
42	37 41	ralsn	Could not format ( A. x e. { ( 2s x.s A ) } x <_s ( 2s x.s A ) <-> ( 2s x.s A ) <_s ( 2s x.s A ) ) : No typesetting found for |- ( A. x e. { ( 2s x.s A ) } x <_s ( 2s x.s A ) <-> ( 2s x.s A ) <_s ( 2s x.s A ) ) with typecode |-
43	40 42	bitri	Could not format ( A. x e. { ( 2s x.s A ) } E. y e. { ( 2s x.s A ) } x <_s y <-> ( 2s x.s A ) <_s ( 2s x.s A ) ) : No typesetting found for |- ( A. x e. { ( 2s x.s A ) } E. y e. { ( 2s x.s A ) } x <_s y <-> ( 2s x.s A ) <_s ( 2s x.s A ) ) with typecode |-
44	36 43	sylibr	Could not format ( ph -> A. x e. { ( 2s x.s A ) } E. y e. { ( 2s x.s A ) } x <_s y ) : No typesetting found for |- ( ph -> A. x e. { ( 2s x.s A ) } E. y e. { ( 2s x.s A ) } x <_s y ) with typecode |-
45		ral0	Could not format A. x e. (/) E. y e. { ( 2s x.s ( A +s 1s ) ) } y <_s x : No typesetting found for |- A. x e. (/) E. y e. { ( 2s x.s ( A +s 1s ) ) } y <_s x with typecode |-
46	45	a1i	Could not format ( ph -> A. x e. (/) E. y e. { ( 2s x.s ( A +s 1s ) ) } y <_s x ) : No typesetting found for |- ( ph -> A. x e. (/) E. y e. { ( 2s x.s ( A +s 1s ) ) } y <_s x ) with typecode |-
47	26 4	addscld	Could not format ( ph -> ( ( 2s x.s A ) +s 1s ) e. No ) : No typesetting found for |- ( ph -> ( ( 2s x.s A ) +s 1s ) e. No ) with typecode |-
48	26	sltp1d	Could not format ( ph -> ( 2s x.s A ) ( 2s x.s A )
49	26 47 48	ssltsn	Could not format ( ph -> { ( 2s x.s A ) } < { ( 2s x.s A ) } <
50	31	sneqd	Could not format ( ph -> { ( ( 2s x.s A ) +s 1s ) } = { ( { ( 2s x.s A ) } |s (/) ) } ) : No typesetting found for |- ( ph -> { ( ( 2s x.s A ) +s 1s ) } = { ( { ( 2s x.s A ) } |s (/) ) } ) with typecode |-
51	49 50	breqtrd	Could not format ( ph -> { ( 2s x.s A ) } < { ( 2s x.s A ) } <
52	25 5	mulscld	Could not format ( ph -> ( 2s x.s ( A +s 1s ) ) e. No ) : No typesetting found for |- ( ph -> ( 2s x.s ( A +s 1s ) ) e. No ) with typecode |-
53	4	sltp1d	$$⊢\phi \to 1_s{<}_s\left(1_s{+}_s{1}_s\right)$$
54		1p1e2s	Could not format ( 1s +s 1s ) = 2s : No typesetting found for |- ( 1s +s 1s ) = 2s with typecode |-
55	53 54	breqtrdi	Could not format ( ph -> 1s 1s
56	4 25 26	sltadd2d	Could not format ( ph -> ( 1s ( ( 2s x.s A ) +s 1s ) ( 1s ( ( 2s x.s A ) +s 1s )
57	55 56	mpbid	Could not format ( ph -> ( ( 2s x.s A ) +s 1s ) ( ( 2s x.s A ) +s 1s )
58	25 2 4	addsdid	Could not format ( ph -> ( 2s x.s ( A +s 1s ) ) = ( ( 2s x.s A ) +s ( 2s x.s 1s ) ) ) : No typesetting found for |- ( ph -> ( 2s x.s ( A +s 1s ) ) = ( ( 2s x.s A ) +s ( 2s x.s 1s ) ) ) with typecode |-
59		mulsrid	Could not format ( 2s e. No -> ( 2s x.s 1s ) = 2s ) : No typesetting found for |- ( 2s e. No -> ( 2s x.s 1s ) = 2s ) with typecode |-
60	24 59	ax-mp	Could not format ( 2s x.s 1s ) = 2s : No typesetting found for |- ( 2s x.s 1s ) = 2s with typecode |-
61	60	oveq2i	Could not format ( ( 2s x.s A ) +s ( 2s x.s 1s ) ) = ( ( 2s x.s A ) +s 2s ) : No typesetting found for |- ( ( 2s x.s A ) +s ( 2s x.s 1s ) ) = ( ( 2s x.s A ) +s 2s ) with typecode |-
62	58 61	eqtrdi	Could not format ( ph -> ( 2s x.s ( A +s 1s ) ) = ( ( 2s x.s A ) +s 2s ) ) : No typesetting found for |- ( ph -> ( 2s x.s ( A +s 1s ) ) = ( ( 2s x.s A ) +s 2s ) ) with typecode |-
63	57 62	breqtrrd	Could not format ( ph -> ( ( 2s x.s A ) +s 1s ) ( ( 2s x.s A ) +s 1s )
64	47 52 63	ssltsn	Could not format ( ph -> { ( ( 2s x.s A ) +s 1s ) } < { ( ( 2s x.s A ) +s 1s ) } <
65	50 64	eqbrtrrd	Could not format ( ph -> { ( { ( 2s x.s A ) } |s (/) ) } < { ( { ( 2s x.s A ) } |s (/) ) } <
66	34 44 46 51 65	cofcut1d	Could not format ( ph -> ( { ( 2s x.s A ) } |s (/) ) = ( { ( 2s x.s A ) } |s { ( 2s x.s ( A +s 1s ) ) } ) ) : No typesetting found for |- ( ph -> ( { ( 2s x.s A ) } |s (/) ) = ( { ( 2s x.s A ) } |s { ( 2s x.s ( A +s 1s ) ) } ) ) with typecode |-
67	11 31 66	3eqtrrd	Could not format ( ph -> ( { ( 2s x.s A ) } |s { ( 2s x.s ( A +s 1s ) ) } ) = ( A +s ( A +s 1s ) ) ) : No typesetting found for |- ( ph -> ( { ( 2s x.s A ) } |s { ( 2s x.s ( A +s 1s ) ) } ) = ( A +s ( A +s 1s ) ) ) with typecode |-
68		eqid	$$⊢\left\{A\right\}{|}_s\left\{A{+}_s{1}_s\right\}=\left\{A\right\}{|}_s\left\{A{+}_s{1}_s\right\}$$
69	2 5 6 67 68	halfcut	Could not format ( ph -> ( { A } |s { ( A +s 1s ) } ) = ( ( A +s ( A +s 1s ) ) /su 2s ) ) : No typesetting found for |- ( ph -> ( { A } |s { ( A +s 1s ) } ) = ( ( A +s ( A +s 1s ) ) /su 2s ) ) with typecode |-
70	11	oveq1d	Could not format ( ph -> ( ( A +s ( A +s 1s ) ) /su 2s ) = ( ( ( 2s x.s A ) +s 1s ) /su 2s ) ) : No typesetting found for |- ( ph -> ( ( A +s ( A +s 1s ) ) /su 2s ) = ( ( ( 2s x.s A ) +s 1s ) /su 2s ) ) with typecode |-
71		2ne0s	Could not format 2s =/= 0s : No typesetting found for |- 2s =/= 0s with typecode |-
72	71	a1i	Could not format ( ph -> 2s =/= 0s ) : No typesetting found for |- ( ph -> 2s =/= 0s ) with typecode |-
73	26 4 25 72	divsdird	Could not format ( ph -> ( ( ( 2s x.s A ) +s 1s ) /su 2s ) = ( ( ( 2s x.s A ) /su 2s ) +s ( 1s /su 2s ) ) ) : No typesetting found for |- ( ph -> ( ( ( 2s x.s A ) +s 1s ) /su 2s ) = ( ( ( 2s x.s A ) /su 2s ) +s ( 1s /su 2s ) ) ) with typecode |-
74	2 25 72	divscan3d	Could not format ( ph -> ( ( 2s x.s A ) /su 2s ) = A ) : No typesetting found for |- ( ph -> ( ( 2s x.s A ) /su 2s ) = A ) with typecode |-
75	74	oveq1d	Could not format ( ph -> ( ( ( 2s x.s A ) /su 2s ) +s ( 1s /su 2s ) ) = ( A +s ( 1s /su 2s ) ) ) : No typesetting found for |- ( ph -> ( ( ( 2s x.s A ) /su 2s ) +s ( 1s /su 2s ) ) = ( A +s ( 1s /su 2s ) ) ) with typecode |-
76	73 75	eqtrd	Could not format ( ph -> ( ( ( 2s x.s A ) +s 1s ) /su 2s ) = ( A +s ( 1s /su 2s ) ) ) : No typesetting found for |- ( ph -> ( ( ( 2s x.s A ) +s 1s ) /su 2s ) = ( A +s ( 1s /su 2s ) ) ) with typecode |-
77	69 70 76	3eqtrd	Could not format ( ph -> ( { A } |s { ( A +s 1s ) } ) = ( A +s ( 1s /su 2s ) ) ) : No typesetting found for |- ( ph -> ( { A } |s { ( A +s 1s ) } ) = ( A +s ( 1s /su 2s ) ) ) with typecode |-