Proof of Theorem bitsuz
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | bitsres 16511 | . . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ ((bits‘𝐴)
∩ (ℤ≥‘𝑁)) = (bits‘((⌊‘(𝐴 / (2↑𝑁))) · (2↑𝑁)))) | 
| 2 | 1 | eqeq1d 2738 | . . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (((bits‘𝐴)
∩ (ℤ≥‘𝑁)) = (bits‘𝐴) ↔ (bits‘((⌊‘(𝐴 / (2↑𝑁))) · (2↑𝑁))) = (bits‘𝐴))) | 
| 3 |  | simpl 482 | . . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ 𝐴 ∈
ℤ) | 
| 4 | 3 | zred 12724 | . . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ 𝐴 ∈
ℝ) | 
| 5 |  | 2nn 12340 | . . . . . . . . 9
⊢ 2 ∈
ℕ | 
| 6 | 5 | a1i 11 | . . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ 2 ∈ ℕ) | 
| 7 |  | simpr 484 | . . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ 𝑁 ∈
ℕ0) | 
| 8 | 6, 7 | nnexpcld 14285 | . . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (2↑𝑁) ∈
ℕ) | 
| 9 | 4, 8 | nndivred 12321 | . . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (𝐴 / (2↑𝑁)) ∈
ℝ) | 
| 10 | 9 | flcld 13839 | . . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (⌊‘(𝐴 /
(2↑𝑁))) ∈
ℤ) | 
| 11 | 8 | nnzd 12642 | . . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (2↑𝑁) ∈
ℤ) | 
| 12 | 10, 11 | zmulcld 12730 | . . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ ((⌊‘(𝐴 /
(2↑𝑁))) ·
(2↑𝑁)) ∈
ℤ) | 
| 13 |  | bitsf1 16484 | . . . . 5
⊢
bits:ℤ–1-1→𝒫 ℕ0 | 
| 14 |  | f1fveq 7283 | . . . . 5
⊢
((bits:ℤ–1-1→𝒫 ℕ0 ∧
(((⌊‘(𝐴 /
(2↑𝑁))) ·
(2↑𝑁)) ∈ ℤ
∧ 𝐴 ∈ ℤ))
→ ((bits‘((⌊‘(𝐴 / (2↑𝑁))) · (2↑𝑁))) = (bits‘𝐴) ↔ ((⌊‘(𝐴 / (2↑𝑁))) · (2↑𝑁)) = 𝐴)) | 
| 15 | 13, 14 | mpan 690 | . . . 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 16317 | . . . . . 6
⊢
(((⌊‘(𝐴
/ (2↑𝑁))) ∈
ℤ ∧ (2↑𝑁)
∈ ℤ) → (2↑𝑁) ∥ ((⌊‘(𝐴 / (2↑𝑁))) · (2↑𝑁))) | 
| 18 | 10, 11, 17 | syl2anc 584 | . . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (2↑𝑁) ∥
((⌊‘(𝐴 /
(2↑𝑁))) ·
(2↑𝑁))) | 
| 19 |  | breq2 5146 | . . . . 5
⊢
(((⌊‘(𝐴
/ (2↑𝑁))) ·
(2↑𝑁)) = 𝐴 → ((2↑𝑁) ∥ ((⌊‘(𝐴 / (2↑𝑁))) · (2↑𝑁)) ↔ (2↑𝑁) ∥ 𝐴)) | 
| 20 | 18, 19 | syl5ibcom 245 | . . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (((⌊‘(𝐴
/ (2↑𝑁))) ·
(2↑𝑁)) = 𝐴 → (2↑𝑁) ∥ 𝐴)) | 
| 21 | 8 | nnne0d 12317 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (2↑𝑁) ≠
0) | 
| 22 |  | dvdsval2 16294 | . . . . . . . . . 10
⊢
(((2↑𝑁) ∈
ℤ ∧ (2↑𝑁)
≠ 0 ∧ 𝐴 ∈
ℤ) → ((2↑𝑁)
∥ 𝐴 ↔ (𝐴 / (2↑𝑁)) ∈ ℤ)) | 
| 23 | 11, 21, 3, 22 | syl3anc 1372 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ ((2↑𝑁) ∥
𝐴 ↔ (𝐴 / (2↑𝑁)) ∈ ℤ)) | 
| 24 | 23 | biimpa 476 | . . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (2↑𝑁) ∥
𝐴) → (𝐴 / (2↑𝑁)) ∈ ℤ) | 
| 25 |  | flid 13849 | . . . . . . . 8
⊢ ((𝐴 / (2↑𝑁)) ∈ ℤ →
(⌊‘(𝐴 /
(2↑𝑁))) = (𝐴 / (2↑𝑁))) | 
| 26 | 24, 25 | syl 17 | . . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (2↑𝑁) ∥
𝐴) →
(⌊‘(𝐴 /
(2↑𝑁))) = (𝐴 / (2↑𝑁))) | 
| 27 | 26 | oveq1d 7447 | . . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (2↑𝑁) ∥
𝐴) →
((⌊‘(𝐴 /
(2↑𝑁))) ·
(2↑𝑁)) = ((𝐴 / (2↑𝑁)) · (2↑𝑁))) | 
| 28 | 3 | zcnd 12725 | . . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ 𝐴 ∈
ℂ) | 
| 29 | 28 | adantr 480 | . . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (2↑𝑁) ∥
𝐴) → 𝐴 ∈ ℂ) | 
| 30 | 8 | nncnd 12283 | . . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (2↑𝑁) ∈
ℂ) | 
| 31 | 30 | adantr 480 | . . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (2↑𝑁) ∥
𝐴) → (2↑𝑁) ∈
ℂ) | 
| 32 |  | 2cnd 12345 | . . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (2↑𝑁) ∥
𝐴) → 2 ∈
ℂ) | 
| 33 |  | 2ne0 12371 | . . . . . . . . 9
⊢ 2 ≠
0 | 
| 34 | 33 | a1i 11 | . . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (2↑𝑁) ∥
𝐴) → 2 ≠
0) | 
| 35 | 7 | nn0zd 12641 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ 𝑁 ∈
ℤ) | 
| 36 | 35 | adantr 480 | . . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (2↑𝑁) ∥
𝐴) → 𝑁 ∈ ℤ) | 
| 37 | 32, 34, 36 | expne0d 14193 | . . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (2↑𝑁) ∥
𝐴) → (2↑𝑁) ≠ 0) | 
| 38 | 29, 31, 37 | divcan1d 12045 | . . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (2↑𝑁) ∥
𝐴) → ((𝐴 / (2↑𝑁)) · (2↑𝑁)) = 𝐴) | 
| 39 | 27, 38 | eqtrd 2776 | . . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
∧ (2↑𝑁) ∥
𝐴) →
((⌊‘(𝐴 /
(2↑𝑁))) ·
(2↑𝑁)) = 𝐴) | 
| 40 | 39 | ex 412 | . . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ ((2↑𝑁) ∥
𝐴 →
((⌊‘(𝐴 /
(2↑𝑁))) ·
(2↑𝑁)) = 𝐴)) | 
| 41 | 20, 40 | impbid 212 | . . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (((⌊‘(𝐴
/ (2↑𝑁))) ·
(2↑𝑁)) = 𝐴 ↔ (2↑𝑁) ∥ 𝐴)) | 
| 42 | 2, 16, 41 | 3bitrrd 306 | . 2
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ ((2↑𝑁) ∥
𝐴 ↔ ((bits‘𝐴) ∩
(ℤ≥‘𝑁)) = (bits‘𝐴))) | 
| 43 |  | dfss2 3968 | . 2
⊢
((bits‘𝐴)
⊆ (ℤ≥‘𝑁) ↔ ((bits‘𝐴) ∩ (ℤ≥‘𝑁)) = (bits‘𝐴)) | 
| 44 | 42, 43 | bitr4di 289 | 1
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ ((2↑𝑁) ∥
𝐴 ↔ (bits‘𝐴) ⊆
(ℤ≥‘𝑁))) |