Proof of Theorem bitsuz
Step | Hyp | Ref
| Expression |
1 | | bitsres 15810 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ ((bits‘𝐴)
∩ (ℤ≥‘𝑁)) = (bits‘((⌊‘(𝐴 / (2↑𝑁))) · (2↑𝑁)))) |
2 | 1 | eqeq1d 2820 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (((bits‘𝐴)
∩ (ℤ≥‘𝑁)) = (bits‘𝐴) ↔ (bits‘((⌊‘(𝐴 / (2↑𝑁))) · (2↑𝑁))) = (bits‘𝐴))) |
3 | | simpl 483 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ 𝐴 ∈
ℤ) |
4 | 3 | zred 12075 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ 𝐴 ∈
ℝ) |
5 | | 2nn 11698 |
. . . . . . . . 9
⊢ 2 ∈
ℕ |
6 | 5 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ 2 ∈ ℕ) |
7 | | simpr 485 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ 𝑁 ∈
ℕ0) |
8 | 6, 7 | nnexpcld 13594 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (2↑𝑁) ∈
ℕ) |
9 | 4, 8 | nndivred 11679 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (𝐴 / (2↑𝑁)) ∈
ℝ) |
10 | 9 | flcld 13156 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (⌊‘(𝐴 /
(2↑𝑁))) ∈
ℤ) |
11 | 8 | nnzd 12074 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (2↑𝑁) ∈
ℤ) |
12 | 10, 11 | zmulcld 12081 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ ((⌊‘(𝐴 /
(2↑𝑁))) ·
(2↑𝑁)) ∈
ℤ) |
13 | | bitsf1 15783 |
. . . . 5
⊢
bits:ℤ–1-1→𝒫 ℕ0 |
14 | | f1fveq 7011 |
. . . . 5
⊢
((bits:ℤ–1-1→𝒫 ℕ0 ∧
(((⌊‘(𝐴 /
(2↑𝑁))) ·
(2↑𝑁)) ∈ ℤ
∧ 𝐴 ∈ ℤ))
→ ((bits‘((⌊‘(𝐴 / (2↑𝑁))) · (2↑𝑁))) = (bits‘𝐴) ↔ ((⌊‘(𝐴 / (2↑𝑁))) · (2↑𝑁)) = 𝐴)) |
15 | 13, 14 | mpan 686 |
. . . 4
⊢
((((⌊‘(𝐴
/ (2↑𝑁))) ·
(2↑𝑁)) ∈ ℤ
∧ 𝐴 ∈ ℤ)
→ ((bits‘((⌊‘(𝐴 / (2↑𝑁))) · (2↑𝑁))) = (bits‘𝐴) ↔ ((⌊‘(𝐴 / (2↑𝑁))) · (2↑𝑁)) = 𝐴)) |
16 | 12, 3, 15 | syl2anc 584 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ ((bits‘((⌊‘(𝐴 / (2↑𝑁))) · (2↑𝑁))) = (bits‘𝐴) ↔ ((⌊‘(𝐴 / (2↑𝑁))) · (2↑𝑁)) = 𝐴)) |
17 | | dvdsmul2 15620 |
. . . . . 6
⊢
(((⌊‘(𝐴
/ (2↑𝑁))) ∈
ℤ ∧ (2↑𝑁)
∈ ℤ) → (2↑𝑁) ∥ ((⌊‘(𝐴 / (2↑𝑁))) · (2↑𝑁))) |
18 | 10, 11, 17 | syl2anc 584 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (2↑𝑁) ∥
((⌊‘(𝐴 /
(2↑𝑁))) ·
(2↑𝑁))) |
19 | | breq2 5061 |
. . . . 5
⊢
(((⌊‘(𝐴
/ (2↑𝑁))) ·
(2↑𝑁)) = 𝐴 → ((2↑𝑁) ∥ ((⌊‘(𝐴 / (2↑𝑁))) · (2↑𝑁)) ↔ (2↑𝑁) ∥ 𝐴)) |
20 | 18, 19 | syl5ibcom 246 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (((⌊‘(𝐴
/ (2↑𝑁))) ·
(2↑𝑁)) = 𝐴 → (2↑𝑁) ∥ 𝐴)) |
21 | 8 | nnne0d 11675 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (2↑𝑁) ≠
0) |
22 | | dvdsval2 15598 |
. . . . . . . . . 10
⊢
(((2↑𝑁) ∈
ℤ ∧ (2↑𝑁)
≠ 0 ∧ 𝐴 ∈
ℤ) → ((2↑𝑁)
∥ 𝐴 ↔ (𝐴 / (2↑𝑁)) ∈ ℤ)) |
23 | 11, 21, 3, 22 | syl3anc 1363 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ ((2↑𝑁) ∥
𝐴 ↔ (𝐴 / (2↑𝑁)) ∈ ℤ)) |
24 | 23 | biimpa 477 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (2↑𝑁) ∥
𝐴) → (𝐴 / (2↑𝑁)) ∈ ℤ) |
25 | | flid 13166 |
. . . . . . . 8
⊢ ((𝐴 / (2↑𝑁)) ∈ ℤ →
(⌊‘(𝐴 /
(2↑𝑁))) = (𝐴 / (2↑𝑁))) |
26 | 24, 25 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (2↑𝑁) ∥
𝐴) →
(⌊‘(𝐴 /
(2↑𝑁))) = (𝐴 / (2↑𝑁))) |
27 | 26 | oveq1d 7160 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (2↑𝑁) ∥
𝐴) →
((⌊‘(𝐴 /
(2↑𝑁))) ·
(2↑𝑁)) = ((𝐴 / (2↑𝑁)) · (2↑𝑁))) |
28 | 3 | zcnd 12076 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ 𝐴 ∈
ℂ) |
29 | 28 | adantr 481 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (2↑𝑁) ∥
𝐴) → 𝐴 ∈ ℂ) |
30 | 8 | nncnd 11642 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (2↑𝑁) ∈
ℂ) |
31 | 30 | adantr 481 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (2↑𝑁) ∥
𝐴) → (2↑𝑁) ∈
ℂ) |
32 | | 2cnd 11703 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (2↑𝑁) ∥
𝐴) → 2 ∈
ℂ) |
33 | | 2ne0 11729 |
. . . . . . . . 9
⊢ 2 ≠
0 |
34 | 33 | a1i 11 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (2↑𝑁) ∥
𝐴) → 2 ≠
0) |
35 | 7 | nn0zd 12073 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ 𝑁 ∈
ℤ) |
36 | 35 | adantr 481 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (2↑𝑁) ∥
𝐴) → 𝑁 ∈ ℤ) |
37 | 32, 34, 36 | expne0d 13504 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (2↑𝑁) ∥
𝐴) → (2↑𝑁) ≠ 0) |
38 | 29, 31, 37 | divcan1d 11405 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (2↑𝑁) ∥
𝐴) → ((𝐴 / (2↑𝑁)) · (2↑𝑁)) = 𝐴) |
39 | 27, 38 | eqtrd 2853 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (2↑𝑁) ∥
𝐴) →
((⌊‘(𝐴 /
(2↑𝑁))) ·
(2↑𝑁)) = 𝐴) |
40 | 39 | ex 413 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ ((2↑𝑁) ∥
𝐴 →
((⌊‘(𝐴 /
(2↑𝑁))) ·
(2↑𝑁)) = 𝐴)) |
41 | 20, 40 | impbid 213 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (((⌊‘(𝐴
/ (2↑𝑁))) ·
(2↑𝑁)) = 𝐴 ↔ (2↑𝑁) ∥ 𝐴)) |
42 | 2, 16, 41 | 3bitrrd 307 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ ((2↑𝑁) ∥
𝐴 ↔ ((bits‘𝐴) ∩
(ℤ≥‘𝑁)) = (bits‘𝐴))) |
43 | | df-ss 3949 |
. 2
⊢
((bits‘𝐴)
⊆ (ℤ≥‘𝑁) ↔ ((bits‘𝐴) ∩ (ℤ≥‘𝑁)) = (bits‘𝐴)) |
44 | 42, 43 | syl6bbr 290 |
1
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ ((2↑𝑁) ∥
𝐴 ↔ (bits‘𝐴) ⊆
(ℤ≥‘𝑁))) |