Theorem nn0sumshdiglemB

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

	Ref	Expression
Assertion	nn0sumshdiglemB	⊢ ( ( ( 𝑎 ∈ ℕ ∧ ( ( 𝑎 − 1 ) / 2 ) ∈ ℕ0 ) ∧ 𝑦 ∈ ℕ ) → ( ∀ 𝑥 ∈ ℕ0 ( ( #b ‘ 𝑥 ) = 𝑦 → 𝑥 = Σ 𝑘 ∈ ( 0 ..^ 𝑦 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑥 ) · ( 2 ↑ 𝑘 ) ) ) → ( ( #b ‘ 𝑎 ) = ( 𝑦 + 1 ) → 𝑎 = Σ 𝑘 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) ) )

Proof

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