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	biimpi	$$⊢\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\to \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$$
207	206	adantr
208	207	oveq1d
209		fzofi	$$⊢\left(0..^y\right)\in \mathrm{Fin}$$
210	209	a1i
211		2cnd
212	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 ℂ$$
213	151 212	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 ℂ$$
214	213	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)$$
215	214	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)$$
216	215	ad2antll
217	216	imp
218	210 211 217	fsummulc1
219	208 218	eqtrd
220	164 200 219	3eqtr4d
221	220	oveq2d
222		eluzelcn	$$⊢a\in {\mathbb{Z}}_{\ge 2}\to a\in ℂ$$
223		peano2cnm	$$⊢a\in ℂ\to a-1\in ℂ$$
224	222 223	syl	$$⊢a\in {\mathbb{Z}}_{\ge 2}\to a-1\in ℂ$$
225		2cnd	$$⊢a\in {\mathbb{Z}}_{\ge 2}\to 2\in ℂ$$
226		2ne0	$$⊢2\ne 0$$
227	226	a1i	$$⊢a\in {\mathbb{Z}}_{\ge 2}\to 2\ne 0$$
228	224 225 227	3jca	$$⊢a\in {\mathbb{Z}}_{\ge 2}\to \left(a-1\in ℂ\wedge 2\in ℂ\wedge 2\ne 0\right)$$
229	228	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)$$
230		divcan1	$$⊢\left(a-1\in ℂ\wedge 2\in ℂ\wedge 2\ne 0\right)\to \left(\frac{a-1}{2}\right)\cdot 2=a-1$$
231	229 230	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$$
232	231	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$$
233		1cnd	$$⊢a\in {\mathbb{Z}}_{\ge 2}\to 1\in ℂ$$
234	233 222	jca	$$⊢a\in {\mathbb{Z}}_{\ge 2}\to \left(1\in ℂ\wedge a\in ℂ\right)$$
235	234	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)$$
236		pncan3	$$⊢\left(1\in ℂ\wedge a\in ℂ\right)\to 1+a-1=a$$
237	235 236	syl	$$⊢\left(\frac{a-1}{2}\in {\mathbb{N}}_0\wedge a\in {\mathbb{Z}}_{\ge 2}\right)\to 1+a-1=a$$
238	232 237	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$$
239	238	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$$
240	239	ad2antll
241	142 221 240	3eqtrrd
242	241	ex
243	242	imim2i
244	243	com13
245	67 244	biimtrid
246	66 245	sylbid
247	246	ex
248	247	com23
249	58 248	sylbid
250	249	com23
251	250	com14
252	251	exp4c
253	252	com35
254	57 253	syl
255	254	ex
256	255	pm2.43a
257	256	com25
258	257	impcom
259	49 258	mpd
260	259	ex
261	41 260	jaoi
262	1 261	sylbi
263	262	imp31