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 mulridd ⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ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 ..^ 𝑀 ) ) )