MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bitsmod Structured version   Visualization version   GIF version

Theorem bitsmod 15440
Description: Truncating the bit sequence after some 𝑀 is equivalent to reducing the argument mod 2↑𝑀. (Contributed by Mario Carneiro, 6-Sep-2016.)
Assertion
Ref Expression
bitsmod ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (bits‘(𝑁 mod (2↑𝑀))) = ((bits‘𝑁) ∩ (0..^𝑀)))

Proof of Theorem bitsmod
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 simpl 474 . . . . . . . 8 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 𝑁 ∈ ℤ)
2 2nn 11344 . . . . . . . . . 10 2 ∈ ℕ
32a1i 11 . . . . . . . . 9 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 2 ∈ ℕ)
4 simpr 477 . . . . . . . . 9 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 𝑀 ∈ ℕ0)
53, 4nnexpcld 13236 . . . . . . . 8 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2↑𝑀) ∈ ℕ)
61, 5zmodcld 12898 . . . . . . 7 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑁 mod (2↑𝑀)) ∈ ℕ0)
76nn0zd 11726 . . . . . 6 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑁 mod (2↑𝑀)) ∈ ℤ)
87biantrurd 528 . . . . 5 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝑥 ∈ ℕ0 ∧ ¬ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))) ↔ ((𝑁 mod (2↑𝑀)) ∈ ℤ ∧ (𝑥 ∈ ℕ0 ∧ ¬ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))))))
91ad2antrr 717 . . . . . . . . . . 11 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → 𝑁 ∈ ℤ)
10 simplr 785 . . . . . . . . . . 11 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → 𝑥 ∈ ℕ0)
11 bitsval2 15429 . . . . . . . . . . 11 ((𝑁 ∈ ℤ ∧ 𝑥 ∈ ℕ0) → (𝑥 ∈ (bits‘𝑁) ↔ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑥)))))
129, 10, 11syl2anc 579 . . . . . . . . . 10 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (𝑥 ∈ (bits‘𝑁) ↔ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑥)))))
13 simpr 477 . . . . . . . . . . 11 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → 𝑥 < 𝑀)
1413biantrud 527 . . . . . . . . . 10 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (𝑥 ∈ (bits‘𝑁) ↔ (𝑥 ∈ (bits‘𝑁) ∧ 𝑥 < 𝑀)))
15 2z 11655 . . . . . . . . . . . . 13 2 ∈ ℤ
1615a1i 11 . . . . . . . . . . . 12 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → 2 ∈ ℤ)
179zred 11728 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → 𝑁 ∈ ℝ)
182a1i 11 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → 2 ∈ ℕ)
1918, 10nnexpcld 13236 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (2↑𝑥) ∈ ℕ)
2017, 19nndivred 11325 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (𝑁 / (2↑𝑥)) ∈ ℝ)
2120flcld 12806 . . . . . . . . . . . 12 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (⌊‘(𝑁 / (2↑𝑥))) ∈ ℤ)
227ad2antrr 717 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (𝑁 mod (2↑𝑀)) ∈ ℤ)
2322zred 11728 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (𝑁 mod (2↑𝑀)) ∈ ℝ)
2423, 19nndivred 11325 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → ((𝑁 mod (2↑𝑀)) / (2↑𝑥)) ∈ ℝ)
2524flcld 12806 . . . . . . . . . . . 12 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) ∈ ℤ)
26 2cnd 11349 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → 2 ∈ ℂ)
2726, 10expp1d 13215 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (2↑(𝑥 + 1)) = ((2↑𝑥) · 2))
28 1nn0 11555 . . . . . . . . . . . . . . . . . . . 20 1 ∈ ℕ0
2928a1i 11 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → 1 ∈ ℕ0)
3010, 29nn0addcld 11601 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (𝑥 + 1) ∈ ℕ0)
3130nn0zd 11726 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (𝑥 + 1) ∈ ℤ)
32 simplr 785 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) → 𝑀 ∈ ℕ0)
3332adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → 𝑀 ∈ ℕ0)
3433nn0zd 11726 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → 𝑀 ∈ ℤ)
35 nn0ltp1le 11681 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ ℕ0𝑀 ∈ ℕ0) → (𝑥 < 𝑀 ↔ (𝑥 + 1) ≤ 𝑀))
3610, 33, 35syl2anc 579 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (𝑥 < 𝑀 ↔ (𝑥 + 1) ≤ 𝑀))
3713, 36mpbid 223 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (𝑥 + 1) ≤ 𝑀)
38 eluz2 11891 . . . . . . . . . . . . . . . . . . 19 (𝑀 ∈ (ℤ‘(𝑥 + 1)) ↔ ((𝑥 + 1) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑥 + 1) ≤ 𝑀))
3931, 34, 37, 38syl3anbrc 1443 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → 𝑀 ∈ (ℤ‘(𝑥 + 1)))
40 dvdsexp 15335 . . . . . . . . . . . . . . . . . 18 ((2 ∈ ℤ ∧ (𝑥 + 1) ∈ ℕ0𝑀 ∈ (ℤ‘(𝑥 + 1))) → (2↑(𝑥 + 1)) ∥ (2↑𝑀))
4116, 30, 39, 40syl3anc 1490 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (2↑(𝑥 + 1)) ∥ (2↑𝑀))
4227, 41eqbrtrrd 4832 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → ((2↑𝑥) · 2) ∥ (2↑𝑀))
435ad2antrr 717 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (2↑𝑀) ∈ ℕ)
4443nnrpd 12067 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (2↑𝑀) ∈ ℝ+)
45 moddifz 12889 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℝ ∧ (2↑𝑀) ∈ ℝ+) → ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ∈ ℤ)
4617, 44, 45syl2anc 579 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ∈ ℤ)
4743nnzd 11727 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (2↑𝑀) ∈ ℤ)
48 2ne0 11382 . . . . . . . . . . . . . . . . . . . 20 2 ≠ 0
4948a1i 11 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → 2 ≠ 0)
5026, 49, 34expne0d 13220 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (2↑𝑀) ≠ 0)
519, 22zsubcld 11733 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (𝑁 − (𝑁 mod (2↑𝑀))) ∈ ℤ)
52 dvdsval2 15269 . . . . . . . . . . . . . . . . . 18 (((2↑𝑀) ∈ ℤ ∧ (2↑𝑀) ≠ 0 ∧ (𝑁 − (𝑁 mod (2↑𝑀))) ∈ ℤ) → ((2↑𝑀) ∥ (𝑁 − (𝑁 mod (2↑𝑀))) ↔ ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ∈ ℤ))
5347, 50, 51, 52syl3anc 1490 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → ((2↑𝑀) ∥ (𝑁 − (𝑁 mod (2↑𝑀))) ↔ ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ∈ ℤ))
5446, 53mpbird 248 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (2↑𝑀) ∥ (𝑁 − (𝑁 mod (2↑𝑀))))
5519nnzd 11727 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (2↑𝑥) ∈ ℤ)
5655, 16zmulcld 11734 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → ((2↑𝑥) · 2) ∈ ℤ)
57 dvdstr 15304 . . . . . . . . . . . . . . . . 17 ((((2↑𝑥) · 2) ∈ ℤ ∧ (2↑𝑀) ∈ ℤ ∧ (𝑁 − (𝑁 mod (2↑𝑀))) ∈ ℤ) → ((((2↑𝑥) · 2) ∥ (2↑𝑀) ∧ (2↑𝑀) ∥ (𝑁 − (𝑁 mod (2↑𝑀)))) → ((2↑𝑥) · 2) ∥ (𝑁 − (𝑁 mod (2↑𝑀)))))
5856, 47, 51, 57syl3anc 1490 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → ((((2↑𝑥) · 2) ∥ (2↑𝑀) ∧ (2↑𝑀) ∥ (𝑁 − (𝑁 mod (2↑𝑀)))) → ((2↑𝑥) · 2) ∥ (𝑁 − (𝑁 mod (2↑𝑀)))))
5942, 54, 58mp2and 690 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → ((2↑𝑥) · 2) ∥ (𝑁 − (𝑁 mod (2↑𝑀))))
6051zcnd 11729 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (𝑁 − (𝑁 mod (2↑𝑀))) ∈ ℂ)
6119nncnd 11291 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (2↑𝑥) ∈ ℂ)
6210nn0zd 11726 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → 𝑥 ∈ ℤ)
6326, 49, 62expne0d 13220 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (2↑𝑥) ≠ 0)
6460, 61, 63divcan2d 11056 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → ((2↑𝑥) · ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥))) = (𝑁 − (𝑁 mod (2↑𝑀))))
6559, 64breqtrrd 4836 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → ((2↑𝑥) · 2) ∥ ((2↑𝑥) · ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥))))
6610nn0red 11598 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → 𝑥 ∈ ℝ)
6733nn0red 11598 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → 𝑀 ∈ ℝ)
6866, 67, 13ltled 10438 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → 𝑥𝑀)
69 eluz2 11891 . . . . . . . . . . . . . . . . . . 19 (𝑀 ∈ (ℤ𝑥) ↔ (𝑥 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑥𝑀))
7062, 34, 68, 69syl3anbrc 1443 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → 𝑀 ∈ (ℤ𝑥))
71 dvdsexp 15335 . . . . . . . . . . . . . . . . . 18 ((2 ∈ ℤ ∧ 𝑥 ∈ ℕ0𝑀 ∈ (ℤ𝑥)) → (2↑𝑥) ∥ (2↑𝑀))
7216, 10, 70, 71syl3anc 1490 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (2↑𝑥) ∥ (2↑𝑀))
73 dvdstr 15304 . . . . . . . . . . . . . . . . . 18 (((2↑𝑥) ∈ ℤ ∧ (2↑𝑀) ∈ ℤ ∧ (𝑁 − (𝑁 mod (2↑𝑀))) ∈ ℤ) → (((2↑𝑥) ∥ (2↑𝑀) ∧ (2↑𝑀) ∥ (𝑁 − (𝑁 mod (2↑𝑀)))) → (2↑𝑥) ∥ (𝑁 − (𝑁 mod (2↑𝑀)))))
7455, 47, 51, 73syl3anc 1490 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (((2↑𝑥) ∥ (2↑𝑀) ∧ (2↑𝑀) ∥ (𝑁 − (𝑁 mod (2↑𝑀)))) → (2↑𝑥) ∥ (𝑁 − (𝑁 mod (2↑𝑀)))))
7572, 54, 74mp2and 690 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (2↑𝑥) ∥ (𝑁 − (𝑁 mod (2↑𝑀))))
76 dvdsval2 15269 . . . . . . . . . . . . . . . . 17 (((2↑𝑥) ∈ ℤ ∧ (2↑𝑥) ≠ 0 ∧ (𝑁 − (𝑁 mod (2↑𝑀))) ∈ ℤ) → ((2↑𝑥) ∥ (𝑁 − (𝑁 mod (2↑𝑀))) ↔ ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)) ∈ ℤ))
7755, 63, 51, 76syl3anc 1490 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → ((2↑𝑥) ∥ (𝑁 − (𝑁 mod (2↑𝑀))) ↔ ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)) ∈ ℤ))
7875, 77mpbid 223 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)) ∈ ℤ)
79 dvdscmulr 15296 . . . . . . . . . . . . . . 15 ((2 ∈ ℤ ∧ ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)) ∈ ℤ ∧ ((2↑𝑥) ∈ ℤ ∧ (2↑𝑥) ≠ 0)) → (((2↑𝑥) · 2) ∥ ((2↑𝑥) · ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥))) ↔ 2 ∥ ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥))))
8016, 78, 55, 63, 79syl112anc 1493 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (((2↑𝑥) · 2) ∥ ((2↑𝑥) · ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥))) ↔ 2 ∥ ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥))))
8165, 80mpbid 223 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → 2 ∥ ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)))
8222zcnd 11729 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (𝑁 mod (2↑𝑀)) ∈ ℂ)
839zcnd 11729 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → 𝑁 ∈ ℂ)
8482, 83pncan3d 10648 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → ((𝑁 mod (2↑𝑀)) + (𝑁 − (𝑁 mod (2↑𝑀)))) = 𝑁)
8584oveq1d 6856 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (((𝑁 mod (2↑𝑀)) + (𝑁 − (𝑁 mod (2↑𝑀)))) / (2↑𝑥)) = (𝑁 / (2↑𝑥)))
8682, 60, 61, 63divdird 11092 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (((𝑁 mod (2↑𝑀)) + (𝑁 − (𝑁 mod (2↑𝑀)))) / (2↑𝑥)) = (((𝑁 mod (2↑𝑀)) / (2↑𝑥)) + ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥))))
8785, 86eqtr3d 2800 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (𝑁 / (2↑𝑥)) = (((𝑁 mod (2↑𝑀)) / (2↑𝑥)) + ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥))))
8887fveq2d 6378 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (⌊‘(𝑁 / (2↑𝑥))) = (⌊‘(((𝑁 mod (2↑𝑀)) / (2↑𝑥)) + ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)))))
89 fladdz 12833 . . . . . . . . . . . . . . . . 17 ((((𝑁 mod (2↑𝑀)) / (2↑𝑥)) ∈ ℝ ∧ ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)) ∈ ℤ) → (⌊‘(((𝑁 mod (2↑𝑀)) / (2↑𝑥)) + ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)))) = ((⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) + ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥))))
9024, 78, 89syl2anc 579 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (⌊‘(((𝑁 mod (2↑𝑀)) / (2↑𝑥)) + ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)))) = ((⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) + ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥))))
9188, 90eqtrd 2798 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (⌊‘(𝑁 / (2↑𝑥))) = ((⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) + ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥))))
9291oveq1d 6856 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → ((⌊‘(𝑁 / (2↑𝑥))) − (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))) = (((⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) + ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥))) − (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))))
9325zcnd 11729 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) ∈ ℂ)
9478zcnd 11729 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)) ∈ ℂ)
9593, 94pncan2d 10647 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (((⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) + ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥))) − (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))) = ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)))
9692, 95eqtrd 2798 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → ((⌊‘(𝑁 / (2↑𝑥))) − (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))) = ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)))
9781, 96breqtrrd 4836 . . . . . . . . . . . 12 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → 2 ∥ ((⌊‘(𝑁 / (2↑𝑥))) − (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))))
98 dvdssub2 15309 . . . . . . . . . . . 12 (((2 ∈ ℤ ∧ (⌊‘(𝑁 / (2↑𝑥))) ∈ ℤ ∧ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) ∈ ℤ) ∧ 2 ∥ ((⌊‘(𝑁 / (2↑𝑥))) − (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))))) → (2 ∥ (⌊‘(𝑁 / (2↑𝑥))) ↔ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))))
9916, 21, 25, 97, 98syl31anc 1492 . . . . . . . . . . 11 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (2 ∥ (⌊‘(𝑁 / (2↑𝑥))) ↔ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))))
10099notbid 309 . . . . . . . . . 10 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑥))) ↔ ¬ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))))
10112, 14, 1003bitr3d 300 . . . . . . . . 9 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → ((𝑥 ∈ (bits‘𝑁) ∧ 𝑥 < 𝑀) ↔ ¬ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))))
102 dvds0 15283 . . . . . . . . . . . . 13 (2 ∈ ℤ → 2 ∥ 0)
10315, 102ax-mp 5 . . . . . . . . . . . 12 2 ∥ 0
1041ad2antrr 717 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → 𝑁 ∈ ℤ)
105104zred 11728 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → 𝑁 ∈ ℝ)
106 2rp 12032 . . . . . . . . . . . . . . . . 17 2 ∈ ℝ+
107106a1i 11 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → 2 ∈ ℝ+)
10832nn0zd 11726 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) → 𝑀 ∈ ℤ)
109108adantr 472 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → 𝑀 ∈ ℤ)
110107, 109rpexpcld 13238 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → (2↑𝑀) ∈ ℝ+)
111105, 110modcld 12881 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → (𝑁 mod (2↑𝑀)) ∈ ℝ)
112 simplr 785 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → 𝑥 ∈ ℕ0)
113112nn0zd 11726 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → 𝑥 ∈ ℤ)
114107, 113rpexpcld 13238 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → (2↑𝑥) ∈ ℝ+)
1156ad2antrr 717 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → (𝑁 mod (2↑𝑀)) ∈ ℕ0)
116115nn0ge0d 11600 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → 0 ≤ (𝑁 mod (2↑𝑀)))
117111, 114, 116divge0d 12109 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → 0 ≤ ((𝑁 mod (2↑𝑀)) / (2↑𝑥)))
118110rpred 12069 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → (2↑𝑀) ∈ ℝ)
119114rpred 12069 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → (2↑𝑥) ∈ ℝ)
120 modlt 12886 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℝ ∧ (2↑𝑀) ∈ ℝ+) → (𝑁 mod (2↑𝑀)) < (2↑𝑀))
121105, 110, 120syl2anc 579 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → (𝑁 mod (2↑𝑀)) < (2↑𝑀))
122107rpred 12069 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → 2 ∈ ℝ)
123 1le2 11486 . . . . . . . . . . . . . . . . . . 19 1 ≤ 2
124123a1i 11 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → 1 ≤ 2)
125 simpr 477 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → ¬ 𝑥 < 𝑀)
126109zred 11728 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → 𝑀 ∈ ℝ)
127112nn0red 11598 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → 𝑥 ∈ ℝ)
128126, 127lenltd 10436 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → (𝑀𝑥 ↔ ¬ 𝑥 < 𝑀))
129125, 128mpbird 248 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → 𝑀𝑥)
130 eluz2 11891 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑀𝑥))
131109, 113, 129, 130syl3anbrc 1443 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → 𝑥 ∈ (ℤ𝑀))
132122, 124, 131leexp2ad 13247 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → (2↑𝑀) ≤ (2↑𝑥))
133111, 118, 119, 121, 132ltletrd 10450 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → (𝑁 mod (2↑𝑀)) < (2↑𝑥))
134114rpcnd 12071 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → (2↑𝑥) ∈ ℂ)
135134mulid1d 10310 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → ((2↑𝑥) · 1) = (2↑𝑥))
136133, 135breqtrrd 4836 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → (𝑁 mod (2↑𝑀)) < ((2↑𝑥) · 1))
137 1red 10293 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → 1 ∈ ℝ)
138111, 137, 114ltdivmuld 12120 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → (((𝑁 mod (2↑𝑀)) / (2↑𝑥)) < 1 ↔ (𝑁 mod (2↑𝑀)) < ((2↑𝑥) · 1)))
139136, 138mpbird 248 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → ((𝑁 mod (2↑𝑀)) / (2↑𝑥)) < 1)
140 1e0p1 11782 . . . . . . . . . . . . . 14 1 = (0 + 1)
141139, 140syl6breq 4849 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → ((𝑁 mod (2↑𝑀)) / (2↑𝑥)) < (0 + 1))
142111, 114rerpdivcld 12100 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → ((𝑁 mod (2↑𝑀)) / (2↑𝑥)) ∈ ℝ)
143 0z 11634 . . . . . . . . . . . . . 14 0 ∈ ℤ
144 flbi 12824 . . . . . . . . . . . . . 14 ((((𝑁 mod (2↑𝑀)) / (2↑𝑥)) ∈ ℝ ∧ 0 ∈ ℤ) → ((⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) = 0 ↔ (0 ≤ ((𝑁 mod (2↑𝑀)) / (2↑𝑥)) ∧ ((𝑁 mod (2↑𝑀)) / (2↑𝑥)) < (0 + 1))))
145142, 143, 144sylancl 580 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → ((⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) = 0 ↔ (0 ≤ ((𝑁 mod (2↑𝑀)) / (2↑𝑥)) ∧ ((𝑁 mod (2↑𝑀)) / (2↑𝑥)) < (0 + 1))))
146117, 141, 145mpbir2and 704 . . . . . . . . . . . 12 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) = 0)
147103, 146syl5breqr 4846 . . . . . . . . . . 11 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))))
148125intnand 482 . . . . . . . . . . 11 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → ¬ (𝑥 ∈ (bits‘𝑁) ∧ 𝑥 < 𝑀))
149147, 1482thd 256 . . . . . . . . . 10 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → (2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) ↔ ¬ (𝑥 ∈ (bits‘𝑁) ∧ 𝑥 < 𝑀)))
150149con2bid 345 . . . . . . . . 9 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → ((𝑥 ∈ (bits‘𝑁) ∧ 𝑥 < 𝑀) ↔ ¬ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))))
151101, 150pm2.61dan 847 . . . . . . . 8 (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) → ((𝑥 ∈ (bits‘𝑁) ∧ 𝑥 < 𝑀) ↔ ¬ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))))
152108biantrurd 528 . . . . . . . 8 (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) → ((𝑥 ∈ (bits‘𝑁) ∧ 𝑥 < 𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑥 ∈ (bits‘𝑁) ∧ 𝑥 < 𝑀))))
153151, 152bitr3d 272 . . . . . . 7 (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) → (¬ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) ↔ (𝑀 ∈ ℤ ∧ (𝑥 ∈ (bits‘𝑁) ∧ 𝑥 < 𝑀))))
154 an12 635 . . . . . . 7 ((𝑀 ∈ ℤ ∧ (𝑥 ∈ (bits‘𝑁) ∧ 𝑥 < 𝑀)) ↔ (𝑥 ∈ (bits‘𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑥 < 𝑀)))
155153, 154syl6bb 278 . . . . . 6 (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) → (¬ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) ↔ (𝑥 ∈ (bits‘𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑥 < 𝑀))))
156155pm5.32da 574 . . . . 5 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝑥 ∈ ℕ0 ∧ ¬ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))) ↔ (𝑥 ∈ ℕ0 ∧ (𝑥 ∈ (bits‘𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑥 < 𝑀)))))
1578, 156bitr3d 272 . . . 4 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 mod (2↑𝑀)) ∈ ℤ ∧ (𝑥 ∈ ℕ0 ∧ ¬ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))))) ↔ (𝑥 ∈ ℕ0 ∧ (𝑥 ∈ (bits‘𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑥 < 𝑀)))))
158 3anass 1116 . . . 4 (((𝑁 mod (2↑𝑀)) ∈ ℤ ∧ 𝑥 ∈ ℕ0 ∧ ¬ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))) ↔ ((𝑁 mod (2↑𝑀)) ∈ ℤ ∧ (𝑥 ∈ ℕ0 ∧ ¬ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))))))
159 elfzo2 12680 . . . . . . 7 (𝑥 ∈ (0..^𝑀) ↔ (𝑥 ∈ (ℤ‘0) ∧ 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀))
160 elnn0uz 11924 . . . . . . . 8 (𝑥 ∈ ℕ0𝑥 ∈ (ℤ‘0))
1611603anbi1i 1196 . . . . . . 7 ((𝑥 ∈ ℕ0𝑀 ∈ ℤ ∧ 𝑥 < 𝑀) ↔ (𝑥 ∈ (ℤ‘0) ∧ 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀))
162 3anass 1116 . . . . . . 7 ((𝑥 ∈ ℕ0𝑀 ∈ ℤ ∧ 𝑥 < 𝑀) ↔ (𝑥 ∈ ℕ0 ∧ (𝑀 ∈ ℤ ∧ 𝑥 < 𝑀)))
163159, 161, 1623bitr2i 290 . . . . . 6 (𝑥 ∈ (0..^𝑀) ↔ (𝑥 ∈ ℕ0 ∧ (𝑀 ∈ ℤ ∧ 𝑥 < 𝑀)))
164163anbi2i 616 . . . . 5 ((𝑥 ∈ (bits‘𝑁) ∧ 𝑥 ∈ (0..^𝑀)) ↔ (𝑥 ∈ (bits‘𝑁) ∧ (𝑥 ∈ ℕ0 ∧ (𝑀 ∈ ℤ ∧ 𝑥 < 𝑀))))
165 an12 635 . . . . 5 ((𝑥 ∈ (bits‘𝑁) ∧ (𝑥 ∈ ℕ0 ∧ (𝑀 ∈ ℤ ∧ 𝑥 < 𝑀))) ↔ (𝑥 ∈ ℕ0 ∧ (𝑥 ∈ (bits‘𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑥 < 𝑀))))
166164, 165bitri 266 . . . 4 ((𝑥 ∈ (bits‘𝑁) ∧ 𝑥 ∈ (0..^𝑀)) ↔ (𝑥 ∈ ℕ0 ∧ (𝑥 ∈ (bits‘𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑥 < 𝑀))))
167157, 158, 1663bitr4g 305 . . 3 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 mod (2↑𝑀)) ∈ ℤ ∧ 𝑥 ∈ ℕ0 ∧ ¬ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))) ↔ (𝑥 ∈ (bits‘𝑁) ∧ 𝑥 ∈ (0..^𝑀))))
168 bitsval 15428 . . 3 (𝑥 ∈ (bits‘(𝑁 mod (2↑𝑀))) ↔ ((𝑁 mod (2↑𝑀)) ∈ ℤ ∧ 𝑥 ∈ ℕ0 ∧ ¬ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))))
169 elin 3957 . . 3 (𝑥 ∈ ((bits‘𝑁) ∩ (0..^𝑀)) ↔ (𝑥 ∈ (bits‘𝑁) ∧ 𝑥 ∈ (0..^𝑀)))
170167, 168, 1693bitr4g 305 . 2 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑥 ∈ (bits‘(𝑁 mod (2↑𝑀))) ↔ 𝑥 ∈ ((bits‘𝑁) ∩ (0..^𝑀))))
171170eqrdv 2762 1 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (bits‘(𝑁 mod (2↑𝑀))) = ((bits‘𝑁) ∩ (0..^𝑀)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  wne 2936  cin 3730   class class class wbr 4808  cfv 6067  (class class class)co 6841  cr 10187  0cc0 10188  1c1 10189   + caddc 10191   · cmul 10193   < clt 10327  cle 10328  cmin 10519   / cdiv 10937  cn 11273  2c2 11326  0cn0 11537  cz 11623  cuz 11885  +crp 12027  ..^cfzo 12672  cfl 12798   mod cmo 12875  cexp 13066  cdvds 15266  bitscbits 15423
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-sep 4940  ax-nul 4948  ax-pow 5000  ax-pr 5061  ax-un 7146  ax-cnex 10244  ax-resscn 10245  ax-1cn 10246  ax-icn 10247  ax-addcl 10248  ax-addrcl 10249  ax-mulcl 10250  ax-mulrcl 10251  ax-mulcom 10252  ax-addass 10253  ax-mulass 10254  ax-distr 10255  ax-i2m1 10256  ax-1ne0 10257  ax-1rid 10258  ax-rnegex 10259  ax-rrecex 10260  ax-cnre 10261  ax-pre-lttri 10262  ax-pre-lttrn 10263  ax-pre-ltadd 10264  ax-pre-mulgt0 10265  ax-pre-sup 10266
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-nel 3040  df-ral 3059  df-rex 3060  df-reu 3061  df-rmo 3062  df-rab 3063  df-v 3351  df-sbc 3596  df-csb 3691  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-pss 3747  df-nul 4079  df-if 4243  df-pw 4316  df-sn 4334  df-pr 4336  df-tp 4338  df-op 4340  df-uni 4594  df-iun 4677  df-br 4809  df-opab 4871  df-mpt 4888  df-tr 4911  df-id 5184  df-eprel 5189  df-po 5197  df-so 5198  df-fr 5235  df-we 5237  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-res 5288  df-ima 5289  df-pred 5864  df-ord 5910  df-on 5911  df-lim 5912  df-suc 5913  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-f1 6072  df-fo 6073  df-f1o 6074  df-fv 6075  df-riota 6802  df-ov 6844  df-oprab 6845  df-mpt2 6846  df-om 7263  df-1st 7365  df-2nd 7366  df-wrecs 7609  df-recs 7671  df-rdg 7709  df-er 7946  df-en 8160  df-dom 8161  df-sdom 8162  df-sup 8554  df-inf 8555  df-pnf 10329  df-mnf 10330  df-xr 10331  df-ltxr 10332  df-le 10333  df-sub 10521  df-neg 10522  df-div 10938  df-nn 11274  df-2 11334  df-n0 11538  df-z 11624  df-uz 11886  df-rp 12028  df-fz 12533  df-fzo 12673  df-fl 12800  df-mod 12876  df-seq 13008  df-exp 13067  df-dvds 15267  df-bits 15426
This theorem is referenced by:  sadaddlem  15470  sadadd  15471  bitsres  15477  smumul  15497
  Copyright terms: Public domain W3C validator