Proof of Theorem bitsshft
Step | Hyp | Ref
| Expression |
1 | | bitsss 15608 |
. . 3
⊢
(bits‘(𝐴
· (2↑𝑁)))
⊆ ℕ0 |
2 | | sseqin2 4112 |
. . 3
⊢
((bits‘(𝐴
· (2↑𝑁)))
⊆ ℕ0 ↔ (ℕ0 ∩
(bits‘(𝐴 ·
(2↑𝑁)))) =
(bits‘(𝐴 ·
(2↑𝑁)))) |
3 | 1, 2 | mpbi 231 |
. 2
⊢
(ℕ0 ∩ (bits‘(𝐴 · (2↑𝑁)))) = (bits‘(𝐴 · (2↑𝑁))) |
4 | | simpll 763 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → 𝐴 ∈ ℤ) |
5 | | 2nn 11558 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ |
6 | 5 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → 2 ∈ ℕ) |
7 | | simplr 765 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → 𝑁 ∈
ℕ0) |
8 | 6, 7 | nnexpcld 13456 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → (2↑𝑁) ∈ ℕ) |
9 | 8 | nnzd 11935 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → (2↑𝑁) ∈ ℤ) |
10 | | dvdsmul2 15465 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧
(2↑𝑁) ∈ ℤ)
→ (2↑𝑁) ∥
(𝐴 · (2↑𝑁))) |
11 | 4, 9, 10 | syl2anc 584 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → (2↑𝑁) ∥ (𝐴 · (2↑𝑁))) |
12 | 4, 9 | zmulcld 11942 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → (𝐴 · (2↑𝑁)) ∈ ℤ) |
13 | | bitsuz 15656 |
. . . . . . . 8
⊢ (((𝐴 · (2↑𝑁)) ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ ((2↑𝑁) ∥
(𝐴 · (2↑𝑁)) ↔ (bits‘(𝐴 · (2↑𝑁))) ⊆
(ℤ≥‘𝑁))) |
14 | 12, 7, 13 | syl2anc 584 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → ((2↑𝑁) ∥ (𝐴 · (2↑𝑁)) ↔ (bits‘(𝐴 · (2↑𝑁))) ⊆
(ℤ≥‘𝑁))) |
15 | 11, 14 | mpbid 233 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → (bits‘(𝐴 · (2↑𝑁))) ⊆
(ℤ≥‘𝑁)) |
16 | 15 | sseld 3888 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → (𝑛 ∈ (bits‘(𝐴 · (2↑𝑁))) → 𝑛 ∈ (ℤ≥‘𝑁))) |
17 | | uznn0sub 12126 |
. . . . 5
⊢ (𝑛 ∈
(ℤ≥‘𝑁) → (𝑛 − 𝑁) ∈
ℕ0) |
18 | 16, 17 | syl6 35 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → (𝑛 ∈ (bits‘(𝐴 · (2↑𝑁))) → (𝑛 − 𝑁) ∈
ℕ0)) |
19 | | bitsss 15608 |
. . . . . 6
⊢
(bits‘𝐴)
⊆ ℕ0 |
20 | 19 | a1i 11 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → (bits‘𝐴) ⊆
ℕ0) |
21 | 20 | sseld 3888 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → ((𝑛 − 𝑁) ∈ (bits‘𝐴) → (𝑛 − 𝑁) ∈
ℕ0)) |
22 | | 2cnd 11563 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (𝑛 ∈
ℕ0 ∧ (𝑛 − 𝑁) ∈ ℕ0)) → 2
∈ ℂ) |
23 | 5 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (𝑛 ∈
ℕ0 ∧ (𝑛 − 𝑁) ∈ ℕ0)) → 2
∈ ℕ) |
24 | 23 | nnne0d 11535 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (𝑛 ∈
ℕ0 ∧ (𝑛 − 𝑁) ∈ ℕ0)) → 2 ≠
0) |
25 | | simplr 765 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (𝑛 ∈
ℕ0 ∧ (𝑛 − 𝑁) ∈ ℕ0)) → 𝑁 ∈
ℕ0) |
26 | 25 | nn0zd 11934 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (𝑛 ∈
ℕ0 ∧ (𝑛 − 𝑁) ∈ ℕ0)) → 𝑁 ∈
ℤ) |
27 | | simprl 767 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (𝑛 ∈
ℕ0 ∧ (𝑛 − 𝑁) ∈ ℕ0)) → 𝑛 ∈
ℕ0) |
28 | 27 | nn0zd 11934 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (𝑛 ∈
ℕ0 ∧ (𝑛 − 𝑁) ∈ ℕ0)) → 𝑛 ∈
ℤ) |
29 | 22, 24, 26, 28 | expsubd 13371 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (𝑛 ∈
ℕ0 ∧ (𝑛 − 𝑁) ∈ ℕ0)) →
(2↑(𝑛 − 𝑁)) = ((2↑𝑛) / (2↑𝑁))) |
30 | 29 | oveq2d 7032 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (𝑛 ∈
ℕ0 ∧ (𝑛 − 𝑁) ∈ ℕ0)) → (𝐴 / (2↑(𝑛 − 𝑁))) = (𝐴 / ((2↑𝑛) / (2↑𝑁)))) |
31 | | simpl 483 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ 𝐴 ∈
ℤ) |
32 | 31 | zcnd 11937 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ 𝐴 ∈
ℂ) |
33 | 32 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (𝑛 ∈
ℕ0 ∧ (𝑛 − 𝑁) ∈ ℕ0)) → 𝐴 ∈
ℂ) |
34 | 23, 27 | nnexpcld 13456 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (𝑛 ∈
ℕ0 ∧ (𝑛 − 𝑁) ∈ ℕ0)) →
(2↑𝑛) ∈
ℕ) |
35 | 34 | nncnd 11502 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (𝑛 ∈
ℕ0 ∧ (𝑛 − 𝑁) ∈ ℕ0)) →
(2↑𝑛) ∈
ℂ) |
36 | 23, 25 | nnexpcld 13456 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (𝑛 ∈
ℕ0 ∧ (𝑛 − 𝑁) ∈ ℕ0)) →
(2↑𝑁) ∈
ℕ) |
37 | 36 | nncnd 11502 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (𝑛 ∈
ℕ0 ∧ (𝑛 − 𝑁) ∈ ℕ0)) →
(2↑𝑁) ∈
ℂ) |
38 | 34 | nnne0d 11535 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (𝑛 ∈
ℕ0 ∧ (𝑛 − 𝑁) ∈ ℕ0)) →
(2↑𝑛) ≠
0) |
39 | 36 | nnne0d 11535 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (𝑛 ∈
ℕ0 ∧ (𝑛 − 𝑁) ∈ ℕ0)) →
(2↑𝑁) ≠
0) |
40 | 33, 35, 37, 38, 39 | divdiv2d 11296 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (𝑛 ∈
ℕ0 ∧ (𝑛 − 𝑁) ∈ ℕ0)) → (𝐴 / ((2↑𝑛) / (2↑𝑁))) = ((𝐴 · (2↑𝑁)) / (2↑𝑛))) |
41 | 30, 40 | eqtr2d 2832 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (𝑛 ∈
ℕ0 ∧ (𝑛 − 𝑁) ∈ ℕ0)) →
((𝐴 · (2↑𝑁)) / (2↑𝑛)) = (𝐴 / (2↑(𝑛 − 𝑁)))) |
42 | 41 | fveq2d 6542 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (𝑛 ∈
ℕ0 ∧ (𝑛 − 𝑁) ∈ ℕ0)) →
(⌊‘((𝐴 ·
(2↑𝑁)) / (2↑𝑛))) = (⌊‘(𝐴 / (2↑(𝑛 − 𝑁))))) |
43 | 42 | breq2d 4974 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (𝑛 ∈
ℕ0 ∧ (𝑛 − 𝑁) ∈ ℕ0)) → (2
∥ (⌊‘((𝐴
· (2↑𝑁)) /
(2↑𝑛))) ↔ 2
∥ (⌊‘(𝐴 /
(2↑(𝑛 − 𝑁)))))) |
44 | 43 | notbid 319 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (𝑛 ∈
ℕ0 ∧ (𝑛 − 𝑁) ∈ ℕ0)) → (¬
2 ∥ (⌊‘((𝐴 · (2↑𝑁)) / (2↑𝑛))) ↔ ¬ 2 ∥
(⌊‘(𝐴 /
(2↑(𝑛 − 𝑁)))))) |
45 | 12 | adantrr 713 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (𝑛 ∈
ℕ0 ∧ (𝑛 − 𝑁) ∈ ℕ0)) → (𝐴 · (2↑𝑁)) ∈
ℤ) |
46 | | bitsval2 15607 |
. . . . . . 7
⊢ (((𝐴 · (2↑𝑁)) ∈ ℤ ∧ 𝑛 ∈ ℕ0)
→ (𝑛 ∈
(bits‘(𝐴 ·
(2↑𝑁))) ↔ ¬ 2
∥ (⌊‘((𝐴
· (2↑𝑁)) /
(2↑𝑛))))) |
47 | 45, 27, 46 | syl2anc 584 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (𝑛 ∈
ℕ0 ∧ (𝑛 − 𝑁) ∈ ℕ0)) → (𝑛 ∈ (bits‘(𝐴 · (2↑𝑁))) ↔ ¬ 2 ∥
(⌊‘((𝐴 ·
(2↑𝑁)) / (2↑𝑛))))) |
48 | | bitsval2 15607 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ (𝑛 − 𝑁) ∈ ℕ0) → ((𝑛 − 𝑁) ∈ (bits‘𝐴) ↔ ¬ 2 ∥
(⌊‘(𝐴 /
(2↑(𝑛 − 𝑁)))))) |
49 | 48 | ad2ant2rl 745 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (𝑛 ∈
ℕ0 ∧ (𝑛 − 𝑁) ∈ ℕ0)) →
((𝑛 − 𝑁) ∈ (bits‘𝐴) ↔ ¬ 2 ∥
(⌊‘(𝐴 /
(2↑(𝑛 − 𝑁)))))) |
50 | 44, 47, 49 | 3bitr4d 312 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (𝑛 ∈
ℕ0 ∧ (𝑛 − 𝑁) ∈ ℕ0)) → (𝑛 ∈ (bits‘(𝐴 · (2↑𝑁))) ↔ (𝑛 − 𝑁) ∈ (bits‘𝐴))) |
51 | 50 | expr 457 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → ((𝑛 − 𝑁) ∈ ℕ0 → (𝑛 ∈ (bits‘(𝐴 · (2↑𝑁))) ↔ (𝑛 − 𝑁) ∈ (bits‘𝐴)))) |
52 | 18, 21, 51 | pm5.21ndd 381 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ 𝑛 ∈
ℕ0) → (𝑛 ∈ (bits‘(𝐴 · (2↑𝑁))) ↔ (𝑛 − 𝑁) ∈ (bits‘𝐴))) |
53 | 52 | rabbi2dva 4114 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (ℕ0 ∩ (bits‘(𝐴 · (2↑𝑁)))) = {𝑛 ∈ ℕ0 ∣ (𝑛 − 𝑁) ∈ (bits‘𝐴)}) |
54 | 3, 53 | syl5reqr 2846 |
1
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ {𝑛 ∈
ℕ0 ∣ (𝑛 − 𝑁) ∈ (bits‘𝐴)} = (bits‘(𝐴 · (2↑𝑁)))) |