Metamath Proof Explorer

Theorem nn0sumshdiglem1

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

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

Proof

Step Hyp Ref Expression
1 fveqeq2 ⊢ ( 𝑎 = 𝑥 → ( ( #b ‘ 𝑎 ) = 𝑦 ↔ ( #b ‘ 𝑥 ) = 𝑦 ) )
2 id ⊢ ( 𝑎 = 𝑥 → 𝑎 = 𝑥 )
3 oveq2 ⊢ ( 𝑎 = 𝑥 → ( 𝑘 ( digit ‘ 2 ) 𝑎 ) = ( 𝑘 ( digit ‘ 2 ) 𝑥 ) )
4 3 oveq1d ⊢ ( 𝑎 = 𝑥 → ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) = ( ( 𝑘 ( digit ‘ 2 ) 𝑥 ) · ( 2 ↑ 𝑘 ) ) )
5 4 sumeq2sdv ⊢ ( 𝑎 = 𝑥 → Σ 𝑘 ∈ ( 0 ..^ 𝑦 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ..^ 𝑦 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑥 ) · ( 2 ↑ 𝑘 ) ) )
6 2 5 eqeq12d ⊢ ( 𝑎 = 𝑥 → ( 𝑎 = Σ 𝑘 ∈ ( 0 ..^ 𝑦 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ↔ 𝑥 = Σ 𝑘 ∈ ( 0 ..^ 𝑦 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑥 ) · ( 2 ↑ 𝑘 ) ) ) )
7 1 6 imbi12d ⊢ ( 𝑎 = 𝑥 → ( ( ( #b ‘ 𝑎 ) = 𝑦 → 𝑎 = Σ 𝑘 ∈ ( 0 ..^ 𝑦 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) ↔ ( ( #b ‘ 𝑥 ) = 𝑦 → 𝑥 = Σ 𝑘 ∈ ( 0 ..^ 𝑦 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑥 ) · ( 2 ↑ 𝑘 ) ) ) ) )
8 7 cbvralvw ⊢ ( ∀ 𝑎 ∈ ℕ0 ( ( #b ‘ 𝑎 ) = 𝑦 → 𝑎 = Σ 𝑘 ∈ ( 0 ..^ 𝑦 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) ↔ ∀ 𝑥 ∈ ℕ0 ( ( #b ‘ 𝑥 ) = 𝑦 → 𝑥 = Σ 𝑘 ∈ ( 0 ..^ 𝑦 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑥 ) · ( 2 ↑ 𝑘 ) ) ) )
9 elnn0 ⊢ ( 𝑎 ∈ ℕ0 ↔ ( 𝑎 ∈ ℕ ∨ 𝑎 = 0 ) )
10 nn0sumshdiglemA ⊢ ( ( ( 𝑎 ∈ ℕ ∧ ( 𝑎 / 2 ) ∈ ℕ ) ∧ 𝑦 ∈ ℕ ) → ( ∀ 𝑥 ∈ ℕ0 ( ( #b ‘ 𝑥 ) = 𝑦 → 𝑥 = Σ 𝑘 ∈ ( 0 ..^ 𝑦 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑥 ) · ( 2 ↑ 𝑘 ) ) ) → ( ( #b ‘ 𝑎 ) = ( 𝑦 + 1 ) → 𝑎 = Σ 𝑘 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) ) )
11 10 expimpd ⊢ ( ( 𝑎 ∈ ℕ ∧ ( 𝑎 / 2 ) ∈ ℕ ) → ( ( 𝑦 ∈ ℕ ∧ ∀ 𝑥 ∈ ℕ0 ( ( #b ‘ 𝑥 ) = 𝑦 → 𝑥 = Σ 𝑘 ∈ ( 0 ..^ 𝑦 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑥 ) · ( 2 ↑ 𝑘 ) ) ) ) → ( ( #b ‘ 𝑎 ) = ( 𝑦 + 1 ) → 𝑎 = Σ 𝑘 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) ) )
12 nn0sumshdiglemB ⊢ ( ( ( 𝑎 ∈ ℕ ∧ ( ( 𝑎 − 1 ) / 2 ) ∈ ℕ0 ) ∧ 𝑦 ∈ ℕ ) → ( ∀ 𝑥 ∈ ℕ0 ( ( #b ‘ 𝑥 ) = 𝑦 → 𝑥 = Σ 𝑘 ∈ ( 0 ..^ 𝑦 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑥 ) · ( 2 ↑ 𝑘 ) ) ) → ( ( #b ‘ 𝑎 ) = ( 𝑦 + 1 ) → 𝑎 = Σ 𝑘 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) ) )
13 12 expimpd ⊢ ( ( 𝑎 ∈ ℕ ∧ ( ( 𝑎 − 1 ) / 2 ) ∈ ℕ0 ) → ( ( 𝑦 ∈ ℕ ∧ ∀ 𝑥 ∈ ℕ0 ( ( #b ‘ 𝑥 ) = 𝑦 → 𝑥 = Σ 𝑘 ∈ ( 0 ..^ 𝑦 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑥 ) · ( 2 ↑ 𝑘 ) ) ) ) → ( ( #b ‘ 𝑎 ) = ( 𝑦 + 1 ) → 𝑎 = Σ 𝑘 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) ) )
14 nneom ⊢ ( 𝑎 ∈ ℕ → ( ( 𝑎 / 2 ) ∈ ℕ ∨ ( ( 𝑎 − 1 ) / 2 ) ∈ ℕ0 ) )
15 11 13 14 mpjaodan ⊢ ( 𝑎 ∈ ℕ → ( ( 𝑦 ∈ ℕ ∧ ∀ 𝑥 ∈ ℕ0 ( ( #b ‘ 𝑥 ) = 𝑦 → 𝑥 = Σ 𝑘 ∈ ( 0 ..^ 𝑦 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑥 ) · ( 2 ↑ 𝑘 ) ) ) ) → ( ( #b ‘ 𝑎 ) = ( 𝑦 + 1 ) → 𝑎 = Σ 𝑘 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) ) )
16 eqcom ⊢ ( 1 = ( 𝑦 + 1 ) ↔ ( 𝑦 + 1 ) = 1 )
17 16 a1i ⊢ ( 𝑦 ∈ ℕ → ( 1 = ( 𝑦 + 1 ) ↔ ( 𝑦 + 1 ) = 1 ) )
18 nncn ⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℂ )
19 1cnd ⊢ ( 𝑦 ∈ ℕ → 1 ∈ ℂ )
20 18 19 19 addlsub ⊢ ( 𝑦 ∈ ℕ → ( ( 𝑦 + 1 ) = 1 ↔ 𝑦 = ( 1 − 1 ) ) )
21 1m1e0 ⊢ ( 1 − 1 ) = 0
22 21 a1i ⊢ ( 𝑦 ∈ ℕ → ( 1 − 1 ) = 0 )
23 22 eqeq2d ⊢ ( 𝑦 ∈ ℕ → ( 𝑦 = ( 1 − 1 ) ↔ 𝑦 = 0 ) )
24 17 20 23 3bitrd ⊢ ( 𝑦 ∈ ℕ → ( 1 = ( 𝑦 + 1 ) ↔ 𝑦 = 0 ) )
25 oveq1 ⊢ ( 𝑦 = 0 → ( 𝑦 + 1 ) = ( 0 + 1 ) )
26 25 oveq2d ⊢ ( 𝑦 = 0 → ( 0 ..^ ( 𝑦 + 1 ) ) = ( 0 ..^ ( 0 + 1 ) ) )
27 0p1e1 ⊢ ( 0 + 1 ) = 1
28 27 oveq2i ⊢ ( 0 ..^ ( 0 + 1 ) ) = ( 0 ..^ 1 )
29 fzo01 ⊢ ( 0 ..^ 1 ) = { 0 }
30 28 29 eqtri ⊢ ( 0 ..^ ( 0 + 1 ) ) = { 0 }
31 26 30 eqtrdi ⊢ ( 𝑦 = 0 → ( 0 ..^ ( 𝑦 + 1 ) ) = { 0 } )
32 31 sumeq1d ⊢ ( 𝑦 = 0 → Σ 𝑘 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) ( ( 𝑘 ( digit ‘ 2 ) 0 ) · ( 2 ↑ 𝑘 ) ) = Σ 𝑘 ∈ { 0 } ( ( 𝑘 ( digit ‘ 2 ) 0 ) · ( 2 ↑ 𝑘 ) ) )
33 0cn ⊢ 0 ∈ ℂ
34 oveq1 ⊢ ( 𝑘 = 0 → ( 𝑘 ( digit ‘ 2 ) 0 ) = ( 0 ( digit ‘ 2 ) 0 ) )
35 2nn ⊢ 2 ∈ ℕ
36 0z ⊢ 0 ∈ ℤ
37 dig0 ⊢ ( ( 2 ∈ ℕ ∧ 0 ∈ ℤ ) → ( 0 ( digit ‘ 2 ) 0 ) = 0 )
38 35 36 37 mp2an ⊢ ( 0 ( digit ‘ 2 ) 0 ) = 0
39 34 38 eqtrdi ⊢ ( 𝑘 = 0 → ( 𝑘 ( digit ‘ 2 ) 0 ) = 0 )
40 oveq2 ⊢ ( 𝑘 = 0 → ( 2 ↑ 𝑘 ) = ( 2 ↑ 0 ) )
41 2cn ⊢ 2 ∈ ℂ
42 exp0 ⊢ ( 2 ∈ ℂ → ( 2 ↑ 0 ) = 1 )
43 41 42 ax-mp ⊢ ( 2 ↑ 0 ) = 1
44 40 43 eqtrdi ⊢ ( 𝑘 = 0 → ( 2 ↑ 𝑘 ) = 1 )
45 39 44 oveq12d ⊢ ( 𝑘 = 0 → ( ( 𝑘 ( digit ‘ 2 ) 0 ) · ( 2 ↑ 𝑘 ) ) = ( 0 · 1 ) )
46 1re ⊢ 1 ∈ ℝ
47 mul02lem2 ⊢ ( 1 ∈ ℝ → ( 0 · 1 ) = 0 )
48 46 47 ax-mp ⊢ ( 0 · 1 ) = 0
49 45 48 eqtrdi ⊢ ( 𝑘 = 0 → ( ( 𝑘 ( digit ‘ 2 ) 0 ) · ( 2 ↑ 𝑘 ) ) = 0 )
50 49 sumsn ⊢ ( ( 0 ∈ ℂ ∧ 0 ∈ ℂ ) → Σ 𝑘 ∈ { 0 } ( ( 𝑘 ( digit ‘ 2 ) 0 ) · ( 2 ↑ 𝑘 ) ) = 0 )
51 33 33 50 mp2an ⊢ Σ 𝑘 ∈ { 0 } ( ( 𝑘 ( digit ‘ 2 ) 0 ) · ( 2 ↑ 𝑘 ) ) = 0
52 32 51 eqtr2di ⊢ ( 𝑦 = 0 → 0 = Σ 𝑘 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) ( ( 𝑘 ( digit ‘ 2 ) 0 ) · ( 2 ↑ 𝑘 ) ) )
53 24 52 syl6bi ⊢ ( 𝑦 ∈ ℕ → ( 1 = ( 𝑦 + 1 ) → 0 = Σ 𝑘 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) ( ( 𝑘 ( digit ‘ 2 ) 0 ) · ( 2 ↑ 𝑘 ) ) ) )
54 53 adantl ⊢ ( ( 𝑎 = 0 ∧ 𝑦 ∈ ℕ ) → ( 1 = ( 𝑦 + 1 ) → 0 = Σ 𝑘 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) ( ( 𝑘 ( digit ‘ 2 ) 0 ) · ( 2 ↑ 𝑘 ) ) ) )
55 fveq2 ⊢ ( 𝑎 = 0 → ( #b ‘ 𝑎 ) = ( #b ‘ 0 ) )
56 blen0 ⊢ ( #b ‘ 0 ) = 1
57 55 56 eqtrdi ⊢ ( 𝑎 = 0 → ( #b ‘ 𝑎 ) = 1 )
58 57 eqeq1d ⊢ ( 𝑎 = 0 → ( ( #b ‘ 𝑎 ) = ( 𝑦 + 1 ) ↔ 1 = ( 𝑦 + 1 ) ) )
59 id ⊢ ( 𝑎 = 0 → 𝑎 = 0 )
60 oveq2 ⊢ ( 𝑎 = 0 → ( 𝑘 ( digit ‘ 2 ) 𝑎 ) = ( 𝑘 ( digit ‘ 2 ) 0 ) )
61 60 oveq1d ⊢ ( 𝑎 = 0 → ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) = ( ( 𝑘 ( digit ‘ 2 ) 0 ) · ( 2 ↑ 𝑘 ) ) )
62 61 sumeq2sdv ⊢ ( 𝑎 = 0 → Σ 𝑘 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) ( ( 𝑘 ( digit ‘ 2 ) 0 ) · ( 2 ↑ 𝑘 ) ) )
63 59 62 eqeq12d ⊢ ( 𝑎 = 0 → ( 𝑎 = Σ 𝑘 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ↔ 0 = Σ 𝑘 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) ( ( 𝑘 ( digit ‘ 2 ) 0 ) · ( 2 ↑ 𝑘 ) ) ) )
64 58 63 imbi12d ⊢ ( 𝑎 = 0 → ( ( ( #b ‘ 𝑎 ) = ( 𝑦 + 1 ) → 𝑎 = Σ 𝑘 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) ↔ ( 1 = ( 𝑦 + 1 ) → 0 = Σ 𝑘 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) ( ( 𝑘 ( digit ‘ 2 ) 0 ) · ( 2 ↑ 𝑘 ) ) ) ) )
65 64 adantr ⊢ ( ( 𝑎 = 0 ∧ 𝑦 ∈ ℕ ) → ( ( ( #b ‘ 𝑎 ) = ( 𝑦 + 1 ) → 𝑎 = Σ 𝑘 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) ↔ ( 1 = ( 𝑦 + 1 ) → 0 = Σ 𝑘 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) ( ( 𝑘 ( digit ‘ 2 ) 0 ) · ( 2 ↑ 𝑘 ) ) ) ) )
66 54 65 mpbird ⊢ ( ( 𝑎 = 0 ∧ 𝑦 ∈ ℕ ) → ( ( #b ‘ 𝑎 ) = ( 𝑦 + 1 ) → 𝑎 = Σ 𝑘 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) )
67 66 a1d ⊢ ( ( 𝑎 = 0 ∧ 𝑦 ∈ ℕ ) → ( ∀ 𝑥 ∈ ℕ0 ( ( #b ‘ 𝑥 ) = 𝑦 → 𝑥 = Σ 𝑘 ∈ ( 0 ..^ 𝑦 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑥 ) · ( 2 ↑ 𝑘 ) ) ) → ( ( #b ‘ 𝑎 ) = ( 𝑦 + 1 ) → 𝑎 = Σ 𝑘 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) ) )
68 67 expimpd ⊢ ( 𝑎 = 0 → ( ( 𝑦 ∈ ℕ ∧ ∀ 𝑥 ∈ ℕ0 ( ( #b ‘ 𝑥 ) = 𝑦 → 𝑥 = Σ 𝑘 ∈ ( 0 ..^ 𝑦 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑥 ) · ( 2 ↑ 𝑘 ) ) ) ) → ( ( #b ‘ 𝑎 ) = ( 𝑦 + 1 ) → 𝑎 = Σ 𝑘 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) ) )
69 15 68 jaoi ⊢ ( ( 𝑎 ∈ ℕ ∨ 𝑎 = 0 ) → ( ( 𝑦 ∈ ℕ ∧ ∀ 𝑥 ∈ ℕ0 ( ( #b ‘ 𝑥 ) = 𝑦 → 𝑥 = Σ 𝑘 ∈ ( 0 ..^ 𝑦 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑥 ) · ( 2 ↑ 𝑘 ) ) ) ) → ( ( #b ‘ 𝑎 ) = ( 𝑦 + 1 ) → 𝑎 = Σ 𝑘 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) ) )
70 9 69 sylbi ⊢ ( 𝑎 ∈ ℕ0 → ( ( 𝑦 ∈ ℕ ∧ ∀ 𝑥 ∈ ℕ0 ( ( #b ‘ 𝑥 ) = 𝑦 → 𝑥 = Σ 𝑘 ∈ ( 0 ..^ 𝑦 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑥 ) · ( 2 ↑ 𝑘 ) ) ) ) → ( ( #b ‘ 𝑎 ) = ( 𝑦 + 1 ) → 𝑎 = Σ 𝑘 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) ) )
71 70 com12 ⊢ ( ( 𝑦 ∈ ℕ ∧ ∀ 𝑥 ∈ ℕ0 ( ( #b ‘ 𝑥 ) = 𝑦 → 𝑥 = Σ 𝑘 ∈ ( 0 ..^ 𝑦 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑥 ) · ( 2 ↑ 𝑘 ) ) ) ) → ( 𝑎 ∈ ℕ0 → ( ( #b ‘ 𝑎 ) = ( 𝑦 + 1 ) → 𝑎 = Σ 𝑘 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) ) )
72 71 ralrimiv ⊢ ( ( 𝑦 ∈ ℕ ∧ ∀ 𝑥 ∈ ℕ0 ( ( #b ‘ 𝑥 ) = 𝑦 → 𝑥 = Σ 𝑘 ∈ ( 0 ..^ 𝑦 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑥 ) · ( 2 ↑ 𝑘 ) ) ) ) → ∀ 𝑎 ∈ ℕ0 ( ( #b ‘ 𝑎 ) = ( 𝑦 + 1 ) → 𝑎 = Σ 𝑘 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) )
73 72 ex ⊢ ( 𝑦 ∈ ℕ → ( ∀ 𝑥 ∈ ℕ0 ( ( #b ‘ 𝑥 ) = 𝑦 → 𝑥 = Σ 𝑘 ∈ ( 0 ..^ 𝑦 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑥 ) · ( 2 ↑ 𝑘 ) ) ) → ∀ 𝑎 ∈ ℕ0 ( ( #b ‘ 𝑎 ) = ( 𝑦 + 1 ) → 𝑎 = Σ 𝑘 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) ) )
74 8 73 syl5bi ⊢ ( 𝑦 ∈ ℕ → ( ∀ 𝑎 ∈ ℕ0 ( ( #b ‘ 𝑎 ) = 𝑦 → 𝑎 = Σ 𝑘 ∈ ( 0 ..^ 𝑦 ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) → ∀ 𝑎 ∈ ℕ0 ( ( #b ‘ 𝑎 ) = ( 𝑦 + 1 ) → 𝑎 = Σ 𝑘 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) ( ( 𝑘 ( digit ‘ 2 ) 𝑎 ) · ( 2 ↑ 𝑘 ) ) ) ) )