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 70 6 73 11 sltrecd 
 |-  ( ph -> ( A  ( E. x e. { A } A <_s x \/ E. y e. ( _Right ` A ) y <_s C ) ) )
75 68 74 mpbird 
 |-  ( ph -> A
76 1 8 75 sltled 
 |-  ( ph -> A <_s C )
77 1 8 1 sleadd2d 
 |-  ( ph -> ( A <_s C <-> ( A +s A ) <_s ( A +s C ) ) )
78 76 77 mpbid 
 |-  ( ph -> ( A +s A ) <_s ( A +s C ) )
79 61 78 eqbrtrd 
 |-  ( ph -> ( 2s x.s A ) <_s ( A +s C ) )
80 ovex 
 |-  ( 2s x.s A ) e. _V
81 breq1 
 |-  ( x = ( 2s x.s A ) -> ( x <_s y <-> ( 2s x.s A ) <_s y ) )
82 81 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 ) )
83 80 82 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 )
84 ovex 
 |-  ( A +s C ) e. _V
85 breq2 
 |-  ( y = ( A +s C ) -> ( ( 2s x.s A ) <_s y <-> ( 2s x.s A ) <_s ( A +s C ) ) )
86 84 85 rexsn 
 |-  ( E. y e. { ( A +s C ) } ( 2s x.s A ) <_s y <-> ( 2s x.s A ) <_s ( A +s C ) )
87 83 86 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 ) )
88 79 87 sylibr 
 |-  ( ph -> A. x e. { ( 2s x.s A ) } E. y e. { ( A +s C ) } x <_s y )
89 slerflex 
 |-  ( B e. No -> B <_s B )
90 2 89 syl 
 |-  ( ph -> B <_s B )
91 breq1 
 |-  ( y = B -> ( y <_s B <-> B <_s B ) )
92 91 rexsng 
 |-  ( B e. No -> ( E. y e. { B } y <_s B <-> B <_s B ) )
93 2 92 syl 
 |-  ( ph -> ( E. y e. { B } y <_s B <-> B <_s B ) )
94 90 93 mpbird 
 |-  ( ph -> E. y e. { B } y <_s B )
95 94 olcd 
 |-  ( ph -> ( E. x e. ( _Left ` B ) C <_s x \/ E. y e. { B } y <_s B ) )
96 lltropt 
 |-  ( _Left ` B ) <
97 96 a1i 
 |-  ( ph -> ( _Left ` B ) <
98 lrcut 
 |-  ( B e. No -> ( ( _Left ` B ) |s ( _Right ` B ) ) = B )
99 2 98 syl 
 |-  ( ph -> ( ( _Left ` B ) |s ( _Right ` B ) ) = B )
100 99 eqcomd 
 |-  ( ph -> B = ( ( _Left ` B ) |s ( _Right ` B ) ) )
101 6 97 11 100 sltrecd 
 |-  ( ph -> ( C  ( E. x e. ( _Left ` B ) C <_s x \/ E. y e. { B } y <_s B ) ) )
102 95 101 mpbird 
 |-  ( ph -> C
103 8 2 102 sltled 
 |-  ( ph -> C <_s B )
104 8 2 2 sleadd2d 
 |-  ( ph -> ( C <_s B <-> ( B +s C ) <_s ( B +s B ) ) )
105 103 104 mpbid 
 |-  ( ph -> ( B +s C ) <_s ( B +s B ) )
106 no2times 
 |-  ( B e. No -> ( 2s x.s B ) = ( B +s B ) )
107 2 106 syl 
 |-  ( ph -> ( 2s x.s B ) = ( B +s B ) )
108 105 107 breqtrrd 
 |-  ( ph -> ( B +s C ) <_s ( 2s x.s B ) )
109 ovex 
 |-  ( 2s x.s B ) e. _V
110 breq2 
 |-  ( x = ( 2s x.s B ) -> ( y <_s x <-> y <_s ( 2s x.s B ) ) )
111 110 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 ) ) )
112 109 111 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 ) )
113 ovex 
 |-  ( B +s C ) e. _V
114 breq1 
 |-  ( y = ( B +s C ) -> ( y <_s ( 2s x.s B ) <-> ( B +s C ) <_s ( 2s x.s B ) ) )
115 113 114 rexsn 
 |-  ( E. y e. { ( B +s C ) } y <_s ( 2s x.s B ) <-> ( B +s C ) <_s ( 2s x.s B ) )
116 112 115 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 ) )
117 108 116 sylibr 
 |-  ( ph -> A. x e. { ( 2s x.s B ) } E. y e. { ( B +s C ) } y <_s x )
118 1 8 addscld 
 |-  ( ph -> ( A +s C ) e. No )
119 1 2 addscld 
 |-  ( ph -> ( A +s B ) e. No )
120 8 2 1 sltadd2d 
 |-  ( ph -> ( C  ( A +s C )
121 102 120 mpbid 
 |-  ( ph -> ( A +s C )
122 118 119 121 ssltsn 
 |-  ( ph -> { ( A +s C ) } <
123 4 sneqd 
 |-  ( ph -> { ( { ( 2s x.s A ) } |s { ( 2s x.s B ) } ) } = { ( A +s B ) } )
124 122 123 breqtrrd 
 |-  ( ph -> { ( A +s C ) } <
125 2 8 addscld 
 |-  ( ph -> ( B +s C ) e. No )
126 2 1 addscomd 
 |-  ( ph -> ( B +s A ) = ( A +s B ) )
127 1 8 2 sltadd2d 
 |-  ( ph -> ( A  ( B +s A )
128 75 127 mpbid 
 |-  ( ph -> ( B +s A )
129 126 128 eqbrtrrd 
 |-  ( ph -> ( A +s B )
130 119 125 129 ssltsn 
 |-  ( ph -> { ( A +s B ) } <
131 123 130 eqbrtrd 
 |-  ( ph -> { ( { ( 2s x.s A ) } |s { ( 2s x.s B ) } ) } <
132 59 88 117 124 131 cofcut1d 
 |-  ( ph -> ( { ( 2s x.s A ) } |s { ( 2s x.s B ) } ) = ( { ( A +s C ) } |s { ( B +s C ) } ) )
133 49 132 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 ) )
134 12 133 eqtrd 
 |-  ( ph -> ( C +s C ) = ( A +s B ) )
135 10 134 eqtrd 
 |-  ( ph -> ( 2s x.s C ) = ( A +s B ) )
136 2ne0s 
 |-  2s =/= 0s
137 136 a1i 
 |-  ( ph -> 2s =/= 0s )
138 0sno 
 |-  0s e. No
139 138 a1i 
 |-  ( T. -> 0s e. No )
140 1sno 
 |-  1s e. No
141 140 a1i 
 |-  ( T. -> 1s e. No )
142 0slt1s 
 |-  0s
143 142 a1i 
 |-  ( T. -> 0s
144 139 141 143 ssltsn 
 |-  ( T. -> { 0s } <
145 144 scutcld 
 |-  ( T. -> ( { 0s } |s { 1s } ) e. No )
146 145 mptru 
 |-  ( { 0s } |s { 1s } ) e. No
147 twocut 
 |-  ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s
148 oveq2 
 |-  ( x = ( { 0s } |s { 1s } ) -> ( 2s x.s x ) = ( 2s x.s ( { 0s } |s { 1s } ) ) )
149 148 eqeq1d 
 |-  ( x = ( { 0s } |s { 1s } ) -> ( ( 2s x.s x ) = 1s <-> ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s ) )
150 149 rspcev 
 |-  ( ( ( { 0s } |s { 1s } ) e. No /\ ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s ) -> E. x e. No ( 2s x.s x ) = 1s )
151 146 147 150 mp2an 
 |-  E. x e. No ( 2s x.s x ) = 1s
152 151 a1i 
 |-  ( ph -> E. x e. No ( 2s x.s x ) = 1s )
153 119 8 51 137 152 divsmulwd 
 |-  ( ph -> ( ( ( A +s B ) /su 2s ) = C <-> ( 2s x.s C ) = ( A +s B ) ) )
154 135 153 mpbird 
 |-  ( ph -> ( ( A +s B ) /su 2s ) = C )
155 154 eqcomd 
 |-  ( ph -> C = ( ( A +s B ) /su 2s ) )