Metamath Proof Explorer

Theorem nn0sumshdiglemB

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

Ref Expression
Assertion nn0sumshdiglemB 
|- ( ( ( a e. NN /\ ( ( a - 1 ) / 2 ) e. NN0 ) /\ y e. NN ) -> ( A. x e. NN0 ( ( #b ` x ) = y -> x = sum_ k e. ( 0 ..^ y ) ( ( k ( digit ` 2 ) x ) x. ( 2 ^ k ) ) ) -> ( ( #b ` a ) = ( y + 1 ) -> a = sum_ k e. ( 0 ..^ ( y + 1 ) ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) ) )

Proof

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