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	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		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		2sno	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	sltmul2d	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	ssltsn	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		slerflex	$$⊢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		lltropt	$$⊢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		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)$$
75	70 6 73 11 74	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)$$
76	68 75	mpbird	$$⊢\phi \to A{<}_{s}C$$
77	1 8 76	sltled	$$⊢\phi \to A{\le }_{s}C$$
78	1 8 1	sleadd2d	$$⊢\phi \to \left(A{\le }_{s}C\leftrightarrow \left(A{+}_{s}A\right){\le }_s\left(A{+}_{s}C\right)\right)$$
79	77 78	mpbid	$$⊢\phi \to \left(A{+}_{s}A\right){\le }_s\left(A{+}_{s}C\right)$$
80	61 79	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 |-
81		ovex	Could not format ( 2s x.s A ) e. _V : No typesetting found for |- ( 2s x.s A ) e. _V with typecode |-
82		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 |-
83	82	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 |-
84	81 83	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 |-
85		ovex	$$⊢A{+}_{s}C\in \mathrm{V}$$
86		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 |-
87	85 86	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 |-
88	84 87	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 |-
89	80 88	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 |-
90		slerflex	$$⊢B\in \mathrm{No}\to B{\le }_{s}B$$
91	2 90	syl	$$⊢\phi \to B{\le }_{s}B$$
92		breq1	$$⊢y=B\to \left(y{\le }_{s}B\leftrightarrow B{\le }_{s}B\right)$$
93	92	rexsng	$$⊢B\in \mathrm{No}\to \left(\exists y\in \left\{B\right\}y{\le }_{s}B\leftrightarrow B{\le }_{s}B\right)$$
94	2 93	syl	$$⊢\phi \to \left(\exists y\in \left\{B\right\}y{\le }_{s}B\leftrightarrow B{\le }_{s}B\right)$$
95	91 94	mpbird	$$⊢\phi \to \exists y\in \left\{B\right\}y{\le }_{s}B$$
96	95	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)$$
97		lltropt	$$⊢L\left(B\right){\ll }_{s}R\left(B\right)$$
98	97	a1i	$$⊢\phi \to L\left(B\right){\ll }_{s}R\left(B\right)$$
99		lrcut	$$⊢B\in \mathrm{No}\to L\left(B\right){|}_{s}R\left(B\right)=B$$
100	2 99	syl	$$⊢\phi \to L\left(B\right){|}_{s}R\left(B\right)=B$$
101	100	eqcomd	$$⊢\phi \to B=L\left(B\right){|}_{s}R\left(B\right)$$
102		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)$$
103	6 98 11 101 102	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)$$
104	96 103	mpbird	$$⊢\phi \to C{<}_{s}B$$
105	8 2 104	sltled	$$⊢\phi \to C{\le }_{s}B$$
106	8 2 2	sleadd2d	$$⊢\phi \to \left(C{\le }_{s}B\leftrightarrow \left(B{+}_{s}C\right){\le }_s\left(B{+}_{s}B\right)\right)$$
107	105 106	mpbid	$$⊢\phi \to \left(B{+}_{s}C\right){\le }_s\left(B{+}_{s}B\right)$$
108		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 |-
109	2 108	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 |-
110	107 109	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 |-
111		ovex	Could not format ( 2s x.s B ) e. _V : No typesetting found for |- ( 2s x.s B ) e. _V with typecode |-
112		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 |-
113	112	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 |-
114	111 113	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 |-
115		ovex	$$⊢B{+}_{s}C\in \mathrm{V}$$
116		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 |-
117	115 116	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 |-
118	114 117	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 |-
119	110 118	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 |-
120	1 8	addscld	$$⊢\phi \to A{+}_{s}C\in \mathrm{No}$$
121	1 2	addscld	$$⊢\phi \to A{+}_{s}B\in \mathrm{No}$$
122	8 2 1	sltadd2d	$$⊢\phi \to \left(C{<}_{s}B\leftrightarrow \left(A{+}_{s}C\right){<}_s\left(A{+}_{s}B\right)\right)$$
123	104 122	mpbid	$$⊢\phi \to \left(A{+}_{s}C\right){<}_s\left(A{+}_{s}B\right)$$
124	120 121 123	ssltsn	$$⊢\phi \to \left\{A{+}_{s}C\right\}{\ll }_s\left\{A{+}_{s}B\right\}$$
125	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 |-
126	124 125	breqtrrd	Could not format ( ph -> { ( A +s C ) } < { ( A +s C ) } <
127	2 8	addscld	$$⊢\phi \to B{+}_{s}C\in \mathrm{No}$$
128	2 1	addscomd	$$⊢\phi \to B{+}_{s}A=A{+}_{s}B$$
129	1 8 2	sltadd2d	$$⊢\phi \to \left(A{<}_{s}C\leftrightarrow \left(B{+}_{s}A\right){<}_s\left(B{+}_{s}C\right)\right)$$
130	76 129	mpbid	$$⊢\phi \to \left(B{+}_{s}A\right){<}_s\left(B{+}_{s}C\right)$$
131	128 130	eqbrtrrd	$$⊢\phi \to \left(A{+}_{s}B\right){<}_s\left(B{+}_{s}C\right)$$
132	121 127 131	ssltsn	$$⊢\phi \to \left\{A{+}_{s}B\right\}{\ll }_s\left\{B{+}_{s}C\right\}$$
133	125 132	eqbrtrd	Could not format ( ph -> { ( { ( 2s x.s A ) } |s { ( 2s x.s B ) } ) } < { ( { ( 2s x.s A ) } |s { ( 2s x.s B ) } ) } <
134	59 89 119 126 133	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 |-
135	49 134 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$$
136	12 135	eqtrd	$$⊢\phi \to C{+}_{s}C=A{+}_{s}B$$
137	10 136	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 |-
138		2ne0s	Could not format 2s =/= 0s : No typesetting found for |- 2s =/= 0s with typecode |-
139	138	a1i	Could not format ( ph -> 2s =/= 0s ) : No typesetting found for |- ( ph -> 2s =/= 0s ) with typecode |-
140		0sno	$$⊢0_s\in \mathrm{No}$$
141	140	a1i	$$⊢\top \to 0_s\in \mathrm{No}$$
142		1sno	$$⊢1_s\in \mathrm{No}$$
143	142	a1i	$$⊢\top \to 1_s\in \mathrm{No}$$
144		0slt1s	$$⊢0_s{<}_s{1}_s$$
145	144	a1i	$$⊢\top \to 0_s{<}_s{1}_s$$
146	141 143 145	ssltsn	$$⊢\top \to \left\{0_s\right\}{\ll }_s\left\{1_s\right\}$$
147	146	scutcld	$$⊢\top \to \left\{0_s\right\}{|}_s\left\{1_s\right\}\in \mathrm{No}$$
148	147	mptru	$$⊢\left\{0_s\right\}{|}_s\left\{1_s\right\}\in \mathrm{No}$$
149		twocut	Could not format ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s : No typesetting found for |- ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s with typecode |-
150		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 |-
151	150	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 |-
152	151	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 |-
153	148 149 152	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 |-
154	153	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 |-
155	121 8 51 139 154	divsmulwd	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 |-
156	137 155	mpbird	Could not format ( ph -> ( ( A +s B ) /su 2s ) = C ) : No typesetting found for |- ( ph -> ( ( A +s B ) /su 2s ) = C ) with typecode |-
157	156	eqcomd	Could not format ( ph -> C = ( ( A +s B ) /su 2s ) ) : No typesetting found for |- ( ph -> C = ( ( A +s B ) /su 2s ) ) with typecode |-