Metamath Proof Explorer


Theorem nn0sumshdiglemB

Description: Lemma for nn0sumshdig (induction step, odd multiplier). (Contributed by AV, 7-Jun-2020)

Ref Expression
Assertion nn0sumshdiglemB a a 1 2 0 y x 0 # b x = y x = k 0 ..^ y k digit 2 x 2 k # b a = y + 1 a = k 0 ..^ y + 1 k digit 2 a 2 k

Proof

Step Hyp Ref Expression
1 elnn1uz2 a a = 1 a 2
2 1t1e1 1 1 = 1
3 2 eqcomi 1 = 1 1
4 simpl a = 1 # b a = y + 1 a = 1
5 oveq2 y + 1 = # b a 0 ..^ y + 1 = 0 ..^ # b a
6 5 eqcoms # b a = y + 1 0 ..^ y + 1 = 0 ..^ # b a
7 fveq2 a = 1 # b a = # b 1
8 blen1 # b 1 = 1
9 7 8 eqtrdi a = 1 # b a = 1
10 9 oveq2d a = 1 0 ..^ # b a = 0 ..^ 1
11 fzo01 0 ..^ 1 = 0
12 10 11 eqtrdi a = 1 0 ..^ # b a = 0
13 6 12 sylan9eqr a = 1 # b a = y + 1 0 ..^ y + 1 = 0
14 13 sumeq1d a = 1 # b a = y + 1 k 0 ..^ y + 1 k digit 2 a 2 k = k 0 k digit 2 a 2 k
15 oveq2 a = 1 k digit 2 a = k digit 2 1
16 15 oveq1d a = 1 k digit 2 a 2 k = k digit 2 1 2 k
17 16 sumeq2sdv a = 1 k 0 k digit 2 a 2 k = k 0 k digit 2 1 2 k
18 c0ex 0 V
19 ax-1cn 1
20 19 19 mulcli 1 1
21 oveq1 k = 0 k digit 2 1 = 0 digit 2 1
22 1ex 1 V
23 22 prid2 1 0 1
24 0dig2pr01 1 0 1 0 digit 2 1 = 1
25 23 24 ax-mp 0 digit 2 1 = 1
26 21 25 eqtrdi k = 0 k digit 2 1 = 1
27 oveq2 k = 0 2 k = 2 0
28 2cn 2
29 exp0 2 2 0 = 1
30 28 29 ax-mp 2 0 = 1
31 27 30 eqtrdi k = 0 2 k = 1
32 26 31 oveq12d k = 0 k digit 2 1 2 k = 1 1
33 32 sumsn 0 V 1 1 k 0 k digit 2 1 2 k = 1 1
34 18 20 33 mp2an k 0 k digit 2 1 2 k = 1 1
35 17 34 eqtrdi a = 1 k 0 k digit 2 a 2 k = 1 1
36 35 adantr a = 1 # b a = y + 1 k 0 k digit 2 a 2 k = 1 1
37 14 36 eqtrd a = 1 # b a = y + 1 k 0 ..^ y + 1 k digit 2 a 2 k = 1 1
38 3 4 37 3eqtr4a a = 1 # b a = y + 1 a = k 0 ..^ y + 1 k digit 2 a 2 k
39 38 ex a = 1 # b a = y + 1 a = k 0 ..^ y + 1 k digit 2 a 2 k
40 39 a1d a = 1 x 0 # b x = y x = k 0 ..^ y k digit 2 x 2 k # b a = y + 1 a = k 0 ..^ y + 1 k digit 2 a 2 k
41 40 2a1d a = 1 a 1 2 0 y x 0 # b x = y x = k 0 ..^ y k digit 2 x 2 k # b a = y + 1 a = k 0 ..^ y + 1 k digit 2 a 2 k
42 eluzge2nn0 a 2 a 0
43 nn0ob a 0 a + 1 2 0 a 1 2 0
44 43 bicomd a 0 a 1 2 0 a + 1 2 0
45 42 44 syl a 2 a 1 2 0 a + 1 2 0
46 blennngt2o2 a 2 a + 1 2 0 # b a = # b a 1 2 + 1
47 46 ex a 2 a + 1 2 0 # b a = # b a 1 2 + 1
48 45 47 sylbid a 2 a 1 2 0 # b a = # b a 1 2 + 1
49 48 imp a 2 a 1 2 0 # b a = # b a 1 2 + 1
50 fveqeq2 x = a 1 2 # b x = y # b a 1 2 = y
51 id x = a 1 2 x = a 1 2
52 oveq2 x = a 1 2 k digit 2 x = k digit 2 a 1 2
53 52 oveq1d x = a 1 2 k digit 2 x 2 k = k digit 2 a 1 2 2 k
54 53 sumeq2sdv x = a 1 2 k 0 ..^ y k digit 2 x 2 k = k 0 ..^ y k digit 2 a 1 2 2 k
55 51 54 eqeq12d x = a 1 2 x = k 0 ..^ y k digit 2 x 2 k a 1 2 = k 0 ..^ y k digit 2 a 1 2 2 k
56 50 55 imbi12d x = a 1 2 # b x = y x = k 0 ..^ y k digit 2 x 2 k # b a 1 2 = y a 1 2 = k 0 ..^ y k digit 2 a 1 2 2 k
57 56 rspcva a 1 2 0 x 0 # b x = y x = k 0 ..^ y k digit 2 x 2 k # b a 1 2 = y a 1 2 = k 0 ..^ y k digit 2 a 1 2 2 k
58 eqeq1 # b a = y + 1 # b a = # b a 1 2 + 1 y + 1 = # b a 1 2 + 1
59 nncn y y
60 59 ad2antll # b a = y + 1 a 1 2 0 a 2 y y
61 blennn0elnn a 1 2 0 # b a 1 2
62 61 nncnd a 1 2 0 # b a 1 2
63 62 adantr a 1 2 0 a 2 # b a 1 2
64 63 ad2antrl # b a = y + 1 a 1 2 0 a 2 y # b a 1 2
65 1cnd # b a = y + 1 a 1 2 0 a 2 y 1
66 60 64 65 addcan2d # b a = y + 1 a 1 2 0 a 2 y y + 1 = # b a 1 2 + 1 y = # b a 1 2
67 eqcom y = # b a 1 2 # b a 1 2 = y
68 nnz y y
69 68 ad2antll # b a = y + 1 a 1 2 0 a 2 y y
70 fzval3 y 0 y = 0 ..^ y + 1
71 69 70 syl # b a = y + 1 a 1 2 0 a 2 y 0 y = 0 ..^ y + 1
72 71 eqcomd # b a = y + 1 a 1 2 0 a 2 y 0 ..^ y + 1 = 0 y
73 72 sumeq1d # b a = y + 1 a 1 2 0 a 2 y k 0 ..^ y + 1 k digit 2 a 2 k = k = 0 y k digit 2 a 2 k
74 nnnn0 y y 0
75 elnn0uz y 0 y 0
76 74 75 sylib y y 0
77 76 ad2antll # b a = y + 1 a 1 2 0 a 2 y y 0
78 2nn 2
79 78 a1i a 1 2 0 a 2 k 0 y 2
80 elfzelz k 0 y k
81 80 adantl a 1 2 0 a 2 k 0 y k
82 nn0rp0 a 0 a 0 +∞
83 42 82 syl a 2 a 0 +∞
84 83 adantl a 1 2 0 a 2 a 0 +∞
85 84 adantr a 1 2 0 a 2 k 0 y a 0 +∞
86 digvalnn0 2 k a 0 +∞ k digit 2 a 0
87 79 81 85 86 syl3anc a 1 2 0 a 2 k 0 y k digit 2 a 0
88 87 ex a 1 2 0 a 2 k 0 y k digit 2 a 0
89 88 ad2antrl # b a = y + 1 a 1 2 0 a 2 y k 0 y k digit 2 a 0
90 89 imp # b a = y + 1 a 1 2 0 a 2 y k 0 y k digit 2 a 0
91 90 nn0cnd # b a = y + 1 a 1 2 0 a 2 y k 0 y k digit 2 a
92 2nn0 2 0
93 92 a1i k 0 y 2 0
94 elfznn0 k 0 y k 0
95 93 94 nn0expcld k 0 y 2 k 0
96 95 nn0cnd k 0 y 2 k
97 96 adantl # b a = y + 1 a 1 2 0 a 2 y k 0 y 2 k
98 91 97 mulcld # b a = y + 1 a 1 2 0 a 2 y k 0 y k digit 2 a 2 k
99 oveq1 k = 0 k digit 2 a = 0 digit 2 a
100 99 27 oveq12d k = 0 k digit 2 a 2 k = 0 digit 2 a 2 0
101 30 oveq2i 0 digit 2 a 2 0 = 0 digit 2 a 1
102 100 101 eqtrdi k = 0 k digit 2 a 2 k = 0 digit 2 a 1
103 77 98 102 fsum1p # b a = y + 1 a 1 2 0 a 2 y k = 0 y k digit 2 a 2 k = 0 digit 2 a 1 + k = 0 + 1 y k digit 2 a 2 k
104 42 adantl a 1 2 0 a 2 a 0
105 42 43 syl a 2 a + 1 2 0 a 1 2 0
106 105 biimparc a 1 2 0 a 2 a + 1 2 0
107 0dig2nn0o a 0 a + 1 2 0 0 digit 2 a = 1
108 104 106 107 syl2anc a 1 2 0 a 2 0 digit 2 a = 1
109 108 ad2antrl # b a = y + 1 a 1 2 0 a 2 y 0 digit 2 a = 1
110 109 oveq1d # b a = y + 1 a 1 2 0 a 2 y 0 digit 2 a 1 = 1 1
111 110 2 eqtrdi # b a = y + 1 a 1 2 0 a 2 y 0 digit 2 a 1 = 1
112 1z 1
113 112 a1i # b a = y + 1 a 1 2 0 a 2 y 1
114 0p1e1 0 + 1 = 1
115 114 112 eqeltri 0 + 1
116 115 a1i # b a = y + 1 a 1 2 0 a 2 y 0 + 1
117 78 a1i a 2 k 0 + 1 y 2
118 elfzelz k 0 + 1 y k
119 118 adantl a 2 k 0 + 1 y k
120 42 adantr a 2 k 0 + 1 y a 0
121 120 82 syl a 2 k 0 + 1 y a 0 +∞
122 117 119 121 86 syl3anc a 2 k 0 + 1 y k digit 2 a 0
123 122 ex a 2 k 0 + 1 y k digit 2 a 0
124 123 adantl a 1 2 0 a 2 k 0 + 1 y k digit 2 a 0
125 124 ad2antrl # b a = y + 1 a 1 2 0 a 2 y k 0 + 1 y k digit 2 a 0
126 125 imp # b a = y + 1 a 1 2 0 a 2 y k 0 + 1 y k digit 2 a 0
127 126 nn0cnd # b a = y + 1 a 1 2 0 a 2 y k 0 + 1 y k digit 2 a
128 2cnd k 0 + 1 y 2
129 elfznn k 1 y k
130 129 nnnn0d k 1 y k 0
131 114 oveq1i 0 + 1 y = 1 y
132 130 131 eleq2s k 0 + 1 y k 0
133 128 132 expcld k 0 + 1 y 2 k
134 133 adantl # b a = y + 1 a 1 2 0 a 2 y k 0 + 1 y 2 k
135 127 134 mulcld # b a = y + 1 a 1 2 0 a 2 y k 0 + 1 y k digit 2 a 2 k
136 oveq1 k = i + 1 k digit 2 a = i + 1 digit 2 a
137 oveq2 k = i + 1 2 k = 2 i + 1
138 136 137 oveq12d k = i + 1 k digit 2 a 2 k = i + 1 digit 2 a 2 i + 1
139 113 116 69 135 138 fsumshftm # b a = y + 1 a 1 2 0 a 2 y k = 0 + 1 y k digit 2 a 2 k = i = 0 + 1 - 1 y 1 i + 1 digit 2 a 2 i + 1
140 111 139 oveq12d # b a = y + 1 a 1 2 0 a 2 y 0 digit 2 a 1 + k = 0 + 1 y k digit 2 a 2 k = 1 + i = 0 + 1 - 1 y 1 i + 1 digit 2 a 2 i + 1
141 73 103 140 3eqtrd # b a = y + 1 a 1 2 0 a 2 y k 0 ..^ y + 1 k digit 2 a 2 k = 1 + i = 0 + 1 - 1 y 1 i + 1 digit 2 a 2 i + 1
142 141 adantl a 1 2 = k 0 ..^ y k digit 2 a 1 2 2 k # b a = y + 1 a 1 2 0 a 2 y k 0 ..^ y + 1 k digit 2 a 2 k = 1 + i = 0 + 1 - 1 y 1 i + 1 digit 2 a 2 i + 1
143 78 a1i a 1 2 0 a 2 i 0 ..^ y 2
144 elfzoelz i 0 ..^ y i
145 144 adantl a 1 2 0 a 2 i 0 ..^ y i
146 nn0rp0 a 1 2 0 a 1 2 0 +∞
147 146 adantr a 1 2 0 a 2 a 1 2 0 +∞
148 147 adantr a 1 2 0 a 2 i 0 ..^ y a 1 2 0 +∞
149 digvalnn0 2 i a 1 2 0 +∞ i digit 2 a 1 2 0
150 143 145 148 149 syl3anc a 1 2 0 a 2 i 0 ..^ y i digit 2 a 1 2 0
151 150 nn0cnd a 1 2 0 a 2 i 0 ..^ y i digit 2 a 1 2
152 151 ex a 1 2 0 a 2 i 0 ..^ y i digit 2 a 1 2
153 152 ad2antrl # b a = y + 1 a 1 2 0 a 2 y i 0 ..^ y i digit 2 a 1 2
154 153 imp # b a = y + 1 a 1 2 0 a 2 y i 0 ..^ y i digit 2 a 1 2
155 92 a1i i 0 ..^ y 2 0
156 elfzonn0 i 0 ..^ y i 0
157 155 156 nn0expcld i 0 ..^ y 2 i 0
158 157 nn0cnd i 0 ..^ y 2 i
159 158 adantl # b a = y + 1 a 1 2 0 a 2 y i 0 ..^ y 2 i
160 2cnd # b a = y + 1 a 1 2 0 a 2 y i 0 ..^ y 2
161 154 159 160 mulassd # b a = y + 1 a 1 2 0 a 2 y i 0 ..^ y i digit 2 a 1 2 2 i 2 = i digit 2 a 1 2 2 i 2
162 161 eqcomd # b a = y + 1 a 1 2 0 a 2 y i 0 ..^ y i digit 2 a 1 2 2 i 2 = i digit 2 a 1 2 2 i 2
163 162 sumeq2dv # b a = y + 1 a 1 2 0 a 2 y i 0 ..^ y i digit 2 a 1 2 2 i 2 = i 0 ..^ y i digit 2 a 1 2 2 i 2
164 163 adantl a 1 2 = k 0 ..^ y k digit 2 a 1 2 2 k # b a = y + 1 a 1 2 0 a 2 y i 0 ..^ y i digit 2 a 1 2 2 i 2 = i 0 ..^ y i digit 2 a 1 2 2 i 2
165 0cn 0
166 pncan1 0 0 + 1 - 1 = 0
167 165 166 ax-mp 0 + 1 - 1 = 0
168 167 a1i y 0 + 1 - 1 = 0
169 168 oveq1d y 0 + 1 - 1 y 1 = 0 y 1
170 fzoval y 0 ..^ y = 0 y 1
171 68 170 syl y 0 ..^ y = 0 y 1
172 169 171 eqtr4d y 0 + 1 - 1 y 1 = 0 ..^ y
173 172 ad2antll # b a = y + 1 a 1 2 0 a 2 y 0 + 1 - 1 y 1 = 0 ..^ y
174 simprlr # b a = y + 1 a 1 2 0 a 2 y a 2
175 elfznn0 i 0 y 1 i 0
176 167 oveq1i 0 + 1 - 1 y 1 = 0 y 1
177 175 176 eleq2s i 0 + 1 - 1 y 1 i 0
178 dignn0flhalf a 2 i 0 i + 1 digit 2 a = i digit 2 a 2
179 174 177 178 syl2an # b a = y + 1 a 1 2 0 a 2 y i 0 + 1 - 1 y 1 i + 1 digit 2 a = i digit 2 a 2
180 eluzelz a 2 a
181 180 adantr a 2 a 1 2 0 a
182 nn0z a 1 2 0 a 1 2
183 zob a a + 1 2 a 1 2
184 180 183 syl a 2 a + 1 2 a 1 2
185 182 184 syl5ibr a 2 a 1 2 0 a + 1 2
186 185 imp a 2 a 1 2 0 a + 1 2
187 181 186 jca a 2 a 1 2 0 a a + 1 2
188 187 ancoms a 1 2 0 a 2 a a + 1 2
189 188 ad2antrl # b a = y + 1 a 1 2 0 a 2 y a a + 1 2
190 189 adantr # b a = y + 1 a 1 2 0 a 2 y i 0 + 1 - 1 y 1 a a + 1 2
191 zofldiv2 a a + 1 2 a 2 = a 1 2
192 190 191 syl # b a = y + 1 a 1 2 0 a 2 y i 0 + 1 - 1 y 1 a 2 = a 1 2
193 192 oveq2d # b a = y + 1 a 1 2 0 a 2 y i 0 + 1 - 1 y 1 i digit 2 a 2 = i digit 2 a 1 2
194 179 193 eqtrd # b a = y + 1 a 1 2 0 a 2 y i 0 + 1 - 1 y 1 i + 1 digit 2 a = i digit 2 a 1 2
195 2cnd i 0 + 1 - 1 y 1 2
196 195 177 expp1d i 0 + 1 - 1 y 1 2 i + 1 = 2 i 2
197 196 adantl # b a = y + 1 a 1 2 0 a 2 y i 0 + 1 - 1 y 1 2 i + 1 = 2 i 2
198 194 197 oveq12d # b a = y + 1 a 1 2 0 a 2 y i 0 + 1 - 1 y 1 i + 1 digit 2 a 2 i + 1 = i digit 2 a 1 2 2 i 2
199 173 198 sumeq12dv # b a = y + 1 a 1 2 0 a 2 y i = 0 + 1 - 1 y 1 i + 1 digit 2 a 2 i + 1 = i 0 ..^ y i digit 2 a 1 2 2 i 2
200 199 adantl a 1 2 = k 0 ..^ y k digit 2 a 1 2 2 k # b a = y + 1 a 1 2 0 a 2 y i = 0 + 1 - 1 y 1 i + 1 digit 2 a 2 i + 1 = i 0 ..^ y i digit 2 a 1 2 2 i 2
201 oveq1 k = i k digit 2 a 1 2 = i digit 2 a 1 2
202 oveq2 k = i 2 k = 2 i
203 201 202 oveq12d k = i k digit 2 a 1 2 2 k = i digit 2 a 1 2 2 i
204 203 cbvsumv k 0 ..^ y k digit 2 a 1 2 2 k = i 0 ..^ y i digit 2 a 1 2 2 i
205 204 eqeq2i a 1 2 = k 0 ..^ y k digit 2 a 1 2 2 k a 1 2 = i 0 ..^ y i digit 2 a 1 2 2 i
206 205 biimpi a 1 2 = k 0 ..^ y k digit 2 a 1 2 2 k a 1 2 = i 0 ..^ y i digit 2 a 1 2 2 i
207 206 adantr a 1 2 = k 0 ..^ y k digit 2 a 1 2 2 k # b a = y + 1 a 1 2 0 a 2 y a 1 2 = i 0 ..^ y i digit 2 a 1 2 2 i
208 207 oveq1d a 1 2 = k 0 ..^ y k digit 2 a 1 2 2 k # b a = y + 1 a 1 2 0 a 2 y a 1 2 2 = i 0 ..^ y i digit 2 a 1 2 2 i 2
209 fzofi 0 ..^ y Fin
210 209 a1i a 1 2 = k 0 ..^ y k digit 2 a 1 2 2 k # b a = y + 1 a 1 2 0 a 2 y 0 ..^ y Fin
211 2cnd a 1 2 = k 0 ..^ y k digit 2 a 1 2 2 k # b a = y + 1 a 1 2 0 a 2 y 2
212 158 adantl a 1 2 0 a 2 i 0 ..^ y 2 i
213 151 212 mulcld a 1 2 0 a 2 i 0 ..^ y i digit 2 a 1 2 2 i
214 213 ex a 1 2 0 a 2 i 0 ..^ y i digit 2 a 1 2 2 i
215 214 adantr a 1 2 0 a 2 y i 0 ..^ y i digit 2 a 1 2 2 i
216 215 ad2antll a 1 2 = k 0 ..^ y k digit 2 a 1 2 2 k # b a = y + 1 a 1 2 0 a 2 y i 0 ..^ y i digit 2 a 1 2 2 i
217 216 imp a 1 2 = k 0 ..^ y k digit 2 a 1 2 2 k # b a = y + 1 a 1 2 0 a 2 y i 0 ..^ y i digit 2 a 1 2 2 i
218 210 211 217 fsummulc1 a 1 2 = k 0 ..^ y k digit 2 a 1 2 2 k # b a = y + 1 a 1 2 0 a 2 y i 0 ..^ y i digit 2 a 1 2 2 i 2 = i 0 ..^ y i digit 2 a 1 2 2 i 2
219 208 218 eqtrd a 1 2 = k 0 ..^ y k digit 2 a 1 2 2 k # b a = y + 1 a 1 2 0 a 2 y a 1 2 2 = i 0 ..^ y i digit 2 a 1 2 2 i 2
220 164 200 219 3eqtr4d a 1 2 = k 0 ..^ y k digit 2 a 1 2 2 k # b a = y + 1 a 1 2 0 a 2 y i = 0 + 1 - 1 y 1 i + 1 digit 2 a 2 i + 1 = a 1 2 2
221 220 oveq2d a 1 2 = k 0 ..^ y k digit 2 a 1 2 2 k # b a = y + 1 a 1 2 0 a 2 y 1 + i = 0 + 1 - 1 y 1 i + 1 digit 2 a 2 i + 1 = 1 + a 1 2 2
222 eluzelcn a 2 a
223 peano2cnm a a 1
224 222 223 syl a 2 a 1
225 2cnd a 2 2
226 2ne0 2 0
227 226 a1i a 2 2 0
228 224 225 227 3jca a 2 a 1 2 2 0
229 228 adantl a 1 2 0 a 2 a 1 2 2 0
230 divcan1 a 1 2 2 0 a 1 2 2 = a 1
231 229 230 syl a 1 2 0 a 2 a 1 2 2 = a 1
232 231 oveq2d a 1 2 0 a 2 1 + a 1 2 2 = 1 + a - 1
233 1cnd a 2 1
234 233 222 jca a 2 1 a
235 234 adantl a 1 2 0 a 2 1 a
236 pncan3 1 a 1 + a - 1 = a
237 235 236 syl a 1 2 0 a 2 1 + a - 1 = a
238 232 237 eqtrd a 1 2 0 a 2 1 + a 1 2 2 = a
239 238 adantr a 1 2 0 a 2 y 1 + a 1 2 2 = a
240 239 ad2antll a 1 2 = k 0 ..^ y k digit 2 a 1 2 2 k # b a = y + 1 a 1 2 0 a 2 y 1 + a 1 2 2 = a
241 142 221 240 3eqtrrd a 1 2 = k 0 ..^ y k digit 2 a 1 2 2 k # b a = y + 1 a 1 2 0 a 2 y a = k 0 ..^ y + 1 k digit 2 a 2 k
242 241 ex a 1 2 = k 0 ..^ y k digit 2 a 1 2 2 k # b a = y + 1 a 1 2 0 a 2 y a = k 0 ..^ y + 1 k digit 2 a 2 k
243 242 imim2i # b a 1 2 = y a 1 2 = k 0 ..^ y k digit 2 a 1 2 2 k # b a 1 2 = y # b a = y + 1 a 1 2 0 a 2 y a = k 0 ..^ y + 1 k digit 2 a 2 k
244 243 com13 # b a = y + 1 a 1 2 0 a 2 y # b a 1 2 = y # b a 1 2 = y a 1 2 = k 0 ..^ y k digit 2 a 1 2 2 k a = k 0 ..^ y + 1 k digit 2 a 2 k
245 67 244 syl5bi # b a = y + 1 a 1 2 0 a 2 y y = # b a 1 2 # b a 1 2 = y a 1 2 = k 0 ..^ y k digit 2 a 1 2 2 k a = k 0 ..^ y + 1 k digit 2 a 2 k
246 66 245 sylbid # b a = y + 1 a 1 2 0 a 2 y y + 1 = # b a 1 2 + 1 # b a 1 2 = y a 1 2 = k 0 ..^ y k digit 2 a 1 2 2 k a = k 0 ..^ y + 1 k digit 2 a 2 k
247 246 ex # b a = y + 1 a 1 2 0 a 2 y y + 1 = # b a 1 2 + 1 # b a 1 2 = y a 1 2 = k 0 ..^ y k digit 2 a 1 2 2 k a = k 0 ..^ y + 1 k digit 2 a 2 k
248 247 com23 # b a = y + 1 y + 1 = # b a 1 2 + 1 a 1 2 0 a 2 y # b a 1 2 = y a 1 2 = k 0 ..^ y k digit 2 a 1 2 2 k a = k 0 ..^ y + 1 k digit 2 a 2 k
249 58 248 sylbid # b a = y + 1 # b a = # b a 1 2 + 1 a 1 2 0 a 2 y # b a 1 2 = y a 1 2 = k 0 ..^ y k digit 2 a 1 2 2 k a = k 0 ..^ y + 1 k digit 2 a 2 k
250 249 com23 # b a = y + 1 a 1 2 0 a 2 y # b a = # b a 1 2 + 1 # b a 1 2 = y a 1 2 = k 0 ..^ y k digit 2 a 1 2 2 k a = k 0 ..^ y + 1 k digit 2 a 2 k
251 250 com14 # b a 1 2 = y a 1 2 = k 0 ..^ y k digit 2 a 1 2 2 k a 1 2 0 a 2 y # b a = # b a 1 2 + 1 # b a = y + 1 a = k 0 ..^ y + 1 k digit 2 a 2 k
252 251 exp4c # b a 1 2 = y a 1 2 = k 0 ..^ y k digit 2 a 1 2 2 k a 1 2 0 a 2 y # b a = # b a 1 2 + 1 # b a = y + 1 a = k 0 ..^ y + 1 k digit 2 a 2 k
253 252 com35 # b a 1 2 = y a 1 2 = k 0 ..^ y k digit 2 a 1 2 2 k a 1 2 0 # b a = # b a 1 2 + 1 y a 2 # b a = y + 1 a = k 0 ..^ y + 1 k digit 2 a 2 k
254 57 253 syl a 1 2 0 x 0 # b x = y x = k 0 ..^ y k digit 2 x 2 k a 1 2 0 # b a = # b a 1 2 + 1 y a 2 # b a = y + 1 a = k 0 ..^ y + 1 k digit 2 a 2 k
255 254 ex a 1 2 0 x 0 # b x = y x = k 0 ..^ y k digit 2 x 2 k a 1 2 0 # b a = # b a 1 2 + 1 y a 2 # b a = y + 1 a = k 0 ..^ y + 1 k digit 2 a 2 k
256 255 pm2.43a a 1 2 0 x 0 # b x = y x = k 0 ..^ y k digit 2 x 2 k # b a = # b a 1 2 + 1 y a 2 # b a = y + 1 a = k 0 ..^ y + 1 k digit 2 a 2 k
257 256 com25 a 1 2 0 a 2 # b a = # b a 1 2 + 1 y x 0 # b x = y x = k 0 ..^ y k digit 2 x 2 k # b a = y + 1 a = k 0 ..^ y + 1 k digit 2 a 2 k
258 257 impcom a 2 a 1 2 0 # b a = # b a 1 2 + 1 y x 0 # b x = y x = k 0 ..^ y k digit 2 x 2 k # b a = y + 1 a = k 0 ..^ y + 1 k digit 2 a 2 k
259 49 258 mpd a 2 a 1 2 0 y x 0 # b x = y x = k 0 ..^ y k digit 2 x 2 k # b a = y + 1 a = k 0 ..^ y + 1 k digit 2 a 2 k
260 259 ex a 2 a 1 2 0 y x 0 # b x = y x = k 0 ..^ y k digit 2 x 2 k # b a = y + 1 a = k 0 ..^ y + 1 k digit 2 a 2 k
261 41 260 jaoi a = 1 a 2 a 1 2 0 y x 0 # b x = y x = k 0 ..^ y k digit 2 x 2 k # b a = y + 1 a = k 0 ..^ y + 1 k digit 2 a 2 k
262 1 261 sylbi a a 1 2 0 y x 0 # b x = y x = k 0 ..^ y k digit 2 x 2 k # b a = y + 1 a = k 0 ..^ y + 1 k digit 2 a 2 k
263 262 imp31 a a 1 2 0 y x 0 # b x = y x = k 0 ..^ y k digit 2 x 2 k # b a = y + 1 a = k 0 ..^ y + 1 k digit 2 a 2 k