Metamath Proof Explorer

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 syl5ibr ⊢ ( 𝑎 ∈ ( ℤ≥ ‘ 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 syl5bi ⊢ ( ( ( #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 ↑ 𝑘 ) ) ) ) )