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 ( 𝑁 ∈ ℤ → ( ℕ0 ∖ ( bits ‘ 𝑁 ) ) = ( bits ‘ ( - 𝑁 − 1 ) ) )

Proof

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