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