Metamath Proof Explorer

Theorem bitsinv1

Description: There is an explicit inverse to the bits function for nonnegative integers (which can be extended to negative integers using bitscmp ), part 1. (Contributed by Mario Carneiro, 7-Sep-2016)

Ref Expression
Assertion bitsinv1 
|- ( N e. NN0 -> sum_ n e. ( bits ` N ) ( 2 ^ n ) = N )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( x = 0 -> ( 0 ..^ x ) = ( 0 ..^ 0 ) )
2 fzo0 
 |-  ( 0 ..^ 0 ) = (/)
3 1 2 eqtrdi 
 |-  ( x = 0 -> ( 0 ..^ x ) = (/) )
4 3 ineq2d 
 |-  ( x = 0 -> ( ( bits ` N ) i^i ( 0 ..^ x ) ) = ( ( bits ` N ) i^i (/) ) )
5 in0 
 |-  ( ( bits ` N ) i^i (/) ) = (/)
6 4 5 eqtrdi 
 |-  ( x = 0 -> ( ( bits ` N ) i^i ( 0 ..^ x ) ) = (/) )
7 6 sumeq1d 
 |-  ( x = 0 -> sum_ n e. ( ( bits ` N ) i^i ( 0 ..^ x ) ) ( 2 ^ n ) = sum_ n e. (/) ( 2 ^ n ) )
8 sum0 
 |-  sum_ n e. (/) ( 2 ^ n ) = 0
9 7 8 eqtrdi 
 |-  ( x = 0 -> sum_ n e. ( ( bits ` N ) i^i ( 0 ..^ x ) ) ( 2 ^ n ) = 0 )
10 oveq2 
 |-  ( x = 0 -> ( 2 ^ x ) = ( 2 ^ 0 ) )
11 2cn 
 |-  2 e. CC
12 exp0 
 |-  ( 2 e. CC -> ( 2 ^ 0 ) = 1 )
13 11 12 ax-mp 
 |-  ( 2 ^ 0 ) = 1
14 10 13 eqtrdi 
 |-  ( x = 0 -> ( 2 ^ x ) = 1 )
15 14 oveq2d 
 |-  ( x = 0 -> ( N mod ( 2 ^ x ) ) = ( N mod 1 ) )
16 9 15 eqeq12d 
 |-  ( x = 0 -> ( sum_ n e. ( ( bits ` N ) i^i ( 0 ..^ x ) ) ( 2 ^ n ) = ( N mod ( 2 ^ x ) ) <-> 0 = ( N mod 1 ) ) )
17 16 imbi2d 
 |-  ( x = 0 -> ( ( N e. NN0 -> sum_ n e. ( ( bits ` N ) i^i ( 0 ..^ x ) ) ( 2 ^ n ) = ( N mod ( 2 ^ x ) ) ) <-> ( N e. NN0 -> 0 = ( N mod 1 ) ) ) )
18 oveq2 
 |-  ( x = k -> ( 0 ..^ x ) = ( 0 ..^ k ) )
19 18 ineq2d 
 |-  ( x = k -> ( ( bits ` N ) i^i ( 0 ..^ x ) ) = ( ( bits ` N ) i^i ( 0 ..^ k ) ) )
20 19 sumeq1d 
 |-  ( x = k -> sum_ n e. ( ( bits ` N ) i^i ( 0 ..^ x ) ) ( 2 ^ n ) = sum_ n e. ( ( bits ` N ) i^i ( 0 ..^ k ) ) ( 2 ^ n ) )
21 oveq2 
 |-  ( x = k -> ( 2 ^ x ) = ( 2 ^ k ) )
22 21 oveq2d 
 |-  ( x = k -> ( N mod ( 2 ^ x ) ) = ( N mod ( 2 ^ k ) ) )
23 20 22 eqeq12d 
 |-  ( x = k -> ( sum_ n e. ( ( bits ` N ) i^i ( 0 ..^ x ) ) ( 2 ^ n ) = ( N mod ( 2 ^ x ) ) <-> sum_ n e. ( ( bits ` N ) i^i ( 0 ..^ k ) ) ( 2 ^ n ) = ( N mod ( 2 ^ k ) ) ) )
24 23 imbi2d 
 |-  ( x = k -> ( ( N e. NN0 -> sum_ n e. ( ( bits ` N ) i^i ( 0 ..^ x ) ) ( 2 ^ n ) = ( N mod ( 2 ^ x ) ) ) <-> ( N e. NN0 -> sum_ n e. ( ( bits ` N ) i^i ( 0 ..^ k ) ) ( 2 ^ n ) = ( N mod ( 2 ^ k ) ) ) ) )
25 oveq2 
 |-  ( x = ( k + 1 ) -> ( 0 ..^ x ) = ( 0 ..^ ( k + 1 ) ) )
26 25 ineq2d 
 |-  ( x = ( k + 1 ) -> ( ( bits ` N ) i^i ( 0 ..^ x ) ) = ( ( bits ` N ) i^i ( 0 ..^ ( k + 1 ) ) ) )
27 26 sumeq1d 
 |-  ( x = ( k + 1 ) -> sum_ n e. ( ( bits ` N ) i^i ( 0 ..^ x ) ) ( 2 ^ n ) = sum_ n e. ( ( bits ` N ) i^i ( 0 ..^ ( k + 1 ) ) ) ( 2 ^ n ) )
28 oveq2 
 |-  ( x = ( k + 1 ) -> ( 2 ^ x ) = ( 2 ^ ( k + 1 ) ) )
29 28 oveq2d 
 |-  ( x = ( k + 1 ) -> ( N mod ( 2 ^ x ) ) = ( N mod ( 2 ^ ( k + 1 ) ) ) )
30 27 29 eqeq12d 
 |-  ( x = ( k + 1 ) -> ( sum_ n e. ( ( bits ` N ) i^i ( 0 ..^ x ) ) ( 2 ^ n ) = ( N mod ( 2 ^ x ) ) <-> sum_ n e. ( ( bits ` N ) i^i ( 0 ..^ ( k + 1 ) ) ) ( 2 ^ n ) = ( N mod ( 2 ^ ( k + 1 ) ) ) ) )
31 30 imbi2d 
 |-  ( x = ( k + 1 ) -> ( ( N e. NN0 -> sum_ n e. ( ( bits ` N ) i^i ( 0 ..^ x ) ) ( 2 ^ n ) = ( N mod ( 2 ^ x ) ) ) <-> ( N e. NN0 -> sum_ n e. ( ( bits ` N ) i^i ( 0 ..^ ( k + 1 ) ) ) ( 2 ^ n ) = ( N mod ( 2 ^ ( k + 1 ) ) ) ) ) )
32 oveq2 
 |-  ( x = N -> ( 0 ..^ x ) = ( 0 ..^ N ) )
33 32 ineq2d 
 |-  ( x = N -> ( ( bits ` N ) i^i ( 0 ..^ x ) ) = ( ( bits ` N ) i^i ( 0 ..^ N ) ) )
34 33 sumeq1d 
 |-  ( x = N -> sum_ n e. ( ( bits ` N ) i^i ( 0 ..^ x ) ) ( 2 ^ n ) = sum_ n e. ( ( bits ` N ) i^i ( 0 ..^ N ) ) ( 2 ^ n ) )
35 oveq2 
 |-  ( x = N -> ( 2 ^ x ) = ( 2 ^ N ) )
36 35 oveq2d 
 |-  ( x = N -> ( N mod ( 2 ^ x ) ) = ( N mod ( 2 ^ N ) ) )
37 34 36 eqeq12d 
 |-  ( x = N -> ( sum_ n e. ( ( bits ` N ) i^i ( 0 ..^ x ) ) ( 2 ^ n ) = ( N mod ( 2 ^ x ) ) <-> sum_ n e. ( ( bits ` N ) i^i ( 0 ..^ N ) ) ( 2 ^ n ) = ( N mod ( 2 ^ N ) ) ) )
38 37 imbi2d 
 |-  ( x = N -> ( ( N e. NN0 -> sum_ n e. ( ( bits ` N ) i^i ( 0 ..^ x ) ) ( 2 ^ n ) = ( N mod ( 2 ^ x ) ) ) <-> ( N e. NN0 -> sum_ n e. ( ( bits ` N ) i^i ( 0 ..^ N ) ) ( 2 ^ n ) = ( N mod ( 2 ^ N ) ) ) ) )
39 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
40 zmod10 
 |-  ( N e. ZZ -> ( N mod 1 ) = 0 )
41 39 40 syl 
 |-  ( N e. NN0 -> ( N mod 1 ) = 0 )
42 41 eqcomd 
 |-  ( N e. NN0 -> 0 = ( N mod 1 ) )
43 oveq1 
 |-  ( sum_ n e. ( ( bits ` N ) i^i ( 0 ..^ k ) ) ( 2 ^ n ) = ( N mod ( 2 ^ k ) ) -> ( sum_ n e. ( ( bits ` N ) i^i ( 0 ..^ k ) ) ( 2 ^ n ) + sum_ n e. ( ( bits ` N ) i^i { k } ) ( 2 ^ n ) ) = ( ( N mod ( 2 ^ k ) ) + sum_ n e. ( ( bits ` N ) i^i { k } ) ( 2 ^ n ) ) )
44 fzonel 
 |-  -. k e. ( 0 ..^ k )
45 44 a1i 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> -. k e. ( 0 ..^ k ) )
46 disjsn 
 |-  ( ( ( 0 ..^ k ) i^i { k } ) = (/) <-> -. k e. ( 0 ..^ k ) )
47 45 46 sylibr 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( 0 ..^ k ) i^i { k } ) = (/) )
48 47 ineq2d 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( bits ` N ) i^i ( ( 0 ..^ k ) i^i { k } ) ) = ( ( bits ` N ) i^i (/) ) )
49 inindi 
 |-  ( ( bits ` N ) i^i ( ( 0 ..^ k ) i^i { k } ) ) = ( ( ( bits ` N ) i^i ( 0 ..^ k ) ) i^i ( ( bits ` N ) i^i { k } ) )
50 48 49 5 3eqtr3g 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( ( bits ` N ) i^i ( 0 ..^ k ) ) i^i ( ( bits ` N ) i^i { k } ) ) = (/) )
51 simpr 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> k e. NN0 )
52 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
53 51 52 eleqtrdi 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> k e. ( ZZ>= ` 0 ) )
54 fzosplitsn 
 |-  ( k e. ( ZZ>= ` 0 ) -> ( 0 ..^ ( k + 1 ) ) = ( ( 0 ..^ k ) u. { k } ) )
55 53 54 syl 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( 0 ..^ ( k + 1 ) ) = ( ( 0 ..^ k ) u. { k } ) )
56 55 ineq2d 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( bits ` N ) i^i ( 0 ..^ ( k + 1 ) ) ) = ( ( bits ` N ) i^i ( ( 0 ..^ k ) u. { k } ) ) )
57 indi 
 |-  ( ( bits ` N ) i^i ( ( 0 ..^ k ) u. { k } ) ) = ( ( ( bits ` N ) i^i ( 0 ..^ k ) ) u. ( ( bits ` N ) i^i { k } ) )
58 56 57 eqtrdi 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( bits ` N ) i^i ( 0 ..^ ( k + 1 ) ) ) = ( ( ( bits ` N ) i^i ( 0 ..^ k ) ) u. ( ( bits ` N ) i^i { k } ) ) )
59 fzofi 
 |-  ( 0 ..^ ( k + 1 ) ) e. Fin
60 inss2 
 |-  ( ( bits ` N ) i^i ( 0 ..^ ( k + 1 ) ) ) C_ ( 0 ..^ ( k + 1 ) )
61 ssfi 
 |-  ( ( ( 0 ..^ ( k + 1 ) ) e. Fin /\ ( ( bits ` N ) i^i ( 0 ..^ ( k + 1 ) ) ) C_ ( 0 ..^ ( k + 1 ) ) ) -> ( ( bits ` N ) i^i ( 0 ..^ ( k + 1 ) ) ) e. Fin )
62 59 60 61 mp2an 
 |-  ( ( bits ` N ) i^i ( 0 ..^ ( k + 1 ) ) ) e. Fin
63 62 a1i 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( bits ` N ) i^i ( 0 ..^ ( k + 1 ) ) ) e. Fin )
64 2nn 
 |-  2 e. NN
65 64 a1i 
 |-  ( ( ( N e. NN0 /\ k e. NN0 ) /\ n e. ( ( bits ` N ) i^i ( 0 ..^ ( k + 1 ) ) ) ) -> 2 e. NN )
66 simpr 
 |-  ( ( ( N e. NN0 /\ k e. NN0 ) /\ n e. ( ( bits ` N ) i^i ( 0 ..^ ( k + 1 ) ) ) ) -> n e. ( ( bits ` N ) i^i ( 0 ..^ ( k + 1 ) ) ) )
67 66 elin2d 
 |-  ( ( ( N e. NN0 /\ k e. NN0 ) /\ n e. ( ( bits ` N ) i^i ( 0 ..^ ( k + 1 ) ) ) ) -> n e. ( 0 ..^ ( k + 1 ) ) )
68 elfzouz 
 |-  ( n e. ( 0 ..^ ( k + 1 ) ) -> n e. ( ZZ>= ` 0 ) )
69 67 68 syl 
 |-  ( ( ( N e. NN0 /\ k e. NN0 ) /\ n e. ( ( bits ` N ) i^i ( 0 ..^ ( k + 1 ) ) ) ) -> n e. ( ZZ>= ` 0 ) )
70 69 52 eleqtrrdi 
 |-  ( ( ( N e. NN0 /\ k e. NN0 ) /\ n e. ( ( bits ` N ) i^i ( 0 ..^ ( k + 1 ) ) ) ) -> n e. NN0 )
71 65 70 nnexpcld 
 |-  ( ( ( N e. NN0 /\ k e. NN0 ) /\ n e. ( ( bits ` N ) i^i ( 0 ..^ ( k + 1 ) ) ) ) -> ( 2 ^ n ) e. NN )
72 71 nncnd 
 |-  ( ( ( N e. NN0 /\ k e. NN0 ) /\ n e. ( ( bits ` N ) i^i ( 0 ..^ ( k + 1 ) ) ) ) -> ( 2 ^ n ) e. CC )
73 50 58 63 72 fsumsplit 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> sum_ n e. ( ( bits ` N ) i^i ( 0 ..^ ( k + 1 ) ) ) ( 2 ^ n ) = ( sum_ n e. ( ( bits ` N ) i^i ( 0 ..^ k ) ) ( 2 ^ n ) + sum_ n e. ( ( bits ` N ) i^i { k } ) ( 2 ^ n ) ) )
74 bitsinv1lem 
 |-  ( ( N e. ZZ /\ k e. NN0 ) -> ( N mod ( 2 ^ ( k + 1 ) ) ) = ( ( N mod ( 2 ^ k ) ) + if ( k e. ( bits ` N ) , ( 2 ^ k ) , 0 ) ) )
75 39 74 sylan 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( N mod ( 2 ^ ( k + 1 ) ) ) = ( ( N mod ( 2 ^ k ) ) + if ( k e. ( bits ` N ) , ( 2 ^ k ) , 0 ) ) )
76 eqeq2 
 |-  ( ( 2 ^ k ) = if ( k e. ( bits ` N ) , ( 2 ^ k ) , 0 ) -> ( sum_ n e. ( ( bits ` N ) i^i { k } ) ( 2 ^ n ) = ( 2 ^ k ) <-> sum_ n e. ( ( bits ` N ) i^i { k } ) ( 2 ^ n ) = if ( k e. ( bits ` N ) , ( 2 ^ k ) , 0 ) ) )
77 eqeq2 
 |-  ( 0 = if ( k e. ( bits ` N ) , ( 2 ^ k ) , 0 ) -> ( sum_ n e. ( ( bits ` N ) i^i { k } ) ( 2 ^ n ) = 0 <-> sum_ n e. ( ( bits ` N ) i^i { k } ) ( 2 ^ n ) = if ( k e. ( bits ` N ) , ( 2 ^ k ) , 0 ) ) )
78 simpr 
 |-  ( ( ( N e. NN0 /\ k e. NN0 ) /\ k e. ( bits ` N ) ) -> k e. ( bits ` N ) )
79 78 snssd 
 |-  ( ( ( N e. NN0 /\ k e. NN0 ) /\ k e. ( bits ` N ) ) -> { k } C_ ( bits ` N ) )
80 sseqin2 
 |-  ( { k } C_ ( bits ` N ) <-> ( ( bits ` N ) i^i { k } ) = { k } )
81 79 80 sylib 
 |-  ( ( ( N e. NN0 /\ k e. NN0 ) /\ k e. ( bits ` N ) ) -> ( ( bits ` N ) i^i { k } ) = { k } )
82 81 sumeq1d 
 |-  ( ( ( N e. NN0 /\ k e. NN0 ) /\ k e. ( bits ` N ) ) -> sum_ n e. ( ( bits ` N ) i^i { k } ) ( 2 ^ n ) = sum_ n e. { k } ( 2 ^ n ) )
83 simplr 
 |-  ( ( ( N e. NN0 /\ k e. NN0 ) /\ k e. ( bits ` N ) ) -> k e. NN0 )
84 64 a1i 
 |-  ( ( ( N e. NN0 /\ k e. NN0 ) /\ k e. ( bits ` N ) ) -> 2 e. NN )
85 84 83 nnexpcld 
 |-  ( ( ( N e. NN0 /\ k e. NN0 ) /\ k e. ( bits ` N ) ) -> ( 2 ^ k ) e. NN )
86 85 nncnd 
 |-  ( ( ( N e. NN0 /\ k e. NN0 ) /\ k e. ( bits ` N ) ) -> ( 2 ^ k ) e. CC )
87 oveq2 
 |-  ( n = k -> ( 2 ^ n ) = ( 2 ^ k ) )
88 87 sumsn 
 |-  ( ( k e. NN0 /\ ( 2 ^ k ) e. CC ) -> sum_ n e. { k } ( 2 ^ n ) = ( 2 ^ k ) )
89 83 86 88 syl2anc 
 |-  ( ( ( N e. NN0 /\ k e. NN0 ) /\ k e. ( bits ` N ) ) -> sum_ n e. { k } ( 2 ^ n ) = ( 2 ^ k ) )
90 82 89 eqtrd 
 |-  ( ( ( N e. NN0 /\ k e. NN0 ) /\ k e. ( bits ` N ) ) -> sum_ n e. ( ( bits ` N ) i^i { k } ) ( 2 ^ n ) = ( 2 ^ k ) )
91 simpr 
 |-  ( ( ( N e. NN0 /\ k e. NN0 ) /\ -. k e. ( bits ` N ) ) -> -. k e. ( bits ` N ) )
92 disjsn 
 |-  ( ( ( bits ` N ) i^i { k } ) = (/) <-> -. k e. ( bits ` N ) )
93 91 92 sylibr 
 |-  ( ( ( N e. NN0 /\ k e. NN0 ) /\ -. k e. ( bits ` N ) ) -> ( ( bits ` N ) i^i { k } ) = (/) )
94 93 sumeq1d 
 |-  ( ( ( N e. NN0 /\ k e. NN0 ) /\ -. k e. ( bits ` N ) ) -> sum_ n e. ( ( bits ` N ) i^i { k } ) ( 2 ^ n ) = sum_ n e. (/) ( 2 ^ n ) )
95 94 8 eqtrdi 
 |-  ( ( ( N e. NN0 /\ k e. NN0 ) /\ -. k e. ( bits ` N ) ) -> sum_ n e. ( ( bits ` N ) i^i { k } ) ( 2 ^ n ) = 0 )
96 76 77 90 95 ifbothda 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> sum_ n e. ( ( bits ` N ) i^i { k } ) ( 2 ^ n ) = if ( k e. ( bits ` N ) , ( 2 ^ k ) , 0 ) )
97 96 oveq2d 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( N mod ( 2 ^ k ) ) + sum_ n e. ( ( bits ` N ) i^i { k } ) ( 2 ^ n ) ) = ( ( N mod ( 2 ^ k ) ) + if ( k e. ( bits ` N ) , ( 2 ^ k ) , 0 ) ) )
98 75 97 eqtr4d 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( N mod ( 2 ^ ( k + 1 ) ) ) = ( ( N mod ( 2 ^ k ) ) + sum_ n e. ( ( bits ` N ) i^i { k } ) ( 2 ^ n ) ) )
99 73 98 eqeq12d 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( sum_ n e. ( ( bits ` N ) i^i ( 0 ..^ ( k + 1 ) ) ) ( 2 ^ n ) = ( N mod ( 2 ^ ( k + 1 ) ) ) <-> ( sum_ n e. ( ( bits ` N ) i^i ( 0 ..^ k ) ) ( 2 ^ n ) + sum_ n e. ( ( bits ` N ) i^i { k } ) ( 2 ^ n ) ) = ( ( N mod ( 2 ^ k ) ) + sum_ n e. ( ( bits ` N ) i^i { k } ) ( 2 ^ n ) ) ) )
100 43 99 syl5ibr 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( sum_ n e. ( ( bits ` N ) i^i ( 0 ..^ k ) ) ( 2 ^ n ) = ( N mod ( 2 ^ k ) ) -> sum_ n e. ( ( bits ` N ) i^i ( 0 ..^ ( k + 1 ) ) ) ( 2 ^ n ) = ( N mod ( 2 ^ ( k + 1 ) ) ) ) )
101 100 expcom 
 |-  ( k e. NN0 -> ( N e. NN0 -> ( sum_ n e. ( ( bits ` N ) i^i ( 0 ..^ k ) ) ( 2 ^ n ) = ( N mod ( 2 ^ k ) ) -> sum_ n e. ( ( bits ` N ) i^i ( 0 ..^ ( k + 1 ) ) ) ( 2 ^ n ) = ( N mod ( 2 ^ ( k + 1 ) ) ) ) ) )
102 101 a2d 
 |-  ( k e. NN0 -> ( ( N e. NN0 -> sum_ n e. ( ( bits ` N ) i^i ( 0 ..^ k ) ) ( 2 ^ n ) = ( N mod ( 2 ^ k ) ) ) -> ( N e. NN0 -> sum_ n e. ( ( bits ` N ) i^i ( 0 ..^ ( k + 1 ) ) ) ( 2 ^ n ) = ( N mod ( 2 ^ ( k + 1 ) ) ) ) ) )
103 17 24 31 38 42 102 nn0ind 
 |-  ( N e. NN0 -> ( N e. NN0 -> sum_ n e. ( ( bits ` N ) i^i ( 0 ..^ N ) ) ( 2 ^ n ) = ( N mod ( 2 ^ N ) ) ) )
104 103 pm2.43i 
 |-  ( N e. NN0 -> sum_ n e. ( ( bits ` N ) i^i ( 0 ..^ N ) ) ( 2 ^ n ) = ( N mod ( 2 ^ N ) ) )
105 id 
 |-  ( N e. NN0 -> N e. NN0 )
106 105 52 eleqtrdi 
 |-  ( N e. NN0 -> N e. ( ZZ>= ` 0 ) )
107 64 a1i 
 |-  ( N e. NN0 -> 2 e. NN )
108 107 105 nnexpcld 
 |-  ( N e. NN0 -> ( 2 ^ N ) e. NN )
109 108 nnzd 
 |-  ( N e. NN0 -> ( 2 ^ N ) e. ZZ )
110 2z 
 |-  2 e. ZZ
111 uzid 
 |-  ( 2 e. ZZ -> 2 e. ( ZZ>= ` 2 ) )
112 110 111 ax-mp 
 |-  2 e. ( ZZ>= ` 2 )
113 bernneq3 
 |-  ( ( 2 e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> N < ( 2 ^ N ) )
114 112 113 mpan 
 |-  ( N e. NN0 -> N < ( 2 ^ N ) )
115 elfzo2 
 |-  ( N e. ( 0 ..^ ( 2 ^ N ) ) <-> ( N e. ( ZZ>= ` 0 ) /\ ( 2 ^ N ) e. ZZ /\ N < ( 2 ^ N ) ) )
116 106 109 114 115 syl3anbrc 
 |-  ( N e. NN0 -> N e. ( 0 ..^ ( 2 ^ N ) ) )
117 bitsfzo 
 |-  ( ( N e. ZZ /\ N e. NN0 ) -> ( N e. ( 0 ..^ ( 2 ^ N ) ) <-> ( bits ` N ) C_ ( 0 ..^ N ) ) )
118 39 105 117 syl2anc 
 |-  ( N e. NN0 -> ( N e. ( 0 ..^ ( 2 ^ N ) ) <-> ( bits ` N ) C_ ( 0 ..^ N ) ) )
119 116 118 mpbid 
 |-  ( N e. NN0 -> ( bits ` N ) C_ ( 0 ..^ N ) )
120 df-ss 
 |-  ( ( bits ` N ) C_ ( 0 ..^ N ) <-> ( ( bits ` N ) i^i ( 0 ..^ N ) ) = ( bits ` N ) )
121 119 120 sylib 
 |-  ( N e. NN0 -> ( ( bits ` N ) i^i ( 0 ..^ N ) ) = ( bits ` N ) )
122 121 sumeq1d 
 |-  ( N e. NN0 -> sum_ n e. ( ( bits ` N ) i^i ( 0 ..^ N ) ) ( 2 ^ n ) = sum_ n e. ( bits ` N ) ( 2 ^ n ) )
123 nn0re 
 |-  ( N e. NN0 -> N e. RR )
124 2rp 
 |-  2 e. RR+
125 124 a1i 
 |-  ( N e. NN0 -> 2 e. RR+ )
126 125 39 rpexpcld 
 |-  ( N e. NN0 -> ( 2 ^ N ) e. RR+ )
127 nn0ge0 
 |-  ( N e. NN0 -> 0 <_ N )
128 modid 
 |-  ( ( ( N e. RR /\ ( 2 ^ N ) e. RR+ ) /\ ( 0 <_ N /\ N < ( 2 ^ N ) ) ) -> ( N mod ( 2 ^ N ) ) = N )
129 123 126 127 114 128 syl22anc 
 |-  ( N e. NN0 -> ( N mod ( 2 ^ N ) ) = N )
130 104 122 129 3eqtr3d 
 |-  ( N e. NN0 -> sum_ n e. ( bits ` N ) ( 2 ^ n ) = N )