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 
|- K = `' ( bits |` NN0 )
Assertion bitsinvp1 
|- ( ( A C_ NN0 /\ N e. NN0 ) -> ( K ` ( A i^i ( 0 ..^ ( N + 1 ) ) ) ) = ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + if ( N e. A , ( 2 ^ N ) , 0 ) ) )

Proof

Step Hyp Ref Expression
1 bitsinv.k 
 |-  K = `' ( bits |` NN0 )
2 fzonel 
 |-  -. N e. ( 0 ..^ N )
3 2 a1i 
 |-  ( ( A C_ NN0 /\ N e. NN0 ) -> -. N e. ( 0 ..^ N ) )
4 disjsn 
 |-  ( ( ( 0 ..^ N ) i^i { N } ) = (/) <-> -. N e. ( 0 ..^ N ) )
5 3 4 sylibr 
 |-  ( ( A C_ NN0 /\ N e. NN0 ) -> ( ( 0 ..^ N ) i^i { N } ) = (/) )
6 5 ineq2d 
 |-  ( ( A C_ NN0 /\ N e. NN0 ) -> ( A i^i ( ( 0 ..^ N ) i^i { N } ) ) = ( A i^i (/) ) )
7 inindi 
 |-  ( A i^i ( ( 0 ..^ N ) i^i { N } ) ) = ( ( A i^i ( 0 ..^ N ) ) i^i ( A i^i { N } ) )
8 in0 
 |-  ( A i^i (/) ) = (/)
9 6 7 8 3eqtr3g 
 |-  ( ( A C_ NN0 /\ N e. NN0 ) -> ( ( A i^i ( 0 ..^ N ) ) i^i ( A i^i { N } ) ) = (/) )
10 simpr 
 |-  ( ( A C_ NN0 /\ N e. NN0 ) -> N e. NN0 )
11 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
12 10 11 eleqtrdi 
 |-  ( ( A C_ NN0 /\ N e. NN0 ) -> N e. ( ZZ>= ` 0 ) )
13 fzosplitsn 
 |-  ( N e. ( ZZ>= ` 0 ) -> ( 0 ..^ ( N + 1 ) ) = ( ( 0 ..^ N ) u. { N } ) )
14 12 13 syl 
 |-  ( ( A C_ NN0 /\ N e. NN0 ) -> ( 0 ..^ ( N + 1 ) ) = ( ( 0 ..^ N ) u. { N } ) )
15 14 ineq2d 
 |-  ( ( A C_ NN0 /\ N e. NN0 ) -> ( A i^i ( 0 ..^ ( N + 1 ) ) ) = ( A i^i ( ( 0 ..^ N ) u. { N } ) ) )
16 indi 
 |-  ( A i^i ( ( 0 ..^ N ) u. { N } ) ) = ( ( A i^i ( 0 ..^ N ) ) u. ( A i^i { N } ) )
17 15 16 eqtrdi 
 |-  ( ( A C_ NN0 /\ N e. NN0 ) -> ( A i^i ( 0 ..^ ( N + 1 ) ) ) = ( ( A i^i ( 0 ..^ N ) ) u. ( A i^i { N } ) ) )
18 fzofi 
 |-  ( 0 ..^ ( N + 1 ) ) e. Fin
19 18 a1i 
 |-  ( ( A C_ NN0 /\ N e. NN0 ) -> ( 0 ..^ ( N + 1 ) ) e. Fin )
20 inss2 
 |-  ( A i^i ( 0 ..^ ( N + 1 ) ) ) C_ ( 0 ..^ ( N + 1 ) )
21 ssfi 
 |-  ( ( ( 0 ..^ ( N + 1 ) ) e. Fin /\ ( A i^i ( 0 ..^ ( N + 1 ) ) ) C_ ( 0 ..^ ( N + 1 ) ) ) -> ( A i^i ( 0 ..^ ( N + 1 ) ) ) e. Fin )
22 19 20 21 sylancl 
 |-  ( ( A C_ NN0 /\ N e. NN0 ) -> ( A i^i ( 0 ..^ ( N + 1 ) ) ) e. Fin )
23 2nn 
 |-  2 e. NN
24 23 a1i 
 |-  ( ( ( A C_ NN0 /\ N e. NN0 ) /\ k e. ( A i^i ( 0 ..^ ( N + 1 ) ) ) ) -> 2 e. NN )
25 inss1 
 |-  ( A i^i ( 0 ..^ ( N + 1 ) ) ) C_ A
26 simpl 
 |-  ( ( A C_ NN0 /\ N e. NN0 ) -> A C_ NN0 )
27 25 26 sstrid 
 |-  ( ( A C_ NN0 /\ N e. NN0 ) -> ( A i^i ( 0 ..^ ( N + 1 ) ) ) C_ NN0 )
28 27 sselda 
 |-  ( ( ( A C_ NN0 /\ N e. NN0 ) /\ k e. ( A i^i ( 0 ..^ ( N + 1 ) ) ) ) -> k e. NN0 )
29 24 28 nnexpcld 
 |-  ( ( ( A C_ NN0 /\ N e. NN0 ) /\ k e. ( A i^i ( 0 ..^ ( N + 1 ) ) ) ) -> ( 2 ^ k ) e. NN )
30 29 nncnd 
 |-  ( ( ( A C_ NN0 /\ N e. NN0 ) /\ k e. ( A i^i ( 0 ..^ ( N + 1 ) ) ) ) -> ( 2 ^ k ) e. CC )
31 9 17 22 30 fsumsplit 
 |-  ( ( A C_ NN0 /\ N e. NN0 ) -> sum_ k e. ( A i^i ( 0 ..^ ( N + 1 ) ) ) ( 2 ^ k ) = ( sum_ k e. ( A i^i ( 0 ..^ N ) ) ( 2 ^ k ) + sum_ k e. ( A i^i { N } ) ( 2 ^ k ) ) )
32 elfpw 
 |-  ( ( A i^i ( 0 ..^ ( N + 1 ) ) ) e. ( ~P NN0 i^i Fin ) <-> ( ( A i^i ( 0 ..^ ( N + 1 ) ) ) C_ NN0 /\ ( A i^i ( 0 ..^ ( N + 1 ) ) ) e. Fin ) )
33 27 22 32 sylanbrc 
 |-  ( ( A C_ NN0 /\ N e. NN0 ) -> ( A i^i ( 0 ..^ ( N + 1 ) ) ) e. ( ~P NN0 i^i Fin ) )
34 1 bitsinv 
 |-  ( ( A i^i ( 0 ..^ ( N + 1 ) ) ) e. ( ~P NN0 i^i Fin ) -> ( K ` ( A i^i ( 0 ..^ ( N + 1 ) ) ) ) = sum_ k e. ( A i^i ( 0 ..^ ( N + 1 ) ) ) ( 2 ^ k ) )
35 33 34 syl 
 |-  ( ( A C_ NN0 /\ N e. NN0 ) -> ( K ` ( A i^i ( 0 ..^ ( N + 1 ) ) ) ) = sum_ k e. ( A i^i ( 0 ..^ ( N + 1 ) ) ) ( 2 ^ k ) )
36 inss1 
 |-  ( A i^i ( 0 ..^ N ) ) C_ A
37 36 26 sstrid 
 |-  ( ( A C_ NN0 /\ N e. NN0 ) -> ( A i^i ( 0 ..^ N ) ) C_ NN0 )
38 fzofi 
 |-  ( 0 ..^ N ) e. Fin
39 38 a1i 
 |-  ( ( A C_ NN0 /\ N e. NN0 ) -> ( 0 ..^ N ) e. Fin )
40 inss2 
 |-  ( A i^i ( 0 ..^ N ) ) C_ ( 0 ..^ N )
41 ssfi 
 |-  ( ( ( 0 ..^ N ) e. Fin /\ ( A i^i ( 0 ..^ N ) ) C_ ( 0 ..^ N ) ) -> ( A i^i ( 0 ..^ N ) ) e. Fin )
42 39 40 41 sylancl 
 |-  ( ( A C_ NN0 /\ N e. NN0 ) -> ( A i^i ( 0 ..^ N ) ) e. Fin )
43 elfpw 
 |-  ( ( A i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) <-> ( ( A i^i ( 0 ..^ N ) ) C_ NN0 /\ ( A i^i ( 0 ..^ N ) ) e. Fin ) )
44 37 42 43 sylanbrc 
 |-  ( ( A C_ NN0 /\ N e. NN0 ) -> ( A i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) )
45 1 bitsinv 
 |-  ( ( A i^i ( 0 ..^ N ) ) e. ( ~P NN0 i^i Fin ) -> ( K ` ( A i^i ( 0 ..^ N ) ) ) = sum_ k e. ( A i^i ( 0 ..^ N ) ) ( 2 ^ k ) )
46 44 45 syl 
 |-  ( ( A C_ NN0 /\ N e. NN0 ) -> ( K ` ( A i^i ( 0 ..^ N ) ) ) = sum_ k e. ( A i^i ( 0 ..^ N ) ) ( 2 ^ k ) )
47 snssi 
 |-  ( N e. A -> { N } C_ A )
48 47 adantl 
 |-  ( ( ( A C_ NN0 /\ N e. NN0 ) /\ N e. A ) -> { N } C_ A )
49 sseqin2 
 |-  ( { N } C_ A <-> ( A i^i { N } ) = { N } )
50 48 49 sylib 
 |-  ( ( ( A C_ NN0 /\ N e. NN0 ) /\ N e. A ) -> ( A i^i { N } ) = { N } )
51 50 sumeq1d 
 |-  ( ( ( A C_ NN0 /\ N e. NN0 ) /\ N e. A ) -> sum_ k e. ( A i^i { N } ) ( 2 ^ k ) = sum_ k e. { N } ( 2 ^ k ) )
52 simpr 
 |-  ( ( ( A C_ NN0 /\ N e. NN0 ) /\ N e. A ) -> N e. A )
53 23 a1i 
 |-  ( ( ( A C_ NN0 /\ N e. NN0 ) /\ N e. A ) -> 2 e. NN )
54 simplr 
 |-  ( ( ( A C_ NN0 /\ N e. NN0 ) /\ N e. A ) -> N e. NN0 )
55 53 54 nnexpcld 
 |-  ( ( ( A C_ NN0 /\ N e. NN0 ) /\ N e. A ) -> ( 2 ^ N ) e. NN )
56 55 nncnd 
 |-  ( ( ( A C_ NN0 /\ N e. NN0 ) /\ N e. A ) -> ( 2 ^ N ) e. CC )
57 oveq2 
 |-  ( k = N -> ( 2 ^ k ) = ( 2 ^ N ) )
58 57 sumsn 
 |-  ( ( N e. A /\ ( 2 ^ N ) e. CC ) -> sum_ k e. { N } ( 2 ^ k ) = ( 2 ^ N ) )
59 52 56 58 syl2anc 
 |-  ( ( ( A C_ NN0 /\ N e. NN0 ) /\ N e. A ) -> sum_ k e. { N } ( 2 ^ k ) = ( 2 ^ N ) )
60 51 59 eqtr2d 
 |-  ( ( ( A C_ NN0 /\ N e. NN0 ) /\ N e. A ) -> ( 2 ^ N ) = sum_ k e. ( A i^i { N } ) ( 2 ^ k ) )
61 simpr 
 |-  ( ( ( A C_ NN0 /\ N e. NN0 ) /\ -. N e. A ) -> -. N e. A )
62 disjsn 
 |-  ( ( A i^i { N } ) = (/) <-> -. N e. A )
63 61 62 sylibr 
 |-  ( ( ( A C_ NN0 /\ N e. NN0 ) /\ -. N e. A ) -> ( A i^i { N } ) = (/) )
64 63 sumeq1d 
 |-  ( ( ( A C_ NN0 /\ N e. NN0 ) /\ -. N e. A ) -> sum_ k e. ( A i^i { N } ) ( 2 ^ k ) = sum_ k e. (/) ( 2 ^ k ) )
65 sum0 
 |-  sum_ k e. (/) ( 2 ^ k ) = 0
66 64 65 eqtr2di 
 |-  ( ( ( A C_ NN0 /\ N e. NN0 ) /\ -. N e. A ) -> 0 = sum_ k e. ( A i^i { N } ) ( 2 ^ k ) )
67 60 66 ifeqda 
 |-  ( ( A C_ NN0 /\ N e. NN0 ) -> if ( N e. A , ( 2 ^ N ) , 0 ) = sum_ k e. ( A i^i { N } ) ( 2 ^ k ) )
68 46 67 oveq12d 
 |-  ( ( A C_ NN0 /\ N e. NN0 ) -> ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + if ( N e. A , ( 2 ^ N ) , 0 ) ) = ( sum_ k e. ( A i^i ( 0 ..^ N ) ) ( 2 ^ k ) + sum_ k e. ( A i^i { N } ) ( 2 ^ k ) ) )
69 31 35 68 3eqtr4d 
 |-  ( ( A C_ NN0 /\ N e. NN0 ) -> ( K ` ( A i^i ( 0 ..^ ( N + 1 ) ) ) ) = ( ( K ` ( A i^i ( 0 ..^ N ) ) ) + if ( N e. A , ( 2 ^ N ) , 0 ) ) )