Metamath Proof Explorer

Theorem nn0sumshdig

Description: A nonnegative integer can be represented as sum of its shifted bits. (Contributed by AV, 7-Jun-2020)

Ref Expression
Assertion nn0sumshdig 
|- ( A e. NN0 -> A = sum_ k e. ( 0 ..^ ( #b ` A ) ) ( ( k ( digit ` 2 ) A ) x. ( 2 ^ k ) ) )

Proof

Step Hyp Ref Expression
1 blennn0elnn 
 |-  ( A e. NN0 -> ( #b ` A ) e. NN )
2 nn0sumshdiglem2 
 |-  ( ( #b ` A ) e. NN -> A. a e. NN0 ( ( #b ` a ) = ( #b ` A ) -> a = sum_ k e. ( 0 ..^ ( #b ` A ) ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) )
3 eqid 
 |-  ( #b ` A ) = ( #b ` A )
4 fveqeq2 
 |-  ( a = A -> ( ( #b ` a ) = ( #b ` A ) <-> ( #b ` A ) = ( #b ` A ) ) )
5 id 
 |-  ( a = A -> a = A )
6 oveq2 
 |-  ( a = A -> ( k ( digit ` 2 ) a ) = ( k ( digit ` 2 ) A ) )
7 6 oveq1d 
 |-  ( a = A -> ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) = ( ( k ( digit ` 2 ) A ) x. ( 2 ^ k ) ) )
8 7 adantr 
 |-  ( ( a = A /\ k e. ( 0 ..^ ( #b ` A ) ) ) -> ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) = ( ( k ( digit ` 2 ) A ) x. ( 2 ^ k ) ) )
9 8 sumeq2dv 
 |-  ( a = A -> sum_ k e. ( 0 ..^ ( #b ` A ) ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) = sum_ k e. ( 0 ..^ ( #b ` A ) ) ( ( k ( digit ` 2 ) A ) x. ( 2 ^ k ) ) )
10 5 9 eqeq12d 
 |-  ( a = A -> ( a = sum_ k e. ( 0 ..^ ( #b ` A ) ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) <-> A = sum_ k e. ( 0 ..^ ( #b ` A ) ) ( ( k ( digit ` 2 ) A ) x. ( 2 ^ k ) ) ) )
11 4 10 imbi12d 
 |-  ( a = A -> ( ( ( #b ` a ) = ( #b ` A ) -> a = sum_ k e. ( 0 ..^ ( #b ` A ) ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) <-> ( ( #b ` A ) = ( #b ` A ) -> A = sum_ k e. ( 0 ..^ ( #b ` A ) ) ( ( k ( digit ` 2 ) A ) x. ( 2 ^ k ) ) ) ) )
12 11 rspcva 
 |-  ( ( A e. NN0 /\ A. a e. NN0 ( ( #b ` a ) = ( #b ` A ) -> a = sum_ k e. ( 0 ..^ ( #b ` A ) ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) ) -> ( ( #b ` A ) = ( #b ` A ) -> A = sum_ k e. ( 0 ..^ ( #b ` A ) ) ( ( k ( digit ` 2 ) A ) x. ( 2 ^ k ) ) ) )
13 3 12 mpi 
 |-  ( ( A e. NN0 /\ A. a e. NN0 ( ( #b ` a ) = ( #b ` A ) -> a = sum_ k e. ( 0 ..^ ( #b ` A ) ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) ) -> A = sum_ k e. ( 0 ..^ ( #b ` A ) ) ( ( k ( digit ` 2 ) A ) x. ( 2 ^ k ) ) )
14 13 ex 
 |-  ( A e. NN0 -> ( A. a e. NN0 ( ( #b ` a ) = ( #b ` A ) -> a = sum_ k e. ( 0 ..^ ( #b ` A ) ) ( ( k ( digit ` 2 ) a ) x. ( 2 ^ k ) ) ) -> A = sum_ k e. ( 0 ..^ ( #b ` A ) ) ( ( k ( digit ` 2 ) A ) x. ( 2 ^ k ) ) ) )
15 2 14 syl5 
 |-  ( A e. NN0 -> ( ( #b ` A ) e. NN -> A = sum_ k e. ( 0 ..^ ( #b ` A ) ) ( ( k ( digit ` 2 ) A ) x. ( 2 ^ k ) ) ) )
16 1 15 mpd 
 |-  ( A e. NN0 -> A = sum_ k e. ( 0 ..^ ( #b ` A ) ) ( ( k ( digit ` 2 ) A ) x. ( 2 ^ k ) ) )