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)

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