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	⊢ ( 𝜑 → 𝐴 ∈ No )
	halfcut.2	⊢ ( 𝜑 → 𝐵 ∈ No )
	halfcut.3	⊢ ( 𝜑 → 𝐴 <s 𝐵 )
	halfcut.4	⊢ ( 𝜑 → ( { ( 2s ·s 𝐴 ) } |s { ( 2s ·s 𝐵 ) } ) = ( 𝐴 +s 𝐵 ) )
	halfcut.5	⊢ 𝐶 = ( { 𝐴 } |s { 𝐵 } )
Assertion	halfcut	⊢ ( 𝜑 → 𝐶 = ( ( 𝐴 +s 𝐵 ) /su 2s ) )

Proof

Step	Hyp	Ref	Expression
1		halfcut.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		halfcut.2	⊢ ( 𝜑 → 𝐵 ∈ No )
3		halfcut.3	⊢ ( 𝜑 → 𝐴 <s 𝐵 )
4		halfcut.4	⊢ ( 𝜑 → ( { ( 2s ·s 𝐴 ) } |s { ( 2s ·s 𝐵 ) } ) = ( 𝐴 +s 𝐵 ) )
5		halfcut.5	⊢ 𝐶 = ( { 𝐴 } |s { 𝐵 } )
6	1 2 3	ssltsn	⊢ ( 𝜑 → { 𝐴 } <<s { 𝐵 } )
7	6	scutcld	⊢ ( 𝜑 → ( { 𝐴 } |s { 𝐵 } ) ∈ No )
8	5 7	eqeltrid	⊢ ( 𝜑 → 𝐶 ∈ No )
9		no2times	⊢ ( 𝐶 ∈ No → ( 2s ·s 𝐶 ) = ( 𝐶 +s 𝐶 ) )
10	8 9	syl	⊢ ( 𝜑 → ( 2s ·s 𝐶 ) = ( 𝐶 +s 𝐶 ) )
11	5	a1i	⊢ ( 𝜑 → 𝐶 = ( { 𝐴 } |s { 𝐵 } ) )
12	6 6 11 11	addsunif	⊢ ( 𝜑 → ( 𝐶 +s 𝐶 ) = ( ( { 𝑥 ∣ ∃ 𝑦 ∈ { 𝐴 } 𝑥 = ( 𝑦 +s 𝐶 ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ { 𝐴 } 𝑥 = ( 𝐶 +s 𝑦 ) } ) |s ( { 𝑥 ∣ ∃ 𝑦 ∈ { 𝐵 } 𝑥 = ( 𝑦 +s 𝐶 ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ { 𝐵 } 𝑥 = ( 𝐶 +s 𝑦 ) } ) ) )
13		oveq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 +s 𝐶 ) = ( 𝐴 +s 𝐶 ) )
14	13	eqeq2d	⊢ ( 𝑦 = 𝐴 → ( 𝑥 = ( 𝑦 +s 𝐶 ) ↔ 𝑥 = ( 𝐴 +s 𝐶 ) ) )
15	14	rexsng	⊢ ( 𝐴 ∈ No → ( ∃ 𝑦 ∈ { 𝐴 } 𝑥 = ( 𝑦 +s 𝐶 ) ↔ 𝑥 = ( 𝐴 +s 𝐶 ) ) )
16	1 15	syl	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ { 𝐴 } 𝑥 = ( 𝑦 +s 𝐶 ) ↔ 𝑥 = ( 𝐴 +s 𝐶 ) ) )
17	16	abbidv	⊢ ( 𝜑 → { 𝑥 ∣ ∃ 𝑦 ∈ { 𝐴 } 𝑥 = ( 𝑦 +s 𝐶 ) } = { 𝑥 ∣ 𝑥 = ( 𝐴 +s 𝐶 ) } )
18		oveq2	⊢ ( 𝑦 = 𝐴 → ( 𝐶 +s 𝑦 ) = ( 𝐶 +s 𝐴 ) )
19	18	eqeq2d	⊢ ( 𝑦 = 𝐴 → ( 𝑥 = ( 𝐶 +s 𝑦 ) ↔ 𝑥 = ( 𝐶 +s 𝐴 ) ) )
20	19	rexsng	⊢ ( 𝐴 ∈ No → ( ∃ 𝑦 ∈ { 𝐴 } 𝑥 = ( 𝐶 +s 𝑦 ) ↔ 𝑥 = ( 𝐶 +s 𝐴 ) ) )
21	1 20	syl	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ { 𝐴 } 𝑥 = ( 𝐶 +s 𝑦 ) ↔ 𝑥 = ( 𝐶 +s 𝐴 ) ) )
22	8 1	addscomd	⊢ ( 𝜑 → ( 𝐶 +s 𝐴 ) = ( 𝐴 +s 𝐶 ) )
23	22	eqeq2d	⊢ ( 𝜑 → ( 𝑥 = ( 𝐶 +s 𝐴 ) ↔ 𝑥 = ( 𝐴 +s 𝐶 ) ) )
24	21 23	bitrd	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ { 𝐴 } 𝑥 = ( 𝐶 +s 𝑦 ) ↔ 𝑥 = ( 𝐴 +s 𝐶 ) ) )
25	24	abbidv	⊢ ( 𝜑 → { 𝑥 ∣ ∃ 𝑦 ∈ { 𝐴 } 𝑥 = ( 𝐶 +s 𝑦 ) } = { 𝑥 ∣ 𝑥 = ( 𝐴 +s 𝐶 ) } )
26	17 25	uneq12d	⊢ ( 𝜑 → ( { 𝑥 ∣ ∃ 𝑦 ∈ { 𝐴 } 𝑥 = ( 𝑦 +s 𝐶 ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ { 𝐴 } 𝑥 = ( 𝐶 +s 𝑦 ) } ) = ( { 𝑥 ∣ 𝑥 = ( 𝐴 +s 𝐶 ) } ∪ { 𝑥 ∣ 𝑥 = ( 𝐴 +s 𝐶 ) } ) )
27		df-sn	⊢ { ( 𝐴 +s 𝐶 ) } = { 𝑥 ∣ 𝑥 = ( 𝐴 +s 𝐶 ) }
28		unidm	⊢ ( { 𝑥 ∣ 𝑥 = ( 𝐴 +s 𝐶 ) } ∪ { 𝑥 ∣ 𝑥 = ( 𝐴 +s 𝐶 ) } ) = { 𝑥 ∣ 𝑥 = ( 𝐴 +s 𝐶 ) }
29	27 28	eqtr4i	⊢ { ( 𝐴 +s 𝐶 ) } = ( { 𝑥 ∣ 𝑥 = ( 𝐴 +s 𝐶 ) } ∪ { 𝑥 ∣ 𝑥 = ( 𝐴 +s 𝐶 ) } )
30	26 29	eqtr4di	⊢ ( 𝜑 → ( { 𝑥 ∣ ∃ 𝑦 ∈ { 𝐴 } 𝑥 = ( 𝑦 +s 𝐶 ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ { 𝐴 } 𝑥 = ( 𝐶 +s 𝑦 ) } ) = { ( 𝐴 +s 𝐶 ) } )
31		oveq1	⊢ ( 𝑦 = 𝐵 → ( 𝑦 +s 𝐶 ) = ( 𝐵 +s 𝐶 ) )
32	31	eqeq2d	⊢ ( 𝑦 = 𝐵 → ( 𝑥 = ( 𝑦 +s 𝐶 ) ↔ 𝑥 = ( 𝐵 +s 𝐶 ) ) )
33	32	rexsng	⊢ ( 𝐵 ∈ No → ( ∃ 𝑦 ∈ { 𝐵 } 𝑥 = ( 𝑦 +s 𝐶 ) ↔ 𝑥 = ( 𝐵 +s 𝐶 ) ) )
34	2 33	syl	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ { 𝐵 } 𝑥 = ( 𝑦 +s 𝐶 ) ↔ 𝑥 = ( 𝐵 +s 𝐶 ) ) )
35	34	abbidv	⊢ ( 𝜑 → { 𝑥 ∣ ∃ 𝑦 ∈ { 𝐵 } 𝑥 = ( 𝑦 +s 𝐶 ) } = { 𝑥 ∣ 𝑥 = ( 𝐵 +s 𝐶 ) } )
36		oveq2	⊢ ( 𝑦 = 𝐵 → ( 𝐶 +s 𝑦 ) = ( 𝐶 +s 𝐵 ) )
37	36	eqeq2d	⊢ ( 𝑦 = 𝐵 → ( 𝑥 = ( 𝐶 +s 𝑦 ) ↔ 𝑥 = ( 𝐶 +s 𝐵 ) ) )
38	37	rexsng	⊢ ( 𝐵 ∈ No → ( ∃ 𝑦 ∈ { 𝐵 } 𝑥 = ( 𝐶 +s 𝑦 ) ↔ 𝑥 = ( 𝐶 +s 𝐵 ) ) )
39	2 38	syl	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ { 𝐵 } 𝑥 = ( 𝐶 +s 𝑦 ) ↔ 𝑥 = ( 𝐶 +s 𝐵 ) ) )
40	8 2	addscomd	⊢ ( 𝜑 → ( 𝐶 +s 𝐵 ) = ( 𝐵 +s 𝐶 ) )
41	40	eqeq2d	⊢ ( 𝜑 → ( 𝑥 = ( 𝐶 +s 𝐵 ) ↔ 𝑥 = ( 𝐵 +s 𝐶 ) ) )
42	39 41	bitrd	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ { 𝐵 } 𝑥 = ( 𝐶 +s 𝑦 ) ↔ 𝑥 = ( 𝐵 +s 𝐶 ) ) )
43	42	abbidv	⊢ ( 𝜑 → { 𝑥 ∣ ∃ 𝑦 ∈ { 𝐵 } 𝑥 = ( 𝐶 +s 𝑦 ) } = { 𝑥 ∣ 𝑥 = ( 𝐵 +s 𝐶 ) } )
44	35 43	uneq12d	⊢ ( 𝜑 → ( { 𝑥 ∣ ∃ 𝑦 ∈ { 𝐵 } 𝑥 = ( 𝑦 +s 𝐶 ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ { 𝐵 } 𝑥 = ( 𝐶 +s 𝑦 ) } ) = ( { 𝑥 ∣ 𝑥 = ( 𝐵 +s 𝐶 ) } ∪ { 𝑥 ∣ 𝑥 = ( 𝐵 +s 𝐶 ) } ) )
45		df-sn	⊢ { ( 𝐵 +s 𝐶 ) } = { 𝑥 ∣ 𝑥 = ( 𝐵 +s 𝐶 ) }
46		unidm	⊢ ( { 𝑥 ∣ 𝑥 = ( 𝐵 +s 𝐶 ) } ∪ { 𝑥 ∣ 𝑥 = ( 𝐵 +s 𝐶 ) } ) = { 𝑥 ∣ 𝑥 = ( 𝐵 +s 𝐶 ) }
47	45 46	eqtr4i	⊢ { ( 𝐵 +s 𝐶 ) } = ( { 𝑥 ∣ 𝑥 = ( 𝐵 +s 𝐶 ) } ∪ { 𝑥 ∣ 𝑥 = ( 𝐵 +s 𝐶 ) } )
48	44 47	eqtr4di	⊢ ( 𝜑 → ( { 𝑥 ∣ ∃ 𝑦 ∈ { 𝐵 } 𝑥 = ( 𝑦 +s 𝐶 ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ { 𝐵 } 𝑥 = ( 𝐶 +s 𝑦 ) } ) = { ( 𝐵 +s 𝐶 ) } )
49	30 48	oveq12d	⊢ ( 𝜑 → ( ( { 𝑥 ∣ ∃ 𝑦 ∈ { 𝐴 } 𝑥 = ( 𝑦 +s 𝐶 ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ { 𝐴 } 𝑥 = ( 𝐶 +s 𝑦 ) } ) |s ( { 𝑥 ∣ ∃ 𝑦 ∈ { 𝐵 } 𝑥 = ( 𝑦 +s 𝐶 ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ { 𝐵 } 𝑥 = ( 𝐶 +s 𝑦 ) } ) ) = ( { ( 𝐴 +s 𝐶 ) } |s { ( 𝐵 +s 𝐶 ) } ) )
50		2sno	⊢ 2s ∈ No
51	50	a1i	⊢ ( 𝜑 → 2s ∈ No )
52	51 1	mulscld	⊢ ( 𝜑 → ( 2s ·s 𝐴 ) ∈ No )
53	51 2	mulscld	⊢ ( 𝜑 → ( 2s ·s 𝐵 ) ∈ No )
54		2nns	⊢ 2s ∈ ℕs
55		nnsgt0	⊢ ( 2s ∈ ℕs → 0s <s 2s )
56	54 55	mp1i	⊢ ( 𝜑 → 0s <s 2s )
57	1 2 51 56	sltmul2d	⊢ ( 𝜑 → ( 𝐴 <s 𝐵 ↔ ( 2s ·s 𝐴 ) <s ( 2s ·s 𝐵 ) ) )
58	3 57	mpbid	⊢ ( 𝜑 → ( 2s ·s 𝐴 ) <s ( 2s ·s 𝐵 ) )
59	52 53 58	ssltsn	⊢ ( 𝜑 → { ( 2s ·s 𝐴 ) } <<s { ( 2s ·s 𝐵 ) } )
60		no2times	⊢ ( 𝐴 ∈ No → ( 2s ·s 𝐴 ) = ( 𝐴 +s 𝐴 ) )
61	1 60	syl	⊢ ( 𝜑 → ( 2s ·s 𝐴 ) = ( 𝐴 +s 𝐴 ) )
62		slerflex	⊢ ( 𝐴 ∈ No → 𝐴 ≤s 𝐴 )
63	1 62	syl	⊢ ( 𝜑 → 𝐴 ≤s 𝐴 )
64		breq2	⊢ ( 𝑥 = 𝐴 → ( 𝐴 ≤s 𝑥 ↔ 𝐴 ≤s 𝐴 ) )
65	64	rexsng	⊢ ( 𝐴 ∈ No → ( ∃ 𝑥 ∈ { 𝐴 } 𝐴 ≤s 𝑥 ↔ 𝐴 ≤s 𝐴 ) )
66	1 65	syl	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ { 𝐴 } 𝐴 ≤s 𝑥 ↔ 𝐴 ≤s 𝐴 ) )
67	63 66	mpbird	⊢ ( 𝜑 → ∃ 𝑥 ∈ { 𝐴 } 𝐴 ≤s 𝑥 )
68	67	orcd	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ { 𝐴 } 𝐴 ≤s 𝑥 ∨ ∃ 𝑦 ∈ ( R ‘ 𝐴 ) 𝑦 ≤s 𝐶 ) )
69		lltropt	⊢ ( L ‘ 𝐴 ) <<s ( R ‘ 𝐴 )
70	69	a1i	⊢ ( 𝜑 → ( L ‘ 𝐴 ) <<s ( R ‘ 𝐴 ) )
71		lrcut	⊢ ( 𝐴 ∈ No → ( ( L ‘ 𝐴 ) |s ( R ‘ 𝐴 ) ) = 𝐴 )
72	1 71	syl	⊢ ( 𝜑 → ( ( L ‘ 𝐴 ) |s ( R ‘ 𝐴 ) ) = 𝐴 )
73	72	eqcomd	⊢ ( 𝜑 → 𝐴 = ( ( L ‘ 𝐴 ) |s ( R ‘ 𝐴 ) ) )
74	70 6 73 11	sltrecd	⊢ ( 𝜑 → ( 𝐴 <s 𝐶 ↔ ( ∃ 𝑥 ∈ { 𝐴 } 𝐴 ≤s 𝑥 ∨ ∃ 𝑦 ∈ ( R ‘ 𝐴 ) 𝑦 ≤s 𝐶 ) ) )
75	68 74	mpbird	⊢ ( 𝜑 → 𝐴 <s 𝐶 )
76	1 8 75	sltled	⊢ ( 𝜑 → 𝐴 ≤s 𝐶 )
77	1 8 1	sleadd2d	⊢ ( 𝜑 → ( 𝐴 ≤s 𝐶 ↔ ( 𝐴 +s 𝐴 ) ≤s ( 𝐴 +s 𝐶 ) ) )
78	76 77	mpbid	⊢ ( 𝜑 → ( 𝐴 +s 𝐴 ) ≤s ( 𝐴 +s 𝐶 ) )
79	61 78	eqbrtrd	⊢ ( 𝜑 → ( 2s ·s 𝐴 ) ≤s ( 𝐴 +s 𝐶 ) )
80		ovex	⊢ ( 2s ·s 𝐴 ) ∈ V
81		breq1	⊢ ( 𝑥 = ( 2s ·s 𝐴 ) → ( 𝑥 ≤s 𝑦 ↔ ( 2s ·s 𝐴 ) ≤s 𝑦 ) )
82	81	rexbidv	⊢ ( 𝑥 = ( 2s ·s 𝐴 ) → ( ∃ 𝑦 ∈ { ( 𝐴 +s 𝐶 ) } 𝑥 ≤s 𝑦 ↔ ∃ 𝑦 ∈ { ( 𝐴 +s 𝐶 ) } ( 2s ·s 𝐴 ) ≤s 𝑦 ) )
83	80 82	ralsn	⊢ ( ∀ 𝑥 ∈ { ( 2s ·s 𝐴 ) } ∃ 𝑦 ∈ { ( 𝐴 +s 𝐶 ) } 𝑥 ≤s 𝑦 ↔ ∃ 𝑦 ∈ { ( 𝐴 +s 𝐶 ) } ( 2s ·s 𝐴 ) ≤s 𝑦 )
84		ovex	⊢ ( 𝐴 +s 𝐶 ) ∈ V
85		breq2	⊢ ( 𝑦 = ( 𝐴 +s 𝐶 ) → ( ( 2s ·s 𝐴 ) ≤s 𝑦 ↔ ( 2s ·s 𝐴 ) ≤s ( 𝐴 +s 𝐶 ) ) )
86	84 85	rexsn	⊢ ( ∃ 𝑦 ∈ { ( 𝐴 +s 𝐶 ) } ( 2s ·s 𝐴 ) ≤s 𝑦 ↔ ( 2s ·s 𝐴 ) ≤s ( 𝐴 +s 𝐶 ) )
87	83 86	bitri	⊢ ( ∀ 𝑥 ∈ { ( 2s ·s 𝐴 ) } ∃ 𝑦 ∈ { ( 𝐴 +s 𝐶 ) } 𝑥 ≤s 𝑦 ↔ ( 2s ·s 𝐴 ) ≤s ( 𝐴 +s 𝐶 ) )
88	79 87	sylibr	⊢ ( 𝜑 → ∀ 𝑥 ∈ { ( 2s ·s 𝐴 ) } ∃ 𝑦 ∈ { ( 𝐴 +s 𝐶 ) } 𝑥 ≤s 𝑦 )
89		slerflex	⊢ ( 𝐵 ∈ No → 𝐵 ≤s 𝐵 )
90	2 89	syl	⊢ ( 𝜑 → 𝐵 ≤s 𝐵 )
91		breq1	⊢ ( 𝑦 = 𝐵 → ( 𝑦 ≤s 𝐵 ↔ 𝐵 ≤s 𝐵 ) )
92	91	rexsng	⊢ ( 𝐵 ∈ No → ( ∃ 𝑦 ∈ { 𝐵 } 𝑦 ≤s 𝐵 ↔ 𝐵 ≤s 𝐵 ) )
93	2 92	syl	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ { 𝐵 } 𝑦 ≤s 𝐵 ↔ 𝐵 ≤s 𝐵 ) )
94	90 93	mpbird	⊢ ( 𝜑 → ∃ 𝑦 ∈ { 𝐵 } 𝑦 ≤s 𝐵 )
95	94	olcd	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( L ‘ 𝐵 ) 𝐶 ≤s 𝑥 ∨ ∃ 𝑦 ∈ { 𝐵 } 𝑦 ≤s 𝐵 ) )
96		lltropt	⊢ ( L ‘ 𝐵 ) <<s ( R ‘ 𝐵 )
97	96	a1i	⊢ ( 𝜑 → ( L ‘ 𝐵 ) <<s ( R ‘ 𝐵 ) )
98		lrcut	⊢ ( 𝐵 ∈ No → ( ( L ‘ 𝐵 ) |s ( R ‘ 𝐵 ) ) = 𝐵 )
99	2 98	syl	⊢ ( 𝜑 → ( ( L ‘ 𝐵 ) |s ( R ‘ 𝐵 ) ) = 𝐵 )
100	99	eqcomd	⊢ ( 𝜑 → 𝐵 = ( ( L ‘ 𝐵 ) |s ( R ‘ 𝐵 ) ) )
101	6 97 11 100	sltrecd	⊢ ( 𝜑 → ( 𝐶 <s 𝐵 ↔ ( ∃ 𝑥 ∈ ( L ‘ 𝐵 ) 𝐶 ≤s 𝑥 ∨ ∃ 𝑦 ∈ { 𝐵 } 𝑦 ≤s 𝐵 ) ) )
102	95 101	mpbird	⊢ ( 𝜑 → 𝐶 <s 𝐵 )
103	8 2 102	sltled	⊢ ( 𝜑 → 𝐶 ≤s 𝐵 )
104	8 2 2	sleadd2d	⊢ ( 𝜑 → ( 𝐶 ≤s 𝐵 ↔ ( 𝐵 +s 𝐶 ) ≤s ( 𝐵 +s 𝐵 ) ) )
105	103 104	mpbid	⊢ ( 𝜑 → ( 𝐵 +s 𝐶 ) ≤s ( 𝐵 +s 𝐵 ) )
106		no2times	⊢ ( 𝐵 ∈ No → ( 2s ·s 𝐵 ) = ( 𝐵 +s 𝐵 ) )
107	2 106	syl	⊢ ( 𝜑 → ( 2s ·s 𝐵 ) = ( 𝐵 +s 𝐵 ) )
108	105 107	breqtrrd	⊢ ( 𝜑 → ( 𝐵 +s 𝐶 ) ≤s ( 2s ·s 𝐵 ) )
109		ovex	⊢ ( 2s ·s 𝐵 ) ∈ V
110		breq2	⊢ ( 𝑥 = ( 2s ·s 𝐵 ) → ( 𝑦 ≤s 𝑥 ↔ 𝑦 ≤s ( 2s ·s 𝐵 ) ) )
111	110	rexbidv	⊢ ( 𝑥 = ( 2s ·s 𝐵 ) → ( ∃ 𝑦 ∈ { ( 𝐵 +s 𝐶 ) } 𝑦 ≤s 𝑥 ↔ ∃ 𝑦 ∈ { ( 𝐵 +s 𝐶 ) } 𝑦 ≤s ( 2s ·s 𝐵 ) ) )
112	109 111	ralsn	⊢ ( ∀ 𝑥 ∈ { ( 2s ·s 𝐵 ) } ∃ 𝑦 ∈ { ( 𝐵 +s 𝐶 ) } 𝑦 ≤s 𝑥 ↔ ∃ 𝑦 ∈ { ( 𝐵 +s 𝐶 ) } 𝑦 ≤s ( 2s ·s 𝐵 ) )
113		ovex	⊢ ( 𝐵 +s 𝐶 ) ∈ V
114		breq1	⊢ ( 𝑦 = ( 𝐵 +s 𝐶 ) → ( 𝑦 ≤s ( 2s ·s 𝐵 ) ↔ ( 𝐵 +s 𝐶 ) ≤s ( 2s ·s 𝐵 ) ) )
115	113 114	rexsn	⊢ ( ∃ 𝑦 ∈ { ( 𝐵 +s 𝐶 ) } 𝑦 ≤s ( 2s ·s 𝐵 ) ↔ ( 𝐵 +s 𝐶 ) ≤s ( 2s ·s 𝐵 ) )
116	112 115	bitri	⊢ ( ∀ 𝑥 ∈ { ( 2s ·s 𝐵 ) } ∃ 𝑦 ∈ { ( 𝐵 +s 𝐶 ) } 𝑦 ≤s 𝑥 ↔ ( 𝐵 +s 𝐶 ) ≤s ( 2s ·s 𝐵 ) )
117	108 116	sylibr	⊢ ( 𝜑 → ∀ 𝑥 ∈ { ( 2s ·s 𝐵 ) } ∃ 𝑦 ∈ { ( 𝐵 +s 𝐶 ) } 𝑦 ≤s 𝑥 )
118	1 8	addscld	⊢ ( 𝜑 → ( 𝐴 +s 𝐶 ) ∈ No )
119	1 2	addscld	⊢ ( 𝜑 → ( 𝐴 +s 𝐵 ) ∈ No )
120	8 2 1	sltadd2d	⊢ ( 𝜑 → ( 𝐶 <s 𝐵 ↔ ( 𝐴 +s 𝐶 ) <s ( 𝐴 +s 𝐵 ) ) )
121	102 120	mpbid	⊢ ( 𝜑 → ( 𝐴 +s 𝐶 ) <s ( 𝐴 +s 𝐵 ) )
122	118 119 121	ssltsn	⊢ ( 𝜑 → { ( 𝐴 +s 𝐶 ) } <<s { ( 𝐴 +s 𝐵 ) } )
123	4	sneqd	⊢ ( 𝜑 → { ( { ( 2s ·s 𝐴 ) } |s { ( 2s ·s 𝐵 ) } ) } = { ( 𝐴 +s 𝐵 ) } )
124	122 123	breqtrrd	⊢ ( 𝜑 → { ( 𝐴 +s 𝐶 ) } <<s { ( { ( 2s ·s 𝐴 ) } |s { ( 2s ·s 𝐵 ) } ) } )
125	2 8	addscld	⊢ ( 𝜑 → ( 𝐵 +s 𝐶 ) ∈ No )
126	2 1	addscomd	⊢ ( 𝜑 → ( 𝐵 +s 𝐴 ) = ( 𝐴 +s 𝐵 ) )
127	1 8 2	sltadd2d	⊢ ( 𝜑 → ( 𝐴 <s 𝐶 ↔ ( 𝐵 +s 𝐴 ) <s ( 𝐵 +s 𝐶 ) ) )
128	75 127	mpbid	⊢ ( 𝜑 → ( 𝐵 +s 𝐴 ) <s ( 𝐵 +s 𝐶 ) )
129	126 128	eqbrtrrd	⊢ ( 𝜑 → ( 𝐴 +s 𝐵 ) <s ( 𝐵 +s 𝐶 ) )
130	119 125 129	ssltsn	⊢ ( 𝜑 → { ( 𝐴 +s 𝐵 ) } <<s { ( 𝐵 +s 𝐶 ) } )
131	123 130	eqbrtrd	⊢ ( 𝜑 → { ( { ( 2s ·s 𝐴 ) } |s { ( 2s ·s 𝐵 ) } ) } <<s { ( 𝐵 +s 𝐶 ) } )
132	59 88 117 124 131	cofcut1d	⊢ ( 𝜑 → ( { ( 2s ·s 𝐴 ) } |s { ( 2s ·s 𝐵 ) } ) = ( { ( 𝐴 +s 𝐶 ) } |s { ( 𝐵 +s 𝐶 ) } ) )
133	49 132 4	3eqtr2d	⊢ ( 𝜑 → ( ( { 𝑥 ∣ ∃ 𝑦 ∈ { 𝐴 } 𝑥 = ( 𝑦 +s 𝐶 ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ { 𝐴 } 𝑥 = ( 𝐶 +s 𝑦 ) } ) |s ( { 𝑥 ∣ ∃ 𝑦 ∈ { 𝐵 } 𝑥 = ( 𝑦 +s 𝐶 ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ { 𝐵 } 𝑥 = ( 𝐶 +s 𝑦 ) } ) ) = ( 𝐴 +s 𝐵 ) )
134	12 133	eqtrd	⊢ ( 𝜑 → ( 𝐶 +s 𝐶 ) = ( 𝐴 +s 𝐵 ) )
135	10 134	eqtrd	⊢ ( 𝜑 → ( 2s ·s 𝐶 ) = ( 𝐴 +s 𝐵 ) )
136		2ne0s	⊢ 2s ≠ 0s
137	136	a1i	⊢ ( 𝜑 → 2s ≠ 0s )
138		0sno	⊢ 0s ∈ No
139	138	a1i	⊢ ( ⊤ → 0s ∈ No )
140		1sno	⊢ 1s ∈ No
141	140	a1i	⊢ ( ⊤ → 1s ∈ No )
142		0slt1s	⊢ 0s <s 1s
143	142	a1i	⊢ ( ⊤ → 0s <s 1s )
144	139 141 143	ssltsn	⊢ ( ⊤ → { 0s } <<s { 1s } )
145	144	scutcld	⊢ ( ⊤ → ( { 0s } |s { 1s } ) ∈ No )
146	145	mptru	⊢ ( { 0s } |s { 1s } ) ∈ No
147		twocut	⊢ ( 2s ·s ( { 0s } |s { 1s } ) ) = 1s
148		oveq2	⊢ ( 𝑥 = ( { 0s } |s { 1s } ) → ( 2s ·s 𝑥 ) = ( 2s ·s ( { 0s } |s { 1s } ) ) )
149	148	eqeq1d	⊢ ( 𝑥 = ( { 0s } |s { 1s } ) → ( ( 2s ·s 𝑥 ) = 1s ↔ ( 2s ·s ( { 0s } |s { 1s } ) ) = 1s ) )
150	149	rspcev	⊢ ( ( ( { 0s } |s { 1s } ) ∈ No ∧ ( 2s ·s ( { 0s } |s { 1s } ) ) = 1s ) → ∃ 𝑥 ∈ No ( 2s ·s 𝑥 ) = 1s )
151	146 147 150	mp2an	⊢ ∃ 𝑥 ∈ No ( 2s ·s 𝑥 ) = 1s
152	151	a1i	⊢ ( 𝜑 → ∃ 𝑥 ∈ No ( 2s ·s 𝑥 ) = 1s )
153	119 8 51 137 152	divsmulwd	⊢ ( 𝜑 → ( ( ( 𝐴 +s 𝐵 ) /su 2s ) = 𝐶 ↔ ( 2s ·s 𝐶 ) = ( 𝐴 +s 𝐵 ) ) )
154	135 153	mpbird	⊢ ( 𝜑 → ( ( 𝐴 +s 𝐵 ) /su 2s ) = 𝐶 )
155	154	eqcomd	⊢ ( 𝜑 → 𝐶 = ( ( 𝐴 +s 𝐵 ) /su 2s ) )