Metamath Proof Explorer


Theorem bitsinvp1

Description: Recursive definition of the inverse of the bits function. (Contributed by Mario Carneiro, 8-Sep-2016)

Ref Expression
Hypothesis bitsinv.k 𝐾 = ( bits ↾ ℕ0 )
Assertion bitsinvp1 ( ( 𝐴 ⊆ ℕ0𝑁 ∈ ℕ0 ) → ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + if ( 𝑁𝐴 , ( 2 ↑ 𝑁 ) , 0 ) ) )

Proof

Step Hyp Ref Expression
1 bitsinv.k 𝐾 = ( bits ↾ ℕ0 )
2 fzonel ¬ 𝑁 ∈ ( 0 ..^ 𝑁 )
3 2 a1i ( ( 𝐴 ⊆ ℕ0𝑁 ∈ ℕ0 ) → ¬ 𝑁 ∈ ( 0 ..^ 𝑁 ) )
4 disjsn ( ( ( 0 ..^ 𝑁 ) ∩ { 𝑁 } ) = ∅ ↔ ¬ 𝑁 ∈ ( 0 ..^ 𝑁 ) )
5 3 4 sylibr ( ( 𝐴 ⊆ ℕ0𝑁 ∈ ℕ0 ) → ( ( 0 ..^ 𝑁 ) ∩ { 𝑁 } ) = ∅ )
6 5 ineq2d ( ( 𝐴 ⊆ ℕ0𝑁 ∈ ℕ0 ) → ( 𝐴 ∩ ( ( 0 ..^ 𝑁 ) ∩ { 𝑁 } ) ) = ( 𝐴 ∩ ∅ ) )
7 inindi ( 𝐴 ∩ ( ( 0 ..^ 𝑁 ) ∩ { 𝑁 } ) ) = ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∩ ( 𝐴 ∩ { 𝑁 } ) )
8 in0 ( 𝐴 ∩ ∅ ) = ∅
9 6 7 8 3eqtr3g ( ( 𝐴 ⊆ ℕ0𝑁 ∈ ℕ0 ) → ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∩ ( 𝐴 ∩ { 𝑁 } ) ) = ∅ )
10 simpr ( ( 𝐴 ⊆ ℕ0𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
11 nn0uz 0 = ( ℤ ‘ 0 )
12 10 11 eleqtrdi ( ( 𝐴 ⊆ ℕ0𝑁 ∈ ℕ0 ) → 𝑁 ∈ ( ℤ ‘ 0 ) )
13 fzosplitsn ( 𝑁 ∈ ( ℤ ‘ 0 ) → ( 0 ..^ ( 𝑁 + 1 ) ) = ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) )
14 12 13 syl ( ( 𝐴 ⊆ ℕ0𝑁 ∈ ℕ0 ) → ( 0 ..^ ( 𝑁 + 1 ) ) = ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) )
15 14 ineq2d ( ( 𝐴 ⊆ ℕ0𝑁 ∈ ℕ0 ) → ( 𝐴 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) = ( 𝐴 ∩ ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) ) )
16 indi ( 𝐴 ∩ ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) ) = ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∪ ( 𝐴 ∩ { 𝑁 } ) )
17 15 16 eqtrdi ( ( 𝐴 ⊆ ℕ0𝑁 ∈ ℕ0 ) → ( 𝐴 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) = ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∪ ( 𝐴 ∩ { 𝑁 } ) ) )
18 fzofi ( 0 ..^ ( 𝑁 + 1 ) ) ∈ Fin
19 18 a1i ( ( 𝐴 ⊆ ℕ0𝑁 ∈ ℕ0 ) → ( 0 ..^ ( 𝑁 + 1 ) ) ∈ Fin )
20 inss2 ( 𝐴 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ⊆ ( 0 ..^ ( 𝑁 + 1 ) )
21 ssfi ( ( ( 0 ..^ ( 𝑁 + 1 ) ) ∈ Fin ∧ ( 𝐴 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ⊆ ( 0 ..^ ( 𝑁 + 1 ) ) ) → ( 𝐴 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ∈ Fin )
22 19 20 21 sylancl ( ( 𝐴 ⊆ ℕ0𝑁 ∈ ℕ0 ) → ( 𝐴 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ∈ Fin )
23 2nn 2 ∈ ℕ
24 23 a1i ( ( ( 𝐴 ⊆ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 𝐴 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) → 2 ∈ ℕ )
25 inss1 ( 𝐴 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ⊆ 𝐴
26 simpl ( ( 𝐴 ⊆ ℕ0𝑁 ∈ ℕ0 ) → 𝐴 ⊆ ℕ0 )
27 25 26 sstrid ( ( 𝐴 ⊆ ℕ0𝑁 ∈ ℕ0 ) → ( 𝐴 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ⊆ ℕ0 )
28 27 sselda ( ( ( 𝐴 ⊆ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 𝐴 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) → 𝑘 ∈ ℕ0 )
29 24 28 nnexpcld ( ( ( 𝐴 ⊆ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 𝐴 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) → ( 2 ↑ 𝑘 ) ∈ ℕ )
30 29 nncnd ( ( ( 𝐴 ⊆ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 𝐴 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) → ( 2 ↑ 𝑘 ) ∈ ℂ )
31 9 17 22 30 fsumsplit ( ( 𝐴 ⊆ ℕ0𝑁 ∈ ℕ0 ) → Σ 𝑘 ∈ ( 𝐴 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ( 2 ↑ 𝑘 ) = ( Σ 𝑘 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ( 2 ↑ 𝑘 ) + Σ 𝑘 ∈ ( 𝐴 ∩ { 𝑁 } ) ( 2 ↑ 𝑘 ) ) )
32 elfpw ( ( 𝐴 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) ↔ ( ( 𝐴 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ⊆ ℕ0 ∧ ( 𝐴 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ∈ Fin ) )
33 27 22 32 sylanbrc ( ( 𝐴 ⊆ ℕ0𝑁 ∈ ℕ0 ) → ( 𝐴 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) )
34 1 bitsinv ( ( 𝐴 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) → ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) = Σ 𝑘 ∈ ( 𝐴 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ( 2 ↑ 𝑘 ) )
35 33 34 syl ( ( 𝐴 ⊆ ℕ0𝑁 ∈ ℕ0 ) → ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) = Σ 𝑘 ∈ ( 𝐴 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ( 2 ↑ 𝑘 ) )
36 inss1 ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ⊆ 𝐴
37 36 26 sstrid ( ( 𝐴 ⊆ ℕ0𝑁 ∈ ℕ0 ) → ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 )
38 fzofi ( 0 ..^ 𝑁 ) ∈ Fin
39 38 a1i ( ( 𝐴 ⊆ ℕ0𝑁 ∈ ℕ0 ) → ( 0 ..^ 𝑁 ) ∈ Fin )
40 inss2 ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 0 ..^ 𝑁 )
41 ssfi ( ( ( 0 ..^ 𝑁 ) ∈ Fin ∧ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 0 ..^ 𝑁 ) ) → ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin )
42 39 40 41 sylancl ( ( 𝐴 ⊆ ℕ0𝑁 ∈ ℕ0 ) → ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin )
43 elfpw ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) ↔ ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 ∧ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin ) )
44 37 42 43 sylanbrc ( ( 𝐴 ⊆ ℕ0𝑁 ∈ ℕ0 ) → ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) )
45 1 bitsinv ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) → ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) = Σ 𝑘 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ( 2 ↑ 𝑘 ) )
46 44 45 syl ( ( 𝐴 ⊆ ℕ0𝑁 ∈ ℕ0 ) → ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) = Σ 𝑘 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ( 2 ↑ 𝑘 ) )
47 snssi ( 𝑁𝐴 → { 𝑁 } ⊆ 𝐴 )
48 47 adantl ( ( ( 𝐴 ⊆ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐴 ) → { 𝑁 } ⊆ 𝐴 )
49 sseqin2 ( { 𝑁 } ⊆ 𝐴 ↔ ( 𝐴 ∩ { 𝑁 } ) = { 𝑁 } )
50 48 49 sylib ( ( ( 𝐴 ⊆ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐴 ) → ( 𝐴 ∩ { 𝑁 } ) = { 𝑁 } )
51 50 sumeq1d ( ( ( 𝐴 ⊆ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐴 ) → Σ 𝑘 ∈ ( 𝐴 ∩ { 𝑁 } ) ( 2 ↑ 𝑘 ) = Σ 𝑘 ∈ { 𝑁 } ( 2 ↑ 𝑘 ) )
52 simpr ( ( ( 𝐴 ⊆ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐴 ) → 𝑁𝐴 )
53 23 a1i ( ( ( 𝐴 ⊆ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐴 ) → 2 ∈ ℕ )
54 simplr ( ( ( 𝐴 ⊆ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐴 ) → 𝑁 ∈ ℕ0 )
55 53 54 nnexpcld ( ( ( 𝐴 ⊆ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐴 ) → ( 2 ↑ 𝑁 ) ∈ ℕ )
56 55 nncnd ( ( ( 𝐴 ⊆ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐴 ) → ( 2 ↑ 𝑁 ) ∈ ℂ )
57 oveq2 ( 𝑘 = 𝑁 → ( 2 ↑ 𝑘 ) = ( 2 ↑ 𝑁 ) )
58 57 sumsn ( ( 𝑁𝐴 ∧ ( 2 ↑ 𝑁 ) ∈ ℂ ) → Σ 𝑘 ∈ { 𝑁 } ( 2 ↑ 𝑘 ) = ( 2 ↑ 𝑁 ) )
59 52 56 58 syl2anc ( ( ( 𝐴 ⊆ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐴 ) → Σ 𝑘 ∈ { 𝑁 } ( 2 ↑ 𝑘 ) = ( 2 ↑ 𝑁 ) )
60 51 59 eqtr2d ( ( ( 𝐴 ⊆ ℕ0𝑁 ∈ ℕ0 ) ∧ 𝑁𝐴 ) → ( 2 ↑ 𝑁 ) = Σ 𝑘 ∈ ( 𝐴 ∩ { 𝑁 } ) ( 2 ↑ 𝑘 ) )
61 simpr ( ( ( 𝐴 ⊆ ℕ0𝑁 ∈ ℕ0 ) ∧ ¬ 𝑁𝐴 ) → ¬ 𝑁𝐴 )
62 disjsn ( ( 𝐴 ∩ { 𝑁 } ) = ∅ ↔ ¬ 𝑁𝐴 )
63 61 62 sylibr ( ( ( 𝐴 ⊆ ℕ0𝑁 ∈ ℕ0 ) ∧ ¬ 𝑁𝐴 ) → ( 𝐴 ∩ { 𝑁 } ) = ∅ )
64 63 sumeq1d ( ( ( 𝐴 ⊆ ℕ0𝑁 ∈ ℕ0 ) ∧ ¬ 𝑁𝐴 ) → Σ 𝑘 ∈ ( 𝐴 ∩ { 𝑁 } ) ( 2 ↑ 𝑘 ) = Σ 𝑘 ∈ ∅ ( 2 ↑ 𝑘 ) )
65 sum0 Σ 𝑘 ∈ ∅ ( 2 ↑ 𝑘 ) = 0
66 64 65 eqtr2di ( ( ( 𝐴 ⊆ ℕ0𝑁 ∈ ℕ0 ) ∧ ¬ 𝑁𝐴 ) → 0 = Σ 𝑘 ∈ ( 𝐴 ∩ { 𝑁 } ) ( 2 ↑ 𝑘 ) )
67 60 66 ifeqda ( ( 𝐴 ⊆ ℕ0𝑁 ∈ ℕ0 ) → if ( 𝑁𝐴 , ( 2 ↑ 𝑁 ) , 0 ) = Σ 𝑘 ∈ ( 𝐴 ∩ { 𝑁 } ) ( 2 ↑ 𝑘 ) )
68 46 67 oveq12d ( ( 𝐴 ⊆ ℕ0𝑁 ∈ ℕ0 ) → ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + if ( 𝑁𝐴 , ( 2 ↑ 𝑁 ) , 0 ) ) = ( Σ 𝑘 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ( 2 ↑ 𝑘 ) + Σ 𝑘 ∈ ( 𝐴 ∩ { 𝑁 } ) ( 2 ↑ 𝑘 ) ) )
69 31 35 68 3eqtr4d ( ( 𝐴 ⊆ ℕ0𝑁 ∈ ℕ0 ) → ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + if ( 𝑁𝐴 , ( 2 ↑ 𝑁 ) , 0 ) ) )