Step | Hyp | Ref
| Expression |
1 | | simpl 485 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
→ 𝑁 ∈
ℤ) |
2 | | 2nn 11704 |
. . . . . . . . . 10
⊢ 2 ∈
ℕ |
3 | 2 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
→ 2 ∈ ℕ) |
4 | | simpr 487 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
→ 𝑀 ∈
ℕ0) |
5 | 3, 4 | nnexpcld 13600 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
→ (2↑𝑀) ∈
ℕ) |
6 | 1, 5 | zmodcld 13254 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
→ (𝑁 mod (2↑𝑀)) ∈
ℕ0) |
7 | 6 | nn0zd 12079 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
→ (𝑁 mod (2↑𝑀)) ∈
ℤ) |
8 | 7 | biantrurd 535 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
→ ((𝑥 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))) ↔ ((𝑁 mod (2↑𝑀)) ∈ ℤ ∧ (𝑥 ∈ ℕ0 ∧ ¬ 2
∥ (⌊‘((𝑁
mod (2↑𝑀)) /
(2↑𝑥))))))) |
9 | 1 | ad2antrr 724 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → 𝑁 ∈ ℤ) |
10 | | simplr 767 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → 𝑥 ∈ ℕ0) |
11 | | bitsval2 15768 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝑥 ∈ ℕ0)
→ (𝑥 ∈
(bits‘𝑁) ↔ ¬
2 ∥ (⌊‘(𝑁
/ (2↑𝑥))))) |
12 | 9, 10, 11 | syl2anc 586 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (𝑥 ∈ (bits‘𝑁) ↔ ¬ 2 ∥
(⌊‘(𝑁 /
(2↑𝑥))))) |
13 | | simpr 487 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → 𝑥 < 𝑀) |
14 | 13 | biantrud 534 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (𝑥 ∈ (bits‘𝑁) ↔ (𝑥 ∈ (bits‘𝑁) ∧ 𝑥 < 𝑀))) |
15 | | 2z 12008 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℤ |
16 | 15 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → 2 ∈ ℤ) |
17 | 9 | zred 12081 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → 𝑁 ∈ ℝ) |
18 | 2 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → 2 ∈ ℕ) |
19 | 18, 10 | nnexpcld 13600 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (2↑𝑥) ∈ ℕ) |
20 | 17, 19 | nndivred 11685 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (𝑁 / (2↑𝑥)) ∈ ℝ) |
21 | 20 | flcld 13162 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (⌊‘(𝑁 / (2↑𝑥))) ∈ ℤ) |
22 | 7 | ad2antrr 724 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (𝑁 mod (2↑𝑀)) ∈ ℤ) |
23 | 22 | zred 12081 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (𝑁 mod (2↑𝑀)) ∈ ℝ) |
24 | 23, 19 | nndivred 11685 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → ((𝑁 mod (2↑𝑀)) / (2↑𝑥)) ∈ ℝ) |
25 | 24 | flcld 13162 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) ∈ ℤ) |
26 | | 2cnd 11709 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → 2 ∈ ℂ) |
27 | 26, 10 | expp1d 13505 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (2↑(𝑥 + 1)) = ((2↑𝑥) · 2)) |
28 | | 1nn0 11907 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 ∈
ℕ0 |
29 | 28 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → 1 ∈
ℕ0) |
30 | 10, 29 | nn0addcld 11953 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (𝑥 + 1) ∈
ℕ0) |
31 | 30 | nn0zd 12079 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (𝑥 + 1) ∈ ℤ) |
32 | | simplr 767 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) → 𝑀 ∈
ℕ0) |
33 | 32 | adantr 483 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → 𝑀 ∈
ℕ0) |
34 | 33 | nn0zd 12079 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → 𝑀 ∈ ℤ) |
35 | | nn0ltp1le 12034 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (𝑥 < 𝑀 ↔ (𝑥 + 1) ≤ 𝑀)) |
36 | 10, 33, 35 | syl2anc 586 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (𝑥 < 𝑀 ↔ (𝑥 + 1) ≤ 𝑀)) |
37 | 13, 36 | mpbid 234 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (𝑥 + 1) ≤ 𝑀) |
38 | | eluz2 12243 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑀 ∈
(ℤ≥‘(𝑥 + 1)) ↔ ((𝑥 + 1) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑥 + 1) ≤ 𝑀)) |
39 | 31, 34, 37, 38 | syl3anbrc 1339 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → 𝑀 ∈ (ℤ≥‘(𝑥 + 1))) |
40 | | dvdsexp 15671 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2
∈ ℤ ∧ (𝑥 +
1) ∈ ℕ0 ∧ 𝑀 ∈ (ℤ≥‘(𝑥 + 1))) → (2↑(𝑥 + 1)) ∥ (2↑𝑀)) |
41 | 16, 30, 39, 40 | syl3anc 1367 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (2↑(𝑥 + 1)) ∥ (2↑𝑀)) |
42 | 27, 41 | eqbrtrrd 5083 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → ((2↑𝑥) · 2) ∥ (2↑𝑀)) |
43 | 5 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (2↑𝑀) ∈ ℕ) |
44 | 43 | nnrpd 12423 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (2↑𝑀) ∈
ℝ+) |
45 | | moddifz 13245 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℝ ∧
(2↑𝑀) ∈
ℝ+) → ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ∈ ℤ) |
46 | 17, 44, 45 | syl2anc 586 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ∈ ℤ) |
47 | 43 | nnzd 12080 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (2↑𝑀) ∈ ℤ) |
48 | | 2ne0 11735 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ≠
0 |
49 | 48 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → 2 ≠ 0) |
50 | 26, 49, 34 | expne0d 13510 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (2↑𝑀) ≠ 0) |
51 | 9, 22 | zsubcld 12086 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (𝑁 − (𝑁 mod (2↑𝑀))) ∈ ℤ) |
52 | | dvdsval2 15604 |
. . . . . . . . . . . . . . . . . 18
⊢
(((2↑𝑀) ∈
ℤ ∧ (2↑𝑀)
≠ 0 ∧ (𝑁 −
(𝑁 mod (2↑𝑀))) ∈ ℤ) →
((2↑𝑀) ∥ (𝑁 − (𝑁 mod (2↑𝑀))) ↔ ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ∈ ℤ)) |
53 | 47, 50, 51, 52 | syl3anc 1367 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → ((2↑𝑀) ∥ (𝑁 − (𝑁 mod (2↑𝑀))) ↔ ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑀)) ∈ ℤ)) |
54 | 46, 53 | mpbird 259 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (2↑𝑀) ∥ (𝑁 − (𝑁 mod (2↑𝑀)))) |
55 | 19 | nnzd 12080 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (2↑𝑥) ∈ ℤ) |
56 | 55, 16 | zmulcld 12087 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → ((2↑𝑥) · 2) ∈
ℤ) |
57 | | dvdstr 15640 |
. . . . . . . . . . . . . . . . 17
⊢
((((2↑𝑥)
· 2) ∈ ℤ ∧ (2↑𝑀) ∈ ℤ ∧ (𝑁 − (𝑁 mod (2↑𝑀))) ∈ ℤ) → ((((2↑𝑥) · 2) ∥
(2↑𝑀) ∧
(2↑𝑀) ∥ (𝑁 − (𝑁 mod (2↑𝑀)))) → ((2↑𝑥) · 2) ∥ (𝑁 − (𝑁 mod (2↑𝑀))))) |
58 | 56, 47, 51, 57 | syl3anc 1367 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → ((((2↑𝑥) · 2) ∥ (2↑𝑀) ∧ (2↑𝑀) ∥ (𝑁 − (𝑁 mod (2↑𝑀)))) → ((2↑𝑥) · 2) ∥ (𝑁 − (𝑁 mod (2↑𝑀))))) |
59 | 42, 54, 58 | mp2and 697 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → ((2↑𝑥) · 2) ∥ (𝑁 − (𝑁 mod (2↑𝑀)))) |
60 | 51 | zcnd 12082 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (𝑁 − (𝑁 mod (2↑𝑀))) ∈ ℂ) |
61 | 19 | nncnd 11648 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (2↑𝑥) ∈ ℂ) |
62 | 10 | nn0zd 12079 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → 𝑥 ∈ ℤ) |
63 | 26, 49, 62 | expne0d 13510 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (2↑𝑥) ≠ 0) |
64 | 60, 61, 63 | divcan2d 11412 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → ((2↑𝑥) · ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥))) = (𝑁 − (𝑁 mod (2↑𝑀)))) |
65 | 59, 64 | breqtrrd 5087 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → ((2↑𝑥) · 2) ∥ ((2↑𝑥) · ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)))) |
66 | 10 | nn0red 11950 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → 𝑥 ∈ ℝ) |
67 | 33 | nn0red 11950 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → 𝑀 ∈ ℝ) |
68 | 66, 67, 13 | ltled 10782 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → 𝑥 ≤ 𝑀) |
69 | | eluz2 12243 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑀 ∈
(ℤ≥‘𝑥) ↔ (𝑥 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑥 ≤ 𝑀)) |
70 | 62, 34, 68, 69 | syl3anbrc 1339 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → 𝑀 ∈ (ℤ≥‘𝑥)) |
71 | | dvdsexp 15671 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2
∈ ℤ ∧ 𝑥
∈ ℕ0 ∧ 𝑀 ∈ (ℤ≥‘𝑥)) → (2↑𝑥) ∥ (2↑𝑀)) |
72 | 16, 10, 70, 71 | syl3anc 1367 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (2↑𝑥) ∥ (2↑𝑀)) |
73 | | dvdstr 15640 |
. . . . . . . . . . . . . . . . . 18
⊢
(((2↑𝑥) ∈
ℤ ∧ (2↑𝑀)
∈ ℤ ∧ (𝑁
− (𝑁 mod
(2↑𝑀))) ∈
ℤ) → (((2↑𝑥) ∥ (2↑𝑀) ∧ (2↑𝑀) ∥ (𝑁 − (𝑁 mod (2↑𝑀)))) → (2↑𝑥) ∥ (𝑁 − (𝑁 mod (2↑𝑀))))) |
74 | 55, 47, 51, 73 | syl3anc 1367 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (((2↑𝑥) ∥ (2↑𝑀) ∧ (2↑𝑀) ∥ (𝑁 − (𝑁 mod (2↑𝑀)))) → (2↑𝑥) ∥ (𝑁 − (𝑁 mod (2↑𝑀))))) |
75 | 72, 54, 74 | mp2and 697 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (2↑𝑥) ∥ (𝑁 − (𝑁 mod (2↑𝑀)))) |
76 | | dvdsval2 15604 |
. . . . . . . . . . . . . . . . 17
⊢
(((2↑𝑥) ∈
ℤ ∧ (2↑𝑥)
≠ 0 ∧ (𝑁 −
(𝑁 mod (2↑𝑀))) ∈ ℤ) →
((2↑𝑥) ∥ (𝑁 − (𝑁 mod (2↑𝑀))) ↔ ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)) ∈ ℤ)) |
77 | 55, 63, 51, 76 | syl3anc 1367 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → ((2↑𝑥) ∥ (𝑁 − (𝑁 mod (2↑𝑀))) ↔ ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)) ∈ ℤ)) |
78 | 75, 77 | mpbid 234 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)) ∈ ℤ) |
79 | | dvdscmulr 15632 |
. . . . . . . . . . . . . . 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 1370 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (((2↑𝑥) · 2) ∥ ((2↑𝑥) · ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥))) ↔ 2 ∥ ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)))) |
81 | 65, 80 | mpbid 234 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → 2 ∥ ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥))) |
82 | 25 | zcnd 12082 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) ∈ ℂ) |
83 | 78 | zcnd 12082 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)) ∈ ℂ) |
84 | 22 | zcnd 12082 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (𝑁 mod (2↑𝑀)) ∈ ℂ) |
85 | 9 | zcnd 12082 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → 𝑁 ∈ ℂ) |
86 | 84, 85 | pncan3d 10994 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → ((𝑁 mod (2↑𝑀)) + (𝑁 − (𝑁 mod (2↑𝑀)))) = 𝑁) |
87 | 86 | oveq1d 7165 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (((𝑁 mod (2↑𝑀)) + (𝑁 − (𝑁 mod (2↑𝑀)))) / (2↑𝑥)) = (𝑁 / (2↑𝑥))) |
88 | 84, 60, 61, 63 | divdird 11448 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (((𝑁 mod (2↑𝑀)) + (𝑁 − (𝑁 mod (2↑𝑀)))) / (2↑𝑥)) = (((𝑁 mod (2↑𝑀)) / (2↑𝑥)) + ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)))) |
89 | 87, 88 | eqtr3d 2858 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (𝑁 / (2↑𝑥)) = (((𝑁 mod (2↑𝑀)) / (2↑𝑥)) + ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)))) |
90 | 89 | fveq2d 6669 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (⌊‘(𝑁 / (2↑𝑥))) = (⌊‘(((𝑁 mod (2↑𝑀)) / (2↑𝑥)) + ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥))))) |
91 | | fladdz 13189 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 mod (2↑𝑀)) / (2↑𝑥)) ∈ ℝ ∧ ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)) ∈ ℤ) →
(⌊‘(((𝑁 mod
(2↑𝑀)) / (2↑𝑥)) + ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)))) = ((⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) + ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)))) |
92 | 24, 78, 91 | syl2anc 586 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (⌊‘(((𝑁 mod (2↑𝑀)) / (2↑𝑥)) + ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)))) = ((⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) + ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)))) |
93 | 90, 92 | eqtrd 2856 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (⌊‘(𝑁 / (2↑𝑥))) = ((⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) + ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥)))) |
94 | 82, 83, 93 | mvrladdd 11047 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → ((⌊‘(𝑁 / (2↑𝑥))) − (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))) = ((𝑁 − (𝑁 mod (2↑𝑀))) / (2↑𝑥))) |
95 | 81, 94 | breqtrrd 5087 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → 2 ∥ ((⌊‘(𝑁 / (2↑𝑥))) − (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))))) |
96 | | dvdssub2 15645 |
. . . . . . . . . . . 12
⊢ (((2
∈ ℤ ∧ (⌊‘(𝑁 / (2↑𝑥))) ∈ ℤ ∧
(⌊‘((𝑁 mod
(2↑𝑀)) / (2↑𝑥))) ∈ ℤ) ∧ 2
∥ ((⌊‘(𝑁
/ (2↑𝑥))) −
(⌊‘((𝑁 mod
(2↑𝑀)) / (2↑𝑥))))) → (2 ∥
(⌊‘(𝑁 /
(2↑𝑥))) ↔ 2
∥ (⌊‘((𝑁
mod (2↑𝑀)) /
(2↑𝑥))))) |
97 | 16, 21, 25, 95, 96 | syl31anc 1369 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (2 ∥ (⌊‘(𝑁 / (2↑𝑥))) ↔ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))))) |
98 | 97 | notbid 320 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → (¬ 2 ∥
(⌊‘(𝑁 /
(2↑𝑥))) ↔ ¬ 2
∥ (⌊‘((𝑁
mod (2↑𝑀)) /
(2↑𝑥))))) |
99 | 12, 14, 98 | 3bitr3d 311 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ 𝑥 < 𝑀) → ((𝑥 ∈ (bits‘𝑁) ∧ 𝑥 < 𝑀) ↔ ¬ 2 ∥
(⌊‘((𝑁 mod
(2↑𝑀)) / (2↑𝑥))))) |
100 | | z0even 15710 |
. . . . . . . . . . . 12
⊢ 2 ∥
0 |
101 | 1 | ad2antrr 724 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → 𝑁 ∈ ℤ) |
102 | 101 | zred 12081 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → 𝑁 ∈ ℝ) |
103 | | 2rp 12388 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℝ+ |
104 | 103 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → 2 ∈
ℝ+) |
105 | 32 | nn0zd 12079 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) → 𝑀 ∈ ℤ) |
106 | 105 | adantr 483 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → 𝑀 ∈ ℤ) |
107 | 104, 106 | rpexpcld 13602 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → (2↑𝑀) ∈
ℝ+) |
108 | 102, 107 | modcld 13237 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → (𝑁 mod (2↑𝑀)) ∈ ℝ) |
109 | | simplr 767 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → 𝑥 ∈ ℕ0) |
110 | 109 | nn0zd 12079 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → 𝑥 ∈ ℤ) |
111 | 104, 110 | rpexpcld 13602 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → (2↑𝑥) ∈
ℝ+) |
112 | 6 | ad2antrr 724 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → (𝑁 mod (2↑𝑀)) ∈
ℕ0) |
113 | 112 | nn0ge0d 11952 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → 0 ≤ (𝑁 mod (2↑𝑀))) |
114 | 108, 111,
113 | divge0d 12465 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → 0 ≤ ((𝑁 mod (2↑𝑀)) / (2↑𝑥))) |
115 | 107 | rpred 12425 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → (2↑𝑀) ∈ ℝ) |
116 | 111 | rpred 12425 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → (2↑𝑥) ∈ ℝ) |
117 | | modlt 13242 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℝ ∧
(2↑𝑀) ∈
ℝ+) → (𝑁 mod (2↑𝑀)) < (2↑𝑀)) |
118 | 102, 107,
117 | syl2anc 586 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → (𝑁 mod (2↑𝑀)) < (2↑𝑀)) |
119 | 104 | rpred 12425 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → 2 ∈ ℝ) |
120 | | 1le2 11840 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ≤
2 |
121 | 120 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → 1 ≤ 2) |
122 | 106 | zred 12081 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → 𝑀 ∈ ℝ) |
123 | 109 | nn0red 11950 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → 𝑥 ∈ ℝ) |
124 | | simpr 487 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → ¬ 𝑥 < 𝑀) |
125 | 122, 123,
124 | nltled 10784 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → 𝑀 ≤ 𝑥) |
126 | | eluz2 12243 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈
(ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥)) |
127 | 106, 110,
125, 126 | syl3anbrc 1339 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → 𝑥 ∈ (ℤ≥‘𝑀)) |
128 | 119, 121,
127 | leexp2ad 13611 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → (2↑𝑀) ≤ (2↑𝑥)) |
129 | 108, 115,
116, 118, 128 | ltletrd 10794 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → (𝑁 mod (2↑𝑀)) < (2↑𝑥)) |
130 | 111 | rpcnd 12427 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → (2↑𝑥) ∈ ℂ) |
131 | 130 | mulid1d 10652 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → ((2↑𝑥) · 1) = (2↑𝑥)) |
132 | 129, 131 | breqtrrd 5087 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → (𝑁 mod (2↑𝑀)) < ((2↑𝑥) · 1)) |
133 | | 1red 10636 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → 1 ∈ ℝ) |
134 | 108, 133,
111 | ltdivmuld 12476 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → (((𝑁 mod (2↑𝑀)) / (2↑𝑥)) < 1 ↔ (𝑁 mod (2↑𝑀)) < ((2↑𝑥) · 1))) |
135 | 132, 134 | mpbird 259 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → ((𝑁 mod (2↑𝑀)) / (2↑𝑥)) < 1) |
136 | | 1e0p1 12134 |
. . . . . . . . . . . . . 14
⊢ 1 = (0 +
1) |
137 | 135, 136 | breqtrdi 5100 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → ((𝑁 mod (2↑𝑀)) / (2↑𝑥)) < (0 + 1)) |
138 | 108, 111 | rerpdivcld 12456 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → ((𝑁 mod (2↑𝑀)) / (2↑𝑥)) ∈ ℝ) |
139 | | 0z 11986 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℤ |
140 | | flbi 13180 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 mod (2↑𝑀)) / (2↑𝑥)) ∈ ℝ ∧ 0 ∈ ℤ)
→ ((⌊‘((𝑁
mod (2↑𝑀)) /
(2↑𝑥))) = 0 ↔ (0
≤ ((𝑁 mod (2↑𝑀)) / (2↑𝑥)) ∧ ((𝑁 mod (2↑𝑀)) / (2↑𝑥)) < (0 + 1)))) |
141 | 138, 139,
140 | sylancl 588 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → ((⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) = 0 ↔ (0 ≤ ((𝑁 mod (2↑𝑀)) / (2↑𝑥)) ∧ ((𝑁 mod (2↑𝑀)) / (2↑𝑥)) < (0 + 1)))) |
142 | 114, 137,
141 | mpbir2and 711 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) = 0) |
143 | 100, 142 | breqtrrid 5097 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))) |
144 | 124 | intnand 491 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → ¬ (𝑥 ∈ (bits‘𝑁) ∧ 𝑥 < 𝑀)) |
145 | 143, 144 | 2thd 267 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → (2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) ↔ ¬ (𝑥 ∈ (bits‘𝑁) ∧ 𝑥 < 𝑀))) |
146 | 145 | con2bid 357 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) ∧ ¬ 𝑥 < 𝑀) → ((𝑥 ∈ (bits‘𝑁) ∧ 𝑥 < 𝑀) ↔ ¬ 2 ∥
(⌊‘((𝑁 mod
(2↑𝑀)) / (2↑𝑥))))) |
147 | 99, 146 | pm2.61dan 811 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) → ((𝑥 ∈ (bits‘𝑁) ∧ 𝑥 < 𝑀) ↔ ¬ 2 ∥
(⌊‘((𝑁 mod
(2↑𝑀)) / (2↑𝑥))))) |
148 | 105 | biantrurd 535 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) → ((𝑥 ∈ (bits‘𝑁) ∧ 𝑥 < 𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑥 ∈ (bits‘𝑁) ∧ 𝑥 < 𝑀)))) |
149 | 147, 148 | bitr3d 283 |
. . . . . . 7
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) → (¬ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) ↔ (𝑀 ∈ ℤ ∧ (𝑥 ∈ (bits‘𝑁) ∧ 𝑥 < 𝑀)))) |
150 | | an12 643 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ (𝑥 ∈ (bits‘𝑁) ∧ 𝑥 < 𝑀)) ↔ (𝑥 ∈ (bits‘𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑥 < 𝑀))) |
151 | 149, 150 | syl6bb 289 |
. . . . . 6
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
ℕ0) → (¬ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))) ↔ (𝑥 ∈ (bits‘𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑥 < 𝑀)))) |
152 | 151 | pm5.32da 581 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
→ ((𝑥 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))) ↔ (𝑥 ∈ ℕ0 ∧ (𝑥 ∈ (bits‘𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑥 < 𝑀))))) |
153 | 8, 152 | bitr3d 283 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
→ (((𝑁 mod
(2↑𝑀)) ∈ ℤ
∧ (𝑥 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥))))) ↔ (𝑥 ∈ ℕ0 ∧ (𝑥 ∈ (bits‘𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑥 < 𝑀))))) |
154 | | 3anass 1091 |
. . . 4
⊢ (((𝑁 mod (2↑𝑀)) ∈ ℤ ∧ 𝑥 ∈ ℕ0 ∧ ¬ 2
∥ (⌊‘((𝑁
mod (2↑𝑀)) /
(2↑𝑥)))) ↔
((𝑁 mod (2↑𝑀)) ∈ ℤ ∧ (𝑥 ∈ ℕ0
∧ ¬ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))))) |
155 | | elfzo2 13035 |
. . . . . . 7
⊢ (𝑥 ∈ (0..^𝑀) ↔ (𝑥 ∈ (ℤ≥‘0)
∧ 𝑀 ∈ ℤ
∧ 𝑥 < 𝑀)) |
156 | | elnn0uz 12277 |
. . . . . . . 8
⊢ (𝑥 ∈ ℕ0
↔ 𝑥 ∈
(ℤ≥‘0)) |
157 | 156 | 3anbi1i 1153 |
. . . . . . 7
⊢ ((𝑥 ∈ ℕ0
∧ 𝑀 ∈ ℤ
∧ 𝑥 < 𝑀) ↔ (𝑥 ∈ (ℤ≥‘0)
∧ 𝑀 ∈ ℤ
∧ 𝑥 < 𝑀)) |
158 | | 3anass 1091 |
. . . . . . 7
⊢ ((𝑥 ∈ ℕ0
∧ 𝑀 ∈ ℤ
∧ 𝑥 < 𝑀) ↔ (𝑥 ∈ ℕ0 ∧ (𝑀 ∈ ℤ ∧ 𝑥 < 𝑀))) |
159 | 155, 157,
158 | 3bitr2i 301 |
. . . . . 6
⊢ (𝑥 ∈ (0..^𝑀) ↔ (𝑥 ∈ ℕ0 ∧ (𝑀 ∈ ℤ ∧ 𝑥 < 𝑀))) |
160 | 159 | anbi2i 624 |
. . . . 5
⊢ ((𝑥 ∈ (bits‘𝑁) ∧ 𝑥 ∈ (0..^𝑀)) ↔ (𝑥 ∈ (bits‘𝑁) ∧ (𝑥 ∈ ℕ0 ∧ (𝑀 ∈ ℤ ∧ 𝑥 < 𝑀)))) |
161 | | an12 643 |
. . . . 5
⊢ ((𝑥 ∈ (bits‘𝑁) ∧ (𝑥 ∈ ℕ0 ∧ (𝑀 ∈ ℤ ∧ 𝑥 < 𝑀))) ↔ (𝑥 ∈ ℕ0 ∧ (𝑥 ∈ (bits‘𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑥 < 𝑀)))) |
162 | 160, 161 | bitri 277 |
. . . 4
⊢ ((𝑥 ∈ (bits‘𝑁) ∧ 𝑥 ∈ (0..^𝑀)) ↔ (𝑥 ∈ ℕ0 ∧ (𝑥 ∈ (bits‘𝑁) ∧ (𝑀 ∈ ℤ ∧ 𝑥 < 𝑀)))) |
163 | 153, 154,
162 | 3bitr4g 316 |
. . 3
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
→ (((𝑁 mod
(2↑𝑀)) ∈ ℤ
∧ 𝑥 ∈
ℕ0 ∧ ¬ 2 ∥ (⌊‘((𝑁 mod (2↑𝑀)) / (2↑𝑥)))) ↔ (𝑥 ∈ (bits‘𝑁) ∧ 𝑥 ∈ (0..^𝑀)))) |
164 | | bitsval 15767 |
. . 3
⊢ (𝑥 ∈ (bits‘(𝑁 mod (2↑𝑀))) ↔ ((𝑁 mod (2↑𝑀)) ∈ ℤ ∧ 𝑥 ∈ ℕ0 ∧ ¬ 2
∥ (⌊‘((𝑁
mod (2↑𝑀)) /
(2↑𝑥))))) |
165 | | elin 4169 |
. . 3
⊢ (𝑥 ∈ ((bits‘𝑁) ∩ (0..^𝑀)) ↔ (𝑥 ∈ (bits‘𝑁) ∧ 𝑥 ∈ (0..^𝑀))) |
166 | 163, 164,
165 | 3bitr4g 316 |
. 2
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
→ (𝑥 ∈
(bits‘(𝑁 mod
(2↑𝑀))) ↔ 𝑥 ∈ ((bits‘𝑁) ∩ (0..^𝑀)))) |
167 | 166 | eqrdv 2819 |
1
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
→ (bits‘(𝑁 mod
(2↑𝑀))) =
((bits‘𝑁) ∩
(0..^𝑀))) |