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 ) ) )