Theorem halfcut

Description: Relate the cut of twice of two numbers to the cut of the numbers. Lemma 4.2 of Gonshor p. 28. (Contributed by Scott Fenton, 7-Aug-2025) Avoid the axiom of infinity. (Proof modified by Scott Fenton, 6-Sep-2025.)

	Ref	Expression
Hypotheses	halfcut.1	$$⊢\phi \to A\in \mathrm{No}$$
	halfcut.2	$$⊢\phi \to B\in \mathrm{No}$$
	halfcut.3	$$⊢\phi \to A{<}_{s}B$$
	halfcut.4	No typesetting found for |- ( ph -> ( { ( 2s x.s A ) } |s { ( 2s x.s B ) } ) = ( A +s B ) ) with typecode |-
	halfcut.5	$$⊢C=\left\{A\right\}{|}_s\left\{B\right\}$$
Assertion	halfcut	Could not format assertion : No typesetting found for |- ( ph -> C = ( ( A +s B ) /su 2s ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		halfcut.1	$$⊢\phi \to A\in \mathrm{No}$$
2		halfcut.2	$$⊢\phi \to B\in \mathrm{No}$$
3		halfcut.3	$$⊢\phi \to A{<}_{s}B$$
4		halfcut.4	Could not format ( ph -> ( { ( 2s x.s A ) } |s { ( 2s x.s B ) } ) = ( A +s B ) ) : No typesetting found for |- ( ph -> ( { ( 2s x.s A ) } |s { ( 2s x.s B ) } ) = ( A +s B ) ) with typecode |-
5		halfcut.5	$$⊢C=\left\{A\right\}{|}_s\left\{B\right\}$$
6	1 2 3	sltssn	$$⊢\phi \to \left\{A\right\}{\ll }_s\left\{B\right\}$$
7	6	cutscld	$$⊢\phi \to \left\{A\right\}{|}_s\left\{B\right\}\in \mathrm{No}$$
8	5 7	eqeltrid	$$⊢\phi \to C\in \mathrm{No}$$
9		no2times	Could not format ( C e. No -> ( 2s x.s C ) = ( C +s C ) ) : No typesetting found for |- ( C e. No -> ( 2s x.s C ) = ( C +s C ) ) with typecode |-
10	8 9	syl	Could not format ( ph -> ( 2s x.s C ) = ( C +s C ) ) : No typesetting found for |- ( ph -> ( 2s x.s C ) = ( C +s C ) ) with typecode |-
11	5	a1i	$$⊢\phi \to C=\left\{A\right\}{|}_s\left\{B\right\}$$
12	6 6 11 11	addsunif	$$⊢\phi \to C{+}_{s}C=\left(\left\{x|\exists y\in \left\{A\right\}x=y{+}_{s}C\right\}\cup \left\{x|\exists y\in \left\{A\right\}x=C{+}_{s}y\right\}\right){|}_s\left(\left\{x|\exists y\in \left\{B\right\}x=y{+}_{s}C\right\}\cup \left\{x|\exists y\in \left\{B\right\}x=C{+}_{s}y\right\}\right)$$
13		oveq1	$$⊢y=A\to y{+}_{s}C=A{+}_{s}C$$
14	13	eqeq2d	$$⊢y=A\to \left(x=y{+}_{s}C\leftrightarrow x=A{+}_{s}C\right)$$
15	14	rexsng	$$⊢A\in \mathrm{No}\to \left(\exists y\in \left\{A\right\}x=y{+}_{s}C\leftrightarrow x=A{+}_{s}C\right)$$
16	1 15	syl	$$⊢\phi \to \left(\exists y\in \left\{A\right\}x=y{+}_{s}C\leftrightarrow x=A{+}_{s}C\right)$$
17	16	abbidv	$$⊢\phi \to \left\{x|\exists y\in \left\{A\right\}x=y{+}_{s}C\right\}=\left\{x|x=A{+}_{s}C\right\}$$
18		oveq2	$$⊢y=A\to C{+}_{s}y=C{+}_{s}A$$
19	18	eqeq2d	$$⊢y=A\to \left(x=C{+}_{s}y\leftrightarrow x=C{+}_{s}A\right)$$
20	19	rexsng	$$⊢A\in \mathrm{No}\to \left(\exists y\in \left\{A\right\}x=C{+}_{s}y\leftrightarrow x=C{+}_{s}A\right)$$
21	1 20	syl	$$⊢\phi \to \left(\exists y\in \left\{A\right\}x=C{+}_{s}y\leftrightarrow x=C{+}_{s}A\right)$$
22	8 1	addscomd	$$⊢\phi \to C{+}_{s}A=A{+}_{s}C$$
23	22	eqeq2d	$$⊢\phi \to \left(x=C{+}_{s}A\leftrightarrow x=A{+}_{s}C\right)$$
24	21 23	bitrd	$$⊢\phi \to \left(\exists y\in \left\{A\right\}x=C{+}_{s}y\leftrightarrow x=A{+}_{s}C\right)$$
25	24	abbidv	$$⊢\phi \to \left\{x|\exists y\in \left\{A\right\}x=C{+}_{s}y\right\}=\left\{x|x=A{+}_{s}C\right\}$$
26	17 25	uneq12d	$$⊢\phi \to \left\{x|\exists y\in \left\{A\right\}x=y{+}_{s}C\right\}\cup \left\{x|\exists y\in \left\{A\right\}x=C{+}_{s}y\right\}=\left\{x|x=A{+}_{s}C\right\}\cup \left\{x|x=A{+}_{s}C\right\}$$
27		df-sn	$$⊢\left\{A{+}_{s}C\right\}=\left\{x|x=A{+}_{s}C\right\}$$
28		unidm	$$⊢\left\{x|x=A{+}_{s}C\right\}\cup \left\{x|x=A{+}_{s}C\right\}=\left\{x|x=A{+}_{s}C\right\}$$
29	27 28	eqtr4i	$$⊢\left\{A{+}_{s}C\right\}=\left\{x|x=A{+}_{s}C\right\}\cup \left\{x|x=A{+}_{s}C\right\}$$
30	26 29	eqtr4di	$$⊢\phi \to \left\{x|\exists y\in \left\{A\right\}x=y{+}_{s}C\right\}\cup \left\{x|\exists y\in \left\{A\right\}x=C{+}_{s}y\right\}=\left\{A{+}_{s}C\right\}$$
31		oveq1	$$⊢y=B\to y{+}_{s}C=B{+}_{s}C$$
32	31	eqeq2d	$$⊢y=B\to \left(x=y{+}_{s}C\leftrightarrow x=B{+}_{s}C\right)$$
33	32	rexsng	$$⊢B\in \mathrm{No}\to \left(\exists y\in \left\{B\right\}x=y{+}_{s}C\leftrightarrow x=B{+}_{s}C\right)$$
34	2 33	syl	$$⊢\phi \to \left(\exists y\in \left\{B\right\}x=y{+}_{s}C\leftrightarrow x=B{+}_{s}C\right)$$
35	34	abbidv	$$⊢\phi \to \left\{x|\exists y\in \left\{B\right\}x=y{+}_{s}C\right\}=\left\{x|x=B{+}_{s}C\right\}$$
36		oveq2	$$⊢y=B\to C{+}_{s}y=C{+}_{s}B$$
37	36	eqeq2d	$$⊢y=B\to \left(x=C{+}_{s}y\leftrightarrow x=C{+}_{s}B\right)$$
38	37	rexsng	$$⊢B\in \mathrm{No}\to \left(\exists y\in \left\{B\right\}x=C{+}_{s}y\leftrightarrow x=C{+}_{s}B\right)$$
39	2 38	syl	$$⊢\phi \to \left(\exists y\in \left\{B\right\}x=C{+}_{s}y\leftrightarrow x=C{+}_{s}B\right)$$
40	8 2	addscomd	$$⊢\phi \to C{+}_{s}B=B{+}_{s}C$$
41	40	eqeq2d	$$⊢\phi \to \left(x=C{+}_{s}B\leftrightarrow x=B{+}_{s}C\right)$$
42	39 41	bitrd	$$⊢\phi \to \left(\exists y\in \left\{B\right\}x=C{+}_{s}y\leftrightarrow x=B{+}_{s}C\right)$$
43	42	abbidv	$$⊢\phi \to \left\{x|\exists y\in \left\{B\right\}x=C{+}_{s}y\right\}=\left\{x|x=B{+}_{s}C\right\}$$
44	35 43	uneq12d	$$⊢\phi \to \left\{x|\exists y\in \left\{B\right\}x=y{+}_{s}C\right\}\cup \left\{x|\exists y\in \left\{B\right\}x=C{+}_{s}y\right\}=\left\{x|x=B{+}_{s}C\right\}\cup \left\{x|x=B{+}_{s}C\right\}$$
45		df-sn	$$⊢\left\{B{+}_{s}C\right\}=\left\{x|x=B{+}_{s}C\right\}$$
46		unidm	$$⊢\left\{x|x=B{+}_{s}C\right\}\cup \left\{x|x=B{+}_{s}C\right\}=\left\{x|x=B{+}_{s}C\right\}$$
47	45 46	eqtr4i	$$⊢\left\{B{+}_{s}C\right\}=\left\{x|x=B{+}_{s}C\right\}\cup \left\{x|x=B{+}_{s}C\right\}$$
48	44 47	eqtr4di	$$⊢\phi \to \left\{x|\exists y\in \left\{B\right\}x=y{+}_{s}C\right\}\cup \left\{x|\exists y\in \left\{B\right\}x=C{+}_{s}y\right\}=\left\{B{+}_{s}C\right\}$$
49	30 48	oveq12d	$$⊢\phi \to \left(\left\{x|\exists y\in \left\{A\right\}x=y{+}_{s}C\right\}\cup \left\{x|\exists y\in \left\{A\right\}x=C{+}_{s}y\right\}\right){|}_s\left(\left\{x|\exists y\in \left\{B\right\}x=y{+}_{s}C\right\}\cup \left\{x|\exists y\in \left\{B\right\}x=C{+}_{s}y\right\}\right)=\left\{A{+}_{s}C\right\}{|}_s\left\{B{+}_{s}C\right\}$$
50		2no	Could not format 2s e. No : No typesetting found for |- 2s e. No with typecode |-
51	50	a1i	Could not format ( ph -> 2s e. No ) : No typesetting found for |- ( ph -> 2s e. No ) with typecode |-
52	51 1	mulscld	Could not format ( ph -> ( 2s x.s A ) e. No ) : No typesetting found for |- ( ph -> ( 2s x.s A ) e. No ) with typecode |-
53	51 2	mulscld	Could not format ( ph -> ( 2s x.s B ) e. No ) : No typesetting found for |- ( ph -> ( 2s x.s B ) e. No ) with typecode |-
54		2nns	Could not format 2s e. NN_s : No typesetting found for |- 2s e. NN_s with typecode |-
55		nnsgt0	Could not format ( 2s e. NN_s -> 0s 0s
56	54 55	mp1i	Could not format ( ph -> 0s 0s
57	1 2 51 56	ltmuls2d	Could not format ( ph -> ( A ( 2s x.s A ) ( A ( 2s x.s A )
58	3 57	mpbid	Could not format ( ph -> ( 2s x.s A ) ( 2s x.s A )
59	52 53 58	sltssn	Could not format ( ph -> { ( 2s x.s A ) } < { ( 2s x.s A ) } <
60		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 |-
61	1 60	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 |-
62		lesid	$$⊢A\in \mathrm{No}\to A{\le }_{s}A$$
63	1 62	syl	$$⊢\phi \to A{\le }_{s}A$$
64		breq2	$$⊢x=A\to \left(A{\le }_{s}x\leftrightarrow A{\le }_{s}A\right)$$
65	64	rexsng	$$⊢A\in \mathrm{No}\to \left(\exists x\in \left\{A\right\}A{\le }_{s}x\leftrightarrow A{\le }_{s}A\right)$$
66	1 65	syl	$$⊢\phi \to \left(\exists x\in \left\{A\right\}A{\le }_{s}x\leftrightarrow A{\le }_{s}A\right)$$
67	63 66	mpbird	$$⊢\phi \to \exists x\in \left\{A\right\}A{\le }_{s}x$$
68	67	orcd	$$⊢\phi \to \left(\exists x\in \left\{A\right\}A{\le }_{s}x\vee \exists y\in R\left(A\right)y{\le }_{s}C\right)$$
69		lltr	$$⊢L\left(A\right){\ll }_{s}R\left(A\right)$$
70	69	a1i	$$⊢\phi \to L\left(A\right){\ll }_{s}R\left(A\right)$$
71		lrcut	$$⊢A\in \mathrm{No}\to L\left(A\right){|}_{s}R\left(A\right)=A$$
72	1 71	syl	$$⊢\phi \to L\left(A\right){|}_{s}R\left(A\right)=A$$
73	72	eqcomd	$$⊢\phi \to A=L\left(A\right){|}_{s}R\left(A\right)$$
74	70 6 73 11	ltsrecd	$$⊢\phi \to \left(A{<}_{s}C\leftrightarrow \left(\exists x\in \left\{A\right\}A{\le }_{s}x\vee \exists y\in R\left(A\right)y{\le }_{s}C\right)\right)$$
75	68 74	mpbird	$$⊢\phi \to A{<}_{s}C$$
76	1 8 75	ltlesd	$$⊢\phi \to A{\le }_{s}C$$
77	1 8 1	leadds2d	$$⊢\phi \to \left(A{\le }_{s}C\leftrightarrow \left(A{+}_{s}A\right){\le }_s\left(A{+}_{s}C\right)\right)$$
78	76 77	mpbid	$$⊢\phi \to \left(A{+}_{s}A\right){\le }_s\left(A{+}_{s}C\right)$$
79	61 78	eqbrtrd	Could not format ( ph -> ( 2s x.s A ) <_s ( A +s C ) ) : No typesetting found for |- ( ph -> ( 2s x.s A ) <_s ( A +s C ) ) with typecode |-
80		ovex	Could not format ( 2s x.s A ) e. _V : No typesetting found for |- ( 2s x.s A ) e. _V with typecode |-
81		breq1	Could not format ( x = ( 2s x.s A ) -> ( x <_s y <-> ( 2s x.s A ) <_s y ) ) : No typesetting found for |- ( x = ( 2s x.s A ) -> ( x <_s y <-> ( 2s x.s A ) <_s y ) ) with typecode |-
82	81	rexbidv	Could not format ( x = ( 2s x.s A ) -> ( E. y e. { ( A +s C ) } x <_s y <-> E. y e. { ( A +s C ) } ( 2s x.s A ) <_s y ) ) : No typesetting found for |- ( x = ( 2s x.s A ) -> ( E. y e. { ( A +s C ) } x <_s y <-> E. y e. { ( A +s C ) } ( 2s x.s A ) <_s y ) ) with typecode |-
83	80 82	ralsn	Could not format ( A. x e. { ( 2s x.s A ) } E. y e. { ( A +s C ) } x <_s y <-> E. y e. { ( A +s C ) } ( 2s x.s A ) <_s y ) : No typesetting found for |- ( A. x e. { ( 2s x.s A ) } E. y e. { ( A +s C ) } x <_s y <-> E. y e. { ( A +s C ) } ( 2s x.s A ) <_s y ) with typecode |-
84		ovex	$$⊢A{+}_{s}C\in \mathrm{V}$$
85		breq2	Could not format ( y = ( A +s C ) -> ( ( 2s x.s A ) <_s y <-> ( 2s x.s A ) <_s ( A +s C ) ) ) : No typesetting found for |- ( y = ( A +s C ) -> ( ( 2s x.s A ) <_s y <-> ( 2s x.s A ) <_s ( A +s C ) ) ) with typecode |-
86	84 85	rexsn	Could not format ( E. y e. { ( A +s C ) } ( 2s x.s A ) <_s y <-> ( 2s x.s A ) <_s ( A +s C ) ) : No typesetting found for |- ( E. y e. { ( A +s C ) } ( 2s x.s A ) <_s y <-> ( 2s x.s A ) <_s ( A +s C ) ) with typecode |-
87	83 86	bitri	Could not format ( A. x e. { ( 2s x.s A ) } E. y e. { ( A +s C ) } x <_s y <-> ( 2s x.s A ) <_s ( A +s C ) ) : No typesetting found for |- ( A. x e. { ( 2s x.s A ) } E. y e. { ( A +s C ) } x <_s y <-> ( 2s x.s A ) <_s ( A +s C ) ) with typecode |-
88	79 87	sylibr	Could not format ( ph -> A. x e. { ( 2s x.s A ) } E. y e. { ( A +s C ) } x <_s y ) : No typesetting found for |- ( ph -> A. x e. { ( 2s x.s A ) } E. y e. { ( A +s C ) } x <_s y ) with typecode |-
89		lesid	$$⊢B\in \mathrm{No}\to B{\le }_{s}B$$
90	2 89	syl	$$⊢\phi \to B{\le }_{s}B$$
91		breq1	$$⊢y=B\to \left(y{\le }_{s}B\leftrightarrow B{\le }_{s}B\right)$$
92	91	rexsng	$$⊢B\in \mathrm{No}\to \left(\exists y\in \left\{B\right\}y{\le }_{s}B\leftrightarrow B{\le }_{s}B\right)$$
93	2 92	syl	$$⊢\phi \to \left(\exists y\in \left\{B\right\}y{\le }_{s}B\leftrightarrow B{\le }_{s}B\right)$$
94	90 93	mpbird	$$⊢\phi \to \exists y\in \left\{B\right\}y{\le }_{s}B$$
95	94	olcd	$$⊢\phi \to \left(\exists x\in L\left(B\right)C{\le }_{s}x\vee \exists y\in \left\{B\right\}y{\le }_{s}B\right)$$
96		lltr	$$⊢L\left(B\right){\ll }_{s}R\left(B\right)$$
97	96	a1i	$$⊢\phi \to L\left(B\right){\ll }_{s}R\left(B\right)$$
98		lrcut	$$⊢B\in \mathrm{No}\to L\left(B\right){|}_{s}R\left(B\right)=B$$
99	2 98	syl	$$⊢\phi \to L\left(B\right){|}_{s}R\left(B\right)=B$$
100	99	eqcomd	$$⊢\phi \to B=L\left(B\right){|}_{s}R\left(B\right)$$
101	6 97 11 100	ltsrecd	$$⊢\phi \to \left(C{<}_{s}B\leftrightarrow \left(\exists x\in L\left(B\right)C{\le }_{s}x\vee \exists y\in \left\{B\right\}y{\le }_{s}B\right)\right)$$
102	95 101	mpbird	$$⊢\phi \to C{<}_{s}B$$
103	8 2 102	ltlesd	$$⊢\phi \to C{\le }_{s}B$$
104	8 2 2	leadds2d	$$⊢\phi \to \left(C{\le }_{s}B\leftrightarrow \left(B{+}_{s}C\right){\le }_s\left(B{+}_{s}B\right)\right)$$
105	103 104	mpbid	$$⊢\phi \to \left(B{+}_{s}C\right){\le }_s\left(B{+}_{s}B\right)$$
106		no2times	Could not format ( B e. No -> ( 2s x.s B ) = ( B +s B ) ) : No typesetting found for |- ( B e. No -> ( 2s x.s B ) = ( B +s B ) ) with typecode |-
107	2 106	syl	Could not format ( ph -> ( 2s x.s B ) = ( B +s B ) ) : No typesetting found for |- ( ph -> ( 2s x.s B ) = ( B +s B ) ) with typecode |-
108	105 107	breqtrrd	Could not format ( ph -> ( B +s C ) <_s ( 2s x.s B ) ) : No typesetting found for |- ( ph -> ( B +s C ) <_s ( 2s x.s B ) ) with typecode |-
109		ovex	Could not format ( 2s x.s B ) e. _V : No typesetting found for |- ( 2s x.s B ) e. _V with typecode |-
110		breq2	Could not format ( x = ( 2s x.s B ) -> ( y <_s x <-> y <_s ( 2s x.s B ) ) ) : No typesetting found for |- ( x = ( 2s x.s B ) -> ( y <_s x <-> y <_s ( 2s x.s B ) ) ) with typecode |-
111	110	rexbidv	Could not format ( x = ( 2s x.s B ) -> ( E. y e. { ( B +s C ) } y <_s x <-> E. y e. { ( B +s C ) } y <_s ( 2s x.s B ) ) ) : No typesetting found for |- ( x = ( 2s x.s B ) -> ( E. y e. { ( B +s C ) } y <_s x <-> E. y e. { ( B +s C ) } y <_s ( 2s x.s B ) ) ) with typecode |-
112	109 111	ralsn	Could not format ( A. x e. { ( 2s x.s B ) } E. y e. { ( B +s C ) } y <_s x <-> E. y e. { ( B +s C ) } y <_s ( 2s x.s B ) ) : No typesetting found for |- ( A. x e. { ( 2s x.s B ) } E. y e. { ( B +s C ) } y <_s x <-> E. y e. { ( B +s C ) } y <_s ( 2s x.s B ) ) with typecode |-
113		ovex	$$⊢B{+}_{s}C\in \mathrm{V}$$
114		breq1	Could not format ( y = ( B +s C ) -> ( y <_s ( 2s x.s B ) <-> ( B +s C ) <_s ( 2s x.s B ) ) ) : No typesetting found for |- ( y = ( B +s C ) -> ( y <_s ( 2s x.s B ) <-> ( B +s C ) <_s ( 2s x.s B ) ) ) with typecode |-
115	113 114	rexsn	Could not format ( E. y e. { ( B +s C ) } y <_s ( 2s x.s B ) <-> ( B +s C ) <_s ( 2s x.s B ) ) : No typesetting found for |- ( E. y e. { ( B +s C ) } y <_s ( 2s x.s B ) <-> ( B +s C ) <_s ( 2s x.s B ) ) with typecode |-
116	112 115	bitri	Could not format ( A. x e. { ( 2s x.s B ) } E. y e. { ( B +s C ) } y <_s x <-> ( B +s C ) <_s ( 2s x.s B ) ) : No typesetting found for |- ( A. x e. { ( 2s x.s B ) } E. y e. { ( B +s C ) } y <_s x <-> ( B +s C ) <_s ( 2s x.s B ) ) with typecode |-
117	108 116	sylibr	Could not format ( ph -> A. x e. { ( 2s x.s B ) } E. y e. { ( B +s C ) } y <_s x ) : No typesetting found for |- ( ph -> A. x e. { ( 2s x.s B ) } E. y e. { ( B +s C ) } y <_s x ) with typecode |-
118	1 8	addscld	$$⊢\phi \to A{+}_{s}C\in \mathrm{No}$$
119	1 2	addscld	$$⊢\phi \to A{+}_{s}B\in \mathrm{No}$$
120	8 2 1	ltadds2d	$$⊢\phi \to \left(C{<}_{s}B\leftrightarrow \left(A{+}_{s}C\right){<}_s\left(A{+}_{s}B\right)\right)$$
121	102 120	mpbid	$$⊢\phi \to \left(A{+}_{s}C\right){<}_s\left(A{+}_{s}B\right)$$
122	118 119 121	sltssn	$$⊢\phi \to \left\{A{+}_{s}C\right\}{\ll }_s\left\{A{+}_{s}B\right\}$$
123	4	sneqd	Could not format ( ph -> { ( { ( 2s x.s A ) } |s { ( 2s x.s B ) } ) } = { ( A +s B ) } ) : No typesetting found for |- ( ph -> { ( { ( 2s x.s A ) } |s { ( 2s x.s B ) } ) } = { ( A +s B ) } ) with typecode |-
124	122 123	breqtrrd	Could not format ( ph -> { ( A +s C ) } < { ( A +s C ) } <
125	2 8	addscld	$$⊢\phi \to B{+}_{s}C\in \mathrm{No}$$
126	2 1	addscomd	$$⊢\phi \to B{+}_{s}A=A{+}_{s}B$$
127	1 8 2	ltadds2d	$$⊢\phi \to \left(A{<}_{s}C\leftrightarrow \left(B{+}_{s}A\right){<}_s\left(B{+}_{s}C\right)\right)$$
128	75 127	mpbid	$$⊢\phi \to \left(B{+}_{s}A\right){<}_s\left(B{+}_{s}C\right)$$
129	126 128	eqbrtrrd	$$⊢\phi \to \left(A{+}_{s}B\right){<}_s\left(B{+}_{s}C\right)$$
130	119 125 129	sltssn	$$⊢\phi \to \left\{A{+}_{s}B\right\}{\ll }_s\left\{B{+}_{s}C\right\}$$
131	123 130	eqbrtrd	Could not format ( ph -> { ( { ( 2s x.s A ) } |s { ( 2s x.s B ) } ) } < { ( { ( 2s x.s A ) } |s { ( 2s x.s B ) } ) } <
132	59 88 117 124 131	cofcut1d	Could not format ( ph -> ( { ( 2s x.s A ) } |s { ( 2s x.s B ) } ) = ( { ( A +s C ) } |s { ( B +s C ) } ) ) : No typesetting found for |- ( ph -> ( { ( 2s x.s A ) } |s { ( 2s x.s B ) } ) = ( { ( A +s C ) } |s { ( B +s C ) } ) ) with typecode |-
133	49 132 4	3eqtr2d	$$⊢\phi \to \left(\left\{x|\exists y\in \left\{A\right\}x=y{+}_{s}C\right\}\cup \left\{x|\exists y\in \left\{A\right\}x=C{+}_{s}y\right\}\right){|}_s\left(\left\{x|\exists y\in \left\{B\right\}x=y{+}_{s}C\right\}\cup \left\{x|\exists y\in \left\{B\right\}x=C{+}_{s}y\right\}\right)=A{+}_{s}B$$
134	12 133	eqtrd	$$⊢\phi \to C{+}_{s}C=A{+}_{s}B$$
135	10 134	eqtrd	Could not format ( ph -> ( 2s x.s C ) = ( A +s B ) ) : No typesetting found for |- ( ph -> ( 2s x.s C ) = ( A +s B ) ) with typecode |-
136		2ne0s	Could not format 2s =/= 0s : No typesetting found for |- 2s =/= 0s with typecode |-
137	136	a1i	Could not format ( ph -> 2s =/= 0s ) : No typesetting found for |- ( ph -> 2s =/= 0s ) with typecode |-
138		0no	$$⊢0_s\in \mathrm{No}$$
139	138	a1i	$$⊢\top \to 0_s\in \mathrm{No}$$
140		1no	$$⊢1_s\in \mathrm{No}$$
141	140	a1i	$$⊢\top \to 1_s\in \mathrm{No}$$
142		0lt1s	$$⊢0_s{<}_s{1}_s$$
143	142	a1i	$$⊢\top \to 0_s{<}_s{1}_s$$
144	139 141 143	sltssn	$$⊢\top \to \left\{0_s\right\}{\ll }_s\left\{1_s\right\}$$
145	144	cutscld	$$⊢\top \to \left\{0_s\right\}{|}_s\left\{1_s\right\}\in \mathrm{No}$$
146	145	mptru	$$⊢\left\{0_s\right\}{|}_s\left\{1_s\right\}\in \mathrm{No}$$
147		twocut	Could not format ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s : No typesetting found for |- ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s with typecode |-
148		oveq2	Could not format ( x = ( { 0s } |s { 1s } ) -> ( 2s x.s x ) = ( 2s x.s ( { 0s } |s { 1s } ) ) ) : No typesetting found for |- ( x = ( { 0s } |s { 1s } ) -> ( 2s x.s x ) = ( 2s x.s ( { 0s } |s { 1s } ) ) ) with typecode |-
149	148	eqeq1d	Could not format ( x = ( { 0s } |s { 1s } ) -> ( ( 2s x.s x ) = 1s <-> ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s ) ) : No typesetting found for |- ( x = ( { 0s } |s { 1s } ) -> ( ( 2s x.s x ) = 1s <-> ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s ) ) with typecode |-
150	149	rspcev	Could not format ( ( ( { 0s } |s { 1s } ) e. No /\ ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s ) -> E. x e. No ( 2s x.s x ) = 1s ) : No typesetting found for |- ( ( ( { 0s } |s { 1s } ) e. No /\ ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s ) -> E. x e. No ( 2s x.s x ) = 1s ) with typecode |-
151	146 147 150	mp2an	Could not format E. x e. No ( 2s x.s x ) = 1s : No typesetting found for |- E. x e. No ( 2s x.s x ) = 1s with typecode |-
152	151	a1i	Could not format ( ph -> E. x e. No ( 2s x.s x ) = 1s ) : No typesetting found for |- ( ph -> E. x e. No ( 2s x.s x ) = 1s ) with typecode |-
153	119 8 51 137 152	divmulswd	Could not format ( ph -> ( ( ( A +s B ) /su 2s ) = C <-> ( 2s x.s C ) = ( A +s B ) ) ) : No typesetting found for |- ( ph -> ( ( ( A +s B ) /su 2s ) = C <-> ( 2s x.s C ) = ( A +s B ) ) ) with typecode |-
154	135 153	mpbird	Could not format ( ph -> ( ( A +s B ) /su 2s ) = C ) : No typesetting found for |- ( ph -> ( ( A +s B ) /su 2s ) = C ) with typecode |-
155	154	eqcomd	Could not format ( ph -> C = ( ( A +s B ) /su 2s ) ) : No typesetting found for |- ( ph -> C = ( ( A +s B ) /su 2s ) ) with typecode |-