Theorem nn0sumshdiglemB

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

	Ref	Expression
Assertion	nn0sumshdiglemB

Proof

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