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