nn0sumshdiglemA

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

		Ref	Expression
	Assertion	nn0sumshdiglemA	$⊢ ((a \in ℕ \land \frac{a}{2} \in ℕ) \land y \in ℕ) \to (\forall x \in ℕ_{0} (#_{b(x)=y\tox = \sum_{k \in (0 ..^y)} (k digit (2) x) 2^{k}\to(#_{b} (a) = y + 1 \to a = \sum_{k \in (0 ..^y + 1)} (k digit (2) a) 2^{k})}))$

Proof

Step	Hyp	Ref	Expression
1		nnnn0	$⊢ \frac{a}{2} \in ℕ \to \frac{a}{2} \in ℕ_{0}$
2		blennn0em1	$⊢ (a \in ℕ \land \frac{a}{2} \in ℕ_{0}) \to #_{b(\frac{a}{2})=#_{b} (a) - 1}$
3	1 2	sylan2	$⊢ (a \in ℕ \land \frac{a}{2} \in ℕ) \to #_{b(\frac{a}{2})=#_{b} (a) - 1}$
4		fveqeq2	$⊢ x = \frac{a}{2} \to (#_{b(x)=y\leftrightarrow#_{b} (\frac{a}{2}) = y})$
5		id	$⊢ x = \frac{a}{2} \to x = \frac{a}{2}$
6		oveq2	$⊢ x = \frac{a}{2} \to k digit (2) x = k digit (2) (\frac{a}{2})$
7	6	oveq1d	$⊢ x = \frac{a}{2} \to (k digit (2) x) 2^{k} = (k digit (2) (\frac{a}{2})) 2^{k}$
8	7	adantr	$⊢ (x = \frac{a}{2} \land k \in (0 ..^y)) \to (k digit (2) x) 2^{k} = (k digit (2) (\frac{a}{2})) 2^{k}$
9	8	sumeq2dv	$⊢ x = \frac{a}{2} \to \sum_{k \in (0 ..^y)} (k digit (2) x) 2^{k} = \sum_{k \in (0 ..^y)} (k digit (2) (\frac{a}{2})) 2^{k}$
10	5 9	eqeq12d	$⊢ x = \frac{a}{2} \to (x = \sum_{k \in (0 ..^y)} (k digit (2) x) 2^{k} \leftrightarrow \frac{a}{2} = \sum_{k \in (0 ..^y)} (k digit (2) (\frac{a}{2})) 2^{k})$
11	4 10	imbi12d	$⊢ x = \frac{a}{2} \to ((#_{b(x)=y\tox = \sum_{k \in (0 ..^y)} (k digit (2) x) 2^{k}\leftrightarrow(#_{b} (\frac{a}{2}) = y \to \frac{a}{2} = \sum_{k \in (0 ..^y)} (k digit (2) (\frac{a}{2})) 2^{k})}))$
12	11	rspcva	$⊢ (\frac{a}{2} \in ℕ_{0} \land \forall x \in ℕ_{0} (#_{b(x)=y\tox = \sum_{k \in (0 ..^y)} (k digit (2) x) 2^{k}\to(#_{b} (\frac{a}{2}) = y \to \frac{a}{2} = \sum_{k \in (0 ..^y)} (k digit (2) (\frac{a}{2})) 2^{k})}))$
13		simpr	$⊢ ((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\to#_{b} (a) = y + 1})$
14	13	oveq1d	$⊢ ((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\to#_{b} (a) - 1 = y + 1 - 1})$
15		nncn	$⊢ y \in ℕ \to y \in ℂ$
16		pncan1	$⊢ y \in ℂ \to y + 1 - 1 = y$
17	15 16	syl	$⊢ y \in ℕ \to y + 1 - 1 = y$
18	14 17	sylan9eq	$⊢ (((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\to#_{b} (a) - 1 = y}))$
19	18	eqeq2d	$⊢ (((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\to(#_{b} (\frac{a}{2}) = #_{b} (a) - 1 \leftrightarrow #_{b} (\frac{a}{2}) = y)}))$
20		nnz	$⊢ y \in ℕ \to y \in ℤ$
21	20	adantl	$⊢ (((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\toy \in ℤ}))$
22		fzval3	$⊢ y \in ℤ \to (0 \dots y) = (0 ..^y + 1)$
23	21 22	syl	$⊢ (((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\to(0 \dots y) = (0 ..^y + 1)}))$
24	23	eqcomd	$⊢ (((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\to(0 ..^y + 1) = (0 \dots y)}))$
25	24	sumeq1d	$⊢ (((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\to\sum_{k \in (0 ..^y + 1)} (k digit (2) a) 2^{k} = \sum_{k = 0}^{y} (k digit (2) a) 2^{k}}))$
26		nnnn0	$⊢ y \in ℕ \to y \in ℕ_{0}$
27		elnn0uz	$⊢ y \in ℕ_{0} \leftrightarrow y \in ℤ_{\geq 0}$
28	26 27	sylib	$⊢ y \in ℕ \to y \in ℤ_{\geq 0}$
29	28	adantl	$⊢ (((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\toy \in ℤ_{\geq 0}}))$
30		2nn	$⊢ 2 \in ℕ$
31	30	a1i	$⊢ ((((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\landk \in (0 \dots y)\to2 \in ℕ})))$
32		elfzelz	$⊢ k \in (0 \dots y) \to k \in ℤ$
33	32	adantl	$⊢ ((((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\landk \in (0 \dots y)\tok \in ℤ})))$
34		nnnn0	$⊢ a \in ℕ \to a \in ℕ_{0}$
35		nn0rp0	$⊢ a \in ℕ_{0} \to a \in [0, +∞)$
36	34 35	syl	$⊢ a \in ℕ \to a \in [0, +∞)$
37	36	ad4antlr	$⊢ ((((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\landk \in (0 \dots y)\toa \in [0, +∞)})))$
38		digvalnn0	$⊢ (2 \in ℕ \land k \in ℤ \land a \in [0, +∞)) \to k digit (2) a \in ℕ_{0}$
39	31 33 37 38	syl3anc	$⊢ ((((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\landk \in (0 \dots y)\tok digit (2) a \in ℕ_{0}})))$
40	39	nn0cnd	$⊢ ((((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\landk \in (0 \dots y)\tok digit (2) a \in ℂ})))$
41		2nn0	$⊢ 2 \in ℕ_{0}$
42	41	a1i	$⊢ k \in (0 \dots y) \to 2 \in ℕ_{0}$
43		elfznn0	$⊢ k \in (0 \dots y) \to k \in ℕ_{0}$
44	42 43	nn0expcld	$⊢ k \in (0 \dots y) \to 2^{k} \in ℕ_{0}$
45	44	nn0cnd	$⊢ k \in (0 \dots y) \to 2^{k} \in ℂ$
46	45	adantl	$⊢ ((((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\landk \in (0 \dots y)\to2^{k} \in ℂ})))$
47	40 46	mulcld	$⊢ ((((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\landk \in (0 \dots y)\to(k digit (2) a) 2^{k} \in ℂ})))$
48		oveq1	$⊢ k = 0 \to k digit (2) a = 0 digit (2) a$
49		oveq2	$⊢ k = 0 \to 2^{k} = 2^{0}$
50	48 49	oveq12d	$⊢ k = 0 \to (k digit (2) a) 2^{k} = (0 digit (2) a) 2^{0}$
51		2cn	$⊢ 2 \in ℂ$
52		exp0	$⊢ 2 \in ℂ \to 2^{0} = 1$
53	51 52	ax-mp	$⊢ 2^{0} = 1$
54	53	oveq2i	$⊢ (0 digit (2) a) 2^{0} = (0 digit (2) a) \cdot 1$
55	50 54	eqtrdi	$⊢ k = 0 \to (k digit (2) a) 2^{k} = (0 digit (2) a) \cdot 1$
56	29 47 55	fsum1p	$⊢ (((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\to\sum_{k = 0}^{y} (k digit (2) a) 2^{k} = (0 digit (2) a) \cdot 1 + \sum_{k = 0 + 1}^{y} (k digit (2) a) 2^{k}}))$
57		0dig2nn0e	$⊢ (a \in ℕ_{0} \land \frac{a}{2} \in ℕ_{0}) \to 0 digit (2) a = 0$
58	34 1 57	syl2anr	$⊢ (\frac{a}{2} \in ℕ \land a \in ℕ) \to 0 digit (2) a = 0$
59	58	oveq1d	$⊢ (\frac{a}{2} \in ℕ \land a \in ℕ) \to (0 digit (2) a) \cdot 1 = 0 \cdot 1$
60		1re	$⊢ 1 \in ℝ$
61		mul02lem2	$⊢ 1 \in ℝ \to 0 \cdot 1 = 0$
62	60 61	ax-mp	$⊢ 0 \cdot 1 = 0$
63	59 62	eqtrdi	$⊢ (\frac{a}{2} \in ℕ \land a \in ℕ) \to (0 digit (2) a) \cdot 1 = 0$
64	63	adantr	$⊢ ((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\to(0 digit (2) a) \cdot 1 = 0})$
65	64	adantr	$⊢ (((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\to(0 digit (2) a) \cdot 1 = 0}))$
66		1z	$⊢ 1 \in ℤ$
67	66	a1i	$⊢ (((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\to1 \in ℤ}))$
68		0p1e1	$⊢ 0 + 1 = 1$
69	68 66	eqeltri	$⊢ 0 + 1 \in ℤ$
70	69	a1i	$⊢ (((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\to0 + 1 \in ℤ}))$
71	30	a1i	$⊢ ((((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\landk \in (0 + 1 \dots y)\to2 \in ℕ})))$
72		elfzelz	$⊢ k \in (0 + 1 \dots y) \to k \in ℤ$
73	72	adantl	$⊢ ((((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\landk \in (0 + 1 \dots y)\tok \in ℤ})))$
74	36	ad4antlr	$⊢ ((((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\landk \in (0 + 1 \dots y)\toa \in [0, +∞)})))$
75	71 73 74 38	syl3anc	$⊢ ((((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\landk \in (0 + 1 \dots y)\tok digit (2) a \in ℕ_{0}})))$
76	75	nn0cnd	$⊢ ((((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\landk \in (0 + 1 \dots y)\tok digit (2) a \in ℂ})))$
77		2cnd	$⊢ k \in (0 + 1 \dots y) \to 2 \in ℂ$
78		elfznn	$⊢ k \in (1 \dots y) \to k \in ℕ$
79	78	nnnn0d	$⊢ k \in (1 \dots y) \to k \in ℕ_{0}$
80	68	oveq1i	$⊢ (0 + 1 \dots y) = (1 \dots y)$
81	79 80	eleq2s	$⊢ k \in (0 + 1 \dots y) \to k \in ℕ_{0}$
82	77 81	expcld	$⊢ k \in (0 + 1 \dots y) \to 2^{k} \in ℂ$
83	82	adantl	$⊢ ((((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\landk \in (0 + 1 \dots y)\to2^{k} \in ℂ})))$
84	76 83	mulcld	$⊢ ((((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\landk \in (0 + 1 \dots y)\to(k digit (2) a) 2^{k} \in ℂ})))$
85		oveq1	$⊢ k = i + 1 \to k digit (2) a = (i + 1) digit (2) a$
86		oveq2	$⊢ k = i + 1 \to 2^{k} = 2^{i + 1}$
87	85 86	oveq12d	$⊢ k = i + 1 \to (k digit (2) a) 2^{k} = ((i + 1) digit (2) a) 2^{i + 1}$
88	67 70 21 84 87	fsumshftm	$⊢ (((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\to\sum_{k = 0 + 1}^{y} (k digit (2) a) 2^{k} = \sum_{i = 0 + 1 - 1}^{y - 1} ((i + 1) digit (2) a) 2^{i + 1}}))$
89	65 88	oveq12d	$⊢ (((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\to(0 digit (2) a) \cdot 1 + \sum_{k = 0 + 1}^{y} (k digit (2) a) 2^{k} = 0 + \sum_{i = 0 + 1 - 1}^{y - 1} ((i + 1) digit (2) a) 2^{i + 1}}))$
90	1	ad4antr	$⊢ ((((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\landi \in (0 ..^y)\to\frac{a}{2} \in ℕ_{0}})))$
91	34	ad4antlr	$⊢ ((((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\landi \in (0 ..^y)\toa \in ℕ_{0}})))$
92		elfzonn0	$⊢ i \in (0 ..^y) \to i \in ℕ_{0}$
93	92	adantl	$⊢ ((((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\landi \in (0 ..^y)\toi \in ℕ_{0}})))$
94		dignn0ehalf	$⊢ (\frac{a}{2} \in ℕ_{0} \land a \in ℕ_{0} \land i \in ℕ_{0}) \to (i + 1) digit (2) a = i digit (2) (\frac{a}{2})$
95	90 91 93 94	syl3anc	$⊢ ((((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\landi \in (0 ..^y)\to(i + 1) digit (2) a = i digit (2) (\frac{a}{2})})))$
96		2cnd	$⊢ i \in (0 ..^y) \to 2 \in ℂ$
97	96 92	expp1d	$⊢ i \in (0 ..^y) \to 2^{i + 1} = 2^{i} \cdot 2$
98	97	adantl	$⊢ ((((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\landi \in (0 ..^y)\to2^{i + 1} = 2^{i} \cdot 2})))$
99	95 98	oveq12d	$⊢ ((((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\landi \in (0 ..^y)\to((i + 1) digit (2) a) 2^{i + 1} = (i digit (2) (\frac{a}{2})) 2^{i} \cdot 2})))$
100	30	a1i	$⊢ ((((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\landi \in (0 ..^y)\to2 \in ℕ})))$
101		elfzoelz	$⊢ i \in (0 ..^y) \to i \in ℤ$
102	101	adantl	$⊢ ((((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\landi \in (0 ..^y)\toi \in ℤ})))$
103		nn0rp0	$⊢ \frac{a}{2} \in ℕ_{0} \to \frac{a}{2} \in [0, +∞)$
104	1 103	syl	$⊢ \frac{a}{2} \in ℕ \to \frac{a}{2} \in [0, +∞)$
105	104	ad4antr	$⊢ ((((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\landi \in (0 ..^y)\to\frac{a}{2} \in [0, +∞)})))$
106		digvalnn0	$⊢ (2 \in ℕ \land i \in ℤ \land \frac{a}{2} \in [0, +∞)) \to i digit (2) (\frac{a}{2}) \in ℕ_{0}$
107	100 102 105 106	syl3anc	$⊢ ((((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\landi \in (0 ..^y)\toi digit (2) (\frac{a}{2}) \in ℕ_{0}})))$
108	107	nn0cnd	$⊢ ((((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\landi \in (0 ..^y)\toi digit (2) (\frac{a}{2}) \in ℂ})))$
109		2re	$⊢ 2 \in ℝ$
110	109	a1i	$⊢ i \in (0 ..^y) \to 2 \in ℝ$
111	110 92	reexpcld	$⊢ i \in (0 ..^y) \to 2^{i} \in ℝ$
112	111	recnd	$⊢ i \in (0 ..^y) \to 2^{i} \in ℂ$
113	112	adantl	$⊢ ((((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\landi \in (0 ..^y)\to2^{i} \in ℂ})))$
114		2cnd	$⊢ ((((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\landi \in (0 ..^y)\to2 \in ℂ})))$
115		mulass	$⊢ (i digit (2) (\frac{a}{2}) \in ℂ \land 2^{i} \in ℂ \land 2 \in ℂ) \to (i digit (2) (\frac{a}{2})) 2^{i} \cdot 2 = (i digit (2) (\frac{a}{2})) 2^{i} \cdot 2$
116	115	eqcomd	$⊢ (i digit (2) (\frac{a}{2}) \in ℂ \land 2^{i} \in ℂ \land 2 \in ℂ) \to (i digit (2) (\frac{a}{2})) 2^{i} \cdot 2 = (i digit (2) (\frac{a}{2})) 2^{i} \cdot 2$
117	108 113 114 116	syl3anc	$⊢ ((((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\landi \in (0 ..^y)\to(i digit (2) (\frac{a}{2})) 2^{i} \cdot 2 = (i digit (2) (\frac{a}{2})) 2^{i} \cdot 2})))$
118	99 117	eqtrd	$⊢ ((((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\landi \in (0 ..^y)\to((i + 1) digit (2) a) 2^{i + 1} = (i digit (2) (\frac{a}{2})) 2^{i} \cdot 2})))$
119	118	sumeq2dv	$⊢ (((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\to\sum_{i \in (0 ..^y)} ((i + 1) digit (2) a) 2^{i + 1} = \sum_{i \in (0 ..^y)} (i digit (2) (\frac{a}{2})) 2^{i} \cdot 2}))$
120		0cn	$⊢ 0 \in ℂ$
121		pncan1	$⊢ 0 \in ℂ \to 0 + 1 - 1 = 0$
122	120 121	ax-mp	$⊢ 0 + 1 - 1 = 0$
123	122	a1i	$⊢ y \in ℕ \to 0 + 1 - 1 = 0$
124	123	oveq1d	$⊢ y \in ℕ \to (0 + 1 - 1 \dots y - 1) = (0 \dots y - 1)$
125		fzoval	$⊢ y \in ℤ \to (0 ..^y) = (0 \dots y - 1)$
126	125	eqcomd	$⊢ y \in ℤ \to (0 \dots y - 1) = (0 ..^y)$
127	20 126	syl	$⊢ y \in ℕ \to (0 \dots y - 1) = (0 ..^y)$
128	124 127	eqtrd	$⊢ y \in ℕ \to (0 + 1 - 1 \dots y - 1) = (0 ..^y)$
129	128	adantl	$⊢ (((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\to(0 + 1 - 1 \dots y - 1) = (0 ..^y)}))$
130	129	sumeq1d	$⊢ (((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\to\sum_{i = 0 + 1 - 1}^{y - 1} ((i + 1) digit (2) a) 2^{i + 1} = \sum_{i \in (0 ..^y)} ((i + 1) digit (2) a) 2^{i + 1}}))$
131	130	oveq2d	$⊢ (((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\to0 + \sum_{i = 0 + 1 - 1}^{y - 1} ((i + 1) digit (2) a) 2^{i + 1} = 0 + \sum_{i \in (0 ..^y)} ((i + 1) digit (2) a) 2^{i + 1}}))$
132		fzofi	$⊢ (0 ..^y) \in Fin$
133	132	a1i	$⊢ (((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\to(0 ..^y) \in Fin}))$
134	101	peano2zd	$⊢ i \in (0 ..^y) \to i + 1 \in ℤ$
135	134	adantl	$⊢ ((((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\landi \in (0 ..^y)\toi + 1 \in ℤ})))$
136	36	ad4antlr	$⊢ ((((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\landi \in (0 ..^y)\toa \in [0, +∞)})))$
137		digvalnn0	$⊢ (2 \in ℕ \land i + 1 \in ℤ \land a \in [0, +∞)) \to (i + 1) digit (2) a \in ℕ_{0}$
138	100 135 136 137	syl3anc	$⊢ ((((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\landi \in (0 ..^y)\to(i + 1) digit (2) a \in ℕ_{0}})))$
139	138	nn0cnd	$⊢ ((((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\landi \in (0 ..^y)\to(i + 1) digit (2) a \in ℂ})))$
140	41	a1i	$⊢ i \in (0 ..^y) \to 2 \in ℕ_{0}$
141		peano2nn0	$⊢ i \in ℕ_{0} \to i + 1 \in ℕ_{0}$
142	92 141	syl	$⊢ i \in (0 ..^y) \to i + 1 \in ℕ_{0}$
143	140 142	nn0expcld	$⊢ i \in (0 ..^y) \to 2^{i + 1} \in ℕ_{0}$
144	143	nn0cnd	$⊢ i \in (0 ..^y) \to 2^{i + 1} \in ℂ$
145	144	adantl	$⊢ ((((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\landi \in (0 ..^y)\to2^{i + 1} \in ℂ})))$
146	139 145	mulcld	$⊢ ((((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\landi \in (0 ..^y)\to((i + 1) digit (2) a) 2^{i + 1} \in ℂ})))$
147	133 146	fsumcl	$⊢ (((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\to\sum_{i \in (0 ..^y)} ((i + 1) digit (2) a) 2^{i + 1} \in ℂ}))$
148	147	addid2d	$⊢ (((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\to0 + \sum_{i \in (0 ..^y)} ((i + 1) digit (2) a) 2^{i + 1} = \sum_{i \in (0 ..^y)} ((i + 1) digit (2) a) 2^{i + 1}}))$
149	131 148	eqtrd	$⊢ (((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\to0 + \sum_{i = 0 + 1 - 1}^{y - 1} ((i + 1) digit (2) a) 2^{i + 1} = \sum_{i \in (0 ..^y)} ((i + 1) digit (2) a) 2^{i + 1}}))$
150		2cnd	$⊢ (((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\to2 \in ℂ}))$
151	140 92	nn0expcld	$⊢ i \in (0 ..^y) \to 2^{i} \in ℕ_{0}$
152	151	nn0cnd	$⊢ i \in (0 ..^y) \to 2^{i} \in ℂ$
153	152	adantl	$⊢ ((((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\landi \in (0 ..^y)\to2^{i} \in ℂ})))$
154	108 153	mulcld	$⊢ ((((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\landi \in (0 ..^y)\to(i digit (2) (\frac{a}{2})) 2^{i} \in ℂ})))$
155	133 150 154	fsummulc1	$⊢ (((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\to\sum_{i \in (0 ..^y)} (i digit (2) (\frac{a}{2})) 2^{i} \cdot 2 = \sum_{i \in (0 ..^y)} (i digit (2) (\frac{a}{2})) 2^{i} \cdot 2}))$
156	119 149 155	3eqtr4d	$⊢ (((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\to0 + \sum_{i = 0 + 1 - 1}^{y - 1} ((i + 1) digit (2) a) 2^{i + 1} = \sum_{i \in (0 ..^y)} (i digit (2) (\frac{a}{2})) 2^{i} \cdot 2}))$
157	89 156	eqtrd	$⊢ (((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\to(0 digit (2) a) \cdot 1 + \sum_{k = 0 + 1}^{y} (k digit (2) a) 2^{k} = \sum_{i \in (0 ..^y)} (i digit (2) (\frac{a}{2})) 2^{i} \cdot 2}))$
158	25 56 157	3eqtrd	$⊢ (((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\to\sum_{k \in (0 ..^y + 1)} (k digit (2) a) 2^{k} = \sum_{i \in (0 ..^y)} (i digit (2) (\frac{a}{2})) 2^{i} \cdot 2}))$
159	158	adantl	$⊢ (\frac{a}{2} = \sum_{k \in (0 ..^y)} (k digit (2) (\frac{a}{2})) 2^{k} \land (((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\to\sum_{k \in (0 ..^y + 1)} (k digit (2) a) 2^{k} = \sum_{i \in (0 ..^y)} (i digit (2) (\frac{a}{2})) 2^{i} \cdot 2})))$
160		oveq1	$⊢ k = i \to k digit (2) (\frac{a}{2}) = i digit (2) (\frac{a}{2})$
161		oveq2	$⊢ k = i \to 2^{k} = 2^{i}$
162	160 161	oveq12d	$⊢ k = i \to (k digit (2) (\frac{a}{2})) 2^{k} = (i digit (2) (\frac{a}{2})) 2^{i}$
163	162	cbvsumv	$⊢ \sum_{k \in (0 ..^y)} (k digit (2) (\frac{a}{2})) 2^{k} = \sum_{i \in (0 ..^y)} (i digit (2) (\frac{a}{2})) 2^{i}$
164	163	a1i	$⊢ (((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\to\sum_{k \in (0 ..^y)} (k digit (2) (\frac{a}{2})) 2^{k} = \sum_{i \in (0 ..^y)} (i digit (2) (\frac{a}{2})) 2^{i}}))$
165	164	eqeq2d	$⊢ (((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\to(\frac{a}{2} = \sum_{k \in (0 ..^y)} (k digit (2) (\frac{a}{2})) 2^{k} \leftrightarrow \frac{a}{2} = \sum_{i \in (0 ..^y)} (i digit (2) (\frac{a}{2})) 2^{i})}))$
166	165	biimpac	$⊢ (\frac{a}{2} = \sum_{k \in (0 ..^y)} (k digit (2) (\frac{a}{2})) 2^{k} \land (((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\to\frac{a}{2} = \sum_{i \in (0 ..^y)} (i digit (2) (\frac{a}{2})) 2^{i}})))$
167	166	eqcomd	$⊢ (\frac{a}{2} = \sum_{k \in (0 ..^y)} (k digit (2) (\frac{a}{2})) 2^{k} \land (((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\to\sum_{i \in (0 ..^y)} (i digit (2) (\frac{a}{2})) 2^{i} = \frac{a}{2}})))$
168	167	oveq1d	$⊢ (\frac{a}{2} = \sum_{k \in (0 ..^y)} (k digit (2) (\frac{a}{2})) 2^{k} \land (((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\to\sum_{i \in (0 ..^y)} (i digit (2) (\frac{a}{2})) 2^{i} \cdot 2 = (\frac{a}{2}) \cdot 2})))$
169		nncn	$⊢ a \in ℕ \to a \in ℂ$
170		2cnd	$⊢ a \in ℕ \to 2 \in ℂ$
171		2ne0	$⊢ 2 \neq 0$
172	171	a1i	$⊢ a \in ℕ \to 2 \neq 0$
173	169 170 172	divcan1d	$⊢ a \in ℕ \to (\frac{a}{2}) \cdot 2 = a$
174	173	ad3antlr	$⊢ (((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\to(\frac{a}{2}) \cdot 2 = a}))$
175	174	adantl	$⊢ (\frac{a}{2} = \sum_{k \in (0 ..^y)} (k digit (2) (\frac{a}{2})) 2^{k} \land (((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\to(\frac{a}{2}) \cdot 2 = a})))$
176	159 168 175	3eqtrrd	$⊢ (\frac{a}{2} = \sum_{k \in (0 ..^y)} (k digit (2) (\frac{a}{2})) 2^{k} \land (((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\toa = \sum_{k \in (0 ..^y + 1)} (k digit (2) a) 2^{k}})))$
177	176	ex	$⊢ \frac{a}{2} = \sum_{k \in (0 ..^y)} (k digit (2) (\frac{a}{2})) 2^{k} \to ((((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\toa = \sum_{k \in (0 ..^y + 1)} (k digit (2) a) 2^{k}})))$
178	177	imim2i	$⊢ (#_{b(\frac{a}{2})=y\to\frac{a}{2} = \sum_{k \in (0 ..^y)} (k digit (2) (\frac{a}{2})) 2^{k}\to(#_{b} (\frac{a}{2}) = y \to ((((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b} (a) = y + 1) \land y \in ℕ) \to a = \sum_{k \in (0 ..^y + 1)} (k digit (2) a) 2^{k}))})$
179	178	com13	$⊢ (((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\to(#_{b} (\frac{a}{2}) = y \to ((#_{b} (\frac{a}{2}) = y \to \frac{a}{2} = \sum_{k \in (0 ..^y)} (k digit (2) (\frac{a}{2})) 2^{k}) \to a = \sum_{k \in (0 ..^y + 1)} (k digit (2) a) 2^{k}))}))$
180	19 179	sylbid	$⊢ (((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\to(#_{b} (\frac{a}{2}) = #_{b} (a) - 1 \to ((#_{b} (\frac{a}{2}) = y \to \frac{a}{2} = \sum_{k \in (0 ..^y)} (k digit (2) (\frac{a}{2})) 2^{k}) \to a = \sum_{k \in (0 ..^y + 1)} (k digit (2) a) 2^{k}))}))$
181	180	com23	$⊢ (((\frac{a}{2} \in ℕ \land a \in ℕ) \land #_{b(a)=y + 1\landy \in ℕ\to((#_{b} (\frac{a}{2}) = y \to \frac{a}{2} = \sum_{k \in (0 ..^y)} (k digit (2) (\frac{a}{2})) 2^{k}) \to (#_{b} (\frac{a}{2}) = #_{b} (a) - 1 \to a = \sum_{k \in (0 ..^y + 1)} (k digit (2) a) 2^{k}))}))$
182	181	exp31	$⊢ (\frac{a}{2} \in ℕ \land a \in ℕ) \to (#_{b(a)=y + 1\to(y \in ℕ \to ((#_{b} (\frac{a}{2}) = y \to \frac{a}{2} = \sum_{k \in (0 ..^y)} (k digit (2) (\frac{a}{2})) 2^{k}) \to (#_{b} (\frac{a}{2}) = #_{b} (a) - 1 \to a = \sum_{k \in (0 ..^y + 1)} (k digit (2) a) 2^{k})))})$
183	182	com25	$⊢ (\frac{a}{2} \in ℕ \land a \in ℕ) \to (#_{b(\frac{a}{2})=#_{b} (a) - 1\to(y \in ℕ \to ((#_{b} (\frac{a}{2}) = y \to \frac{a}{2} = \sum_{k \in (0 ..^y)} (k digit (2) (\frac{a}{2})) 2^{k}) \to (#_{b} (a) = y + 1 \to a = \sum_{k \in (0 ..^y + 1)} (k digit (2) a) 2^{k})))})$
184	183	com14	$⊢ (#_{b(\frac{a}{2})=y\to\frac{a}{2} = \sum_{k \in (0 ..^y)} (k digit (2) (\frac{a}{2})) 2^{k}\to(#_{b} (\frac{a}{2}) = #_{b} (a) - 1 \to (y \in ℕ \to ((\frac{a}{2} \in ℕ \land a \in ℕ) \to (#_{b} (a) = y + 1 \to a = \sum_{k \in (0 ..^y + 1)} (k digit (2) a) 2^{k}))))})$
185	12 184	syl	$⊢ (\frac{a}{2} \in ℕ_{0} \land \forall x \in ℕ_{0} (#_{b(x)=y\tox = \sum_{k \in (0 ..^y)} (k digit (2) x) 2^{k}\to(#_{b} (\frac{a}{2}) = #_{b} (a) - 1 \to (y \in ℕ \to ((\frac{a}{2} \in ℕ \land a \in ℕ) \to (#_{b} (a) = y + 1 \to a = \sum_{k \in (0 ..^y + 1)} (k digit (2) a) 2^{k}))))}))$
186	185	ex	$⊢ \frac{a}{2} \in ℕ_{0} \to (\forall x \in ℕ_{0} (#_{b(x)=y\tox = \sum_{k \in (0 ..^y)} (k digit (2) x) 2^{k}\to(#_{b} (\frac{a}{2}) = #_{b} (a) - 1 \to (y \in ℕ \to ((\frac{a}{2} \in ℕ \land a \in ℕ) \to (#_{b} (a) = y + 1 \to a = \sum_{k \in (0 ..^y + 1)} (k digit (2) a) 2^{k}))))}))$
187	186	com25	$⊢ \frac{a}{2} \in ℕ_{0} \to ((\frac{a}{2} \in ℕ \land a \in ℕ) \to (#_{b(\frac{a}{2})=#_{b} (a) - 1\to(y \in ℕ \to (\forall x \in ℕ_{0} \to (#_{b} (a) = y + 1 \to a = \sum_{k \in (0 ..^y + 1)} (k digit (2) a) 2^{k})))}))$
188	187	expdcom	$⊢ \frac{a}{2} \in ℕ \to (a \in ℕ \to (\frac{a}{2} \in ℕ_{0} \to (#_{b(\frac{a}{2})=#_{b} (a) - 1\to(y \in ℕ \to (\forall x \in ℕ_{0} \to (#_{b} (a) = y + 1 \to a = \sum_{k \in (0 ..^y + 1)} (k digit (2) a) 2^{k})))})))$
189	1 188	mpid	$⊢ \frac{a}{2} \in ℕ \to (a \in ℕ \to (#_{b(\frac{a}{2})=#_{b} (a) - 1\to(y \in ℕ \to (\forall x \in ℕ_{0} \to (#_{b} (a) = y + 1 \to a = \sum_{k \in (0 ..^y + 1)} (k digit (2) a) 2^{k})))}))$
190	189	impcom	$⊢ (a \in ℕ \land \frac{a}{2} \in ℕ) \to (#_{b(\frac{a}{2})=#_{b} (a) - 1\to(y \in ℕ \to (\forall x \in ℕ_{0} \to (#_{b} (a) = y + 1 \to a = \sum_{k \in (0 ..^y + 1)} (k digit (2) a) 2^{k})))})$
191	3 190	mpd	$⊢ (a \in ℕ \land \frac{a}{2} \in ℕ) \to (y \in ℕ \to (\forall x \in ℕ_{0} (#_{b(x)=y\tox = \sum_{k \in (0 ..^y)} (k digit (2) x) 2^{k}\to(#_{b} (a) = y + 1 \to a = \sum_{k \in (0 ..^y + 1)} (k digit (2) a) 2^{k})})))$
192	191	imp	$⊢ ((a \in ℕ \land \frac{a}{2} \in ℕ) \land y \in ℕ) \to (\forall x \in ℕ_{0} (#_{b(x)=y\tox = \sum_{k \in (0 ..^y)} (k digit (2) x) 2^{k}\to(#_{b} (a) = y + 1 \to a = \sum_{k \in (0 ..^y + 1)} (k digit (2) a) 2^{k})}))$

Metamath Proof Explorer

Theorem nn0sumshdiglemA

Proof