Metamath Proof Explorer


Theorem bitsmod

Description: Truncating the bit sequence after some M is equivalent to reducing the argument mod 2 ^ M . (Contributed by Mario Carneiro, 6-Sep-2016)

Ref Expression
Assertion bitsmod ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( bits ‘ ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) = ( ( bits ‘ 𝑁 ) ∩ ( 0 ..^ 𝑀 ) ) )

Proof

Step Hyp Ref Expression
1 simpl ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 𝑁 ∈ ℤ )
2 2nn 2 ∈ ℕ
3 2 a1i ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 2 ∈ ℕ )
4 simpr ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 𝑀 ∈ ℕ0 )
5 3 4 nnexpcld ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 2 ↑ 𝑀 ) ∈ ℕ )
6 1 5 zmodcld ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℕ0 )
7 6 nn0zd ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℤ )
8 7 biantrurd ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑥 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) ↔ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℤ ∧ ( 𝑥 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) ) ) )
9 1 ad2antrr ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 𝑁 ∈ ℤ )
10 simplr ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 𝑥 ∈ ℕ0 )
11 bitsval2 ( ( 𝑁 ∈ ℤ ∧ 𝑥 ∈ ℕ0 ) → ( 𝑥 ∈ ( bits ‘ 𝑁 ) ↔ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑥 ) ) ) ) )
12 9 10 11 syl2anc ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 𝑥 ∈ ( bits ‘ 𝑁 ) ↔ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑥 ) ) ) ) )
13 simpr ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 𝑥 < 𝑀 )
14 13 biantrud ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 𝑥 ∈ ( bits ‘ 𝑁 ) ↔ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ 𝑥 < 𝑀 ) ) )
15 2z 2 ∈ ℤ
16 15 a1i ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 2 ∈ ℤ )
17 9 zred ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 𝑁 ∈ ℝ )
18 2 a1i ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 2 ∈ ℕ )
19 18 10 nnexpcld ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑥 ) ∈ ℕ )
20 17 19 nndivred ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 𝑁 / ( 2 ↑ 𝑥 ) ) ∈ ℝ )
21 20 flcld ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑥 ) ) ) ∈ ℤ )
22 7 ad2antrr ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℤ )
23 22 zred ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℝ )
24 23 19 nndivred ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ∈ ℝ )
25 24 flcld ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ∈ ℤ )
26 19 nnzd ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑥 ) ∈ ℤ )
27 26 16 zmulcld ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( 2 ↑ 𝑥 ) · 2 ) ∈ ℤ )
28 5 ad2antrr ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑀 ) ∈ ℕ )
29 28 nnzd ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑀 ) ∈ ℤ )
30 9 22 zsubcld ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ∈ ℤ )
31 2cnd ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 2 ∈ ℂ )
32 31 10 expp1d ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 2 ↑ ( 𝑥 + 1 ) ) = ( ( 2 ↑ 𝑥 ) · 2 ) )
33 1nn0 1 ∈ ℕ0
34 33 a1i ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 1 ∈ ℕ0 )
35 10 34 nn0addcld ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 𝑥 + 1 ) ∈ ℕ0 )
36 35 nn0zd ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 𝑥 + 1 ) ∈ ℤ )
37 simplr ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → 𝑀 ∈ ℕ0 )
38 37 adantr ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 𝑀 ∈ ℕ0 )
39 38 nn0zd ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 𝑀 ∈ ℤ )
40 nn0ltp1le ( ( 𝑥 ∈ ℕ0𝑀 ∈ ℕ0 ) → ( 𝑥 < 𝑀 ↔ ( 𝑥 + 1 ) ≤ 𝑀 ) )
41 10 38 40 syl2anc ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 𝑥 < 𝑀 ↔ ( 𝑥 + 1 ) ≤ 𝑀 ) )
42 13 41 mpbid ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 𝑥 + 1 ) ≤ 𝑀 )
43 eluz2 ( 𝑀 ∈ ( ℤ ‘ ( 𝑥 + 1 ) ) ↔ ( ( 𝑥 + 1 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ ( 𝑥 + 1 ) ≤ 𝑀 ) )
44 36 39 42 43 syl3anbrc ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 𝑀 ∈ ( ℤ ‘ ( 𝑥 + 1 ) ) )
45 dvdsexp ( ( 2 ∈ ℤ ∧ ( 𝑥 + 1 ) ∈ ℕ0𝑀 ∈ ( ℤ ‘ ( 𝑥 + 1 ) ) ) → ( 2 ↑ ( 𝑥 + 1 ) ) ∥ ( 2 ↑ 𝑀 ) )
46 16 35 44 45 syl3anc ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 2 ↑ ( 𝑥 + 1 ) ) ∥ ( 2 ↑ 𝑀 ) )
47 32 46 eqbrtrrd ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( 2 ↑ 𝑥 ) · 2 ) ∥ ( 2 ↑ 𝑀 ) )
48 28 nnrpd ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑀 ) ∈ ℝ+ )
49 moddifz ( ( 𝑁 ∈ ℝ ∧ ( 2 ↑ 𝑀 ) ∈ ℝ+ ) → ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ∈ ℤ )
50 17 48 49 syl2anc ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ∈ ℤ )
51 2ne0 2 ≠ 0
52 51 a1i ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 2 ≠ 0 )
53 31 52 39 expne0d ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑀 ) ≠ 0 )
54 dvdsval2 ( ( ( 2 ↑ 𝑀 ) ∈ ℤ ∧ ( 2 ↑ 𝑀 ) ≠ 0 ∧ ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ∈ ℤ ) → ( ( 2 ↑ 𝑀 ) ∥ ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ↔ ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ∈ ℤ ) )
55 29 53 30 54 syl3anc ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( 2 ↑ 𝑀 ) ∥ ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ↔ ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ∈ ℤ ) )
56 50 55 mpbird ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑀 ) ∥ ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) )
57 27 29 30 47 56 dvdstrd ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( 2 ↑ 𝑥 ) · 2 ) ∥ ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) )
58 30 zcnd ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ∈ ℂ )
59 19 nncnd ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑥 ) ∈ ℂ )
60 10 nn0zd ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 𝑥 ∈ ℤ )
61 31 52 60 expne0d ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑥 ) ≠ 0 )
62 58 59 61 divcan2d ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( 2 ↑ 𝑥 ) · ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ) = ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) )
63 57 62 breqtrrd ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( 2 ↑ 𝑥 ) · 2 ) ∥ ( ( 2 ↑ 𝑥 ) · ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ) )
64 10 nn0red ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 𝑥 ∈ ℝ )
65 38 nn0red ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 𝑀 ∈ ℝ )
66 64 65 13 ltled ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 𝑥𝑀 )
67 eluz2 ( 𝑀 ∈ ( ℤ𝑥 ) ↔ ( 𝑥 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑥𝑀 ) )
68 60 39 66 67 syl3anbrc ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 𝑀 ∈ ( ℤ𝑥 ) )
69 dvdsexp ( ( 2 ∈ ℤ ∧ 𝑥 ∈ ℕ0𝑀 ∈ ( ℤ𝑥 ) ) → ( 2 ↑ 𝑥 ) ∥ ( 2 ↑ 𝑀 ) )
70 16 10 68 69 syl3anc ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑥 ) ∥ ( 2 ↑ 𝑀 ) )
71 26 29 30 70 56 dvdstrd ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑥 ) ∥ ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) )
72 dvdsval2 ( ( ( 2 ↑ 𝑥 ) ∈ ℤ ∧ ( 2 ↑ 𝑥 ) ≠ 0 ∧ ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ∈ ℤ ) → ( ( 2 ↑ 𝑥 ) ∥ ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ↔ ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ∈ ℤ ) )
73 26 61 30 72 syl3anc ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( 2 ↑ 𝑥 ) ∥ ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ↔ ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ∈ ℤ ) )
74 71 73 mpbid ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ∈ ℤ )
75 dvdscmulr ( ( 2 ∈ ℤ ∧ ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ∈ ℤ ∧ ( ( 2 ↑ 𝑥 ) ∈ ℤ ∧ ( 2 ↑ 𝑥 ) ≠ 0 ) ) → ( ( ( 2 ↑ 𝑥 ) · 2 ) ∥ ( ( 2 ↑ 𝑥 ) · ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ) ↔ 2 ∥ ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ) )
76 16 74 26 61 75 syl112anc ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( ( 2 ↑ 𝑥 ) · 2 ) ∥ ( ( 2 ↑ 𝑥 ) · ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ) ↔ 2 ∥ ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ) )
77 63 76 mpbid ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 2 ∥ ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) )
78 25 zcnd ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ∈ ℂ )
79 74 zcnd ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ∈ ℂ )
80 22 zcnd ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℂ )
81 9 zcnd ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 𝑁 ∈ ℂ )
82 80 81 pncan3d ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) + ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ) = 𝑁 )
83 82 oveq1d ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) + ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ) / ( 2 ↑ 𝑥 ) ) = ( 𝑁 / ( 2 ↑ 𝑥 ) ) )
84 80 58 59 61 divdird ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) + ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ) / ( 2 ↑ 𝑥 ) ) = ( ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) + ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ) )
85 83 84 eqtr3d ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 𝑁 / ( 2 ↑ 𝑥 ) ) = ( ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) + ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ) )
86 85 fveq2d ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑥 ) ) ) = ( ⌊ ‘ ( ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) + ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ) ) )
87 fladdz ( ( ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ∈ ℝ ∧ ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ∈ ℤ ) → ( ⌊ ‘ ( ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) + ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ) ) = ( ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) + ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ) )
88 24 74 87 syl2anc ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ⌊ ‘ ( ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) + ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ) ) = ( ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) + ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ) )
89 86 88 eqtrd ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑥 ) ) ) = ( ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) + ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ) )
90 78 79 89 mvrladdd ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑥 ) ) ) − ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) = ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) )
91 77 90 breqtrrd ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 2 ∥ ( ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑥 ) ) ) − ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) )
92 dvdssub2 ( ( ( 2 ∈ ℤ ∧ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑥 ) ) ) ∈ ℤ ∧ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ∈ ℤ ) ∧ 2 ∥ ( ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑥 ) ) ) − ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) ) → ( 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑥 ) ) ) ↔ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) )
93 16 21 25 91 92 syl31anc ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑥 ) ) ) ↔ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) )
94 93 notbid ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑥 ) ) ) ↔ ¬ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) )
95 12 14 94 3bitr3d ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ 𝑥 < 𝑀 ) ↔ ¬ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) )
96 z0even 2 ∥ 0
97 1 ad2antrr ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 𝑁 ∈ ℤ )
98 97 zred ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 𝑁 ∈ ℝ )
99 2rp 2 ∈ ℝ+
100 99 a1i ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 2 ∈ ℝ+ )
101 37 nn0zd ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → 𝑀 ∈ ℤ )
102 101 adantr ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 𝑀 ∈ ℤ )
103 100 102 rpexpcld ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑀 ) ∈ ℝ+ )
104 98 103 modcld ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℝ )
105 simplr ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 𝑥 ∈ ℕ0 )
106 105 nn0zd ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 𝑥 ∈ ℤ )
107 100 106 rpexpcld ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑥 ) ∈ ℝ+ )
108 6 ad2antrr ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℕ0 )
109 108 nn0ge0d ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 0 ≤ ( 𝑁 mod ( 2 ↑ 𝑀 ) ) )
110 104 107 109 divge0d ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 0 ≤ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) )
111 103 rpred ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑀 ) ∈ ℝ )
112 107 rpred ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑥 ) ∈ ℝ )
113 modlt ( ( 𝑁 ∈ ℝ ∧ ( 2 ↑ 𝑀 ) ∈ ℝ+ ) → ( 𝑁 mod ( 2 ↑ 𝑀 ) ) < ( 2 ↑ 𝑀 ) )
114 98 103 113 syl2anc ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( 𝑁 mod ( 2 ↑ 𝑀 ) ) < ( 2 ↑ 𝑀 ) )
115 100 rpred ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 2 ∈ ℝ )
116 1le2 1 ≤ 2
117 116 a1i ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 1 ≤ 2 )
118 102 zred ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 𝑀 ∈ ℝ )
119 105 nn0red ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 𝑥 ∈ ℝ )
120 simpr ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ¬ 𝑥 < 𝑀 )
121 118 119 120 nltled ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 𝑀𝑥 )
122 eluz2 ( 𝑥 ∈ ( ℤ𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑀𝑥 ) )
123 102 106 121 122 syl3anbrc ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 𝑥 ∈ ( ℤ𝑀 ) )
124 115 117 123 leexp2ad ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑀 ) ≤ ( 2 ↑ 𝑥 ) )
125 104 111 112 114 124 ltletrd ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( 𝑁 mod ( 2 ↑ 𝑀 ) ) < ( 2 ↑ 𝑥 ) )
126 107 rpcnd ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑥 ) ∈ ℂ )
127 126 mulid1d ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( ( 2 ↑ 𝑥 ) · 1 ) = ( 2 ↑ 𝑥 ) )
128 125 127 breqtrrd ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( 𝑁 mod ( 2 ↑ 𝑀 ) ) < ( ( 2 ↑ 𝑥 ) · 1 ) )
129 1red ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 1 ∈ ℝ )
130 104 129 107 ltdivmuld ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) < 1 ↔ ( 𝑁 mod ( 2 ↑ 𝑀 ) ) < ( ( 2 ↑ 𝑥 ) · 1 ) ) )
131 128 130 mpbird ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) < 1 )
132 1e0p1 1 = ( 0 + 1 )
133 131 132 breqtrdi ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) < ( 0 + 1 ) )
134 104 107 rerpdivcld ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ∈ ℝ )
135 0z 0 ∈ ℤ
136 flbi ( ( ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ∈ ℝ ∧ 0 ∈ ℤ ) → ( ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) = 0 ↔ ( 0 ≤ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ∧ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) < ( 0 + 1 ) ) ) )
137 134 135 136 sylancl ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) = 0 ↔ ( 0 ≤ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ∧ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) < ( 0 + 1 ) ) ) )
138 110 133 137 mpbir2and ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) = 0 )
139 96 138 breqtrrid ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) )
140 120 intnand ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ¬ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ 𝑥 < 𝑀 ) )
141 139 140 2thd ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ↔ ¬ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ 𝑥 < 𝑀 ) ) )
142 141 con2bid ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ 𝑥 < 𝑀 ) ↔ ¬ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) )
143 95 142 pm2.61dan ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ 𝑥 < 𝑀 ) ↔ ¬ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) )
144 101 biantrurd ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ 𝑥 < 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ 𝑥 < 𝑀 ) ) ) )
145 143 144 bitr3d ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ¬ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ↔ ( 𝑀 ∈ ℤ ∧ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ 𝑥 < 𝑀 ) ) ) )
146 an12 ( ( 𝑀 ∈ ℤ ∧ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ 𝑥 < 𝑀 ) ) ↔ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀 ) ) )
147 145 146 bitrdi ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ¬ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ↔ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀 ) ) ) )
148 147 pm5.32da ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑥 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) ↔ ( 𝑥 ∈ ℕ0 ∧ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀 ) ) ) ) )
149 8 148 bitr3d ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℤ ∧ ( 𝑥 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) ) ↔ ( 𝑥 ∈ ℕ0 ∧ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀 ) ) ) ) )
150 3anass ( ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℤ ∧ 𝑥 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) ↔ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℤ ∧ ( 𝑥 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) ) )
151 elfzo2 ( 𝑥 ∈ ( 0 ..^ 𝑀 ) ↔ ( 𝑥 ∈ ( ℤ ‘ 0 ) ∧ 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀 ) )
152 elnn0uz ( 𝑥 ∈ ℕ0𝑥 ∈ ( ℤ ‘ 0 ) )
153 152 3anbi1i ( ( 𝑥 ∈ ℕ0𝑀 ∈ ℤ ∧ 𝑥 < 𝑀 ) ↔ ( 𝑥 ∈ ( ℤ ‘ 0 ) ∧ 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀 ) )
154 3anass ( ( 𝑥 ∈ ℕ0𝑀 ∈ ℤ ∧ 𝑥 < 𝑀 ) ↔ ( 𝑥 ∈ ℕ0 ∧ ( 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀 ) ) )
155 151 153 154 3bitr2i ( 𝑥 ∈ ( 0 ..^ 𝑀 ) ↔ ( 𝑥 ∈ ℕ0 ∧ ( 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀 ) ) )
156 155 anbi2i ( ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ 𝑥 ∈ ( 0 ..^ 𝑀 ) ) ↔ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ ( 𝑥 ∈ ℕ0 ∧ ( 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀 ) ) ) )
157 an12 ( ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ ( 𝑥 ∈ ℕ0 ∧ ( 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀 ) ) ) ↔ ( 𝑥 ∈ ℕ0 ∧ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀 ) ) ) )
158 156 157 bitri ( ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ 𝑥 ∈ ( 0 ..^ 𝑀 ) ) ↔ ( 𝑥 ∈ ℕ0 ∧ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀 ) ) ) )
159 149 150 158 3bitr4g ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℤ ∧ 𝑥 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) ↔ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ 𝑥 ∈ ( 0 ..^ 𝑀 ) ) ) )
160 bitsval ( 𝑥 ∈ ( bits ‘ ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ↔ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℤ ∧ 𝑥 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) )
161 elin ( 𝑥 ∈ ( ( bits ‘ 𝑁 ) ∩ ( 0 ..^ 𝑀 ) ) ↔ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ 𝑥 ∈ ( 0 ..^ 𝑀 ) ) )
162 159 160 161 3bitr4g ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑥 ∈ ( bits ‘ ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ↔ 𝑥 ∈ ( ( bits ‘ 𝑁 ) ∩ ( 0 ..^ 𝑀 ) ) ) )
163 162 eqrdv ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( bits ‘ ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) = ( ( bits ‘ 𝑁 ) ∩ ( 0 ..^ 𝑀 ) ) )