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

Theorem bitsmod 16234
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 483 . . . . . . . 8 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 𝑁 ∈ ℤ)
2 2nn 12139 . . . . . . . . . 10 2 ∈ ℕ
32a1i 11 . . . . . . . . 9 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 2 ∈ ℕ)
4 simpr 485 . . . . . . . . 9 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 𝑀 ∈ ℕ0)
53, 4nnexpcld 14053 . . . . . . . 8 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (2↑𝑀) ∈ ℕ)
61, 5zmodcld 13705 . . . . . . 7 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑁 mod (2↑𝑀)) ∈ ℕ0)
76nn0zd 12517 . . . . . 6 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑁 mod (2↑𝑀)) ∈ ℤ)
87biantrurd 533 . . . . 5 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝑥 ∈ ℕ0 ∧ ¬ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))) ↔ ((𝑁 mod (2↑𝑀)) ∈ ℤ ∧ (𝑥 ∈ ℕ0 ∧ ¬ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))))))
91ad2antrr 723 . . . . . . . . . . 11 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → 𝑁 ∈ ℤ)
10 simplr 766 . . . . . . . . . . 11 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → 𝑥 ∈ ℕ0)
11 bitsval2 16223 . . . . . . . . . . 11 ((𝑁 ∈ ℤ ∧ 𝑥 ∈ ℕ0) → (𝑥 ∈ (bits‘𝑁) ↔ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑥)))))
129, 10, 11syl2anc 584 . . . . . . . . . 10 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (𝑥 ∈ (bits‘𝑁) ↔ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑥)))))
13 simpr 485 . . . . . . . . . . 11 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → 𝑥 < 𝑀)
1413biantrud 532 . . . . . . . . . 10 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (𝑥 ∈ (bits‘𝑁) ↔ (𝑥 ∈ (bits‘𝑁) ∧ 𝑥 < 𝑀)))
15 2z 12445 . . . . . . . . . . . . 13 2 ∈ ℤ
1615a1i 11 . . . . . . . . . . . 12 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → 2 ∈ ℤ)
179zred 12519 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → 𝑁 ∈ ℝ)
182a1i 11 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → 2 ∈ ℕ)
1918, 10nnexpcld 14053 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (2↑𝑥) ∈ ℕ)
2017, 19nndivred 12120 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (𝑁 / (2↑𝑥)) ∈ ℝ)
2120flcld 13611 . . . . . . . . . . . 12 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (⌊‘(𝑁 / (2↑𝑥))) ∈ ℤ)
227ad2antrr 723 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (𝑁 mod (2↑𝑀)) ∈ ℤ)
2322zred 12519 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (𝑁 mod (2↑𝑀)) ∈ ℝ)
2423, 19nndivred 12120 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → ((𝑁 mod (2↑𝑀)) / (2↑𝑥)) ∈ ℝ)
2524flcld 13611 . . . . . . . . . . . 12 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) ∈ ℤ)
2619nnzd 12518 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (2↑𝑥) ∈ ℤ)
2726, 16zmulcld 12525 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → ((2↑𝑥) · 2) ∈ ℤ)
285ad2antrr 723 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (2↑𝑀) ∈ ℕ)
2928nnzd 12518 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (2↑𝑀) ∈ ℤ)
309, 22zsubcld 12524 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (𝑁 − (𝑁 mod (2↑𝑀))) ∈ ℤ)
31 2cnd 12144 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → 2 ∈ ℂ)
3231, 10expp1d 13958 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (2↑(𝑥 + 1)) = ((2↑𝑥) · 2))
33 1nn0 12342 . . . . . . . . . . . . . . . . . . . 20 1 ∈ ℕ0
3433a1i 11 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → 1 ∈ ℕ0)
3510, 34nn0addcld 12390 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (𝑥 + 1) ∈ ℕ0)
3635nn0zd 12517 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (𝑥 + 1) ∈ ℤ)
37 simplr 766 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) → 𝑀 ∈ ℕ0)
3837adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → 𝑀 ∈ ℕ0)
3938nn0zd 12517 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → 𝑀 ∈ ℤ)
40 nn0ltp1le 12471 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ ℕ0𝑀 ∈ ℕ0) → (𝑥 < 𝑀 ↔ (𝑥 + 1) ≤ 𝑀))
4110, 38, 40syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (𝑥 < 𝑀 ↔ (𝑥 + 1) ≤ 𝑀))
4213, 41mpbid 231 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (𝑥 + 1) ≤ 𝑀)
43 eluz2 12681 . . . . . . . . . . . . . . . . . . 19 (𝑀 ∈ (ℤ‘(𝑥 + 1)) ↔ ((𝑥 + 1) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑥 + 1) ≤ 𝑀))
4436, 39, 42, 43syl3anbrc 1342 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → 𝑀 ∈ (ℤ‘(𝑥 + 1)))
45 dvdsexp 16128 . . . . . . . . . . . . . . . . . 18 ((2 ∈ ℤ ∧ (𝑥 + 1) ∈ ℕ0𝑀 ∈ (ℤ‘(𝑥 + 1))) → (2↑(𝑥 + 1)) ∥ (2↑𝑀))
4616, 35, 44, 45syl3anc 1370 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (2↑(𝑥 + 1)) ∥ (2↑𝑀))
4732, 46eqbrtrrd 5113 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → ((2↑𝑥) · 2) ∥ (2↑𝑀))
4828nnrpd 12863 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (2↑𝑀) ∈ ℝ+)
49 moddifz 13696 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℝ ∧ (2↑𝑀) ∈ ℝ+) → ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ∈ ℤ)
5017, 48, 49syl2anc 584 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ∈ ℤ)
51 2ne0 12170 . . . . . . . . . . . . . . . . . . . 20 2 ≠ 0
5251a1i 11 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → 2 ≠ 0)
5331, 52, 39expne0d 13963 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (2↑𝑀) ≠ 0)
54 dvdsval2 16057 . . . . . . . . . . . . . . . . . 18 (((2↑𝑀) ∈ ℤ ∧ (2↑𝑀) ≠ 0 ∧ (𝑁 − (𝑁 mod (2↑𝑀))) ∈ ℤ) → ((2↑𝑀) ∥ (𝑁 − (𝑁 mod (2↑𝑀))) ↔ ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ∈ ℤ))
5529, 53, 30, 54syl3anc 1370 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → ((2↑𝑀) ∥ (𝑁 − (𝑁 mod (2↑𝑀))) ↔ ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ∈ ℤ))
5650, 55mpbird 256 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (2↑𝑀) ∥ (𝑁 − (𝑁 mod (2↑𝑀))))
5727, 29, 30, 47, 56dvdstrd 16095 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → ((2↑𝑥) · 2) ∥ (𝑁 − (𝑁 mod (2↑𝑀))))
5830zcnd 12520 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (𝑁 − (𝑁 mod (2↑𝑀))) ∈ ℂ)
5919nncnd 12082 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (2↑𝑥) ∈ ℂ)
6010nn0zd 12517 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → 𝑥 ∈ ℤ)
6131, 52, 60expne0d 13963 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (2↑𝑥) ≠ 0)
6258, 59, 61divcan2d 11846 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → ((2↑𝑥) · ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥))) = (𝑁 − (𝑁 mod (2↑𝑀))))
6357, 62breqtrrd 5117 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → ((2↑𝑥) · 2) ∥ ((2↑𝑥) · ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥))))
6410nn0red 12387 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → 𝑥 ∈ ℝ)
6538nn0red 12387 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → 𝑀 ∈ ℝ)
6664, 65, 13ltled 11216 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → 𝑥𝑀)
67 eluz2 12681 . . . . . . . . . . . . . . . . . . 19 (𝑀 ∈ (ℤ𝑥) ↔ (𝑥 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑥𝑀))
6860, 39, 66, 67syl3anbrc 1342 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → 𝑀 ∈ (ℤ𝑥))
69 dvdsexp 16128 . . . . . . . . . . . . . . . . . 18 ((2 ∈ ℤ ∧ 𝑥 ∈ ℕ0𝑀 ∈ (ℤ𝑥)) → (2↑𝑥) ∥ (2↑𝑀))
7016, 10, 68, 69syl3anc 1370 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (2↑𝑥) ∥ (2↑𝑀))
7126, 29, 30, 70, 56dvdstrd 16095 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (2↑𝑥) ∥ (𝑁 − (𝑁 mod (2↑𝑀))))
72 dvdsval2 16057 . . . . . . . . . . . . . . . . 17 (((2↑𝑥) ∈ ℤ ∧ (2↑𝑥) ≠ 0 ∧ (𝑁 − (𝑁 mod (2↑𝑀))) ∈ ℤ) → ((2↑𝑥) ∥ (𝑁 − (𝑁 mod (2↑𝑀))) ↔ ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)) ∈ ℤ))
7326, 61, 30, 72syl3anc 1370 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → ((2↑𝑥) ∥ (𝑁 − (𝑁 mod (2↑𝑀))) ↔ ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)) ∈ ℤ))
7471, 73mpbid 231 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)) ∈ ℤ)
75 dvdscmulr 16085 . . . . . . . . . . . . . . 15 ((2 ∈ ℤ ∧ ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)) ∈ ℤ ∧ ((2↑𝑥) ∈ ℤ ∧ (2↑𝑥) ≠ 0)) → (((2↑𝑥) · 2) ∥ ((2↑𝑥) · ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥))) ↔ 2 ∥ ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥))))
7616, 74, 26, 61, 75syl112anc 1373 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (((2↑𝑥) · 2) ∥ ((2↑𝑥) · ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥))) ↔ 2 ∥ ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥))))
7763, 76mpbid 231 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → 2 ∥ ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)))
7825zcnd 12520 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) ∈ ℂ)
7974zcnd 12520 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)) ∈ ℂ)
8022zcnd 12520 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (𝑁 mod (2↑𝑀)) ∈ ℂ)
819zcnd 12520 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → 𝑁 ∈ ℂ)
8280, 81pncan3d 11428 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → ((𝑁 mod (2↑𝑀)) + (𝑁 − (𝑁 mod (2↑𝑀)))) = 𝑁)
8382oveq1d 7344 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (((𝑁 mod (2↑𝑀)) + (𝑁 − (𝑁 mod (2↑𝑀)))) / (2↑𝑥)) = (𝑁 / (2↑𝑥)))
8480, 58, 59, 61divdird 11882 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (((𝑁 mod (2↑𝑀)) + (𝑁 − (𝑁 mod (2↑𝑀)))) / (2↑𝑥)) = (((𝑁 mod (2↑𝑀)) / (2↑𝑥)) + ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥))))
8583, 84eqtr3d 2778 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (𝑁 / (2↑𝑥)) = (((𝑁 mod (2↑𝑀)) / (2↑𝑥)) + ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥))))
8685fveq2d 6823 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (⌊‘(𝑁 / (2↑𝑥))) = (⌊‘(((𝑁 mod (2↑𝑀)) / (2↑𝑥)) + ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)))))
87 fladdz 13638 . . . . . . . . . . . . . . . 16 ((((𝑁 mod (2↑𝑀)) / (2↑𝑥)) ∈ ℝ ∧ ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)) ∈ ℤ) → (⌊‘(((𝑁 mod (2↑𝑀)) / (2↑𝑥)) + ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)))) = ((⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) + ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥))))
8824, 74, 87syl2anc 584 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (⌊‘(((𝑁 mod (2↑𝑀)) / (2↑𝑥)) + ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)))) = ((⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) + ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥))))
8986, 88eqtrd 2776 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (⌊‘(𝑁 / (2↑𝑥))) = ((⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) + ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥))))
9078, 79, 89mvrladdd 11481 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → ((⌊‘(𝑁 / (2↑𝑥))) − (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))) = ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)))
9177, 90breqtrrd 5117 . . . . . . . . . . . 12 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → 2 ∥ ((⌊‘(𝑁 / (2↑𝑥))) − (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))))
92 dvdssub2 16101 . . . . . . . . . . . 12 (((2 ∈ ℤ ∧ (⌊‘(𝑁 / (2↑𝑥))) ∈ ℤ ∧ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) ∈ ℤ) ∧ 2 ∥ ((⌊‘(𝑁 / (2↑𝑥))) − (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))))) → (2 ∥ (⌊‘(𝑁 / (2↑𝑥))) ↔ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))))
9316, 21, 25, 91, 92syl31anc 1372 . . . . . . . . . . 11 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (2 ∥ (⌊‘(𝑁 / (2↑𝑥))) ↔ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))))
9493notbid 317 . . . . . . . . . 10 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → (¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑥))) ↔ ¬ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))))
9512, 14, 943bitr3d 308 . . . . . . . . 9 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ 𝑥 < 𝑀) → ((𝑥 ∈ (bits‘𝑁) ∧ 𝑥 < 𝑀) ↔ ¬ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))))
96 z0even 16167 . . . . . . . . . . . 12 2 ∥ 0
971ad2antrr 723 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → 𝑁 ∈ ℤ)
9897zred 12519 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → 𝑁 ∈ ℝ)
99 2rp 12828 . . . . . . . . . . . . . . . . 17 2 ∈ ℝ+
10099a1i 11 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → 2 ∈ ℝ+)
10137nn0zd 12517 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) → 𝑀 ∈ ℤ)
102101adantr 481 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → 𝑀 ∈ ℤ)
103100, 102rpexpcld 14055 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → (2↑𝑀) ∈ ℝ+)
10498, 103modcld 13688 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → (𝑁 mod (2↑𝑀)) ∈ ℝ)
105 simplr 766 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → 𝑥 ∈ ℕ0)
106105nn0zd 12517 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → 𝑥 ∈ ℤ)
107100, 106rpexpcld 14055 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → (2↑𝑥) ∈ ℝ+)
1086ad2antrr 723 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → (𝑁 mod (2↑𝑀)) ∈ ℕ0)
109108nn0ge0d 12389 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → 0 ≤ (𝑁 mod (2↑𝑀)))
110104, 107, 109divge0d 12905 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → 0 ≤ ((𝑁 mod (2↑𝑀)) / (2↑𝑥)))
111103rpred 12865 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → (2↑𝑀) ∈ ℝ)
112107rpred 12865 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → (2↑𝑥) ∈ ℝ)
113 modlt 13693 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℝ ∧ (2↑𝑀) ∈ ℝ+) → (𝑁 mod (2↑𝑀)) < (2↑𝑀))
11498, 103, 113syl2anc 584 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → (𝑁 mod (2↑𝑀)) < (2↑𝑀))
115100rpred 12865 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → 2 ∈ ℝ)
116 1le2 12275 . . . . . . . . . . . . . . . . . . 19 1 ≤ 2
117116a1i 11 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → 1 ≤ 2)
118102zred 12519 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → 𝑀 ∈ ℝ)
119105nn0red 12387 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → 𝑥 ∈ ℝ)
120 simpr 485 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → ¬ 𝑥 < 𝑀)
121118, 119, 120nltled 11218 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → 𝑀𝑥)
122 eluz2 12681 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑀𝑥))
123102, 106, 121, 122syl3anbrc 1342 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → 𝑥 ∈ (ℤ𝑀))
124115, 117, 123leexp2ad 14064 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → (2↑𝑀) ≤ (2↑𝑥))
125104, 111, 112, 114, 124ltletrd 11228 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → (𝑁 mod (2↑𝑀)) < (2↑𝑥))
126107rpcnd 12867 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → (2↑𝑥) ∈ ℂ)
127126mulid1d 11085 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → ((2↑𝑥) · 1) = (2↑𝑥))
128125, 127breqtrrd 5117 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → (𝑁 mod (2↑𝑀)) < ((2↑𝑥) · 1))
129 1red 11069 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → 1 ∈ ℝ)
130104, 129, 107ltdivmuld 12916 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → (((𝑁 mod (2↑𝑀)) / (2↑𝑥)) < 1 ↔ (𝑁 mod (2↑𝑀)) < ((2↑𝑥) · 1)))
131128, 130mpbird 256 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → ((𝑁 mod (2↑𝑀)) / (2↑𝑥)) < 1)
132 1e0p1 12572 . . . . . . . . . . . . . 14 1 = (0 + 1)
133131, 132breqtrdi 5130 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → ((𝑁 mod (2↑𝑀)) / (2↑𝑥)) < (0 + 1))
134104, 107rerpdivcld 12896 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → ((𝑁 mod (2↑𝑀)) / (2↑𝑥)) ∈ ℝ)
135 0z 12423 . . . . . . . . . . . . . 14 0 ∈ ℤ
136 flbi 13629 . . . . . . . . . . . . . 14 ((((𝑁 mod (2↑𝑀)) / (2↑𝑥)) ∈ ℝ ∧ 0 ∈ ℤ) → ((⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) = 0 ↔ (0 ≤ ((𝑁 mod (2↑𝑀)) / (2↑𝑥)) ∧ ((𝑁 mod (2↑𝑀)) / (2↑𝑥)) < (0 + 1))))
137134, 135, 136sylancl 586 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → ((⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) = 0 ↔ (0 ≤ ((𝑁 mod (2↑𝑀)) / (2↑𝑥)) ∧ ((𝑁 mod (2↑𝑀)) / (2↑𝑥)) < (0 + 1))))
138110, 133, 137mpbir2and 710 . . . . . . . . . . . 12 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) = 0)
13996, 138breqtrrid 5127 . . . . . . . . . . 11 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))))
140120intnand 489 . . . . . . . . . . 11 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → ¬ (𝑥 ∈ (bits‘𝑁) ∧ 𝑥 < 𝑀))
141139, 1402thd 264 . . . . . . . . . 10 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → (2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) ↔ ¬ (𝑥 ∈ (bits‘𝑁) ∧ 𝑥 < 𝑀)))
142141con2bid 354 . . . . . . . . 9 ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ ¬ 𝑥 < 𝑀) → ((𝑥 ∈ (bits‘𝑁) ∧ 𝑥 < 𝑀) ↔ ¬ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))))
14395, 142pm2.61dan 810 . . . . . . . 8 (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) → ((𝑥 ∈ (bits‘𝑁) ∧ 𝑥 < 𝑀) ↔ ¬ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))))
144101biantrurd 533 . . . . . . . 8 (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) → ((𝑥 ∈ (bits‘𝑁) ∧ 𝑥 < 𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑥 ∈ (bits‘𝑁) ∧ 𝑥 < 𝑀))))
145143, 144bitr3d 280 . . . . . . 7 (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) → (¬ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) ↔ (𝑀 ∈ ℤ ∧ (𝑥 ∈ (bits‘𝑁) ∧ 𝑥 < 𝑀))))
146 an12 642 . . . . . . 7 ((𝑀 ∈ ℤ ∧ (𝑥 ∈ (bits‘𝑁) ∧ 𝑥 < 𝑀)) ↔ (𝑥 ∈ (bits‘𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑥 < 𝑀)))
147145, 146bitrdi 286 . . . . . 6 (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) → (¬ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) ↔ (𝑥 ∈ (bits‘𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑥 < 𝑀))))
148147pm5.32da 579 . . . . 5 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝑥 ∈ ℕ0 ∧ ¬ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))) ↔ (𝑥 ∈ ℕ0 ∧ (𝑥 ∈ (bits‘𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑥 < 𝑀)))))
1498, 148bitr3d 280 . . . 4 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 mod (2↑𝑀)) ∈ ℤ ∧ (𝑥 ∈ ℕ0 ∧ ¬ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))))) ↔ (𝑥 ∈ ℕ0 ∧ (𝑥 ∈ (bits‘𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑥 < 𝑀)))))
150 3anass 1094 . . . 4 (((𝑁 mod (2↑𝑀)) ∈ ℤ ∧ 𝑥 ∈ ℕ0 ∧ ¬ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))) ↔ ((𝑁 mod (2↑𝑀)) ∈ ℤ ∧ (𝑥 ∈ ℕ0 ∧ ¬ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))))))
151 elfzo2 13483 . . . . . . 7 (𝑥 ∈ (0..^𝑀) ↔ (𝑥 ∈ (ℤ‘0) ∧ 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀))
152 elnn0uz 12716 . . . . . . . 8 (𝑥 ∈ ℕ0𝑥 ∈ (ℤ‘0))
1531523anbi1i 1156 . . . . . . 7 ((𝑥 ∈ ℕ0𝑀 ∈ ℤ ∧ 𝑥 < 𝑀) ↔ (𝑥 ∈ (ℤ‘0) ∧ 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀))
154 3anass 1094 . . . . . . 7 ((𝑥 ∈ ℕ0𝑀 ∈ ℤ ∧ 𝑥 < 𝑀) ↔ (𝑥 ∈ ℕ0 ∧ (𝑀 ∈ ℤ ∧ 𝑥 < 𝑀)))
155151, 153, 1543bitr2i 298 . . . . . 6 (𝑥 ∈ (0..^𝑀) ↔ (𝑥 ∈ ℕ0 ∧ (𝑀 ∈ ℤ ∧ 𝑥 < 𝑀)))
156155anbi2i 623 . . . . 5 ((𝑥 ∈ (bits‘𝑁) ∧ 𝑥 ∈ (0..^𝑀)) ↔ (𝑥 ∈ (bits‘𝑁) ∧ (𝑥 ∈ ℕ0 ∧ (𝑀 ∈ ℤ ∧ 𝑥 < 𝑀))))
157 an12 642 . . . . 5 ((𝑥 ∈ (bits‘𝑁) ∧ (𝑥 ∈ ℕ0 ∧ (𝑀 ∈ ℤ ∧ 𝑥 < 𝑀))) ↔ (𝑥 ∈ ℕ0 ∧ (𝑥 ∈ (bits‘𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑥 < 𝑀))))
158156, 157bitri 274 . . . 4 ((𝑥 ∈ (bits‘𝑁) ∧ 𝑥 ∈ (0..^𝑀)) ↔ (𝑥 ∈ ℕ0 ∧ (𝑥 ∈ (bits‘𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑥 < 𝑀))))
159149, 150, 1583bitr4g 313 . . 3 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (((𝑁 mod (2↑𝑀)) ∈ ℤ ∧ 𝑥 ∈ ℕ0 ∧ ¬ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))) ↔ (𝑥 ∈ (bits‘𝑁) ∧ 𝑥 ∈ (0..^𝑀))))
160 bitsval 16222 . . 3 (𝑥 ∈ (bits‘(𝑁 mod (2↑𝑀))) ↔ ((𝑁 mod (2↑𝑀)) ∈ ℤ ∧ 𝑥 ∈ ℕ0 ∧ ¬ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))))
161 elin 3913 . . 3 (𝑥 ∈ ((bits‘𝑁) ∩ (0..^𝑀)) ↔ (𝑥 ∈ (bits‘𝑁) ∧ 𝑥 ∈ (0..^𝑀)))
162159, 160, 1613bitr4g 313 . 2 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑥 ∈ (bits‘(𝑁 mod (2↑𝑀))) ↔ 𝑥 ∈ ((bits‘𝑁) ∩ (0..^𝑀))))
163162eqrdv 2734 1 ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (bits‘(𝑁 mod (2↑𝑀))) = ((bits‘𝑁) ∩ (0..^𝑀)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3a 1086   = wceq 1540  wcel 2105  wne 2940  cin 3896   class class class wbr 5089  cfv 6473  (class class class)co 7329  cr 10963  0cc0 10964  1c1 10965   + caddc 10967   · cmul 10969   < clt 11102  cle 11103  cmin 11298   / cdiv 11725  cn 12066  2c2 12121  0cn0 12326  cz 12412  cuz 12675  +crp 12823  ..^cfzo 13475  cfl 13603   mod cmo 13682  cexp 13875  cdvds 16054  bitscbits 16217
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5240  ax-nul 5247  ax-pow 5305  ax-pr 5369  ax-un 7642  ax-cnex 11020  ax-resscn 11021  ax-1cn 11022  ax-icn 11023  ax-addcl 11024  ax-addrcl 11025  ax-mulcl 11026  ax-mulrcl 11027  ax-mulcom 11028  ax-addass 11029  ax-mulass 11030  ax-distr 11031  ax-i2m1 11032  ax-1ne0 11033  ax-1rid 11034  ax-rnegex 11035  ax-rrecex 11036  ax-cnre 11037  ax-pre-lttri 11038  ax-pre-lttrn 11039  ax-pre-ltadd 11040  ax-pre-mulgt0 11041  ax-pre-sup 11042
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4269  df-if 4473  df-pw 4548  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4852  df-iun 4940  df-br 5090  df-opab 5152  df-mpt 5173  df-tr 5207  df-id 5512  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5569  df-we 5571  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-pred 6232  df-ord 6299  df-on 6300  df-lim 6301  df-suc 6302  df-iota 6425  df-fun 6475  df-fn 6476  df-f 6477  df-f1 6478  df-fo 6479  df-f1o 6480  df-fv 6481  df-riota 7286  df-ov 7332  df-oprab 7333  df-mpo 7334  df-om 7773  df-1st 7891  df-2nd 7892  df-frecs 8159  df-wrecs 8190  df-recs 8264  df-rdg 8303  df-er 8561  df-en 8797  df-dom 8798  df-sdom 8799  df-sup 9291  df-inf 9292  df-pnf 11104  df-mnf 11105  df-xr 11106  df-ltxr 11107  df-le 11108  df-sub 11300  df-neg 11301  df-div 11726  df-nn 12067  df-2 12129  df-n0 12327  df-z 12413  df-uz 12676  df-rp 12824  df-fz 13333  df-fzo 13476  df-fl 13605  df-mod 13683  df-seq 13815  df-exp 13876  df-dvds 16055  df-bits 16220
This theorem is referenced by:  sadaddlem  16264  sadadd  16265  bitsres  16271  smumul  16291
  Copyright terms: Public domain W3C validator