Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  nn0sumshdiglemB Structured version   Visualization version   Unicode version

Theorem nn0sumshdiglemB 40800
Description: Lemma for nn0sumshdig 40803 (induction step, odd multiplicant). (Contributed by AV, 7-Jun-2020.)
Assertion
Ref Expression
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 ) ) ) ) )
Distinct variable group:    k, a, x, y

Proof of Theorem nn0sumshdiglemB
Dummy variable  i is distinct from all other variables.
StepHypRef Expression
1 elnn1uz2 11269 . . 3  |-  ( a  e.  NN  <->  ( a  =  1  \/  a  e.  ( ZZ>= `  2 )
) )
2 1t1e1 10791 . . . . . . . . 9  |-  ( 1  x.  1 )  =  1
32eqcomi 2471 . . . . . . . 8  |-  1  =  ( 1  x.  1 )
4 simpl 463 . . . . . . . 8  |-  ( ( a  =  1  /\  (#b `  a )  =  ( y  +  1 ) )  -> 
a  =  1 )
5 oveq2 6328 . . . . . . . . . . . 12  |-  ( ( y  +  1 )  =  (#b `  a
)  ->  ( 0..^ ( y  +  1 ) )  =  ( 0..^ (#b `  a
) ) )
65eqcoms 2470 . . . . . . . . . . 11  |-  ( (#b
`  a )  =  ( y  +  1 )  ->  ( 0..^ ( y  +  1 ) )  =  ( 0..^ (#b `  a
) ) )
7 fveq2 5892 . . . . . . . . . . . . . 14  |-  ( a  =  1  ->  (#b `  a )  =  (#b
`  1 ) )
8 blen1 40764 . . . . . . . . . . . . . 14  |-  (#b ` 
1 )  =  1
97, 8syl6eq 2512 . . . . . . . . . . . . 13  |-  ( a  =  1  ->  (#b `  a )  =  1 )
109oveq2d 6336 . . . . . . . . . . . 12  |-  ( a  =  1  ->  (
0..^ (#b `  a
) )  =  ( 0..^ 1 ) )
11 fzo01 12032 . . . . . . . . . . . 12  |-  ( 0..^ 1 )  =  {
0 }
1210, 11syl6eq 2512 . . . . . . . . . . 11  |-  ( a  =  1  ->  (
0..^ (#b `  a
) )  =  {
0 } )
136, 12sylan9eqr 2518 . . . . . . . . . 10  |-  ( ( a  =  1  /\  (#b `  a )  =  ( y  +  1 ) )  -> 
( 0..^ ( y  +  1 ) )  =  { 0 } )
1413sumeq1d 13822 . . . . . . . . 9  |-  ( ( 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 6328 . . . . . . . . . . . . 13  |-  ( a  =  1  ->  (
k (digit `  2
) a )  =  ( k (digit ` 
2 ) 1 ) )
1615oveq1d 6335 . . . . . . . . . . . 12  |-  ( a  =  1  ->  (
( k (digit ` 
2 ) a )  x.  ( 2 ^ k ) )  =  ( ( k (digit `  2 ) 1 )  x.  ( 2 ^ k ) ) )
1716sumeq2sdv 13825 . . . . . . . . . . 11  |-  ( 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 9668 . . . . . . . . . . . 12  |-  0  e.  _V
19 ax-1cn 9628 . . . . . . . . . . . . 13  |-  1  e.  CC
2019, 19mulcli 9679 . . . . . . . . . . . 12  |-  ( 1  x.  1 )  e.  CC
21 oveq1 6327 . . . . . . . . . . . . . . 15  |-  ( k  =  0  ->  (
k (digit `  2
) 1 )  =  ( 0 (digit ` 
2 ) 1 ) )
22 1ex 9669 . . . . . . . . . . . . . . . . 17  |-  1  e.  _V
2322prid2 4094 . . . . . . . . . . . . . . . 16  |-  1  e.  { 0 ,  1 }
24 0dig2pr01 40790 . . . . . . . . . . . . . . . 16  |-  ( 1  e.  { 0 ,  1 }  ->  (
0 (digit `  2
) 1 )  =  1 )
2523, 24ax-mp 5 . . . . . . . . . . . . . . 15  |-  ( 0 (digit `  2 )
1 )  =  1
2621, 25syl6eq 2512 . . . . . . . . . . . . . 14  |-  ( k  =  0  ->  (
k (digit `  2
) 1 )  =  1 )
27 oveq2 6328 . . . . . . . . . . . . . . 15  |-  ( k  =  0  ->  (
2 ^ k )  =  ( 2 ^ 0 ) )
28 2cn 10713 . . . . . . . . . . . . . . . 16  |-  2  e.  CC
29 exp0 12314 . . . . . . . . . . . . . . . 16  |-  ( 2  e.  CC  ->  (
2 ^ 0 )  =  1 )
3028, 29ax-mp 5 . . . . . . . . . . . . . . 15  |-  ( 2 ^ 0 )  =  1
3127, 30syl6eq 2512 . . . . . . . . . . . . . 14  |-  ( k  =  0  ->  (
2 ^ k )  =  1 )
3226, 31oveq12d 6338 . . . . . . . . . . . . 13  |-  ( k  =  0  ->  (
( k (digit ` 
2 ) 1 )  x.  ( 2 ^ k ) )  =  ( 1  x.  1 ) )
3332sumsn 13862 . . . . . . . . . . . 12  |-  ( ( 0  e.  _V  /\  ( 1  x.  1 )  e.  CC )  ->  sum_ k  e.  {
0 }  ( ( k (digit `  2
) 1 )  x.  ( 2 ^ k
) )  =  ( 1  x.  1 ) )
3418, 20, 33mp2an 683 . . . . . . . . . . 11  |-  sum_ k  e.  { 0 }  (
( k (digit ` 
2 ) 1 )  x.  ( 2 ^ k ) )  =  ( 1  x.  1 )
3517, 34syl6eq 2512 . . . . . . . . . 10  |-  ( a  =  1  ->  sum_ k  e.  { 0 }  (
( k (digit ` 
2 ) a )  x.  ( 2 ^ k ) )  =  ( 1  x.  1 ) )
3635adantr 471 . . . . . . . . 9  |-  ( ( a  =  1  /\  (#b `  a )  =  ( y  +  1 ) )  ->  sum_ k  e.  { 0 }  ( ( k (digit `  2 )
a )  x.  (
2 ^ k ) )  =  ( 1  x.  1 ) )
3714, 36eqtrd 2496 . . . . . . . 8  |-  ( ( a  =  1  /\  (#b `  a )  =  ( y  +  1 ) )  ->  sum_ k  e.  ( 0..^ ( y  +  1 ) ) ( ( k (digit `  2
) a )  x.  ( 2 ^ k
) )  =  ( 1  x.  1 ) )
383, 4, 373eqtr4a 2522 . . . . . . 7  |-  ( ( a  =  1  /\  (#b `  a )  =  ( y  +  1 ) )  -> 
a  =  sum_ k  e.  ( 0..^ ( y  +  1 ) ) ( ( k (digit `  2 ) a )  x.  ( 2 ^ k ) ) )
3938ex 440 . . . . . 6  |-  ( a  =  1  ->  (
(#b `  a )  =  ( y  +  1 )  ->  a  =  sum_ k  e.  ( 0..^ ( y  +  1 ) ) ( ( k (digit ` 
2 ) a )  x.  ( 2 ^ k ) ) ) )
4039a1d 26 . . . . 5  |-  ( 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
) ) ) ) )
41402a1d 27 . . . 4  |-  ( 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 11232 . . . . . . . . 9  |-  ( a  e.  ( ZZ>= `  2
)  ->  a  e.  NN0 )
43 nn0ob 40699 . . . . . . . . . 10  |-  ( a  e.  NN0  ->  ( ( ( a  +  1 )  /  2 )  e.  NN0  <->  ( ( a  -  1 )  / 
2 )  e.  NN0 ) )
4443bicomd 206 . . . . . . . . 9  |-  ( a  e.  NN0  ->  ( ( ( a  -  1 )  /  2 )  e.  NN0  <->  ( ( a  +  1 )  / 
2 )  e.  NN0 ) )
4542, 44syl 17 . . . . . . . 8  |-  ( a  e.  ( ZZ>= `  2
)  ->  ( (
( a  -  1 )  /  2 )  e.  NN0  <->  ( ( a  +  1 )  / 
2 )  e.  NN0 ) )
46 blennngt2o2 40772 . . . . . . . . 9  |-  ( ( a  e.  ( ZZ>= ` 
2 )  /\  (
( a  +  1 )  /  2 )  e.  NN0 )  -> 
(#b `  a )  =  ( (#b `  ( ( a  - 
1 )  /  2
) )  +  1 ) )
4746ex 440 . . . . . . . 8  |-  ( a  e.  ( ZZ>= `  2
)  ->  ( (
( a  +  1 )  /  2 )  e.  NN0  ->  (#b `  a )  =  ( (#b `  ( ( a  -  1 )  /  2 ) )  +  1 ) ) )
4845, 47sylbid 223 . . . . . . 7  |-  ( a  e.  ( ZZ>= `  2
)  ->  ( (
( a  -  1 )  /  2 )  e.  NN0  ->  (#b `  a )  =  ( (#b `  ( ( a  -  1 )  /  2 ) )  +  1 ) ) )
4948imp 435 . . . . . 6  |-  ( ( a  e.  ( ZZ>= ` 
2 )  /\  (
( a  -  1 )  /  2 )  e.  NN0 )  -> 
(#b `  a )  =  ( (#b `  ( ( a  - 
1 )  /  2
) )  +  1 ) )
50 fveq2 5892 . . . . . . . . . . . . . 14  |-  ( x  =  ( ( a  -  1 )  / 
2 )  ->  (#b `  x )  =  (#b
`  ( ( a  -  1 )  / 
2 ) ) )
5150eqeq1d 2464 . . . . . . . . . . . . 13  |-  ( x  =  ( ( a  -  1 )  / 
2 )  ->  (
(#b `  x )  =  y  <->  (#b `  ( ( a  -  1 )  /  2 ) )  =  y ) )
52 id 22 . . . . . . . . . . . . . 14  |-  ( x  =  ( ( a  -  1 )  / 
2 )  ->  x  =  ( ( a  -  1 )  / 
2 ) )
53 oveq2 6328 . . . . . . . . . . . . . . . 16  |-  ( x  =  ( ( a  -  1 )  / 
2 )  ->  (
k (digit `  2
) x )  =  ( k (digit ` 
2 ) ( ( a  -  1 )  /  2 ) ) )
5453oveq1d 6335 . . . . . . . . . . . . . . 15  |-  ( x  =  ( ( a  -  1 )  / 
2 )  ->  (
( k (digit ` 
2 ) x )  x.  ( 2 ^ k ) )  =  ( ( k (digit `  2 ) ( ( a  -  1 )  /  2 ) )  x.  ( 2 ^ k ) ) )
5554sumeq2sdv 13825 . . . . . . . . . . . . . 14  |-  ( 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 ) ) )
5652, 55eqeq12d 2477 . . . . . . . . . . . . 13  |-  ( 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 ) ) ) )
5751, 56imbi12d 326 . . . . . . . . . . . 12  |-  ( 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
) ) ) ) )
5857rspcva 3160 . . . . . . . . . . 11  |-  ( ( ( ( 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
) ) ) )
59 eqeq1 2466 . . . . . . . . . . . . . . . 16  |-  ( (#b
`  a )  =  ( y  +  1 )  ->  ( (#b `  a )  =  ( (#b `  ( ( a  -  1 )  /  2 ) )  +  1 )  <->  ( y  +  1 )  =  ( (#b `  (
( a  -  1 )  /  2 ) )  +  1 ) ) )
60 nncn 10650 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  NN  ->  y  e.  CC )
6160ad2antll 740 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( (#b `  a )  =  ( y  +  1 )  /\  (
( ( ( a  -  1 )  / 
2 )  e.  NN0  /\  a  e.  ( ZZ>= ` 
2 ) )  /\  y  e.  NN )
)  ->  y  e.  CC )
62 blennn0elnn 40757 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( a  -  1 )  /  2 )  e.  NN0  ->  (#b `  ( ( a  - 
1 )  /  2
) )  e.  NN )
6362nncnd 10658 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( a  -  1 )  /  2 )  e.  NN0  ->  (#b `  ( ( a  - 
1 )  /  2
) )  e.  CC )
6463adantr 471 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( a  - 
1 )  /  2
)  e.  NN0  /\  a  e.  ( ZZ>= ` 
2 ) )  -> 
(#b `  ( (
a  -  1 )  /  2 ) )  e.  CC )
6564ad2antrl 739 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( (#b `  a )  =  ( y  +  1 )  /\  (
( ( ( a  -  1 )  / 
2 )  e.  NN0  /\  a  e.  ( ZZ>= ` 
2 ) )  /\  y  e.  NN )
)  ->  (#b `  (
( a  -  1 )  /  2 ) )  e.  CC )
66 1cnd 9690 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( (#b `  a )  =  ( y  +  1 )  /\  (
( ( ( a  -  1 )  / 
2 )  e.  NN0  /\  a  e.  ( ZZ>= ` 
2 ) )  /\  y  e.  NN )
)  ->  1  e.  CC )
6761, 65, 66addcan2d 9868 . . . . . . . . . . . . . . . . . . 19  |-  ( ( (#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 ) ) ) )
68 eqcom 2469 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  (#b `  (
( a  -  1 )  /  2 ) )  <->  (#b `  ( ( a  -  1 )  /  2 ) )  =  y )
69 nnz 10993 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( y  e.  NN  ->  y  e.  ZZ )
7069ad2antll 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( (#b `  a )  =  ( y  +  1 )  /\  (
( ( ( a  -  1 )  / 
2 )  e.  NN0  /\  a  e.  ( ZZ>= ` 
2 ) )  /\  y  e.  NN )
)  ->  y  e.  ZZ )
71 fzval3 12020 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  e.  ZZ  ->  (
0 ... y )  =  ( 0..^ ( y  +  1 ) ) )
7270, 71syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( (#b `  a )  =  ( y  +  1 )  /\  (
( ( ( a  -  1 )  / 
2 )  e.  NN0  /\  a  e.  ( ZZ>= ` 
2 ) )  /\  y  e.  NN )
)  ->  ( 0 ... y )  =  ( 0..^ ( y  +  1 ) ) )
7372eqcomd 2468 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( (#b `  a )  =  ( y  +  1 )  /\  (
( ( ( a  -  1 )  / 
2 )  e.  NN0  /\  a  e.  ( ZZ>= ` 
2 ) )  /\  y  e.  NN )
)  ->  ( 0..^ ( y  +  1 ) )  =  ( 0 ... y ) )
7473sumeq1d 13822 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( (#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 ) ) )
75 nnnn0 10910 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  e.  NN  ->  y  e.  NN0 )
76 elnn0uz 11230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  e.  NN0  <->  y  e.  (
ZZ>= `  0 ) )
7775, 76sylib 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( y  e.  NN  ->  y  e.  ( ZZ>= `  0 )
)
7877ad2antll 740 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( (#b `  a )  =  ( y  +  1 )  /\  (
( ( ( a  -  1 )  / 
2 )  e.  NN0  /\  a  e.  ( ZZ>= ` 
2 ) )  /\  y  e.  NN )
)  ->  y  e.  ( ZZ>= `  0 )
)
79 2nn 10801 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  2  e.  NN
8079a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( a  -  1 )  / 
2 )  e.  NN0  /\  a  e.  ( ZZ>= ` 
2 ) )  /\  k  e.  ( 0 ... y ) )  ->  2  e.  NN )
81 elfzelz 11835 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( k  e.  ( 0 ... y )  ->  k  e.  ZZ )
8281adantl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( a  -  1 )  / 
2 )  e.  NN0  /\  a  e.  ( ZZ>= ` 
2 ) )  /\  k  e.  ( 0 ... y ) )  ->  k  e.  ZZ )
83 nn0rp0 11774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( a  e.  NN0  ->  a  e.  ( 0 [,) +oo ) )
8442, 83syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( a  e.  ( ZZ>= `  2
)  ->  a  e.  ( 0 [,) +oo ) )
8584adantl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( a  - 
1 )  /  2
)  e.  NN0  /\  a  e.  ( ZZ>= ` 
2 ) )  -> 
a  e.  ( 0 [,) +oo ) )
8685adantr 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( a  -  1 )  / 
2 )  e.  NN0  /\  a  e.  ( ZZ>= ` 
2 ) )  /\  k  e.  ( 0 ... y ) )  ->  a  e.  ( 0 [,) +oo )
)
87 digvalnn0 40779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( 2  e.  NN  /\  k  e.  ZZ  /\  a  e.  ( 0 [,) +oo ) )  ->  (
k (digit `  2
) a )  e. 
NN0 )
8880, 82, 86, 87syl3anc 1276 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ( a  -  1 )  / 
2 )  e.  NN0  /\  a  e.  ( ZZ>= ` 
2 ) )  /\  k  e.  ( 0 ... y ) )  ->  ( k (digit `  2 ) a )  e.  NN0 )
8988ex 440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( a  - 
1 )  /  2
)  e.  NN0  /\  a  e.  ( ZZ>= ` 
2 ) )  -> 
( k  e.  ( 0 ... y )  ->  ( k (digit `  2 ) a )  e.  NN0 )
)
9089ad2antrl 739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( (#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 ) )
9190imp 435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( (#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 )
9291nn0cnd 10961 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( (#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 )
93 2nn0 10920 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  2  e.  NN0
9493a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( k  e.  ( 0 ... y )  ->  2  e.  NN0 )
95 elfznn0 11922 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( k  e.  ( 0 ... y )  ->  k  e.  NN0 )
9694, 95nn0expcld 12476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( k  e.  ( 0 ... y )  ->  (
2 ^ k )  e.  NN0 )
9796nn0cnd 10961 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( k  e.  ( 0 ... y )  ->  (
2 ^ k )  e.  CC )
9897adantl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( (#b `  a
)  =  ( y  +  1 )  /\  ( ( ( ( a  -  1 )  /  2 )  e. 
NN0  /\  a  e.  ( ZZ>= `  2 )
)  /\  y  e.  NN ) )  /\  k  e.  ( 0 ... y
) )  ->  (
2 ^ k )  e.  CC )
9992, 98mulcld 9694 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( (#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 )
100 oveq1 6327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( k  =  0  ->  (
k (digit `  2
) a )  =  ( 0 (digit ` 
2 ) a ) )
101100, 27oveq12d 6338 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( k  =  0  ->  (
( k (digit ` 
2 ) a )  x.  ( 2 ^ k ) )  =  ( ( 0 (digit `  2 ) a )  x.  ( 2 ^ 0 ) ) )
10230oveq2i 6331 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( 0 (digit `  2
) a )  x.  ( 2 ^ 0 ) )  =  ( ( 0 (digit ` 
2 ) a )  x.  1 )
103101, 102syl6eq 2512 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( k  =  0  ->  (
( k (digit ` 
2 ) a )  x.  ( 2 ^ k ) )  =  ( ( 0 (digit `  2 ) a )  x.  1 ) )
10478, 99, 103fsum1p 13869 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( (#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 ) ) ) )
10542adantl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( a  - 
1 )  /  2
)  e.  NN0  /\  a  e.  ( ZZ>= ` 
2 ) )  -> 
a  e.  NN0 )
10642, 43syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( a  e.  ( ZZ>= `  2
)  ->  ( (
( a  +  1 )  /  2 )  e.  NN0  <->  ( ( a  -  1 )  / 
2 )  e.  NN0 ) )
107106biimparc 494 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( a  - 
1 )  /  2
)  e.  NN0  /\  a  e.  ( ZZ>= ` 
2 ) )  -> 
( ( a  +  1 )  /  2
)  e.  NN0 )
108 0dig2nn0o 40793 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( a  e.  NN0  /\  ( ( a  +  1 )  /  2
)  e.  NN0 )  ->  ( 0 (digit ` 
2 ) a )  =  1 )
109105, 107, 108syl2anc 671 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( a  - 
1 )  /  2
)  e.  NN0  /\  a  e.  ( ZZ>= ` 
2 ) )  -> 
( 0 (digit ` 
2 ) a )  =  1 )
110109ad2antrl 739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( (#b `  a )  =  ( y  +  1 )  /\  (
( ( ( a  -  1 )  / 
2 )  e.  NN0  /\  a  e.  ( ZZ>= ` 
2 ) )  /\  y  e.  NN )
)  ->  ( 0 (digit `  2 )
a )  =  1 )
111110oveq1d 6335 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( (#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 ) )
112111, 2syl6eq 2512 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( (#b `  a )  =  ( y  +  1 )  /\  (
( ( ( a  -  1 )  / 
2 )  e.  NN0  /\  a  e.  ( ZZ>= ` 
2 ) )  /\  y  e.  NN )
)  ->  ( (
0 (digit `  2
) a )  x.  1 )  =  1 )
113 1z 11001 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  1  e.  ZZ
114113a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( (#b `  a )  =  ( y  +  1 )  /\  (
( ( ( a  -  1 )  / 
2 )  e.  NN0  /\  a  e.  ( ZZ>= ` 
2 ) )  /\  y  e.  NN )
)  ->  1  e.  ZZ )
115 0p1e1 10754 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( 0  +  1 )  =  1
116115, 113eqeltri 2536 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( 0  +  1 )  e.  ZZ
117116a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( (#b `  a )  =  ( y  +  1 )  /\  (
( ( ( a  -  1 )  / 
2 )  e.  NN0  /\  a  e.  ( ZZ>= ` 
2 ) )  /\  y  e.  NN )
)  ->  ( 0  +  1 )  e.  ZZ )
11879a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( a  e.  ( ZZ>= ` 
2 )  /\  k  e.  ( ( 0  +  1 ) ... y
) )  ->  2  e.  NN )
119 elfzelz 11835 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( k  e.  ( ( 0  +  1 ) ... y )  ->  k  e.  ZZ )
120119adantl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( a  e.  ( ZZ>= ` 
2 )  /\  k  e.  ( ( 0  +  1 ) ... y
) )  ->  k  e.  ZZ )
12142adantr 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( a  e.  ( ZZ>= ` 
2 )  /\  k  e.  ( ( 0  +  1 ) ... y
) )  ->  a  e.  NN0 )
122121, 83syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( a  e.  ( ZZ>= ` 
2 )  /\  k  e.  ( ( 0  +  1 ) ... y
) )  ->  a  e.  ( 0 [,) +oo ) )
123118, 120, 122, 87syl3anc 1276 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( a  e.  ( ZZ>= ` 
2 )  /\  k  e.  ( ( 0  +  1 ) ... y
) )  ->  (
k (digit `  2
) a )  e. 
NN0 )
124123ex 440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( a  e.  ( ZZ>= `  2
)  ->  ( k  e.  ( ( 0  +  1 ) ... y
)  ->  ( k
(digit `  2 )
a )  e.  NN0 ) )
125124adantl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( a  - 
1 )  /  2
)  e.  NN0  /\  a  e.  ( ZZ>= ` 
2 ) )  -> 
( k  e.  ( ( 0  +  1 ) ... y )  ->  ( k (digit `  2 ) a )  e.  NN0 )
)
126125ad2antrl 739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( (#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 ) )
127126imp 435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( (#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 )
128127nn0cnd 10961 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( (#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 )
129 2cnd 10715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( k  e.  ( ( 0  +  1 ) ... y )  ->  2  e.  CC )
130 elfznn 11863 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( k  e.  ( 1 ... y )  ->  k  e.  NN )
131130nnnn0d 10959 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( k  e.  ( 1 ... y )  ->  k  e.  NN0 )
132115oveq1i 6330 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( 0  +  1 ) ... y )  =  ( 1 ... y
)
133131, 132eleq2s 2558 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( k  e.  ( ( 0  +  1 ) ... y )  ->  k  e.  NN0 )
134129, 133expcld 12454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( k  e.  ( ( 0  +  1 ) ... y )  ->  (
2 ^ k )  e.  CC )
135134adantl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( (#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 )
136128, 135mulcld 9694 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( (#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 )
137 oveq1 6327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( k  =  ( i  +  1 )  ->  (
k (digit `  2
) a )  =  ( ( i  +  1 ) (digit ` 
2 ) a ) )
138 oveq2 6328 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( k  =  ( i  +  1 )  ->  (
2 ^ k )  =  ( 2 ^ ( i  +  1 ) ) )
139137, 138oveq12d 6338 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( k  =  ( i  +  1 )  ->  (
( k (digit ` 
2 ) a )  x.  ( 2 ^ k ) )  =  ( ( ( i  +  1 ) (digit `  2 ) a )  x.  ( 2 ^ ( i  +  1 ) ) ) )
140114, 117, 70, 136, 139fsumshftm 13897 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( (#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 ) ) ) )
141112, 140oveq12d 6338 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( (#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 ) ) ) ) )
14274, 104, 1413eqtrd 2500 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( (#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 ) ) ) ) )
143142adantl 472 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( 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 ) ) ) ) )
14479a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( a  -  1 )  / 
2 )  e.  NN0  /\  a  e.  ( ZZ>= ` 
2 ) )  /\  i  e.  ( 0..^ y ) )  -> 
2  e.  NN )
145 elfzoelz 11957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( i  e.  ( 0..^ y )  ->  i  e.  ZZ )
146145adantl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( a  -  1 )  / 
2 )  e.  NN0  /\  a  e.  ( ZZ>= ` 
2 ) )  /\  i  e.  ( 0..^ y ) )  -> 
i  e.  ZZ )
147 nn0rp0 11774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( a  -  1 )  /  2 )  e.  NN0  ->  ( ( a  -  1 )  /  2 )  e.  ( 0 [,) +oo ) )
148147adantr 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( a  - 
1 )  /  2
)  e.  NN0  /\  a  e.  ( ZZ>= ` 
2 ) )  -> 
( ( a  - 
1 )  /  2
)  e.  ( 0 [,) +oo ) )
149148adantr 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( a  -  1 )  / 
2 )  e.  NN0  /\  a  e.  ( ZZ>= ` 
2 ) )  /\  i  e.  ( 0..^ y ) )  -> 
( ( a  - 
1 )  /  2
)  e.  ( 0 [,) +oo ) )
150 digvalnn0 40779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( 2  e.  NN  /\  i  e.  ZZ  /\  (
( a  -  1 )  /  2 )  e.  ( 0 [,) +oo ) )  ->  (
i (digit `  2
) ( ( a  -  1 )  / 
2 ) )  e. 
NN0 )
151144, 146, 149, 150syl3anc 1276 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( a  -  1 )  / 
2 )  e.  NN0  /\  a  e.  ( ZZ>= ` 
2 ) )  /\  i  e.  ( 0..^ y ) )  -> 
( i (digit ` 
2 ) ( ( a  -  1 )  /  2 ) )  e.  NN0 )
152151nn0cnd 10961 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( a  -  1 )  / 
2 )  e.  NN0  /\  a  e.  ( ZZ>= ` 
2 ) )  /\  i  e.  ( 0..^ y ) )  -> 
( i (digit ` 
2 ) ( ( a  -  1 )  /  2 ) )  e.  CC )
153152ex 440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( a  - 
1 )  /  2
)  e.  NN0  /\  a  e.  ( ZZ>= ` 
2 ) )  -> 
( i  e.  ( 0..^ y )  -> 
( i (digit ` 
2 ) ( ( a  -  1 )  /  2 ) )  e.  CC ) )
154153ad2antrl 739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( (#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 ) )
155154imp 435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( (#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 )
15693a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( i  e.  ( 0..^ y )  ->  2  e.  NN0 )
157 elfzonn0 11997 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( i  e.  ( 0..^ y )  ->  i  e.  NN0 )
158156, 157nn0expcld 12476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( i  e.  ( 0..^ y )  ->  ( 2 ^ i )  e. 
NN0 )
159158nn0cnd 10961 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( i  e.  ( 0..^ y )  ->  ( 2 ^ i )  e.  CC )
160159adantl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( (#b `  a
)  =  ( y  +  1 )  /\  ( ( ( ( a  -  1 )  /  2 )  e. 
NN0  /\  a  e.  ( ZZ>= `  2 )
)  /\  y  e.  NN ) )  /\  i  e.  ( 0..^ y ) )  ->  ( 2 ^ i )  e.  CC )
161 2cnd 10715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( (#b `  a
)  =  ( y  +  1 )  /\  ( ( ( ( a  -  1 )  /  2 )  e. 
NN0  /\  a  e.  ( ZZ>= `  2 )
)  /\  y  e.  NN ) )  /\  i  e.  ( 0..^ y ) )  ->  2  e.  CC )
162155, 160, 161mulassd 9697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( (#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 ) ) )
163162eqcomd 2468 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( (#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 ) )
164163sumeq2dv 13824 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( (#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 ) )
165164adantl 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( 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 ) )
166 0cn 9666 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  0  e.  CC
167 pncan1 10076 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( 0  e.  CC  ->  (
( 0  +  1 )  -  1 )  =  0 )
168166, 167ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( 0  +  1 )  -  1 )  =  0
169168a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  e.  NN  ->  (
( 0  +  1 )  -  1 )  =  0 )
170169oveq1d 6335 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( y  e.  NN  ->  (
( ( 0  +  1 )  -  1 ) ... ( y  -  1 ) )  =  ( 0 ... ( y  -  1 ) ) )
171 fzoval 11958 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  e.  ZZ  ->  (
0..^ y )  =  ( 0 ... (
y  -  1 ) ) )
17269, 171syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( y  e.  NN  ->  (
0..^ y )  =  ( 0 ... (
y  -  1 ) ) )
173170, 172eqtr4d 2499 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  e.  NN  ->  (
( ( 0  +  1 )  -  1 ) ... ( y  -  1 ) )  =  ( 0..^ y ) )
174173ad2antll 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( (#b `  a )  =  ( y  +  1 )  /\  (
( ( ( a  -  1 )  / 
2 )  e.  NN0  /\  a  e.  ( ZZ>= ` 
2 ) )  /\  y  e.  NN )
)  ->  ( (
( 0  +  1 )  -  1 ) ... ( y  - 
1 ) )  =  ( 0..^ y ) )
175 simprlr 778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( (#b `  a )  =  ( y  +  1 )  /\  (
( ( ( a  -  1 )  / 
2 )  e.  NN0  /\  a  e.  ( ZZ>= ` 
2 ) )  /\  y  e.  NN )
)  ->  a  e.  ( ZZ>= `  2 )
)
176 elfznn0 11922 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( i  e.  ( 0 ... ( y  -  1 ) )  ->  i  e.  NN0 )
177168oveq1i 6330 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( 0  +  1 )  -  1 ) ... ( y  - 
1 ) )  =  ( 0 ... (
y  -  1 ) )
178176, 177eleq2s 2558 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( i  e.  ( ( ( 0  +  1 )  -  1 ) ... ( y  -  1 ) )  ->  i  e.  NN0 )
179 dignn0flhalf 40798 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( a  e.  ( ZZ>= ` 
2 )  /\  i  e.  NN0 )  ->  (
( i  +  1 ) (digit `  2
) a )  =  ( i (digit ` 
2 ) ( |_
`  ( a  / 
2 ) ) ) )
180175, 178, 179syl2an 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( (#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 ) ) ) )
181 eluzelz 11202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( a  e.  ( ZZ>= `  2
)  ->  a  e.  ZZ )
182181adantr 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( a  e.  ( ZZ>= ` 
2 )  /\  (
( a  -  1 )  /  2 )  e.  NN0 )  -> 
a  e.  ZZ )
183 nn0z 10994 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( a  -  1 )  /  2 )  e.  NN0  ->  ( ( a  -  1 )  /  2 )  e.  ZZ )
184 zob 38898 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( a  e.  ZZ  ->  (
( ( a  +  1 )  /  2
)  e.  ZZ  <->  ( (
a  -  1 )  /  2 )  e.  ZZ ) )
185181, 184syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( a  e.  ( ZZ>= `  2
)  ->  ( (
( a  +  1 )  /  2 )  e.  ZZ  <->  ( (
a  -  1 )  /  2 )  e.  ZZ ) )
186183, 185syl5ibr 229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( a  e.  ( ZZ>= `  2
)  ->  ( (
( a  -  1 )  /  2 )  e.  NN0  ->  ( ( a  +  1 )  /  2 )  e.  ZZ ) )
187186imp 435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( a  e.  ( ZZ>= ` 
2 )  /\  (
( a  -  1 )  /  2 )  e.  NN0 )  -> 
( ( a  +  1 )  /  2
)  e.  ZZ )
188182, 187jca 539 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( a  e.  ( ZZ>= ` 
2 )  /\  (
( a  -  1 )  /  2 )  e.  NN0 )  -> 
( a  e.  ZZ  /\  ( ( a  +  1 )  /  2
)  e.  ZZ ) )
189188ancoms 459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( a  - 
1 )  /  2
)  e.  NN0  /\  a  e.  ( ZZ>= ` 
2 ) )  -> 
( a  e.  ZZ  /\  ( ( a  +  1 )  /  2
)  e.  ZZ ) )
190189ad2antrl 739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( (#b `  a )  =  ( y  +  1 )  /\  (
( ( ( a  -  1 )  / 
2 )  e.  NN0  /\  a  e.  ( ZZ>= ` 
2 ) )  /\  y  e.  NN )
)  ->  ( a  e.  ZZ  /\  ( ( a  +  1 )  /  2 )  e.  ZZ ) )
191190adantr 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( (#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 ) )
192 zofldiv2 40707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( a  e.  ZZ  /\  ( ( a  +  1 )  /  2
)  e.  ZZ )  ->  ( |_ `  ( a  /  2
) )  =  ( ( a  -  1 )  /  2 ) )
193191, 192syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( (#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
) )
194193oveq2d 6336 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( (#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 ) ) )
195180, 194eqtrd 2496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( (#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 ) ) )
196 2cnd 10715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( i  e.  ( ( ( 0  +  1 )  -  1 ) ... ( y  -  1 ) )  ->  2  e.  CC )
197196, 178expp1d 12455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( i  e.  ( ( ( 0  +  1 )  -  1 ) ... ( y  -  1 ) )  ->  (
2 ^ ( i  +  1 ) )  =  ( ( 2 ^ i )  x.  2 ) )
198197adantl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( (#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 ) )
199195, 198oveq12d 6338 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( (#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 ) ) )
200174, 199sumeq12dv 13827 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( (#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 ) ) )
201200adantl 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( 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 ) ) )
202 oveq1 6327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( k  =  i  ->  (
k (digit `  2
) ( ( a  -  1 )  / 
2 ) )  =  ( i (digit ` 
2 ) ( ( a  -  1 )  /  2 ) ) )
203 oveq2 6328 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( k  =  i  ->  (
2 ^ k )  =  ( 2 ^ i ) )
204202, 203oveq12d 6338 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( k  =  i  ->  (
( k (digit ` 
2 ) ( ( a  -  1 )  /  2 ) )  x.  ( 2 ^ k ) )  =  ( ( i (digit `  2 ) ( ( a  -  1 )  /  2 ) )  x.  ( 2 ^ i ) ) )
205204cbvsumv 13817 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  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 ) )
206205eqeq2i 2474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( 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 ) ) )
207206biimpi 199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( 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 ) ) )
208207adantr 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( 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 ) ) )
209208oveq1d 6335 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( 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 ) )
210 fzofi 12225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( 0..^ y )  e.  Fin
211210a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( 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 )
212 2cnd 10715 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( 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 )
213159adantl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( a  -  1 )  / 
2 )  e.  NN0  /\  a  e.  ( ZZ>= ` 
2 ) )  /\  i  e.  ( 0..^ y ) )  -> 
( 2 ^ i
)  e.  CC )
214152, 213mulcld 9694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ( a  -  1 )  / 
2 )  e.  NN0  /\  a  e.  ( ZZ>= ` 
2 ) )  /\  i  e.  ( 0..^ y ) )  -> 
( ( i (digit `  2 ) ( ( a  -  1 )  /  2 ) )  x.  ( 2 ^ i ) )  e.  CC )
215214ex 440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( a  - 
1 )  /  2
)  e.  NN0  /\  a  e.  ( ZZ>= ` 
2 ) )  -> 
( i  e.  ( 0..^ y )  -> 
( ( i (digit `  2 ) ( ( a  -  1 )  /  2 ) )  x.  ( 2 ^ i ) )  e.  CC ) )
216215adantr 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( 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 ) )
217216ad2antll 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( 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 ) )
218217imp 435 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( 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 )
219211, 212, 218fsummulc1 13901 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( 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 ) )
220209, 219eqtrd 2496 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( 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 ) )
221165, 201, 2203eqtr4d 2506 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( 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 ) )
222221oveq2d 6336 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( 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 ) ) )
223 eluzelcn 11204 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( a  e.  ( ZZ>= `  2
)  ->  a  e.  CC )
224 peano2cnm 9971 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( a  e.  CC  ->  (
a  -  1 )  e.  CC )
225223, 224syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( a  e.  ( ZZ>= `  2
)  ->  ( a  -  1 )  e.  CC )
226 2cnd 10715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( a  e.  ( ZZ>= `  2
)  ->  2  e.  CC )
227 2ne0 10735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  2  =/=  0
228227a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( a  e.  ( ZZ>= `  2
)  ->  2  =/=  0 )
229225, 226, 2283jca 1194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( a  e.  ( ZZ>= `  2
)  ->  ( (
a  -  1 )  e.  CC  /\  2  e.  CC  /\  2  =/=  0 ) )
230229adantl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( a  - 
1 )  /  2
)  e.  NN0  /\  a  e.  ( ZZ>= ` 
2 ) )  -> 
( ( a  - 
1 )  e.  CC  /\  2  e.  CC  /\  2  =/=  0 ) )
231 divcan1 10312 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( a  -  1 )  e.  CC  /\  2  e.  CC  /\  2  =/=  0 )  ->  (
( ( a  - 
1 )  /  2
)  x.  2 )  =  ( a  - 
1 ) )
232230, 231syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( a  - 
1 )  /  2
)  e.  NN0  /\  a  e.  ( ZZ>= ` 
2 ) )  -> 
( ( ( a  -  1 )  / 
2 )  x.  2 )  =  ( a  -  1 ) )
233232oveq2d 6336 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( a  - 
1 )  /  2
)  e.  NN0  /\  a  e.  ( ZZ>= ` 
2 ) )  -> 
( 1  +  ( ( ( a  - 
1 )  /  2
)  x.  2 ) )  =  ( 1  +  ( a  - 
1 ) ) )
234 1cnd 9690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( a  e.  ( ZZ>= `  2
)  ->  1  e.  CC )
235234, 223jca 539 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( a  e.  ( ZZ>= `  2
)  ->  ( 1  e.  CC  /\  a  e.  CC ) )
236235adantl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( a  - 
1 )  /  2
)  e.  NN0  /\  a  e.  ( ZZ>= ` 
2 ) )  -> 
( 1  e.  CC  /\  a  e.  CC ) )
237 pncan3 9914 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( 1  e.  CC  /\  a  e.  CC )  ->  ( 1  +  ( a  -  1 ) )  =  a )
238236, 237syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( a  - 
1 )  /  2
)  e.  NN0  /\  a  e.  ( ZZ>= ` 
2 ) )  -> 
( 1  +  ( a  -  1 ) )  =  a )
239233, 238eqtrd 2496 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( a  - 
1 )  /  2
)  e.  NN0  /\  a  e.  ( ZZ>= ` 
2 ) )  -> 
( 1  +  ( ( ( a  - 
1 )  /  2
)  x.  2 ) )  =  a )
240239adantr 471 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( a  -  1 )  / 
2 )  e.  NN0  /\  a  e.  ( ZZ>= ` 
2 ) )  /\  y  e.  NN )  ->  ( 1  +  ( ( ( a  - 
1 )  /  2
)  x.  2 ) )  =  a )
241240ad2antll 740 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( 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 )
242143, 222, 2413eqtrrd 2501 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( 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 ) ) )
243242ex 440 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( 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 ) ) ) )
244243imim2i 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( (#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
) ) ) ) )
245244com13 83 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( (#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
) ) ) ) )
24668, 245syl5bi 225 . . . . . . . . . . . . . . . . . . 19  |-  ( ( (#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
) ) ) ) )
24767, 246sylbid 223 . . . . . . . . . . . . . . . . . 18  |-  ( ( (#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
) ) ) ) )
248247ex 440 . . . . . . . . . . . . . . . . 17  |-  ( (#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 ) ) ) ) ) )
249248com23 81 . . . . . . . . . . . . . . . 16  |-  ( (#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 ) ) ) ) ) )
25059, 249sylbid 223 . . . . . . . . . . . . . . 15  |-  ( (#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
) ) ) ) ) )
251250com23 81 . . . . . . . . . . . . . 14  |-  ( (#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
) ) ) ) ) )
252251com14 91 . . . . . . . . . . . . 13  |-  ( ( (#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 ) ) ) ) ) )
253252exp4c 617 . . . . . . . . . . . 12  |-  ( ( (#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 ) ) ) ) ) ) ) )
254253com35 93 . . . . . . . . . . 11  |-  ( ( (#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 ) ) ) ) ) ) ) )
25558, 254syl 17 . . . . . . . . . 10  |-  ( ( ( ( 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 ) ) ) ) ) ) ) )
256255ex 440 . . . . . . . . 9  |-  ( ( ( 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 ) ) ) ) ) ) ) ) )
257256pm2.43a 51 . . . . . . . 8  |-  ( ( ( 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 ) ) ) ) ) ) ) )
258257com25 94 . . . . . . 7  |-  ( ( ( 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 ) ) ) ) ) ) ) )
259258impcom 436 . . . . . 6  |-  ( ( 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
) ) ) ) ) ) )
26049, 259mpd 15 . . . . 5  |-  ( ( 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 ) ) ) ) ) )
261260ex 440 . . . 4  |-  ( 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
) ) ) ) ) ) )
26241, 261jaoi 385 . . 3  |-  ( ( 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 ) ) ) ) ) ) )
2631, 262sylbi 200 . 2  |-  ( 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
) ) ) ) ) ) )
264263imp31 438 1  |-  ( ( ( 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 ) ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    \/ wo 374    /\ wa 375    /\ w3a 991    = wceq 1455    e. wcel 1898    =/= wne 2633   A.wral 2749   _Vcvv 3057   {csn 3980   {cpr 3982   ` cfv 5605  (class class class)co 6320   Fincfn 7600   CCcc 9568   0cc0 9570   1c1 9571    + caddc 9573    x. cmul 9575   +oocpnf 9703    - cmin 9891    / cdiv 10302   NNcn 10642   2c2 10692   NN0cn0 10903   ZZcz 10971   ZZ>=cuz 11193   [,)cico 11671   ...cfz 11819  ..^cfzo 11952   |_cfl 12064   ^cexp 12310   sum_csu 13807  #bcblen 40749  digitcdig 40775
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4531  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615  ax-inf2 8177  ax-cnex 9626  ax-resscn 9627  ax-1cn 9628  ax-icn 9629  ax-addcl 9630  ax-addrcl 9631  ax-mulcl 9632  ax-mulrcl 9633  ax-mulcom 9634  ax-addass 9635  ax-mulass 9636  ax-distr 9637  ax-i2m1 9638  ax-1ne0 9639  ax-1rid 9640  ax-rnegex 9641  ax-rrecex 9642  ax-cnre 9643  ax-pre-lttri 9644  ax-pre-lttrn 9645  ax-pre-ltadd 9646  ax-pre-mulgt0 9647  ax-pre-sup 9648  ax-addf 9649  ax-mulf 9650
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-fal 1461  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rmo 2757  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-int 4249  df-iun 4294  df-iin 4295  df-br 4419  df-opab 4478  df-mpt 4479  df-tr 4514  df-eprel 4767  df-id 4771  df-po 4777  df-so 4778  df-fr 4815  df-se 4816  df-we 4817  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-pred 5403  df-ord 5449  df-on 5450  df-lim 5451  df-suc 5452  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-fv 5613  df-isom 5614  df-riota 6282  df-ov 6323  df-oprab 6324  df-mpt2 6325  df-of 6563  df-om 6725  df-1st 6825  df-2nd 6826  df-supp 6947  df-wrecs 7059  df-recs 7121  df-rdg 7159  df-1o 7213  df-2o 7214  df-oadd 7217  df-er 7394  df-map 7505  df-pm 7506  df-ixp 7554  df-en 7601  df-dom 7602  df-sdom 7603  df-fin 7604  df-fsupp 7915  df-fi 7956  df-sup 7987  df-inf 7988  df-oi 8056  df-card 8404  df-cda 8629  df-pnf 9708  df-mnf 9709  df-xr 9710  df-ltxr 9711  df-le 9712  df-sub 9893  df-neg 9894  df-div 10303  df-nn 10643  df-2 10701  df-3 10702  df-4 10703  df-5 10704  df-6 10705  df-7 10706  df-8 10707  df-9 10708  df-10 10709  df-n0 10904  df-z 10972  df-dec 11086  df-uz 11194  df-q 11299  df-rp 11337  df-xneg 11443  df-xadd 11444  df-xmul 11445  df-ioo 11673  df-ioc 11674  df-ico 11675  df-icc 11676  df-fz 11820  df-fzo 11953  df-fl 12066  df-mod 12135  df-seq 12252  df-exp 12311  df-fac 12498  df-bc 12526  df-hash 12554  df-shft 13185  df-cj 13217  df-re 13218  df-im 13219  df-sqrt 13353  df-abs 13354  df-limsup 13581  df-clim 13607  df-rlim 13608  df-sum 13808  df-ef 14176  df-sin 14178  df-cos 14179  df-pi 14181  df-dvds 14361  df-struct 15178  df-ndx 15179  df-slot 15180  df-base 15181  df-sets 15182  df-ress 15183  df-plusg 15258  df-mulr 15259  df-starv 15260  df-sca 15261  df-vsca 15262  df-ip 15263  df-tset 15264  df-ple 15265  df-ds 15267  df-unif 15268  df-hom 15269  df-cco 15270  df-rest 15376  df-topn 15377  df-0g 15395  df-gsum 15396  df-topgen 15397  df-pt 15398  df-prds 15401  df-xrs 15455  df-qtop 15461  df-imas 15462  df-xps 15465  df-mre 15547  df-mrc 15548  df-acs 15550  df-mgm 16543  df-sgrp 16582  df-mnd 16592  df-submnd 16638  df-mulg 16731  df-cntz 17026  df-cmn 17487  df-psmet 19017  df-xmet 19018  df-met 19019  df-bl 19020  df-mopn 19021  df-fbas 19022  df-fg 19023  df-cnfld 19026  df-top 19976  df-bases 19977  df-topon 19978  df-topsp 19979  df-cld 20089  df-ntr 20090  df-cls 20091  df-nei 20169  df-lp 20207  df-perf 20208  df-cn 20298  df-cnp 20299  df-haus 20386  df-tx 20632  df-hmeo 20825  df-fil 20916  df-fm 21008  df-flim 21009  df-flf 21010  df-xms 21390  df-ms 21391  df-tms 21392  df-cncf 21965  df-limc 22877  df-dv 22878  df-log 23562  df-cxp 23563  df-logb 23758  df-blen 40750  df-dig 40776
This theorem is referenced by:  nn0sumshdiglem1  40801
  Copyright terms: Public domain W3C validator