Metamath Proof Explorer

Theorem bitscmp

Description: The bit complement of N is -u N - 1 . (Thus, by bitsfi , all negative numbers have cofinite bits representations.) (Contributed by Mario Carneiro, 5-Sep-2016)

Ref Expression
Assertion bitscmp 
|- ( N e. ZZ -> ( NN0 \ ( bits ` N ) ) = ( bits ` ( -u N - 1 ) ) )

Proof

Step Hyp Ref Expression
1 bitsval2 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( m e. ( bits ` N ) <-> -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) )
2 2z 
 |-  2 e. ZZ
3 2 a1i 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> 2 e. ZZ )
4 simpl 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> N e. ZZ )
5 4 zred 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> N e. RR )
6 2nn 
 |-  2 e. NN
7 6 a1i 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> 2 e. NN )
8 simpr 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> m e. NN0 )
9 7 8 nnexpcld 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( 2 ^ m ) e. NN )
10 5 9 nndivred 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( N / ( 2 ^ m ) ) e. RR )
11 10 flcld 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( |_ ` ( N / ( 2 ^ m ) ) ) e. ZZ )
12 dvdsnegb 
 |-  ( ( 2 e. ZZ /\ ( |_ ` ( N / ( 2 ^ m ) ) ) e. ZZ ) -> ( 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) <-> 2 || -u ( |_ ` ( N / ( 2 ^ m ) ) ) ) )
13 3 11 12 syl2anc 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) <-> 2 || -u ( |_ ` ( N / ( 2 ^ m ) ) ) ) )
14 13 notbid 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) <-> -. 2 || -u ( |_ ` ( N / ( 2 ^ m ) ) ) ) )
15 11 znegcld 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> -u ( |_ ` ( N / ( 2 ^ m ) ) ) e. ZZ )
16 oddm1even 
 |-  ( -u ( |_ ` ( N / ( 2 ^ m ) ) ) e. ZZ -> ( -. 2 || -u ( |_ ` ( N / ( 2 ^ m ) ) ) <-> 2 || ( -u ( |_ ` ( N / ( 2 ^ m ) ) ) - 1 ) ) )
17 15 16 syl 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( -. 2 || -u ( |_ ` ( N / ( 2 ^ m ) ) ) <-> 2 || ( -u ( |_ ` ( N / ( 2 ^ m ) ) ) - 1 ) ) )
18 flltp1 
 |-  ( ( N / ( 2 ^ m ) ) e. RR -> ( N / ( 2 ^ m ) ) < ( ( |_ ` ( N / ( 2 ^ m ) ) ) + 1 ) )
19 10 18 syl 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( N / ( 2 ^ m ) ) < ( ( |_ ` ( N / ( 2 ^ m ) ) ) + 1 ) )
20 11 zred 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( |_ ` ( N / ( 2 ^ m ) ) ) e. RR )
21 1red 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> 1 e. RR )
22 20 21 readdcld 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( ( |_ ` ( N / ( 2 ^ m ) ) ) + 1 ) e. RR )
23 10 22 ltnegd 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( ( N / ( 2 ^ m ) ) < ( ( |_ ` ( N / ( 2 ^ m ) ) ) + 1 ) <-> -u ( ( |_ ` ( N / ( 2 ^ m ) ) ) + 1 ) < -u ( N / ( 2 ^ m ) ) ) )
24 19 23 mpbid 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> -u ( ( |_ ` ( N / ( 2 ^ m ) ) ) + 1 ) < -u ( N / ( 2 ^ m ) ) )
25 20 recnd 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( |_ ` ( N / ( 2 ^ m ) ) ) e. CC )
26 21 recnd 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> 1 e. CC )
27 25 26 negdi2d 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> -u ( ( |_ ` ( N / ( 2 ^ m ) ) ) + 1 ) = ( -u ( |_ ` ( N / ( 2 ^ m ) ) ) - 1 ) )
28 5 recnd 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> N e. CC )
29 9 nncnd 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( 2 ^ m ) e. CC )
30 9 nnne0d 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( 2 ^ m ) =/= 0 )
31 28 29 30 divnegd 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> -u ( N / ( 2 ^ m ) ) = ( -u N / ( 2 ^ m ) ) )
32 24 27 31 3brtr3d 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( -u ( |_ ` ( N / ( 2 ^ m ) ) ) - 1 ) < ( -u N / ( 2 ^ m ) ) )
33 1zzd 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> 1 e. ZZ )
34 15 33 zsubcld 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( -u ( |_ ` ( N / ( 2 ^ m ) ) ) - 1 ) e. ZZ )
35 34 zred 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( -u ( |_ ` ( N / ( 2 ^ m ) ) ) - 1 ) e. RR )
36 5 renegcld 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> -u N e. RR )
37 9 nnrpd 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( 2 ^ m ) e. RR+ )
38 35 36 37 ltmuldivd 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( ( ( -u ( |_ ` ( N / ( 2 ^ m ) ) ) - 1 ) x. ( 2 ^ m ) ) < -u N <-> ( -u ( |_ ` ( N / ( 2 ^ m ) ) ) - 1 ) < ( -u N / ( 2 ^ m ) ) ) )
39 32 38 mpbird 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( ( -u ( |_ ` ( N / ( 2 ^ m ) ) ) - 1 ) x. ( 2 ^ m ) ) < -u N )
40 9 nnzd 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( 2 ^ m ) e. ZZ )
41 34 40 zmulcld 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( ( -u ( |_ ` ( N / ( 2 ^ m ) ) ) - 1 ) x. ( 2 ^ m ) ) e. ZZ )
42 4 znegcld 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> -u N e. ZZ )
43 zltlem1 
 |-  ( ( ( ( -u ( |_ ` ( N / ( 2 ^ m ) ) ) - 1 ) x. ( 2 ^ m ) ) e. ZZ /\ -u N e. ZZ ) -> ( ( ( -u ( |_ ` ( N / ( 2 ^ m ) ) ) - 1 ) x. ( 2 ^ m ) ) < -u N <-> ( ( -u ( |_ ` ( N / ( 2 ^ m ) ) ) - 1 ) x. ( 2 ^ m ) ) <_ ( -u N - 1 ) ) )
44 41 42 43 syl2anc 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( ( ( -u ( |_ ` ( N / ( 2 ^ m ) ) ) - 1 ) x. ( 2 ^ m ) ) < -u N <-> ( ( -u ( |_ ` ( N / ( 2 ^ m ) ) ) - 1 ) x. ( 2 ^ m ) ) <_ ( -u N - 1 ) ) )
45 39 44 mpbid 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( ( -u ( |_ ` ( N / ( 2 ^ m ) ) ) - 1 ) x. ( 2 ^ m ) ) <_ ( -u N - 1 ) )
46 36 21 resubcld 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( -u N - 1 ) e. RR )
47 35 46 37 lemuldivd 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( ( ( -u ( |_ ` ( N / ( 2 ^ m ) ) ) - 1 ) x. ( 2 ^ m ) ) <_ ( -u N - 1 ) <-> ( -u ( |_ ` ( N / ( 2 ^ m ) ) ) - 1 ) <_ ( ( -u N - 1 ) / ( 2 ^ m ) ) ) )
48 45 47 mpbid 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( -u ( |_ ` ( N / ( 2 ^ m ) ) ) - 1 ) <_ ( ( -u N - 1 ) / ( 2 ^ m ) ) )
49 flle 
 |-  ( ( N / ( 2 ^ m ) ) e. RR -> ( |_ ` ( N / ( 2 ^ m ) ) ) <_ ( N / ( 2 ^ m ) ) )
50 10 49 syl 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( |_ ` ( N / ( 2 ^ m ) ) ) <_ ( N / ( 2 ^ m ) ) )
51 20 10 lenegd 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( ( |_ ` ( N / ( 2 ^ m ) ) ) <_ ( N / ( 2 ^ m ) ) <-> -u ( N / ( 2 ^ m ) ) <_ -u ( |_ ` ( N / ( 2 ^ m ) ) ) ) )
52 50 51 mpbid 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> -u ( N / ( 2 ^ m ) ) <_ -u ( |_ ` ( N / ( 2 ^ m ) ) ) )
53 31 52 eqbrtrrd 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( -u N / ( 2 ^ m ) ) <_ -u ( |_ ` ( N / ( 2 ^ m ) ) ) )
54 20 renegcld 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> -u ( |_ ` ( N / ( 2 ^ m ) ) ) e. RR )
55 36 54 37 ledivmuld 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( ( -u N / ( 2 ^ m ) ) <_ -u ( |_ ` ( N / ( 2 ^ m ) ) ) <-> -u N <_ ( ( 2 ^ m ) x. -u ( |_ ` ( N / ( 2 ^ m ) ) ) ) ) )
56 53 55 mpbid 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> -u N <_ ( ( 2 ^ m ) x. -u ( |_ ` ( N / ( 2 ^ m ) ) ) ) )
57 40 15 zmulcld 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( ( 2 ^ m ) x. -u ( |_ ` ( N / ( 2 ^ m ) ) ) ) e. ZZ )
58 zlem1lt 
 |-  ( ( -u N e. ZZ /\ ( ( 2 ^ m ) x. -u ( |_ ` ( N / ( 2 ^ m ) ) ) ) e. ZZ ) -> ( -u N <_ ( ( 2 ^ m ) x. -u ( |_ ` ( N / ( 2 ^ m ) ) ) ) <-> ( -u N - 1 ) < ( ( 2 ^ m ) x. -u ( |_ ` ( N / ( 2 ^ m ) ) ) ) ) )
59 42 57 58 syl2anc 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( -u N <_ ( ( 2 ^ m ) x. -u ( |_ ` ( N / ( 2 ^ m ) ) ) ) <-> ( -u N - 1 ) < ( ( 2 ^ m ) x. -u ( |_ ` ( N / ( 2 ^ m ) ) ) ) ) )
60 56 59 mpbid 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( -u N - 1 ) < ( ( 2 ^ m ) x. -u ( |_ ` ( N / ( 2 ^ m ) ) ) ) )
61 46 54 37 ltdivmuld 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( ( ( -u N - 1 ) / ( 2 ^ m ) ) < -u ( |_ ` ( N / ( 2 ^ m ) ) ) <-> ( -u N - 1 ) < ( ( 2 ^ m ) x. -u ( |_ ` ( N / ( 2 ^ m ) ) ) ) ) )
62 60 61 mpbird 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( ( -u N - 1 ) / ( 2 ^ m ) ) < -u ( |_ ` ( N / ( 2 ^ m ) ) ) )
63 25 negcld 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> -u ( |_ ` ( N / ( 2 ^ m ) ) ) e. CC )
64 63 26 npcand 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( ( -u ( |_ ` ( N / ( 2 ^ m ) ) ) - 1 ) + 1 ) = -u ( |_ ` ( N / ( 2 ^ m ) ) ) )
65 62 64 breqtrrd 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( ( -u N - 1 ) / ( 2 ^ m ) ) < ( ( -u ( |_ ` ( N / ( 2 ^ m ) ) ) - 1 ) + 1 ) )
66 46 9 nndivred 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( ( -u N - 1 ) / ( 2 ^ m ) ) e. RR )
67 flbi 
 |-  ( ( ( ( -u N - 1 ) / ( 2 ^ m ) ) e. RR /\ ( -u ( |_ ` ( N / ( 2 ^ m ) ) ) - 1 ) e. ZZ ) -> ( ( |_ ` ( ( -u N - 1 ) / ( 2 ^ m ) ) ) = ( -u ( |_ ` ( N / ( 2 ^ m ) ) ) - 1 ) <-> ( ( -u ( |_ ` ( N / ( 2 ^ m ) ) ) - 1 ) <_ ( ( -u N - 1 ) / ( 2 ^ m ) ) /\ ( ( -u N - 1 ) / ( 2 ^ m ) ) < ( ( -u ( |_ ` ( N / ( 2 ^ m ) ) ) - 1 ) + 1 ) ) ) )
68 66 34 67 syl2anc 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( ( |_ ` ( ( -u N - 1 ) / ( 2 ^ m ) ) ) = ( -u ( |_ ` ( N / ( 2 ^ m ) ) ) - 1 ) <-> ( ( -u ( |_ ` ( N / ( 2 ^ m ) ) ) - 1 ) <_ ( ( -u N - 1 ) / ( 2 ^ m ) ) /\ ( ( -u N - 1 ) / ( 2 ^ m ) ) < ( ( -u ( |_ ` ( N / ( 2 ^ m ) ) ) - 1 ) + 1 ) ) ) )
69 48 65 68 mpbir2and 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( |_ ` ( ( -u N - 1 ) / ( 2 ^ m ) ) ) = ( -u ( |_ ` ( N / ( 2 ^ m ) ) ) - 1 ) )
70 69 breq2d 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( 2 || ( |_ ` ( ( -u N - 1 ) / ( 2 ^ m ) ) ) <-> 2 || ( -u ( |_ ` ( N / ( 2 ^ m ) ) ) - 1 ) ) )
71 17 70 bitr4d 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( -. 2 || -u ( |_ ` ( N / ( 2 ^ m ) ) ) <-> 2 || ( |_ ` ( ( -u N - 1 ) / ( 2 ^ m ) ) ) ) )
72 1 14 71 3bitrd 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( m e. ( bits ` N ) <-> 2 || ( |_ ` ( ( -u N - 1 ) / ( 2 ^ m ) ) ) ) )
73 72 notbid 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( -. m e. ( bits ` N ) <-> -. 2 || ( |_ ` ( ( -u N - 1 ) / ( 2 ^ m ) ) ) ) )
74 73 pm5.32da 
 |-  ( N e. ZZ -> ( ( m e. NN0 /\ -. m e. ( bits ` N ) ) <-> ( m e. NN0 /\ -. 2 || ( |_ ` ( ( -u N - 1 ) / ( 2 ^ m ) ) ) ) ) )
75 znegcl 
 |-  ( N e. ZZ -> -u N e. ZZ )
76 1zzd 
 |-  ( N e. ZZ -> 1 e. ZZ )
77 75 76 zsubcld 
 |-  ( N e. ZZ -> ( -u N - 1 ) e. ZZ )
78 77 biantrurd 
 |-  ( N e. ZZ -> ( ( m e. NN0 /\ -. 2 || ( |_ ` ( ( -u N - 1 ) / ( 2 ^ m ) ) ) ) <-> ( ( -u N - 1 ) e. ZZ /\ ( m e. NN0 /\ -. 2 || ( |_ ` ( ( -u N - 1 ) / ( 2 ^ m ) ) ) ) ) ) )
79 74 78 bitrd 
 |-  ( N e. ZZ -> ( ( m e. NN0 /\ -. m e. ( bits ` N ) ) <-> ( ( -u N - 1 ) e. ZZ /\ ( m e. NN0 /\ -. 2 || ( |_ ` ( ( -u N - 1 ) / ( 2 ^ m ) ) ) ) ) ) )
80 eldif 
 |-  ( m e. ( NN0 \ ( bits ` N ) ) <-> ( m e. NN0 /\ -. m e. ( bits ` N ) ) )
81 bitsval 
 |-  ( m e. ( bits ` ( -u N - 1 ) ) <-> ( ( -u N - 1 ) e. ZZ /\ m e. NN0 /\ -. 2 || ( |_ ` ( ( -u N - 1 ) / ( 2 ^ m ) ) ) ) )
82 3anass 
 |-  ( ( ( -u N - 1 ) e. ZZ /\ m e. NN0 /\ -. 2 || ( |_ ` ( ( -u N - 1 ) / ( 2 ^ m ) ) ) ) <-> ( ( -u N - 1 ) e. ZZ /\ ( m e. NN0 /\ -. 2 || ( |_ ` ( ( -u N - 1 ) / ( 2 ^ m ) ) ) ) ) )
83 81 82 bitri 
 |-  ( m e. ( bits ` ( -u N - 1 ) ) <-> ( ( -u N - 1 ) e. ZZ /\ ( m e. NN0 /\ -. 2 || ( |_ ` ( ( -u N - 1 ) / ( 2 ^ m ) ) ) ) ) )
84 79 80 83 3bitr4g 
 |-  ( N e. ZZ -> ( m e. ( NN0 \ ( bits ` N ) ) <-> m e. ( bits ` ( -u N - 1 ) ) ) )
85 84 eqrdv 
 |-  ( N e. ZZ -> ( NN0 \ ( bits ` N ) ) = ( bits ` ( -u N - 1 ) ) )