Step | Hyp | Ref
| Expression |
1 | | simpl 473 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
→ 𝑁 ∈
ℤ) |
2 | | 2nn 11185 |
. . . . . . . . . 10
⊢ 2 ∈
ℕ |
3 | 2 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
→ 2 ∈ ℕ) |
4 | | simpr 477 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
→ 𝑀 ∈
ℕ0) |
5 | 3, 4 | nnexpcld 13030 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
→ (2↑𝑀) ∈
ℕ) |
6 | 1, 5 | zmodcld 12691 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
→ (𝑁 mod (2↑𝑀)) ∈
ℕ0) |
7 | 6 | nn0zd 11480 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
→ (𝑁 mod (2↑𝑀)) ∈
ℤ) |
8 | 7 | biantrurd 529 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
→ ((𝑥 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))) ↔ ((𝑁 mod (2↑𝑀)) ∈ ℤ ∧ (𝑥 ∈ ℕ0 ∧ ¬ 2
∥ (⌊‘((𝑁
mod (2↑𝑀)) /
(2↑𝑥))))))) |
9 | 1 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → 𝑁 ∈ ℤ) |
10 | | simplr 792 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → 𝑥 ∈ ℕ0) |
11 | | bitsval2 15147 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝑥 ∈ ℕ0)
→ (𝑥 ∈
(bits‘𝑁) ↔ ¬
2 ∥ (⌊‘(𝑁
/ (2↑𝑥))))) |
12 | 9, 10, 11 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (𝑥 ∈ (bits‘𝑁) ↔ ¬ 2 ∥
(⌊‘(𝑁 /
(2↑𝑥))))) |
13 | | simpr 477 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → 𝑥 < 𝑀) |
14 | 13 | biantrud 528 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (𝑥 ∈ (bits‘𝑁) ↔ (𝑥 ∈ (bits‘𝑁) ∧ 𝑥 < 𝑀))) |
15 | | 2z 11409 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℤ |
16 | 15 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → 2 ∈ ℤ) |
17 | 9 | zred 11482 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → 𝑁 ∈ ℝ) |
18 | 2 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → 2 ∈ ℕ) |
19 | 18, 10 | nnexpcld 13030 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (2↑𝑥) ∈ ℕ) |
20 | 17, 19 | nndivred 11069 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (𝑁 / (2↑𝑥)) ∈ ℝ) |
21 | 20 | flcld 12599 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (⌊‘(𝑁 / (2↑𝑥))) ∈ ℤ) |
22 | 7 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (𝑁 mod (2↑𝑀)) ∈ ℤ) |
23 | 22 | zred 11482 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (𝑁 mod (2↑𝑀)) ∈ ℝ) |
24 | 23, 19 | nndivred 11069 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → ((𝑁 mod (2↑𝑀)) / (2↑𝑥)) ∈ ℝ) |
25 | 24 | flcld 12599 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) ∈ ℤ) |
26 | | 2cnd 11093 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → 2 ∈ ℂ) |
27 | 26, 10 | expp1d 13009 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (2↑(𝑥 + 1)) = ((2↑𝑥) · 2)) |
28 | | 1nn0 11308 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 ∈
ℕ0 |
29 | 28 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → 1 ∈
ℕ0) |
30 | 10, 29 | nn0addcld 11355 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (𝑥 + 1) ∈
ℕ0) |
31 | 30 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (𝑥 + 1) ∈ ℤ) |
32 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) → 𝑀 ∈
ℕ0) |
33 | 32 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → 𝑀 ∈
ℕ0) |
34 | 33 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → 𝑀 ∈ ℤ) |
35 | | nn0ltp1le 11435 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (𝑥 < 𝑀 ↔ (𝑥 + 1) ≤ 𝑀)) |
36 | 10, 33, 35 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (𝑥 < 𝑀 ↔ (𝑥 + 1) ≤ 𝑀)) |
37 | 13, 36 | mpbid 222 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (𝑥 + 1) ≤ 𝑀) |
38 | | eluz2 11693 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑀 ∈
(ℤ≥‘(𝑥 + 1)) ↔ ((𝑥 + 1) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑥 + 1) ≤ 𝑀)) |
39 | 31, 34, 37, 38 | syl3anbrc 1246 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → 𝑀 ∈ (ℤ≥‘(𝑥 + 1))) |
40 | | dvdsexp 15049 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2
∈ ℤ ∧ (𝑥 +
1) ∈ ℕ0 ∧ 𝑀 ∈ (ℤ≥‘(𝑥 + 1))) → (2↑(𝑥 + 1)) ∥ (2↑𝑀)) |
41 | 16, 30, 39, 40 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (2↑(𝑥 + 1)) ∥ (2↑𝑀)) |
42 | 27, 41 | eqbrtrrd 4677 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → ((2↑𝑥) · 2) ∥ (2↑𝑀)) |
43 | 5 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (2↑𝑀) ∈ ℕ) |
44 | 43 | nnrpd 11870 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (2↑𝑀) ∈
ℝ+) |
45 | | moddifz 12682 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℝ ∧
(2↑𝑀) ∈
ℝ+) → ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ∈ ℤ) |
46 | 17, 44, 45 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ∈ ℤ) |
47 | 43 | nnzd 11481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (2↑𝑀) ∈ ℤ) |
48 | | 2ne0 11113 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ≠
0 |
49 | 48 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → 2 ≠ 0) |
50 | 26, 49, 34 | expne0d 13014 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (2↑𝑀) ≠ 0) |
51 | 9, 22 | zsubcld 11487 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (𝑁 − (𝑁 mod (2↑𝑀))) ∈ ℤ) |
52 | | dvdsval2 14986 |
. . . . . . . . . . . . . . . . . 18
⊢
(((2↑𝑀) ∈
ℤ ∧ (2↑𝑀)
≠ 0 ∧ (𝑁 −
(𝑁 mod (2↑𝑀))) ∈ ℤ) →
((2↑𝑀) ∥ (𝑁 − (𝑁 mod (2↑𝑀))) ↔ ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ∈ ℤ)) |
53 | 47, 50, 51, 52 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → ((2↑𝑀) ∥ (𝑁 − (𝑁 mod (2↑𝑀))) ↔ ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ∈ ℤ)) |
54 | 46, 53 | mpbird 247 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (2↑𝑀) ∥ (𝑁 − (𝑁 mod (2↑𝑀)))) |
55 | 19 | nnzd 11481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (2↑𝑥) ∈ ℤ) |
56 | 55, 16 | zmulcld 11488 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → ((2↑𝑥) · 2) ∈
ℤ) |
57 | | dvdstr 15018 |
. . . . . . . . . . . . . . . . 17
⊢
((((2↑𝑥)
· 2) ∈ ℤ ∧ (2↑𝑀) ∈ ℤ ∧ (𝑁 − (𝑁 mod (2↑𝑀))) ∈ ℤ) → ((((2↑𝑥) · 2) ∥
(2↑𝑀) ∧
(2↑𝑀) ∥ (𝑁 − (𝑁 mod (2↑𝑀)))) → ((2↑𝑥) · 2) ∥ (𝑁 − (𝑁 mod (2↑𝑀))))) |
58 | 56, 47, 51, 57 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → ((((2↑𝑥) · 2) ∥ (2↑𝑀) ∧ (2↑𝑀) ∥ (𝑁 − (𝑁 mod (2↑𝑀)))) → ((2↑𝑥) · 2) ∥ (𝑁 − (𝑁 mod (2↑𝑀))))) |
59 | 42, 54, 58 | mp2and 715 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → ((2↑𝑥) · 2) ∥ (𝑁 − (𝑁 mod (2↑𝑀)))) |
60 | 51 | zcnd 11483 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (𝑁 − (𝑁 mod (2↑𝑀))) ∈ ℂ) |
61 | 19 | nncnd 11036 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (2↑𝑥) ∈ ℂ) |
62 | 10 | nn0zd 11480 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → 𝑥 ∈ ℤ) |
63 | 26, 49, 62 | expne0d 13014 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (2↑𝑥) ≠ 0) |
64 | 60, 61, 63 | divcan2d 10803 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → ((2↑𝑥) · ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥))) = (𝑁 − (𝑁 mod (2↑𝑀)))) |
65 | 59, 64 | breqtrrd 4681 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → ((2↑𝑥) · 2) ∥ ((2↑𝑥) · ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)))) |
66 | 10 | nn0red 11352 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → 𝑥 ∈ ℝ) |
67 | 33 | nn0red 11352 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → 𝑀 ∈ ℝ) |
68 | 66, 67, 13 | ltled 10185 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → 𝑥 ≤ 𝑀) |
69 | | eluz2 11693 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑀 ∈
(ℤ≥‘𝑥) ↔ (𝑥 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑥 ≤ 𝑀)) |
70 | 62, 34, 68, 69 | syl3anbrc 1246 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → 𝑀 ∈ (ℤ≥‘𝑥)) |
71 | | dvdsexp 15049 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2
∈ ℤ ∧ 𝑥
∈ ℕ0 ∧ 𝑀 ∈ (ℤ≥‘𝑥)) → (2↑𝑥) ∥ (2↑𝑀)) |
72 | 16, 10, 70, 71 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (2↑𝑥) ∥ (2↑𝑀)) |
73 | | dvdstr 15018 |
. . . . . . . . . . . . . . . . . 18
⊢
(((2↑𝑥) ∈
ℤ ∧ (2↑𝑀)
∈ ℤ ∧ (𝑁
− (𝑁 mod
(2↑𝑀))) ∈
ℤ) → (((2↑𝑥) ∥ (2↑𝑀) ∧ (2↑𝑀) ∥ (𝑁 − (𝑁 mod (2↑𝑀)))) → (2↑𝑥) ∥ (𝑁 − (𝑁 mod (2↑𝑀))))) |
74 | 55, 47, 51, 73 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (((2↑𝑥) ∥ (2↑𝑀) ∧ (2↑𝑀) ∥ (𝑁 − (𝑁 mod (2↑𝑀)))) → (2↑𝑥) ∥ (𝑁 − (𝑁 mod (2↑𝑀))))) |
75 | 72, 54, 74 | mp2and 715 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (2↑𝑥) ∥ (𝑁 − (𝑁 mod (2↑𝑀)))) |
76 | | dvdsval2 14986 |
. . . . . . . . . . . . . . . . 17
⊢
(((2↑𝑥) ∈
ℤ ∧ (2↑𝑥)
≠ 0 ∧ (𝑁 −
(𝑁 mod (2↑𝑀))) ∈ ℤ) →
((2↑𝑥) ∥ (𝑁 − (𝑁 mod (2↑𝑀))) ↔ ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)) ∈ ℤ)) |
77 | 55, 63, 51, 76 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → ((2↑𝑥) ∥ (𝑁 − (𝑁 mod (2↑𝑀))) ↔ ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)) ∈ ℤ)) |
78 | 75, 77 | mpbid 222 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)) ∈ ℤ) |
79 | | dvdscmulr 15010 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℤ ∧ ((𝑁
− (𝑁 mod
(2↑𝑀))) /
(2↑𝑥)) ∈ ℤ
∧ ((2↑𝑥) ∈
ℤ ∧ (2↑𝑥)
≠ 0)) → (((2↑𝑥) · 2) ∥ ((2↑𝑥) · ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥))) ↔ 2 ∥ ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)))) |
80 | 16, 78, 55, 63, 79 | syl112anc 1330 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (((2↑𝑥) · 2) ∥ ((2↑𝑥) · ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥))) ↔ 2 ∥ ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)))) |
81 | 65, 80 | mpbid 222 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → 2 ∥ ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥))) |
82 | 22 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (𝑁 mod (2↑𝑀)) ∈ ℂ) |
83 | 9 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → 𝑁 ∈ ℂ) |
84 | 82, 83 | pncan3d 10395 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → ((𝑁 mod (2↑𝑀)) + (𝑁 − (𝑁 mod (2↑𝑀)))) = 𝑁) |
85 | 84 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (((𝑁 mod (2↑𝑀)) + (𝑁 − (𝑁 mod (2↑𝑀)))) / (2↑𝑥)) = (𝑁 / (2↑𝑥))) |
86 | 82, 60, 61, 63 | divdird 10839 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (((𝑁 mod (2↑𝑀)) + (𝑁 − (𝑁 mod (2↑𝑀)))) / (2↑𝑥)) = (((𝑁 mod (2↑𝑀)) / (2↑𝑥)) + ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)))) |
87 | 85, 86 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (𝑁 / (2↑𝑥)) = (((𝑁 mod (2↑𝑀)) / (2↑𝑥)) + ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)))) |
88 | 87 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (⌊‘(𝑁 / (2↑𝑥))) = (⌊‘(((𝑁 mod (2↑𝑀)) / (2↑𝑥)) + ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥))))) |
89 | | fladdz 12626 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 mod (2↑𝑀)) / (2↑𝑥)) ∈ ℝ ∧ ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)) ∈ ℤ) →
(⌊‘(((𝑁 mod
(2↑𝑀)) / (2↑𝑥)) + ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)))) = ((⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) + ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)))) |
90 | 24, 78, 89 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (⌊‘(((𝑁 mod (2↑𝑀)) / (2↑𝑥)) + ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)))) = ((⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) + ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)))) |
91 | 88, 90 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (⌊‘(𝑁 / (2↑𝑥))) = ((⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) + ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)))) |
92 | 91 | oveq1d 6665 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → ((⌊‘(𝑁 / (2↑𝑥))) − (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))) = (((⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) + ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥))) − (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))))) |
93 | 25 | zcnd 11483 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) ∈ ℂ) |
94 | 78 | zcnd 11483 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)) ∈ ℂ) |
95 | 93, 94 | pncan2d 10394 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (((⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) + ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥))) − (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))) = ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥))) |
96 | 92, 95 | eqtrd 2656 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → ((⌊‘(𝑁 / (2↑𝑥))) − (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))) = ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥))) |
97 | 81, 96 | breqtrrd 4681 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → 2 ∥ ((⌊‘(𝑁 / (2↑𝑥))) − (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))))) |
98 | | dvdssub2 15023 |
. . . . . . . . . . . 12
⊢ (((2
∈ ℤ ∧ (⌊‘(𝑁 / (2↑𝑥))) ∈ ℤ ∧
(⌊‘((𝑁 mod
(2↑𝑀)) / (2↑𝑥))) ∈ ℤ) ∧ 2
∥ ((⌊‘(𝑁
/ (2↑𝑥))) −
(⌊‘((𝑁 mod
(2↑𝑀)) / (2↑𝑥))))) → (2 ∥
(⌊‘(𝑁 /
(2↑𝑥))) ↔ 2
∥ (⌊‘((𝑁
mod (2↑𝑀)) /
(2↑𝑥))))) |
99 | 16, 21, 25, 97, 98 | syl31anc 1329 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (2 ∥ (⌊‘(𝑁 / (2↑𝑥))) ↔ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))))) |
100 | 99 | notbid 308 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (¬ 2 ∥
(⌊‘(𝑁 /
(2↑𝑥))) ↔ ¬ 2
∥ (⌊‘((𝑁
mod (2↑𝑀)) /
(2↑𝑥))))) |
101 | 12, 14, 100 | 3bitr3d 298 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → ((𝑥 ∈ (bits‘𝑁) ∧ 𝑥 < 𝑀) ↔ ¬ 2 ∥
(⌊‘((𝑁 mod
(2↑𝑀)) / (2↑𝑥))))) |
102 | | dvds0 14997 |
. . . . . . . . . . . . 13
⊢ (2 ∈
ℤ → 2 ∥ 0) |
103 | 15, 102 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ 2 ∥
0 |
104 | 1 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → 𝑁 ∈ ℤ) |
105 | 104 | zred 11482 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → 𝑁 ∈ ℝ) |
106 | | 2rp 11837 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℝ+ |
107 | 106 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → 2 ∈
ℝ+) |
108 | 32 | nn0zd 11480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) → 𝑀 ∈ ℤ) |
109 | 108 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → 𝑀 ∈ ℤ) |
110 | 107, 109 | rpexpcld 13032 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → (2↑𝑀) ∈
ℝ+) |
111 | 105, 110 | modcld 12674 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → (𝑁 mod (2↑𝑀)) ∈ ℝ) |
112 | | simplr 792 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → 𝑥 ∈ ℕ0) |
113 | 112 | nn0zd 11480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → 𝑥 ∈ ℤ) |
114 | 107, 113 | rpexpcld 13032 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → (2↑𝑥) ∈
ℝ+) |
115 | 6 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → (𝑁 mod (2↑𝑀)) ∈
ℕ0) |
116 | 115 | nn0ge0d 11354 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → 0 ≤ (𝑁 mod (2↑𝑀))) |
117 | 111, 114,
116 | divge0d 11912 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → 0 ≤ ((𝑁 mod (2↑𝑀)) / (2↑𝑥))) |
118 | 110 | rpred 11872 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → (2↑𝑀) ∈ ℝ) |
119 | 114 | rpred 11872 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → (2↑𝑥) ∈ ℝ) |
120 | | modlt 12679 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℝ ∧
(2↑𝑀) ∈
ℝ+) → (𝑁 mod (2↑𝑀)) < (2↑𝑀)) |
121 | 105, 110,
120 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → (𝑁 mod (2↑𝑀)) < (2↑𝑀)) |
122 | 107 | rpred 11872 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → 2 ∈ ℝ) |
123 | | 1le2 11241 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ≤
2 |
124 | 123 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → 1 ≤ 2) |
125 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → ¬ 𝑥 < 𝑀) |
126 | 109 | zred 11482 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → 𝑀 ∈ ℝ) |
127 | 112 | nn0red 11352 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → 𝑥 ∈ ℝ) |
128 | 126, 127 | lenltd 10183 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → (𝑀 ≤ 𝑥 ↔ ¬ 𝑥 < 𝑀)) |
129 | 125, 128 | mpbird 247 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → 𝑀 ≤ 𝑥) |
130 | | eluz2 11693 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈
(ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥)) |
131 | 109, 113,
129, 130 | syl3anbrc 1246 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → 𝑥 ∈ (ℤ≥‘𝑀)) |
132 | 122, 124,
131 | leexp2ad 13041 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → (2↑𝑀) ≤ (2↑𝑥)) |
133 | 111, 118,
119, 121, 132 | ltletrd 10197 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → (𝑁 mod (2↑𝑀)) < (2↑𝑥)) |
134 | 114 | rpcnd 11874 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → (2↑𝑥) ∈ ℂ) |
135 | 134 | mulid1d 10057 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → ((2↑𝑥) · 1) = (2↑𝑥)) |
136 | 133, 135 | breqtrrd 4681 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → (𝑁 mod (2↑𝑀)) < ((2↑𝑥) · 1)) |
137 | | 1red 10055 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → 1 ∈ ℝ) |
138 | 111, 137,
114 | ltdivmuld 11923 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → (((𝑁 mod (2↑𝑀)) / (2↑𝑥)) < 1 ↔ (𝑁 mod (2↑𝑀)) < ((2↑𝑥) · 1))) |
139 | 136, 138 | mpbird 247 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → ((𝑁 mod (2↑𝑀)) / (2↑𝑥)) < 1) |
140 | | 1e0p1 11552 |
. . . . . . . . . . . . . 14
⊢ 1 = (0 +
1) |
141 | 139, 140 | syl6breq 4694 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → ((𝑁 mod (2↑𝑀)) / (2↑𝑥)) < (0 + 1)) |
142 | 111, 114 | rerpdivcld 11903 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → ((𝑁 mod (2↑𝑀)) / (2↑𝑥)) ∈ ℝ) |
143 | | 0z 11388 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℤ |
144 | | flbi 12617 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 mod (2↑𝑀)) / (2↑𝑥)) ∈ ℝ ∧ 0 ∈ ℤ)
→ ((⌊‘((𝑁
mod (2↑𝑀)) /
(2↑𝑥))) = 0 ↔ (0
≤ ((𝑁 mod (2↑𝑀)) / (2↑𝑥)) ∧ ((𝑁 mod (2↑𝑀)) / (2↑𝑥)) < (0 + 1)))) |
145 | 142, 143,
144 | sylancl 694 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → ((⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) = 0 ↔ (0 ≤ ((𝑁 mod (2↑𝑀)) / (2↑𝑥)) ∧ ((𝑁 mod (2↑𝑀)) / (2↑𝑥)) < (0 + 1)))) |
146 | 117, 141,
145 | mpbir2and 957 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) = 0) |
147 | 103, 146 | syl5breqr 4691 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))) |
148 | 125 | intnand 962 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → ¬ (𝑥 ∈ (bits‘𝑁) ∧ 𝑥 < 𝑀)) |
149 | 147, 148 | 2thd 255 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → (2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) ↔ ¬ (𝑥 ∈ (bits‘𝑁) ∧ 𝑥 < 𝑀))) |
150 | 149 | con2bid 344 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → ((𝑥 ∈ (bits‘𝑁) ∧ 𝑥 < 𝑀) ↔ ¬ 2 ∥
(⌊‘((𝑁 mod
(2↑𝑀)) / (2↑𝑥))))) |
151 | 101, 150 | pm2.61dan 832 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) → ((𝑥 ∈ (bits‘𝑁) ∧ 𝑥 < 𝑀) ↔ ¬ 2 ∥
(⌊‘((𝑁 mod
(2↑𝑀)) / (2↑𝑥))))) |
152 | 108 | biantrurd 529 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) → ((𝑥 ∈ (bits‘𝑁) ∧ 𝑥 < 𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑥 ∈ (bits‘𝑁) ∧ 𝑥 < 𝑀)))) |
153 | 151, 152 | bitr3d 270 |
. . . . . . 7
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) → (¬ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) ↔ (𝑀 ∈ ℤ ∧ (𝑥 ∈ (bits‘𝑁) ∧ 𝑥 < 𝑀)))) |
154 | | an12 838 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ (𝑥 ∈ (bits‘𝑁) ∧ 𝑥 < 𝑀)) ↔ (𝑥 ∈ (bits‘𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑥 < 𝑀))) |
155 | 153, 154 | syl6bb 276 |
. . . . . 6
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) → (¬ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) ↔ (𝑥 ∈ (bits‘𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑥 < 𝑀)))) |
156 | 155 | pm5.32da 673 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
→ ((𝑥 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))) ↔ (𝑥 ∈ ℕ0 ∧ (𝑥 ∈ (bits‘𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑥 < 𝑀))))) |
157 | 8, 156 | bitr3d 270 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
→ (((𝑁 mod
(2↑𝑀)) ∈ ℤ
∧ (𝑥 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))))) ↔ (𝑥 ∈ ℕ0 ∧ (𝑥 ∈ (bits‘𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑥 < 𝑀))))) |
158 | | 3anass 1042 |
. . . 4
⊢ (((𝑁 mod (2↑𝑀)) ∈ ℤ ∧ 𝑥 ∈ ℕ0 ∧ ¬ 2
∥ (⌊‘((𝑁
mod (2↑𝑀)) /
(2↑𝑥)))) ↔
((𝑁 mod (2↑𝑀)) ∈ ℤ ∧ (𝑥 ∈ ℕ0
∧ ¬ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))))) |
159 | | elfzo2 12473 |
. . . . . . 7
⊢ (𝑥 ∈ (0..^𝑀) ↔ (𝑥 ∈ (ℤ≥‘0)
∧ 𝑀 ∈ ℤ
∧ 𝑥 < 𝑀)) |
160 | | elnn0uz 11725 |
. . . . . . . 8
⊢ (𝑥 ∈ ℕ0
↔ 𝑥 ∈
(ℤ≥‘0)) |
161 | 160 | 3anbi1i 1253 |
. . . . . . 7
⊢ ((𝑥 ∈ ℕ0
∧ 𝑀 ∈ ℤ
∧ 𝑥 < 𝑀) ↔ (𝑥 ∈ (ℤ≥‘0)
∧ 𝑀 ∈ ℤ
∧ 𝑥 < 𝑀)) |
162 | | 3anass 1042 |
. . . . . . 7
⊢ ((𝑥 ∈ ℕ0
∧ 𝑀 ∈ ℤ
∧ 𝑥 < 𝑀) ↔ (𝑥 ∈ ℕ0 ∧ (𝑀 ∈ ℤ ∧ 𝑥 < 𝑀))) |
163 | 159, 161,
162 | 3bitr2i 288 |
. . . . . 6
⊢ (𝑥 ∈ (0..^𝑀) ↔ (𝑥 ∈ ℕ0 ∧ (𝑀 ∈ ℤ ∧ 𝑥 < 𝑀))) |
164 | 163 | anbi2i 730 |
. . . . 5
⊢ ((𝑥 ∈ (bits‘𝑁) ∧ 𝑥 ∈ (0..^𝑀)) ↔ (𝑥 ∈ (bits‘𝑁) ∧ (𝑥 ∈ ℕ0 ∧ (𝑀 ∈ ℤ ∧ 𝑥 < 𝑀)))) |
165 | | an12 838 |
. . . . 5
⊢ ((𝑥 ∈ (bits‘𝑁) ∧ (𝑥 ∈ ℕ0 ∧ (𝑀 ∈ ℤ ∧ 𝑥 < 𝑀))) ↔ (𝑥 ∈ ℕ0 ∧ (𝑥 ∈ (bits‘𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑥 < 𝑀)))) |
166 | 164, 165 | bitri 264 |
. . . 4
⊢ ((𝑥 ∈ (bits‘𝑁) ∧ 𝑥 ∈ (0..^𝑀)) ↔ (𝑥 ∈ ℕ0 ∧ (𝑥 ∈ (bits‘𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑥 < 𝑀)))) |
167 | 157, 158,
166 | 3bitr4g 303 |
. . 3
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
→ (((𝑁 mod
(2↑𝑀)) ∈ ℤ
∧ 𝑥 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))) ↔ (𝑥 ∈ (bits‘𝑁) ∧ 𝑥 ∈ (0..^𝑀)))) |
168 | | bitsval 15146 |
. . 3
⊢ (𝑥 ∈ (bits‘(𝑁 mod (2↑𝑀))) ↔ ((𝑁 mod (2↑𝑀)) ∈ ℤ ∧ 𝑥 ∈ ℕ0 ∧ ¬ 2
∥ (⌊‘((𝑁
mod (2↑𝑀)) /
(2↑𝑥))))) |
169 | | elin 3796 |
. . 3
⊢ (𝑥 ∈ ((bits‘𝑁) ∩ (0..^𝑀)) ↔ (𝑥 ∈ (bits‘𝑁) ∧ 𝑥 ∈ (0..^𝑀))) |
170 | 167, 168,
169 | 3bitr4g 303 |
. 2
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
→ (𝑥 ∈
(bits‘(𝑁 mod
(2↑𝑀))) ↔ 𝑥 ∈ ((bits‘𝑁) ∩ (0..^𝑀)))) |
171 | 170 | eqrdv 2620 |
1
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
→ (bits‘(𝑁 mod
(2↑𝑀))) =
((bits‘𝑁) ∩
(0..^𝑀))) |