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 
|- ( ph -> A e. No )
halfcut.2 
|- ( ph -> B e. No )
halfcut.3 
|- ( ph -> A
halfcut.4 
|- ( ph -> ( { ( 2s x.s A ) } |s { ( 2s x.s B ) } ) = ( A +s B ) )
halfcut.5 
|- C = ( { A } |s { B } )
Assertion halfcut 
|- ( ph -> C = ( ( A +s B ) /su 2s ) )

Proof

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