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)

	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	ssltsn	$$⊢\phi \to \left\{A\right\}{\ll }_s\left\{B\right\}$$
7	6	scutcld	$$⊢\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		df-sn	$$⊢\left\{A{+}_{s}C\right\}=\left\{x|x=A{+}_{s}C\right\}$$
19	17 18	eqtr4di	$$⊢\phi \to \left\{x|\exists y\in \left\{A\right\}x=y{+}_{s}C\right\}=\left\{A{+}_{s}C\right\}$$
20		oveq2	$$⊢y=A\to C{+}_{s}y=C{+}_{s}A$$
21	20	eqeq2d	$$⊢y=A\to \left(x=C{+}_{s}y\leftrightarrow x=C{+}_{s}A\right)$$
22	21	rexsng	$$⊢A\in \mathrm{No}\to \left(\exists y\in \left\{A\right\}x=C{+}_{s}y\leftrightarrow x=C{+}_{s}A\right)$$
23	1 22	syl	$$⊢\phi \to \left(\exists y\in \left\{A\right\}x=C{+}_{s}y\leftrightarrow x=C{+}_{s}A\right)$$
24	8 1	addscomd	$$⊢\phi \to C{+}_{s}A=A{+}_{s}C$$
25	24	eqeq2d	$$⊢\phi \to \left(x=C{+}_{s}A\leftrightarrow x=A{+}_{s}C\right)$$
26	23 25	bitrd	$$⊢\phi \to \left(\exists y\in \left\{A\right\}x=C{+}_{s}y\leftrightarrow x=A{+}_{s}C\right)$$
27	26	abbidv	$$⊢\phi \to \left\{x|\exists y\in \left\{A\right\}x=C{+}_{s}y\right\}=\left\{x|x=A{+}_{s}C\right\}$$
28	27 18	eqtr4di	$$⊢\phi \to \left\{x|\exists y\in \left\{A\right\}x=C{+}_{s}y\right\}=\left\{A{+}_{s}C\right\}$$
29	19 28	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\{A{+}_{s}C\right\}\cup \left\{A{+}_{s}C\right\}$$
30		unidm	$$⊢\left\{A{+}_{s}C\right\}\cup \left\{A{+}_{s}C\right\}=\left\{A{+}_{s}C\right\}$$
31	29 30	eqtrdi	$$⊢\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\}$$
32		oveq1	$$⊢y=B\to y{+}_{s}C=B{+}_{s}C$$
33	32	eqeq2d	$$⊢y=B\to \left(x=y{+}_{s}C\leftrightarrow x=B{+}_{s}C\right)$$
34	33	rexsng	$$⊢B\in \mathrm{No}\to \left(\exists y\in \left\{B\right\}x=y{+}_{s}C\leftrightarrow x=B{+}_{s}C\right)$$
35	2 34	syl	$$⊢\phi \to \left(\exists y\in \left\{B\right\}x=y{+}_{s}C\leftrightarrow x=B{+}_{s}C\right)$$
36	35	abbidv	$$⊢\phi \to \left\{x|\exists y\in \left\{B\right\}x=y{+}_{s}C\right\}=\left\{x|x=B{+}_{s}C\right\}$$
37		df-sn	$$⊢\left\{B{+}_{s}C\right\}=\left\{x|x=B{+}_{s}C\right\}$$
38	36 37	eqtr4di	$$⊢\phi \to \left\{x|\exists y\in \left\{B\right\}x=y{+}_{s}C\right\}=\left\{B{+}_{s}C\right\}$$
39		oveq2	$$⊢y=B\to C{+}_{s}y=C{+}_{s}B$$
40	39	eqeq2d	$$⊢y=B\to \left(x=C{+}_{s}y\leftrightarrow x=C{+}_{s}B\right)$$
41	40	rexsng	$$⊢B\in \mathrm{No}\to \left(\exists y\in \left\{B\right\}x=C{+}_{s}y\leftrightarrow x=C{+}_{s}B\right)$$
42	2 41	syl	$$⊢\phi \to \left(\exists y\in \left\{B\right\}x=C{+}_{s}y\leftrightarrow x=C{+}_{s}B\right)$$
43	8 2	addscomd	$$⊢\phi \to C{+}_{s}B=B{+}_{s}C$$
44	43	eqeq2d	$$⊢\phi \to \left(x=C{+}_{s}B\leftrightarrow x=B{+}_{s}C\right)$$
45	42 44	bitrd	$$⊢\phi \to \left(\exists y\in \left\{B\right\}x=C{+}_{s}y\leftrightarrow x=B{+}_{s}C\right)$$
46	45	abbidv	$$⊢\phi \to \left\{x|\exists y\in \left\{B\right\}x=C{+}_{s}y\right\}=\left\{x|x=B{+}_{s}C\right\}$$
47	46 37	eqtr4di	$$⊢\phi \to \left\{x|\exists y\in \left\{B\right\}x=C{+}_{s}y\right\}=\left\{B{+}_{s}C\right\}$$
48	38 47	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\{B{+}_{s}C\right\}\cup \left\{B{+}_{s}C\right\}$$
49		unidm	$$⊢\left\{B{+}_{s}C\right\}\cup \left\{B{+}_{s}C\right\}=\left\{B{+}_{s}C\right\}$$
50	48 49	eqtrdi	$$⊢\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\}$$
51	31 50	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\}$$
52		2sno	Could not format 2s e. No : No typesetting found for |- 2s e. No with typecode |-
53	52	a1i	Could not format ( ph -> 2s e. No ) : No typesetting found for |- ( ph -> 2s e. No ) with typecode |-
54	53 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 |-
55	53 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 |-
56		2nns	Could not format 2s e. NN_s : No typesetting found for |- 2s e. NN_s with typecode |-
57		nnsgt0	Could not format ( 2s e. NN_s -> 0s 0s
58	56 57	mp1i	Could not format ( ph -> 0s 0s
59	1 2 53 58	sltmul2d	Could not format ( ph -> ( A ( 2s x.s A ) ( A ( 2s x.s A )
60	3 59	mpbid	Could not format ( ph -> ( 2s x.s A ) ( 2s x.s A )
61	54 55 60	ssltsn	Could not format ( ph -> { ( 2s x.s A ) } < { ( 2s x.s A ) } <
62	1 8	addscld	$$⊢\phi \to A{+}_{s}C\in \mathrm{No}$$
63		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 |-
64	1 63	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 |-
65		slerflex	$$⊢A\in \mathrm{No}\to A{\le }_{s}A$$
66	1 65	syl	$$⊢\phi \to A{\le }_{s}A$$
67		breq2	$$⊢x=A\to \left(A{\le }_{s}x\leftrightarrow A{\le }_{s}A\right)$$
68	67	rexsng	$$⊢A\in \mathrm{No}\to \left(\exists x\in \left\{A\right\}A{\le }_{s}x\leftrightarrow A{\le }_{s}A\right)$$
69	1 68	syl	$$⊢\phi \to \left(\exists x\in \left\{A\right\}A{\le }_{s}x\leftrightarrow A{\le }_{s}A\right)$$
70	66 69	mpbird	$$⊢\phi \to \exists x\in \left\{A\right\}A{\le }_{s}x$$
71	70	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)$$
72		lltropt	$$⊢L\left(A\right){\ll }_{s}R\left(A\right)$$
73	72	a1i	$$⊢\phi \to L\left(A\right){\ll }_{s}R\left(A\right)$$
74		lrcut	$$⊢A\in \mathrm{No}\to L\left(A\right){|}_{s}R\left(A\right)=A$$
75	1 74	syl	$$⊢\phi \to L\left(A\right){|}_{s}R\left(A\right)=A$$
76	75	eqcomd	$$⊢\phi \to A=L\left(A\right){|}_{s}R\left(A\right)$$
77		sltrec	$$⊢\left(\left(L\left(A\right){\ll }_{s}R\left(A\right)\wedge \left\{A\right\}{\ll }_s\left\{B\right\}\right)\wedge \left(A=L\left(A\right){|}_{s}R\left(A\right)\wedge C=\left\{A\right\}{|}_s\left\{B\right\}\right)\right)\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)$$
78	73 6 76 11 77	syl22anc	$$⊢\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)$$
79	71 78	mpbird	$$⊢\phi \to A{<}_{s}C$$
80	1 8 1	sltadd2d	$$⊢\phi \to \left(A{<}_{s}C\leftrightarrow \left(A{+}_{s}A\right){<}_s\left(A{+}_{s}C\right)\right)$$
81	79 80	mpbid	$$⊢\phi \to \left(A{+}_{s}A\right){<}_s\left(A{+}_{s}C\right)$$
82	64 81	eqbrtrd	Could not format ( ph -> ( 2s x.s A ) ( 2s x.s A )
83	54 62 82	sltled	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 |-
84		ovex	$$⊢A{+}_{s}C\in \mathrm{V}$$
85		breq2	$$⊢y=A{+}_{s}C\to \left(x{\le }_{s}y\leftrightarrow x{\le }_s\left(A{+}_{s}C\right)\right)$$
86	84 85	rexsn	$$⊢\exists y\in \left\{A{+}_{s}C\right\}x{\le }_{s}y\leftrightarrow x{\le }_s\left(A{+}_{s}C\right)$$
87	86	ralbii	Could not format ( A. x e. { ( 2s x.s A ) } E. y e. { ( A +s C ) } x <_s y <-> A. x e. { ( 2s x.s A ) } x <_s ( A +s C ) ) : No typesetting found for |- ( A. x e. { ( 2s x.s A ) } E. y e. { ( A +s C ) } x <_s y <-> A. x e. { ( 2s x.s A ) } x <_s ( A +s C ) ) with typecode |-
88		ovex	Could not format ( 2s x.s A ) e. _V : No typesetting found for |- ( 2s x.s A ) e. _V with typecode |-
89		breq1	Could not format ( x = ( 2s x.s A ) -> ( x <_s ( A +s C ) <-> ( 2s x.s A ) <_s ( A +s C ) ) ) : No typesetting found for |- ( x = ( 2s x.s A ) -> ( x <_s ( A +s C ) <-> ( 2s x.s A ) <_s ( A +s C ) ) ) with typecode |-
90	88 89	ralsn	Could not format ( A. x e. { ( 2s x.s A ) } x <_s ( A +s C ) <-> ( 2s x.s A ) <_s ( A +s C ) ) : No typesetting found for |- ( A. x e. { ( 2s x.s A ) } x <_s ( A +s C ) <-> ( 2s x.s A ) <_s ( A +s C ) ) with typecode |-
91	87 90	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 |-
92	83 91	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 |-
93	2 8	addscld	$$⊢\phi \to B{+}_{s}C\in \mathrm{No}$$
94		slerflex	$$⊢B\in \mathrm{No}\to B{\le }_{s}B$$
95	2 94	syl	$$⊢\phi \to B{\le }_{s}B$$
96		breq1	$$⊢y=B\to \left(y{\le }_{s}B\leftrightarrow B{\le }_{s}B\right)$$
97	96	rexsng	$$⊢B\in \mathrm{No}\to \left(\exists y\in \left\{B\right\}y{\le }_{s}B\leftrightarrow B{\le }_{s}B\right)$$
98	2 97	syl	$$⊢\phi \to \left(\exists y\in \left\{B\right\}y{\le }_{s}B\leftrightarrow B{\le }_{s}B\right)$$
99	95 98	mpbird	$$⊢\phi \to \exists y\in \left\{B\right\}y{\le }_{s}B$$
100	99	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)$$
101		lltropt	$$⊢L\left(B\right){\ll }_{s}R\left(B\right)$$
102	101	a1i	$$⊢\phi \to L\left(B\right){\ll }_{s}R\left(B\right)$$
103		lrcut	$$⊢B\in \mathrm{No}\to L\left(B\right){|}_{s}R\left(B\right)=B$$
104	2 103	syl	$$⊢\phi \to L\left(B\right){|}_{s}R\left(B\right)=B$$
105	104	eqcomd	$$⊢\phi \to B=L\left(B\right){|}_{s}R\left(B\right)$$
106		sltrec	$$⊢\left(\left(\left\{A\right\}{\ll }_s\left\{B\right\}\wedge L\left(B\right){\ll }_{s}R\left(B\right)\right)\wedge \left(C=\left\{A\right\}{|}_s\left\{B\right\}\wedge B=L\left(B\right){|}_{s}R\left(B\right)\right)\right)\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)$$
107	6 102 11 105 106	syl22anc	$$⊢\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)$$
108	100 107	mpbird	$$⊢\phi \to C{<}_{s}B$$
109	8 2 2	sltadd2d	$$⊢\phi \to \left(C{<}_{s}B\leftrightarrow \left(B{+}_{s}C\right){<}_s\left(B{+}_{s}B\right)\right)$$
110	108 109	mpbid	$$⊢\phi \to \left(B{+}_{s}C\right){<}_s\left(B{+}_{s}B\right)$$
111		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 |-
112	2 111	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 |-
113	110 112	breqtrrd	Could not format ( ph -> ( B +s C ) ( B +s C )
114	93 55 113	sltled	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 |-
115		ovex	$$⊢B{+}_{s}C\in \mathrm{V}$$
116		breq1	$$⊢y=B{+}_{s}C\to \left(y{\le }_{s}x\leftrightarrow \left(B{+}_{s}C\right){\le }_{s}x\right)$$
117	115 116	rexsn	$$⊢\exists y\in \left\{B{+}_{s}C\right\}y{\le }_{s}x\leftrightarrow \left(B{+}_{s}C\right){\le }_{s}x$$
118	117	ralbii	Could not format ( A. x e. { ( 2s x.s B ) } E. y e. { ( B +s C ) } y <_s x <-> A. x e. { ( 2s x.s B ) } ( B +s C ) <_s x ) : No typesetting found for |- ( A. x e. { ( 2s x.s B ) } E. y e. { ( B +s C ) } y <_s x <-> A. x e. { ( 2s x.s B ) } ( B +s C ) <_s x ) with typecode |-
119		ovex	Could not format ( 2s x.s B ) e. _V : No typesetting found for |- ( 2s x.s B ) e. _V with typecode |-
120		breq2	Could not format ( x = ( 2s x.s B ) -> ( ( B +s C ) <_s x <-> ( B +s C ) <_s ( 2s x.s B ) ) ) : No typesetting found for |- ( x = ( 2s x.s B ) -> ( ( B +s C ) <_s x <-> ( B +s C ) <_s ( 2s x.s B ) ) ) with typecode |-
121	119 120	ralsn	Could not format ( A. x e. { ( 2s x.s B ) } ( B +s C ) <_s x <-> ( B +s C ) <_s ( 2s x.s B ) ) : No typesetting found for |- ( A. x e. { ( 2s x.s B ) } ( B +s C ) <_s x <-> ( B +s C ) <_s ( 2s x.s B ) ) with typecode |-
122	118 121	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 |-
123	114 122	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 |-
124	1 2	addscld	$$⊢\phi \to A{+}_{s}B\in \mathrm{No}$$
125	8 2 1	sltadd2d	$$⊢\phi \to \left(C{<}_{s}B\leftrightarrow \left(A{+}_{s}C\right){<}_s\left(A{+}_{s}B\right)\right)$$
126	108 125	mpbid	$$⊢\phi \to \left(A{+}_{s}C\right){<}_s\left(A{+}_{s}B\right)$$
127	62 124 126	ssltsn	$$⊢\phi \to \left\{A{+}_{s}C\right\}{\ll }_s\left\{A{+}_{s}B\right\}$$
128	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 |-
129	127 128	breqtrrd	Could not format ( ph -> { ( A +s C ) } < { ( A +s C ) } <
130	1 2	addscomd	$$⊢\phi \to A{+}_{s}B=B{+}_{s}A$$
131	1 8 2	sltadd2d	$$⊢\phi \to \left(A{<}_{s}C\leftrightarrow \left(B{+}_{s}A\right){<}_s\left(B{+}_{s}C\right)\right)$$
132	79 131	mpbid	$$⊢\phi \to \left(B{+}_{s}A\right){<}_s\left(B{+}_{s}C\right)$$
133	130 132	eqbrtrd	$$⊢\phi \to \left(A{+}_{s}B\right){<}_s\left(B{+}_{s}C\right)$$
134	124 93 133	ssltsn	$$⊢\phi \to \left\{A{+}_{s}B\right\}{\ll }_s\left\{B{+}_{s}C\right\}$$
135	128 134	eqbrtrd	Could not format ( ph -> { ( { ( 2s x.s A ) } |s { ( 2s x.s B ) } ) } < { ( { ( 2s x.s A ) } |s { ( 2s x.s B ) } ) } <
136	61 92 123 129 135	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 |-
137	51 136 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$$
138	10 12 137	3eqtrd	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 |-
139		2ne0s	Could not format 2s =/= 0s : No typesetting found for |- 2s =/= 0s with typecode |-
140	139	a1i	Could not format ( ph -> 2s =/= 0s ) : No typesetting found for |- ( ph -> 2s =/= 0s ) with typecode |-
141	124 8 53 140	divsmuld	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 |-
142	138 141	mpbird	Could not format ( ph -> ( ( A +s B ) /su 2s ) = C ) : No typesetting found for |- ( ph -> ( ( A +s B ) /su 2s ) = C ) with typecode |-
143	142	eqcomd	Could not format ( ph -> C = ( ( A +s B ) /su 2s ) ) : No typesetting found for |- ( ph -> C = ( ( A +s B ) /su 2s ) ) with typecode |-