Proof of Theorem bitsres
Step | Hyp | Ref
| Expression |
1 | | simpl 486 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ 𝐴 ∈
ℤ) |
2 | | 2nn 11903 |
. . . . . . . 8
⊢ 2 ∈
ℕ |
3 | 2 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ 2 ∈ ℕ) |
4 | | simpr 488 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ 𝑁 ∈
ℕ0) |
5 | 3, 4 | nnexpcld 13812 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (2↑𝑁) ∈
ℕ) |
6 | 1, 5 | zmodcld 13465 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (𝐴 mod (2↑𝑁)) ∈
ℕ0) |
7 | 6 | nn0zd 12280 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (𝐴 mod (2↑𝑁)) ∈
ℤ) |
8 | 7 | znegcld 12284 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ -(𝐴 mod
(2↑𝑁)) ∈
ℤ) |
9 | | sadadd 16026 |
. . 3
⊢ ((-(𝐴 mod (2↑𝑁)) ∈ ℤ ∧ 𝐴 ∈ ℤ) → ((bits‘-(𝐴 mod (2↑𝑁))) sadd (bits‘𝐴)) = (bits‘(-(𝐴 mod (2↑𝑁)) + 𝐴))) |
10 | 8, 1, 9 | syl2anc 587 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ ((bits‘-(𝐴 mod
(2↑𝑁))) sadd
(bits‘𝐴)) =
(bits‘(-(𝐴 mod
(2↑𝑁)) + 𝐴))) |
11 | | sadadd 16026 |
. . . . . 6
⊢ ((-(𝐴 mod (2↑𝑁)) ∈ ℤ ∧ (𝐴 mod (2↑𝑁)) ∈ ℤ) →
((bits‘-(𝐴 mod
(2↑𝑁))) sadd
(bits‘(𝐴 mod
(2↑𝑁)))) =
(bits‘(-(𝐴 mod
(2↑𝑁)) + (𝐴 mod (2↑𝑁))))) |
12 | 8, 7, 11 | syl2anc 587 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ ((bits‘-(𝐴 mod
(2↑𝑁))) sadd
(bits‘(𝐴 mod
(2↑𝑁)))) =
(bits‘(-(𝐴 mod
(2↑𝑁)) + (𝐴 mod (2↑𝑁))))) |
13 | 8 | zcnd 12283 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ -(𝐴 mod
(2↑𝑁)) ∈
ℂ) |
14 | 7 | zcnd 12283 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (𝐴 mod (2↑𝑁)) ∈
ℂ) |
15 | 13, 14 | addcomd 11034 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (-(𝐴 mod
(2↑𝑁)) + (𝐴 mod (2↑𝑁))) = ((𝐴 mod (2↑𝑁)) + -(𝐴 mod (2↑𝑁)))) |
16 | 14 | negidd 11179 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ ((𝐴 mod
(2↑𝑁)) + -(𝐴 mod (2↑𝑁))) = 0) |
17 | 15, 16 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (-(𝐴 mod
(2↑𝑁)) + (𝐴 mod (2↑𝑁))) = 0) |
18 | 17 | fveq2d 6721 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (bits‘(-(𝐴 mod
(2↑𝑁)) + (𝐴 mod (2↑𝑁)))) = (bits‘0)) |
19 | | 0bits 15998 |
. . . . . 6
⊢
(bits‘0) = ∅ |
20 | 18, 19 | eqtrdi 2794 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (bits‘(-(𝐴 mod
(2↑𝑁)) + (𝐴 mod (2↑𝑁)))) = ∅) |
21 | 12, 20 | eqtrd 2777 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ ((bits‘-(𝐴 mod
(2↑𝑁))) sadd
(bits‘(𝐴 mod
(2↑𝑁)))) =
∅) |
22 | 21 | oveq1d 7228 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (((bits‘-(𝐴
mod (2↑𝑁))) sadd
(bits‘(𝐴 mod
(2↑𝑁)))) sadd
((bits‘𝐴) ∩
(ℤ≥‘𝑁))) = (∅ sadd ((bits‘𝐴) ∩
(ℤ≥‘𝑁)))) |
23 | | bitsss 15985 |
. . . . 5
⊢
(bits‘-(𝐴 mod
(2↑𝑁))) ⊆
ℕ0 |
24 | | bitsss 15985 |
. . . . 5
⊢
(bits‘(𝐴 mod
(2↑𝑁))) ⊆
ℕ0 |
25 | | inss1 4143 |
. . . . . 6
⊢
((bits‘𝐴)
∩ (ℤ≥‘𝑁)) ⊆ (bits‘𝐴) |
26 | | bitsss 15985 |
. . . . . . 7
⊢
(bits‘𝐴)
⊆ ℕ0 |
27 | 26 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (bits‘𝐴)
⊆ ℕ0) |
28 | 25, 27 | sstrid 3912 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ ((bits‘𝐴)
∩ (ℤ≥‘𝑁)) ⊆
ℕ0) |
29 | | sadass 16030 |
. . . . 5
⊢
(((bits‘-(𝐴
mod (2↑𝑁))) ⊆
ℕ0 ∧ (bits‘(𝐴 mod (2↑𝑁))) ⊆ ℕ0 ∧
((bits‘𝐴) ∩
(ℤ≥‘𝑁)) ⊆ ℕ0) →
(((bits‘-(𝐴 mod
(2↑𝑁))) sadd
(bits‘(𝐴 mod
(2↑𝑁)))) sadd
((bits‘𝐴) ∩
(ℤ≥‘𝑁))) = ((bits‘-(𝐴 mod (2↑𝑁))) sadd ((bits‘(𝐴 mod (2↑𝑁))) sadd ((bits‘𝐴) ∩ (ℤ≥‘𝑁))))) |
30 | 23, 24, 28, 29 | mp3an12i 1467 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (((bits‘-(𝐴
mod (2↑𝑁))) sadd
(bits‘(𝐴 mod
(2↑𝑁)))) sadd
((bits‘𝐴) ∩
(ℤ≥‘𝑁))) = ((bits‘-(𝐴 mod (2↑𝑁))) sadd ((bits‘(𝐴 mod (2↑𝑁))) sadd ((bits‘𝐴) ∩ (ℤ≥‘𝑁))))) |
31 | | bitsmod 15995 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (bits‘(𝐴 mod
(2↑𝑁))) =
((bits‘𝐴) ∩
(0..^𝑁))) |
32 | 31 | oveq1d 7228 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ ((bits‘(𝐴 mod
(2↑𝑁))) sadd
((bits‘𝐴) ∩
(ℤ≥‘𝑁))) = (((bits‘𝐴) ∩ (0..^𝑁)) sadd ((bits‘𝐴) ∩ (ℤ≥‘𝑁)))) |
33 | | inss1 4143 |
. . . . . . . . . 10
⊢
((bits‘𝐴)
∩ (0..^𝑁)) ⊆
(bits‘𝐴) |
34 | 33, 27 | sstrid 3912 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ ((bits‘𝐴)
∩ (0..^𝑁)) ⊆
ℕ0) |
35 | | fzouzdisj 13278 |
. . . . . . . . . . . 12
⊢
((0..^𝑁) ∩
(ℤ≥‘𝑁)) = ∅ |
36 | 35 | ineq2i 4124 |
. . . . . . . . . . 11
⊢
((bits‘𝐴)
∩ ((0..^𝑁) ∩
(ℤ≥‘𝑁))) = ((bits‘𝐴) ∩ ∅) |
37 | | inindi 4141 |
. . . . . . . . . . 11
⊢
((bits‘𝐴)
∩ ((0..^𝑁) ∩
(ℤ≥‘𝑁))) = (((bits‘𝐴) ∩ (0..^𝑁)) ∩ ((bits‘𝐴) ∩ (ℤ≥‘𝑁))) |
38 | | in0 4306 |
. . . . . . . . . . 11
⊢
((bits‘𝐴)
∩ ∅) = ∅ |
39 | 36, 37, 38 | 3eqtr3i 2773 |
. . . . . . . . . 10
⊢
(((bits‘𝐴)
∩ (0..^𝑁)) ∩
((bits‘𝐴) ∩
(ℤ≥‘𝑁))) = ∅ |
40 | 39 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (((bits‘𝐴)
∩ (0..^𝑁)) ∩
((bits‘𝐴) ∩
(ℤ≥‘𝑁))) = ∅) |
41 | 34, 28, 40 | saddisj 16024 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (((bits‘𝐴)
∩ (0..^𝑁)) sadd
((bits‘𝐴) ∩
(ℤ≥‘𝑁))) = (((bits‘𝐴) ∩ (0..^𝑁)) ∪ ((bits‘𝐴) ∩ (ℤ≥‘𝑁)))) |
42 | | indi 4188 |
. . . . . . . 8
⊢
((bits‘𝐴)
∩ ((0..^𝑁) ∪
(ℤ≥‘𝑁))) = (((bits‘𝐴) ∩ (0..^𝑁)) ∪ ((bits‘𝐴) ∩ (ℤ≥‘𝑁))) |
43 | 41, 42 | eqtr4di 2796 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (((bits‘𝐴)
∩ (0..^𝑁)) sadd
((bits‘𝐴) ∩
(ℤ≥‘𝑁))) = ((bits‘𝐴) ∩ ((0..^𝑁) ∪ (ℤ≥‘𝑁)))) |
44 | | nn0uz 12476 |
. . . . . . . . . 10
⊢
ℕ0 = (ℤ≥‘0) |
45 | 4, 44 | eleqtrdi 2848 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ 𝑁 ∈
(ℤ≥‘0)) |
46 | | fzouzsplit 13277 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘0) → (ℤ≥‘0) =
((0..^𝑁) ∪
(ℤ≥‘𝑁))) |
47 | 45, 46 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (ℤ≥‘0) = ((0..^𝑁) ∪ (ℤ≥‘𝑁))) |
48 | 44, 47 | syl5eq 2790 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ ℕ0 = ((0..^𝑁) ∪ (ℤ≥‘𝑁))) |
49 | 26, 48 | sseqtrid 3953 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (bits‘𝐴)
⊆ ((0..^𝑁) ∪
(ℤ≥‘𝑁))) |
50 | | df-ss 3883 |
. . . . . . . 8
⊢
((bits‘𝐴)
⊆ ((0..^𝑁) ∪
(ℤ≥‘𝑁)) ↔ ((bits‘𝐴) ∩ ((0..^𝑁) ∪ (ℤ≥‘𝑁))) = (bits‘𝐴)) |
51 | 49, 50 | sylib 221 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ ((bits‘𝐴)
∩ ((0..^𝑁) ∪
(ℤ≥‘𝑁))) = (bits‘𝐴)) |
52 | 43, 51 | eqtrd 2777 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (((bits‘𝐴)
∩ (0..^𝑁)) sadd
((bits‘𝐴) ∩
(ℤ≥‘𝑁))) = (bits‘𝐴)) |
53 | 32, 52 | eqtrd 2777 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ ((bits‘(𝐴 mod
(2↑𝑁))) sadd
((bits‘𝐴) ∩
(ℤ≥‘𝑁))) = (bits‘𝐴)) |
54 | 53 | oveq2d 7229 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ ((bits‘-(𝐴 mod
(2↑𝑁))) sadd
((bits‘(𝐴 mod
(2↑𝑁))) sadd
((bits‘𝐴) ∩
(ℤ≥‘𝑁)))) = ((bits‘-(𝐴 mod (2↑𝑁))) sadd (bits‘𝐴))) |
55 | 30, 54 | eqtrd 2777 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (((bits‘-(𝐴
mod (2↑𝑁))) sadd
(bits‘(𝐴 mod
(2↑𝑁)))) sadd
((bits‘𝐴) ∩
(ℤ≥‘𝑁))) = ((bits‘-(𝐴 mod (2↑𝑁))) sadd (bits‘𝐴))) |
56 | | sadid2 16028 |
. . . 4
⊢
(((bits‘𝐴)
∩ (ℤ≥‘𝑁)) ⊆ ℕ0 →
(∅ sadd ((bits‘𝐴) ∩ (ℤ≥‘𝑁))) = ((bits‘𝐴) ∩
(ℤ≥‘𝑁))) |
57 | 28, 56 | syl 17 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (∅ sadd ((bits‘𝐴) ∩ (ℤ≥‘𝑁))) = ((bits‘𝐴) ∩
(ℤ≥‘𝑁))) |
58 | 22, 55, 57 | 3eqtr3d 2785 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ ((bits‘-(𝐴 mod
(2↑𝑁))) sadd
(bits‘𝐴)) =
((bits‘𝐴) ∩
(ℤ≥‘𝑁))) |
59 | 1 | zcnd 12283 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ 𝐴 ∈
ℂ) |
60 | 13, 59 | addcomd 11034 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (-(𝐴 mod
(2↑𝑁)) + 𝐴) = (𝐴 + -(𝐴 mod (2↑𝑁)))) |
61 | 59, 14 | negsubd 11195 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (𝐴 + -(𝐴 mod (2↑𝑁))) = (𝐴 − (𝐴 mod (2↑𝑁)))) |
62 | 59, 14 | subcld 11189 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (𝐴 − (𝐴 mod (2↑𝑁))) ∈ ℂ) |
63 | 5 | nncnd 11846 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (2↑𝑁) ∈
ℂ) |
64 | 5 | nnne0d 11880 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (2↑𝑁) ≠
0) |
65 | 62, 63, 64 | divcan1d 11609 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (((𝐴 − (𝐴 mod (2↑𝑁))) / (2↑𝑁)) · (2↑𝑁)) = (𝐴 − (𝐴 mod (2↑𝑁)))) |
66 | 1 | zred 12282 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ 𝐴 ∈
ℝ) |
67 | 5 | nnrpd 12626 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (2↑𝑁) ∈
ℝ+) |
68 | | moddiffl 13455 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧
(2↑𝑁) ∈
ℝ+) → ((𝐴 − (𝐴 mod (2↑𝑁))) / (2↑𝑁)) = (⌊‘(𝐴 / (2↑𝑁)))) |
69 | 66, 67, 68 | syl2anc 587 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ ((𝐴 − (𝐴 mod (2↑𝑁))) / (2↑𝑁)) = (⌊‘(𝐴 / (2↑𝑁)))) |
70 | 69 | oveq1d 7228 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (((𝐴 − (𝐴 mod (2↑𝑁))) / (2↑𝑁)) · (2↑𝑁)) = ((⌊‘(𝐴 / (2↑𝑁))) · (2↑𝑁))) |
71 | 61, 65, 70 | 3eqtr2d 2783 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (𝐴 + -(𝐴 mod (2↑𝑁))) = ((⌊‘(𝐴 / (2↑𝑁))) · (2↑𝑁))) |
72 | 60, 71 | eqtrd 2777 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (-(𝐴 mod
(2↑𝑁)) + 𝐴) = ((⌊‘(𝐴 / (2↑𝑁))) · (2↑𝑁))) |
73 | 72 | fveq2d 6721 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (bits‘(-(𝐴 mod
(2↑𝑁)) + 𝐴)) =
(bits‘((⌊‘(𝐴 / (2↑𝑁))) · (2↑𝑁)))) |
74 | 10, 58, 73 | 3eqtr3d 2785 |
1
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ ((bits‘𝐴)
∩ (ℤ≥‘𝑁)) = (bits‘((⌊‘(𝐴 / (2↑𝑁))) · (2↑𝑁)))) |