Theorem nn0sumshdiglem2

Description: Lemma 2 for nn0sumshdig . (Contributed by AV, 7-Jun-2020)

	Ref	Expression
Assertion	nn0sumshdiglem2

Proof

Step	Hyp	Ref	Expression
1		eqeq2
2		oveq2	$$⊢x=1\to \left(0..^x\right)=\left(0..^1\right)$$
3		fzo01	$$⊢\left(0..^1\right)=\left\{0\right\}$$
4	2 3	eqtrdi	$$⊢x=1\to \left(0..^x\right)=\left\{0\right\}$$
5	4	sumeq1d	$$⊢x=1\to \sum _{k\in \left(0..^x\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)a\right)2^k$$
6	5	eqeq2d	$$⊢x=1\to \left(a=\sum _{k\in \left(0..^x\right)}\left(k\mathrm{digit}\left(2\right)a\right)2^k\leftrightarrow a=\sum _{k\in \left\{0\right\}}\left(k\mathrm{digit}\left(2\right)a\right)2^k\right)$$
7	1 6	imbi12d
8	7	ralbidv
9		eqeq2
10		oveq2	$$⊢x=y\to \left(0..^x\right)=\left(0..^y\right)$$
11	10	sumeq1d	$$⊢x=y\to \sum _{k\in \left(0..^x\right)}\left(k\mathrm{digit}\left(2\right)a\right)2^k=\sum _{k\in \left(0..^y\right)}\left(k\mathrm{digit}\left(2\right)a\right)2^k$$
12	11	eqeq2d	$$⊢x=y\to \left(a=\sum _{k\in \left(0..^x\right)}\left(k\mathrm{digit}\left(2\right)a\right)2^k\leftrightarrow a=\sum _{k\in \left(0..^y\right)}\left(k\mathrm{digit}\left(2\right)a\right)2^k\right)$$
13	9 12	imbi12d
14	13	ralbidv
15		eqeq2
16		oveq2	$$⊢x=y+1\to \left(0..^x\right)=\left(0..^y+1\right)$$
17	16	sumeq1d	$$⊢x=y+1\to \sum _{k\in \left(0..^x\right)}\left(k\mathrm{digit}\left(2\right)a\right)2^k=\sum _{k\in \left(0..^y+1\right)}\left(k\mathrm{digit}\left(2\right)a\right)2^k$$
18	17	eqeq2d	$$⊢x=y+1\to \left(a=\sum _{k\in \left(0..^x\right)}\left(k\mathrm{digit}\left(2\right)a\right)2^k\leftrightarrow a=\sum _{k\in \left(0..^y+1\right)}\left(k\mathrm{digit}\left(2\right)a\right)2^k\right)$$
19	15 18	imbi12d
20	19	ralbidv
21		eqeq2
22		oveq2	$$⊢x=L\to \left(0..^x\right)=\left(0..^L\right)$$
23	22	sumeq1d	$$⊢x=L\to \sum _{k\in \left(0..^x\right)}\left(k\mathrm{digit}\left(2\right)a\right)2^k=\sum _{k\in \left(0..^L\right)}\left(k\mathrm{digit}\left(2\right)a\right)2^k$$
24	23	eqeq2d	$$⊢x=L\to \left(a=\sum _{k\in \left(0..^x\right)}\left(k\mathrm{digit}\left(2\right)a\right)2^k\leftrightarrow a=\sum _{k\in \left(0..^L\right)}\left(k\mathrm{digit}\left(2\right)a\right)2^k\right)$$
25	21 24	imbi12d
26	25	ralbidv
27		0cnd	$$⊢a\in {\mathbb{N}}_0\to 0\in ℂ$$
28		2nn	$$⊢2\in \mathbb{N}$$
29	28	a1i	$$⊢a\in {\mathbb{N}}_0\to 2\in \mathbb{N}$$
30		0zd	$$⊢a\in {\mathbb{N}}_0\to 0\in \mathbb{Z}$$
31		nn0rp0	$$⊢a\in {\mathbb{N}}_0\to a\in \left[0,\mathrm{+\infty }\right)$$
32		digvalnn0	$$⊢\left(2\in \mathbb{N}\wedge 0\in \mathbb{Z}\wedge a\in \left[0,\mathrm{+\infty }\right)\right)\to 0\mathrm{digit}\left(2\right)a\in {\mathbb{N}}_0$$
33	29 30 31 32	syl3anc	$$⊢a\in {\mathbb{N}}_0\to 0\mathrm{digit}\left(2\right)a\in {\mathbb{N}}_0$$
34	33	nn0cnd	$$⊢a\in {\mathbb{N}}_0\to 0\mathrm{digit}\left(2\right)a\in ℂ$$
35		1cnd	$$⊢a\in {\mathbb{N}}_0\to 1\in ℂ$$
36	34 35	mulcld	$$⊢a\in {\mathbb{N}}_0\to \left(0\mathrm{digit}\left(2\right)a\right)\cdot 1\in ℂ$$
37	27 36	jca	$$⊢a\in {\mathbb{N}}_0\to \left(0\in ℂ\wedge \left(0\mathrm{digit}\left(2\right)a\right)\cdot 1\in ℂ\right)$$
38	37	adantr
39		oveq1	$$⊢k=0\to k\mathrm{digit}\left(2\right)a=0\mathrm{digit}\left(2\right)a$$
40		oveq2	$$⊢k=0\to 2^k=2^0$$
41		2cn	$$⊢2\in ℂ$$
42		exp0	$$⊢2\in ℂ\to 2^0=1$$
43	41 42	ax-mp	$$⊢2^0=1$$
44	40 43	eqtrdi	$$⊢k=0\to 2^k=1$$
45	39 44	oveq12d	$$⊢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$$
46	45	sumsn	$$⊢\left(0\in ℂ\wedge \left(0\mathrm{digit}\left(2\right)a\right)\cdot 1\in ℂ\right)\to \sum _{k\in \left\{0\right\}}\left(k\mathrm{digit}\left(2\right)a\right)2^k=\left(0\mathrm{digit}\left(2\right)a\right)\cdot 1$$
47	38 46	syl
48	34	adantr
49	48	mulid1d
50		blen1b
51	50	biimpa
52		vex	$$⊢a\in \mathrm{V}$$
53	52	elpr	$$⊢a\in \left\{0,1\right\}\leftrightarrow \left(a=0\vee a=1\right)$$
54	51 53	sylibr
55		0dig2pr01	$$⊢a\in \left\{0,1\right\}\to 0\mathrm{digit}\left(2\right)a=a$$
56	54 55	syl
57	47 49 56	3eqtrrd
58	57	ex
59	58	rgen
60		nn0sumshdiglem1
61	8 14 20 26 59 60	nnind