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 ( 𝑁 ∈ ℕ0 → Σ 𝑛 ∈ ( bits ‘ 𝑁 ) ( 2 ↑ 𝑛 ) = 𝑁 )

Proof

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