Metamath Proof Explorer

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 sltrec ⊢ ( ( ( ( L ‘ 𝐴 ) <<s ( R ‘ 𝐴 ) ∧ { 𝐴 } <<s { 𝐵 } ) ∧ ( 𝐴 = ( ( L ‘ 𝐴 ) |s ( R ‘ 𝐴 ) ) ∧ 𝐶 = ( { 𝐴 } |s { 𝐵 } ) ) ) → ( 𝐴 <s 𝐶 ↔ ( ∃ 𝑥 ∈ { 𝐴 } 𝐴 ≤s 𝑥 ∨ ∃ 𝑦 ∈ ( R ‘ 𝐴 ) 𝑦 ≤s 𝐶 ) ) )
75 70 6 73 11 74 syl22anc ⊢ ( 𝜑 → ( 𝐴 <s 𝐶 ↔ ( ∃ 𝑥 ∈ { 𝐴 } 𝐴 ≤s 𝑥 ∨ ∃ 𝑦 ∈ ( R ‘ 𝐴 ) 𝑦 ≤s 𝐶 ) ) )
76 68 75 mpbird ⊢ ( 𝜑 → 𝐴 <s 𝐶 )
77 1 8 76 sltled ⊢ ( 𝜑 → 𝐴 ≤s 𝐶 )
78 1 8 1 sleadd2d ⊢ ( 𝜑 → ( 𝐴 ≤s 𝐶 ↔ ( 𝐴 +s 𝐴 ) ≤s ( 𝐴 +s 𝐶 ) ) )
79 77 78 mpbid ⊢ ( 𝜑 → ( 𝐴 +s 𝐴 ) ≤s ( 𝐴 +s 𝐶 ) )
80 61 79 eqbrtrd ⊢ ( 𝜑 → ( 2s ·s 𝐴 ) ≤s ( 𝐴 +s 𝐶 ) )
81 ovex ⊢ ( 2s ·s 𝐴 ) ∈ V
82 breq1 ⊢ ( 𝑥 = ( 2s ·s 𝐴 ) → ( 𝑥 ≤s 𝑦 ↔ ( 2s ·s 𝐴 ) ≤s 𝑦 ) )
83 82 rexbidv ⊢ ( 𝑥 = ( 2s ·s 𝐴 ) → ( ∃ 𝑦 ∈ { ( 𝐴 +s 𝐶 ) } 𝑥 ≤s 𝑦 ↔ ∃ 𝑦 ∈ { ( 𝐴 +s 𝐶 ) } ( 2s ·s 𝐴 ) ≤s 𝑦 ) )
84 81 83 ralsn ⊢ ( ∀ 𝑥 ∈ { ( 2s ·s 𝐴 ) } ∃ 𝑦 ∈ { ( 𝐴 +s 𝐶 ) } 𝑥 ≤s 𝑦 ↔ ∃ 𝑦 ∈ { ( 𝐴 +s 𝐶 ) } ( 2s ·s 𝐴 ) ≤s 𝑦 )
85 ovex ⊢ ( 𝐴 +s 𝐶 ) ∈ V
86 breq2 ⊢ ( 𝑦 = ( 𝐴 +s 𝐶 ) → ( ( 2s ·s 𝐴 ) ≤s 𝑦 ↔ ( 2s ·s 𝐴 ) ≤s ( 𝐴 +s 𝐶 ) ) )
87 85 86 rexsn ⊢ ( ∃ 𝑦 ∈ { ( 𝐴 +s 𝐶 ) } ( 2s ·s 𝐴 ) ≤s 𝑦 ↔ ( 2s ·s 𝐴 ) ≤s ( 𝐴 +s 𝐶 ) )
88 84 87 bitri ⊢ ( ∀ 𝑥 ∈ { ( 2s ·s 𝐴 ) } ∃ 𝑦 ∈ { ( 𝐴 +s 𝐶 ) } 𝑥 ≤s 𝑦 ↔ ( 2s ·s 𝐴 ) ≤s ( 𝐴 +s 𝐶 ) )
89 80 88 sylibr ⊢ ( 𝜑 → ∀ 𝑥 ∈ { ( 2s ·s 𝐴 ) } ∃ 𝑦 ∈ { ( 𝐴 +s 𝐶 ) } 𝑥 ≤s 𝑦 )
90 slerflex ⊢ ( 𝐵 ∈ No → 𝐵 ≤s 𝐵 )
91 2 90 syl ⊢ ( 𝜑 → 𝐵 ≤s 𝐵 )
92 breq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 ≤s 𝐵 ↔ 𝐵 ≤s 𝐵 ) )
93 92 rexsng ⊢ ( 𝐵 ∈ No → ( ∃ 𝑦 ∈ { 𝐵 } 𝑦 ≤s 𝐵 ↔ 𝐵 ≤s 𝐵 ) )
94 2 93 syl ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ { 𝐵 } 𝑦 ≤s 𝐵 ↔ 𝐵 ≤s 𝐵 ) )
95 91 94 mpbird ⊢ ( 𝜑 → ∃ 𝑦 ∈ { 𝐵 } 𝑦 ≤s 𝐵 )
96 95 olcd ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( L ‘ 𝐵 ) 𝐶 ≤s 𝑥 ∨ ∃ 𝑦 ∈ { 𝐵 } 𝑦 ≤s 𝐵 ) )
97 lltropt ⊢ ( L ‘ 𝐵 ) <<s ( R ‘ 𝐵 )
98 97 a1i ⊢ ( 𝜑 → ( L ‘ 𝐵 ) <<s ( R ‘ 𝐵 ) )
99 lrcut ⊢ ( 𝐵 ∈ No → ( ( L ‘ 𝐵 ) |s ( R ‘ 𝐵 ) ) = 𝐵 )
100 2 99 syl ⊢ ( 𝜑 → ( ( L ‘ 𝐵 ) |s ( R ‘ 𝐵 ) ) = 𝐵 )
101 100 eqcomd ⊢ ( 𝜑 → 𝐵 = ( ( L ‘ 𝐵 ) |s ( R ‘ 𝐵 ) ) )
102 sltrec ⊢ ( ( ( { 𝐴 } <<s { 𝐵 } ∧ ( L ‘ 𝐵 ) <<s ( R ‘ 𝐵 ) ) ∧ ( 𝐶 = ( { 𝐴 } |s { 𝐵 } ) ∧ 𝐵 = ( ( L ‘ 𝐵 ) |s ( R ‘ 𝐵 ) ) ) ) → ( 𝐶 <s 𝐵 ↔ ( ∃ 𝑥 ∈ ( L ‘ 𝐵 ) 𝐶 ≤s 𝑥 ∨ ∃ 𝑦 ∈ { 𝐵 } 𝑦 ≤s 𝐵 ) ) )
103 6 98 11 101 102 syl22anc ⊢ ( 𝜑 → ( 𝐶 <s 𝐵 ↔ ( ∃ 𝑥 ∈ ( L ‘ 𝐵 ) 𝐶 ≤s 𝑥 ∨ ∃ 𝑦 ∈ { 𝐵 } 𝑦 ≤s 𝐵 ) ) )
104 96 103 mpbird ⊢ ( 𝜑 → 𝐶 <s 𝐵 )
105 8 2 104 sltled ⊢ ( 𝜑 → 𝐶 ≤s 𝐵 )
106 8 2 2 sleadd2d ⊢ ( 𝜑 → ( 𝐶 ≤s 𝐵 ↔ ( 𝐵 +s 𝐶 ) ≤s ( 𝐵 +s 𝐵 ) ) )
107 105 106 mpbid ⊢ ( 𝜑 → ( 𝐵 +s 𝐶 ) ≤s ( 𝐵 +s 𝐵 ) )
108 no2times ⊢ ( 𝐵 ∈ No → ( 2s ·s 𝐵 ) = ( 𝐵 +s 𝐵 ) )
109 2 108 syl ⊢ ( 𝜑 → ( 2s ·s 𝐵 ) = ( 𝐵 +s 𝐵 ) )
110 107 109 breqtrrd ⊢ ( 𝜑 → ( 𝐵 +s 𝐶 ) ≤s ( 2s ·s 𝐵 ) )
111 ovex ⊢ ( 2s ·s 𝐵 ) ∈ V
112 breq2 ⊢ ( 𝑥 = ( 2s ·s 𝐵 ) → ( 𝑦 ≤s 𝑥 ↔ 𝑦 ≤s ( 2s ·s 𝐵 ) ) )
113 112 rexbidv ⊢ ( 𝑥 = ( 2s ·s 𝐵 ) → ( ∃ 𝑦 ∈ { ( 𝐵 +s 𝐶 ) } 𝑦 ≤s 𝑥 ↔ ∃ 𝑦 ∈ { ( 𝐵 +s 𝐶 ) } 𝑦 ≤s ( 2s ·s 𝐵 ) ) )
114 111 113 ralsn ⊢ ( ∀ 𝑥 ∈ { ( 2s ·s 𝐵 ) } ∃ 𝑦 ∈ { ( 𝐵 +s 𝐶 ) } 𝑦 ≤s 𝑥 ↔ ∃ 𝑦 ∈ { ( 𝐵 +s 𝐶 ) } 𝑦 ≤s ( 2s ·s 𝐵 ) )
115 ovex ⊢ ( 𝐵 +s 𝐶 ) ∈ V
116 breq1 ⊢ ( 𝑦 = ( 𝐵 +s 𝐶 ) → ( 𝑦 ≤s ( 2s ·s 𝐵 ) ↔ ( 𝐵 +s 𝐶 ) ≤s ( 2s ·s 𝐵 ) ) )
117 115 116 rexsn ⊢ ( ∃ 𝑦 ∈ { ( 𝐵 +s 𝐶 ) } 𝑦 ≤s ( 2s ·s 𝐵 ) ↔ ( 𝐵 +s 𝐶 ) ≤s ( 2s ·s 𝐵 ) )
118 114 117 bitri ⊢ ( ∀ 𝑥 ∈ { ( 2s ·s 𝐵 ) } ∃ 𝑦 ∈ { ( 𝐵 +s 𝐶 ) } 𝑦 ≤s 𝑥 ↔ ( 𝐵 +s 𝐶 ) ≤s ( 2s ·s 𝐵 ) )
119 110 118 sylibr ⊢ ( 𝜑 → ∀ 𝑥 ∈ { ( 2s ·s 𝐵 ) } ∃ 𝑦 ∈ { ( 𝐵 +s 𝐶 ) } 𝑦 ≤s 𝑥 )
120 1 8 addscld ⊢ ( 𝜑 → ( 𝐴 +s 𝐶 ) ∈ No )
121 1 2 addscld ⊢ ( 𝜑 → ( 𝐴 +s 𝐵 ) ∈ No )
122 8 2 1 sltadd2d ⊢ ( 𝜑 → ( 𝐶 <s 𝐵 ↔ ( 𝐴 +s 𝐶 ) <s ( 𝐴 +s 𝐵 ) ) )
123 104 122 mpbid ⊢ ( 𝜑 → ( 𝐴 +s 𝐶 ) <s ( 𝐴 +s 𝐵 ) )
124 120 121 123 ssltsn ⊢ ( 𝜑 → { ( 𝐴 +s 𝐶 ) } <<s { ( 𝐴 +s 𝐵 ) } )
125 4 sneqd ⊢ ( 𝜑 → { ( { ( 2s ·s 𝐴 ) } |s { ( 2s ·s 𝐵 ) } ) } = { ( 𝐴 +s 𝐵 ) } )
126 124 125 breqtrrd ⊢ ( 𝜑 → { ( 𝐴 +s 𝐶 ) } <<s { ( { ( 2s ·s 𝐴 ) } |s { ( 2s ·s 𝐵 ) } ) } )
127 2 8 addscld ⊢ ( 𝜑 → ( 𝐵 +s 𝐶 ) ∈ No )
128 2 1 addscomd ⊢ ( 𝜑 → ( 𝐵 +s 𝐴 ) = ( 𝐴 +s 𝐵 ) )
129 1 8 2 sltadd2d ⊢ ( 𝜑 → ( 𝐴 <s 𝐶 ↔ ( 𝐵 +s 𝐴 ) <s ( 𝐵 +s 𝐶 ) ) )
130 76 129 mpbid ⊢ ( 𝜑 → ( 𝐵 +s 𝐴 ) <s ( 𝐵 +s 𝐶 ) )
131 128 130 eqbrtrrd ⊢ ( 𝜑 → ( 𝐴 +s 𝐵 ) <s ( 𝐵 +s 𝐶 ) )
132 121 127 131 ssltsn ⊢ ( 𝜑 → { ( 𝐴 +s 𝐵 ) } <<s { ( 𝐵 +s 𝐶 ) } )
133 125 132 eqbrtrd ⊢ ( 𝜑 → { ( { ( 2s ·s 𝐴 ) } |s { ( 2s ·s 𝐵 ) } ) } <<s { ( 𝐵 +s 𝐶 ) } )
134 59 89 119 126 133 cofcut1d ⊢ ( 𝜑 → ( { ( 2s ·s 𝐴 ) } |s { ( 2s ·s 𝐵 ) } ) = ( { ( 𝐴 +s 𝐶 ) } |s { ( 𝐵 +s 𝐶 ) } ) )
135 49 134 4 3eqtr2d ⊢ ( 𝜑 → ( ( { 𝑥 ∣ ∃ 𝑦 ∈ { 𝐴 } 𝑥 = ( 𝑦 +s 𝐶 ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ { 𝐴 } 𝑥 = ( 𝐶 +s 𝑦 ) } ) |s ( { 𝑥 ∣ ∃ 𝑦 ∈ { 𝐵 } 𝑥 = ( 𝑦 +s 𝐶 ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ { 𝐵 } 𝑥 = ( 𝐶 +s 𝑦 ) } ) ) = ( 𝐴 +s 𝐵 ) )
136 12 135 eqtrd ⊢ ( 𝜑 → ( 𝐶 +s 𝐶 ) = ( 𝐴 +s 𝐵 ) )
137 10 136 eqtrd ⊢ ( 𝜑 → ( 2s ·s 𝐶 ) = ( 𝐴 +s 𝐵 ) )
138 2ne0s ⊢ 2s ≠ 0s
139 138 a1i ⊢ ( 𝜑 → 2s ≠ 0s )
140 0sno ⊢ 0s ∈ No
141 140 a1i ⊢ ( ⊤ → 0s ∈ No )
142 1sno ⊢ 1s ∈ No
143 142 a1i ⊢ ( ⊤ → 1s ∈ No )
144 0slt1s ⊢ 0s <s 1s
145 144 a1i ⊢ ( ⊤ → 0s <s 1s )
146 141 143 145 ssltsn ⊢ ( ⊤ → { 0s } <<s { 1s } )
147 146 scutcld ⊢ ( ⊤ → ( { 0s } |s { 1s } ) ∈ No )
148 147 mptru ⊢ ( { 0s } |s { 1s } ) ∈ No
149 twocut ⊢ ( 2s ·s ( { 0s } |s { 1s } ) ) = 1s
150 oveq2 ⊢ ( 𝑥 = ( { 0s } |s { 1s } ) → ( 2s ·s 𝑥 ) = ( 2s ·s ( { 0s } |s { 1s } ) ) )
151 150 eqeq1d ⊢ ( 𝑥 = ( { 0s } |s { 1s } ) → ( ( 2s ·s 𝑥 ) = 1s ↔ ( 2s ·s ( { 0s } |s { 1s } ) ) = 1s ) )
152 151 rspcev ⊢ ( ( ( { 0s } |s { 1s } ) ∈ No ∧ ( 2s ·s ( { 0s } |s { 1s } ) ) = 1s ) → ∃ 𝑥 ∈ No ( 2s ·s 𝑥 ) = 1s )
153 148 149 152 mp2an ⊢ ∃ 𝑥 ∈ No ( 2s ·s 𝑥 ) = 1s
154 153 a1i ⊢ ( 𝜑 → ∃ 𝑥 ∈ No ( 2s ·s 𝑥 ) = 1s )
155 121 8 51 139 154 divsmulwd ⊢ ( 𝜑 → ( ( ( 𝐴 +s 𝐵 ) /su 2s ) = 𝐶 ↔ ( 2s ·s 𝐶 ) = ( 𝐴 +s 𝐵 ) ) )
156 137 155 mpbird ⊢ ( 𝜑 → ( ( 𝐴 +s 𝐵 ) /su 2s ) = 𝐶 )
157 156 eqcomd ⊢ ( 𝜑 → 𝐶 = ( ( 𝐴 +s 𝐵 ) /su 2s ) )