Metamath Proof Explorer


Theorem nn0sumshdiglemA

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

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

Proof

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