Proof of Theorem sadaddlem
Step | Hyp | Ref
| Expression |
1 | | sadaddlem.k |
. . . . . . . . . . . . 13
⊢ 𝐾 = ◡(bits ↾
ℕ0) |
2 | 1 | fveq1i 6546 |
. . . . . . . . . . . 12
⊢ (𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) = (◡(bits ↾
ℕ0)‘((bits‘𝐴) ∩ (0..^𝑁))) |
3 | | sadaddlem.1 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 ∈ ℤ) |
4 | | 2nn 11564 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℕ |
5 | 4 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 2 ∈
ℕ) |
6 | | sadaddlem.3 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
7 | 5, 6 | nnexpcld 13460 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (2↑𝑁) ∈ ℕ) |
8 | 3, 7 | zmodcld 13114 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴 mod (2↑𝑁)) ∈
ℕ0) |
9 | 8 | fvresd 6565 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((bits ↾
ℕ0)‘(𝐴 mod (2↑𝑁))) = (bits‘(𝐴 mod (2↑𝑁)))) |
10 | | bitsmod 15622 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (bits‘(𝐴 mod
(2↑𝑁))) =
((bits‘𝐴) ∩
(0..^𝑁))) |
11 | 3, 6, 10 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (bits‘(𝐴 mod (2↑𝑁))) = ((bits‘𝐴) ∩ (0..^𝑁))) |
12 | 9, 11 | eqtrd 2833 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((bits ↾
ℕ0)‘(𝐴 mod (2↑𝑁))) = ((bits‘𝐴) ∩ (0..^𝑁))) |
13 | | bitsf1o 15631 |
. . . . . . . . . . . . . 14
⊢ (bits
↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩
Fin) |
14 | | f1ocnvfv 6907 |
. . . . . . . . . . . . . 14
⊢ (((bits
↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩ Fin)
∧ (𝐴 mod (2↑𝑁)) ∈ ℕ0)
→ (((bits ↾ ℕ0)‘(𝐴 mod (2↑𝑁))) = ((bits‘𝐴) ∩ (0..^𝑁)) → (◡(bits ↾
ℕ0)‘((bits‘𝐴) ∩ (0..^𝑁))) = (𝐴 mod (2↑𝑁)))) |
15 | 13, 8, 14 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((bits ↾
ℕ0)‘(𝐴 mod (2↑𝑁))) = ((bits‘𝐴) ∩ (0..^𝑁)) → (◡(bits ↾
ℕ0)‘((bits‘𝐴) ∩ (0..^𝑁))) = (𝐴 mod (2↑𝑁)))) |
16 | 12, 15 | mpd 15 |
. . . . . . . . . . . 12
⊢ (𝜑 → (◡(bits ↾
ℕ0)‘((bits‘𝐴) ∩ (0..^𝑁))) = (𝐴 mod (2↑𝑁))) |
17 | 2, 16 | syl5eq 2845 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) = (𝐴 mod (2↑𝑁))) |
18 | 17 | oveq2d 7039 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) = (𝐴 − (𝐴 mod (2↑𝑁)))) |
19 | 18 | oveq1d 7038 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) / (2↑𝑁)) = ((𝐴 − (𝐴 mod (2↑𝑁))) / (2↑𝑁))) |
20 | 3 | zred 11941 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ ℝ) |
21 | 7 | nnrpd 12283 |
. . . . . . . . . 10
⊢ (𝜑 → (2↑𝑁) ∈
ℝ+) |
22 | | moddifz 13105 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧
(2↑𝑁) ∈
ℝ+) → ((𝐴 − (𝐴 mod (2↑𝑁))) / (2↑𝑁)) ∈ ℤ) |
23 | 20, 21, 22 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴 − (𝐴 mod (2↑𝑁))) / (2↑𝑁)) ∈ ℤ) |
24 | 19, 23 | eqeltrd 2885 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) / (2↑𝑁)) ∈ ℤ) |
25 | 7 | nnzd 11940 |
. . . . . . . . 9
⊢ (𝜑 → (2↑𝑁) ∈ ℤ) |
26 | 7 | nnne0d 11541 |
. . . . . . . . 9
⊢ (𝜑 → (2↑𝑁) ≠ 0) |
27 | | inss1 4131 |
. . . . . . . . . . . . . 14
⊢
((bits‘𝐴)
∩ (0..^𝑁)) ⊆
(bits‘𝐴) |
28 | | bitsss 15612 |
. . . . . . . . . . . . . 14
⊢
(bits‘𝐴)
⊆ ℕ0 |
29 | 27, 28 | sstri 3904 |
. . . . . . . . . . . . 13
⊢
((bits‘𝐴)
∩ (0..^𝑁)) ⊆
ℕ0 |
30 | | fzofi 13196 |
. . . . . . . . . . . . . 14
⊢
(0..^𝑁) ∈
Fin |
31 | | inss2 4132 |
. . . . . . . . . . . . . 14
⊢
((bits‘𝐴)
∩ (0..^𝑁)) ⊆
(0..^𝑁) |
32 | | ssfi 8591 |
. . . . . . . . . . . . . 14
⊢
(((0..^𝑁) ∈ Fin
∧ ((bits‘𝐴) ∩
(0..^𝑁)) ⊆ (0..^𝑁)) → ((bits‘𝐴) ∩ (0..^𝑁)) ∈ Fin) |
33 | 30, 31, 32 | mp2an 688 |
. . . . . . . . . . . . 13
⊢
((bits‘𝐴)
∩ (0..^𝑁)) ∈
Fin |
34 | | elfpw 8679 |
. . . . . . . . . . . . 13
⊢
(((bits‘𝐴)
∩ (0..^𝑁)) ∈
(𝒫 ℕ0 ∩ Fin) ↔ (((bits‘𝐴) ∩ (0..^𝑁)) ⊆ ℕ0 ∧
((bits‘𝐴) ∩
(0..^𝑁)) ∈
Fin)) |
35 | 29, 33, 34 | mpbir2an 707 |
. . . . . . . . . . . 12
⊢
((bits‘𝐴)
∩ (0..^𝑁)) ∈
(𝒫 ℕ0 ∩ Fin) |
36 | | f1ocnv 6502 |
. . . . . . . . . . . . . . 15
⊢ ((bits
↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩ Fin)
→ ◡(bits ↾
ℕ0):(𝒫 ℕ0 ∩ Fin)–1-1-onto→ℕ0) |
37 | | f1of 6490 |
. . . . . . . . . . . . . . 15
⊢ (◡(bits ↾
ℕ0):(𝒫 ℕ0 ∩ Fin)–1-1-onto→ℕ0 → ◡(bits ↾
ℕ0):(𝒫 ℕ0 ∩
Fin)⟶ℕ0) |
38 | 13, 36, 37 | mp2b 10 |
. . . . . . . . . . . . . 14
⊢ ◡(bits ↾
ℕ0):(𝒫 ℕ0 ∩
Fin)⟶ℕ0 |
39 | 1 | feq1i 6380 |
. . . . . . . . . . . . . 14
⊢ (𝐾:(𝒫 ℕ0
∩ Fin)⟶ℕ0 ↔ ◡(bits ↾
ℕ0):(𝒫 ℕ0 ∩
Fin)⟶ℕ0) |
40 | 38, 39 | mpbir 232 |
. . . . . . . . . . . . 13
⊢ 𝐾:(𝒫 ℕ0
∩ Fin)⟶ℕ0 |
41 | 40 | ffvelrni 6722 |
. . . . . . . . . . . 12
⊢
(((bits‘𝐴)
∩ (0..^𝑁)) ∈
(𝒫 ℕ0 ∩ Fin) → (𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) ∈
ℕ0) |
42 | 35, 41 | mp1i 13 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) ∈
ℕ0) |
43 | 42 | nn0zd 11939 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) ∈ ℤ) |
44 | 3, 43 | zsubcld 11946 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) ∈ ℤ) |
45 | | dvdsval2 15447 |
. . . . . . . . 9
⊢
(((2↑𝑁) ∈
ℤ ∧ (2↑𝑁)
≠ 0 ∧ (𝐴 −
(𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) ∈ ℤ) → ((2↑𝑁) ∥ (𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) ↔ ((𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) / (2↑𝑁)) ∈ ℤ)) |
46 | 25, 26, 44, 45 | syl3anc 1364 |
. . . . . . . 8
⊢ (𝜑 → ((2↑𝑁) ∥ (𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) ↔ ((𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) / (2↑𝑁)) ∈ ℤ)) |
47 | 24, 46 | mpbird 258 |
. . . . . . 7
⊢ (𝜑 → (2↑𝑁) ∥ (𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁))))) |
48 | 1 | fveq1i 6546 |
. . . . . . . . . . . 12
⊢ (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))) = (◡(bits ↾
ℕ0)‘((bits‘𝐵) ∩ (0..^𝑁))) |
49 | | sadaddlem.2 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐵 ∈ ℤ) |
50 | 49, 7 | zmodcld 13114 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐵 mod (2↑𝑁)) ∈
ℕ0) |
51 | 50 | fvresd 6565 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((bits ↾
ℕ0)‘(𝐵 mod (2↑𝑁))) = (bits‘(𝐵 mod (2↑𝑁)))) |
52 | | bitsmod 15622 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (bits‘(𝐵 mod
(2↑𝑁))) =
((bits‘𝐵) ∩
(0..^𝑁))) |
53 | 49, 6, 52 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (bits‘(𝐵 mod (2↑𝑁))) = ((bits‘𝐵) ∩ (0..^𝑁))) |
54 | 51, 53 | eqtrd 2833 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((bits ↾
ℕ0)‘(𝐵 mod (2↑𝑁))) = ((bits‘𝐵) ∩ (0..^𝑁))) |
55 | | f1ocnvfv 6907 |
. . . . . . . . . . . . . 14
⊢ (((bits
↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩ Fin)
∧ (𝐵 mod (2↑𝑁)) ∈ ℕ0)
→ (((bits ↾ ℕ0)‘(𝐵 mod (2↑𝑁))) = ((bits‘𝐵) ∩ (0..^𝑁)) → (◡(bits ↾
ℕ0)‘((bits‘𝐵) ∩ (0..^𝑁))) = (𝐵 mod (2↑𝑁)))) |
56 | 13, 50, 55 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((bits ↾
ℕ0)‘(𝐵 mod (2↑𝑁))) = ((bits‘𝐵) ∩ (0..^𝑁)) → (◡(bits ↾
ℕ0)‘((bits‘𝐵) ∩ (0..^𝑁))) = (𝐵 mod (2↑𝑁)))) |
57 | 54, 56 | mpd 15 |
. . . . . . . . . . . 12
⊢ (𝜑 → (◡(bits ↾
ℕ0)‘((bits‘𝐵) ∩ (0..^𝑁))) = (𝐵 mod (2↑𝑁))) |
58 | 48, 57 | syl5eq 2845 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))) = (𝐵 mod (2↑𝑁))) |
59 | 58 | oveq2d 7039 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) = (𝐵 − (𝐵 mod (2↑𝑁)))) |
60 | 59 | oveq1d 7038 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) / (2↑𝑁)) = ((𝐵 − (𝐵 mod (2↑𝑁))) / (2↑𝑁))) |
61 | 49 | zred 11941 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ℝ) |
62 | | moddifz 13105 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ℝ ∧
(2↑𝑁) ∈
ℝ+) → ((𝐵 − (𝐵 mod (2↑𝑁))) / (2↑𝑁)) ∈ ℤ) |
63 | 61, 21, 62 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐵 − (𝐵 mod (2↑𝑁))) / (2↑𝑁)) ∈ ℤ) |
64 | 60, 63 | eqeltrd 2885 |
. . . . . . . 8
⊢ (𝜑 → ((𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) / (2↑𝑁)) ∈ ℤ) |
65 | | inss1 4131 |
. . . . . . . . . . . . . 14
⊢
((bits‘𝐵)
∩ (0..^𝑁)) ⊆
(bits‘𝐵) |
66 | | bitsss 15612 |
. . . . . . . . . . . . . 14
⊢
(bits‘𝐵)
⊆ ℕ0 |
67 | 65, 66 | sstri 3904 |
. . . . . . . . . . . . 13
⊢
((bits‘𝐵)
∩ (0..^𝑁)) ⊆
ℕ0 |
68 | | inss2 4132 |
. . . . . . . . . . . . . 14
⊢
((bits‘𝐵)
∩ (0..^𝑁)) ⊆
(0..^𝑁) |
69 | | ssfi 8591 |
. . . . . . . . . . . . . 14
⊢
(((0..^𝑁) ∈ Fin
∧ ((bits‘𝐵) ∩
(0..^𝑁)) ⊆ (0..^𝑁)) → ((bits‘𝐵) ∩ (0..^𝑁)) ∈ Fin) |
70 | 30, 68, 69 | mp2an 688 |
. . . . . . . . . . . . 13
⊢
((bits‘𝐵)
∩ (0..^𝑁)) ∈
Fin |
71 | | elfpw 8679 |
. . . . . . . . . . . . 13
⊢
(((bits‘𝐵)
∩ (0..^𝑁)) ∈
(𝒫 ℕ0 ∩ Fin) ↔ (((bits‘𝐵) ∩ (0..^𝑁)) ⊆ ℕ0 ∧
((bits‘𝐵) ∩
(0..^𝑁)) ∈
Fin)) |
72 | 67, 70, 71 | mpbir2an 707 |
. . . . . . . . . . . 12
⊢
((bits‘𝐵)
∩ (0..^𝑁)) ∈
(𝒫 ℕ0 ∩ Fin) |
73 | 40 | ffvelrni 6722 |
. . . . . . . . . . . 12
⊢
(((bits‘𝐵)
∩ (0..^𝑁)) ∈
(𝒫 ℕ0 ∩ Fin) → (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))) ∈
ℕ0) |
74 | 72, 73 | mp1i 13 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))) ∈
ℕ0) |
75 | 74 | nn0zd 11939 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))) ∈ ℤ) |
76 | 49, 75 | zsubcld 11946 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) ∈ ℤ) |
77 | | dvdsval2 15447 |
. . . . . . . . 9
⊢
(((2↑𝑁) ∈
ℤ ∧ (2↑𝑁)
≠ 0 ∧ (𝐵 −
(𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) ∈ ℤ) → ((2↑𝑁) ∥ (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) ↔ ((𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) / (2↑𝑁)) ∈ ℤ)) |
78 | 25, 26, 76, 77 | syl3anc 1364 |
. . . . . . . 8
⊢ (𝜑 → ((2↑𝑁) ∥ (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) ↔ ((𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) / (2↑𝑁)) ∈ ℤ)) |
79 | 64, 78 | mpbird 258 |
. . . . . . 7
⊢ (𝜑 → (2↑𝑁) ∥ (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))))) |
80 | | dvds2add 15480 |
. . . . . . . 8
⊢
(((2↑𝑁) ∈
ℤ ∧ (𝐴 −
(𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) ∈ ℤ ∧ (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) ∈ ℤ) → (((2↑𝑁) ∥ (𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) ∧ (2↑𝑁) ∥ (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))))) → (2↑𝑁) ∥ ((𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) + (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))))))) |
81 | 25, 44, 76, 80 | syl3anc 1364 |
. . . . . . 7
⊢ (𝜑 → (((2↑𝑁) ∥ (𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) ∧ (2↑𝑁) ∥ (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))))) → (2↑𝑁) ∥ ((𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) + (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))))))) |
82 | 47, 79, 81 | mp2and 695 |
. . . . . 6
⊢ (𝜑 → (2↑𝑁) ∥ ((𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) + (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))))) |
83 | 3 | zcnd 11942 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℂ) |
84 | 49 | zcnd 11942 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℂ) |
85 | 42 | nn0cnd 11811 |
. . . . . . 7
⊢ (𝜑 → (𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) ∈ ℂ) |
86 | 74 | nn0cnd 11811 |
. . . . . . 7
⊢ (𝜑 → (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))) ∈ ℂ) |
87 | 83, 84, 85, 86 | addsub4d 10898 |
. . . . . 6
⊢ (𝜑 → ((𝐴 + 𝐵) − ((𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) + (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))))) = ((𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) + (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))))) |
88 | 82, 87 | breqtrrd 4996 |
. . . . 5
⊢ (𝜑 → (2↑𝑁) ∥ ((𝐴 + 𝐵) − ((𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) + (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))))) |
89 | 3, 49 | zaddcld 11945 |
. . . . . 6
⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℤ) |
90 | 43, 75 | zaddcld 11945 |
. . . . . 6
⊢ (𝜑 → ((𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) + (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) ∈ ℤ) |
91 | | moddvds 15455 |
. . . . . 6
⊢
(((2↑𝑁) ∈
ℕ ∧ (𝐴 + 𝐵) ∈ ℤ ∧ ((𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) + (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) ∈ ℤ) → (((𝐴 + 𝐵) mod (2↑𝑁)) = (((𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) + (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) mod (2↑𝑁)) ↔ (2↑𝑁) ∥ ((𝐴 + 𝐵) − ((𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) + (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))))))) |
92 | 7, 89, 90, 91 | syl3anc 1364 |
. . . . 5
⊢ (𝜑 → (((𝐴 + 𝐵) mod (2↑𝑁)) = (((𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) + (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) mod (2↑𝑁)) ↔ (2↑𝑁) ∥ ((𝐴 + 𝐵) − ((𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) + (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))))))) |
93 | 88, 92 | mpbird 258 |
. . . 4
⊢ (𝜑 → ((𝐴 + 𝐵) mod (2↑𝑁)) = (((𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) + (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) mod (2↑𝑁))) |
94 | 28 | a1i 11 |
. . . . 5
⊢ (𝜑 → (bits‘𝐴) ⊆
ℕ0) |
95 | 66 | a1i 11 |
. . . . 5
⊢ (𝜑 → (bits‘𝐵) ⊆
ℕ0) |
96 | | sadaddlem.c |
. . . . 5
⊢ 𝐶 = seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦
if(cadd(𝑚 ∈
(bits‘𝐴), 𝑚 ∈ (bits‘𝐵), ∅ ∈ 𝑐), 1o, ∅)),
(𝑛 ∈
ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) |
97 | 94, 95, 96, 6, 1 | sadadd3 15647 |
. . . 4
⊢ (𝜑 → ((𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) mod (2↑𝑁)) = (((𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) + (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) mod (2↑𝑁))) |
98 | | inss1 4131 |
. . . . . . . . 9
⊢
(((bits‘𝐴)
sadd (bits‘𝐵)) ∩
(0..^𝑁)) ⊆
((bits‘𝐴) sadd
(bits‘𝐵)) |
99 | | sadcl 15648 |
. . . . . . . . . 10
⊢
(((bits‘𝐴)
⊆ ℕ0 ∧ (bits‘𝐵) ⊆ ℕ0) →
((bits‘𝐴) sadd
(bits‘𝐵)) ⊆
ℕ0) |
100 | 28, 66, 99 | mp2an 688 |
. . . . . . . . 9
⊢
((bits‘𝐴) sadd
(bits‘𝐵)) ⊆
ℕ0 |
101 | 98, 100 | sstri 3904 |
. . . . . . . 8
⊢
(((bits‘𝐴)
sadd (bits‘𝐵)) ∩
(0..^𝑁)) ⊆
ℕ0 |
102 | | inss2 4132 |
. . . . . . . . 9
⊢
(((bits‘𝐴)
sadd (bits‘𝐵)) ∩
(0..^𝑁)) ⊆ (0..^𝑁) |
103 | | ssfi 8591 |
. . . . . . . . 9
⊢
(((0..^𝑁) ∈ Fin
∧ (((bits‘𝐴) sadd
(bits‘𝐵)) ∩
(0..^𝑁)) ⊆ (0..^𝑁)) → (((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)) ∈ Fin) |
104 | 30, 102, 103 | mp2an 688 |
. . . . . . . 8
⊢
(((bits‘𝐴)
sadd (bits‘𝐵)) ∩
(0..^𝑁)) ∈
Fin |
105 | | elfpw 8679 |
. . . . . . . 8
⊢
((((bits‘𝐴)
sadd (bits‘𝐵)) ∩
(0..^𝑁)) ∈ (𝒫
ℕ0 ∩ Fin) ↔ ((((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)) ⊆ ℕ0 ∧
(((bits‘𝐴) sadd
(bits‘𝐵)) ∩
(0..^𝑁)) ∈
Fin)) |
106 | 101, 104,
105 | mpbir2an 707 |
. . . . . . 7
⊢
(((bits‘𝐴)
sadd (bits‘𝐵)) ∩
(0..^𝑁)) ∈ (𝒫
ℕ0 ∩ Fin) |
107 | 40 | ffvelrni 6722 |
. . . . . . 7
⊢
((((bits‘𝐴)
sadd (bits‘𝐵)) ∩
(0..^𝑁)) ∈ (𝒫
ℕ0 ∩ Fin) → (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) ∈
ℕ0) |
108 | 106, 107 | mp1i 13 |
. . . . . 6
⊢ (𝜑 → (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) ∈
ℕ0) |
109 | 108 | nn0red 11810 |
. . . . 5
⊢ (𝜑 → (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) ∈ ℝ) |
110 | 108 | nn0ge0d 11812 |
. . . . 5
⊢ (𝜑 → 0 ≤ (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))) |
111 | 1 | fveq1i 6546 |
. . . . . . . . . 10
⊢ (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) = (◡(bits ↾
ℕ0)‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) |
112 | 111 | fveq2i 6548 |
. . . . . . . . 9
⊢ ((bits
↾ ℕ0)‘(𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))) = ((bits ↾
ℕ0)‘(◡(bits
↾ ℕ0)‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))) |
113 | 108 | fvresd 6565 |
. . . . . . . . 9
⊢ (𝜑 → ((bits ↾
ℕ0)‘(𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))) = (bits‘(𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))))) |
114 | 106 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin)) |
115 | | f1ocnvfv2 6906 |
. . . . . . . . . 10
⊢ (((bits
↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩ Fin)
∧ (((bits‘𝐴) sadd
(bits‘𝐵)) ∩
(0..^𝑁)) ∈ (𝒫
ℕ0 ∩ Fin)) → ((bits ↾
ℕ0)‘(◡(bits
↾ ℕ0)‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))) = (((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) |
116 | 13, 114, 115 | sylancr 587 |
. . . . . . . . 9
⊢ (𝜑 → ((bits ↾
ℕ0)‘(◡(bits
↾ ℕ0)‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))) = (((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) |
117 | 112, 113,
116 | 3eqtr3a 2857 |
. . . . . . . 8
⊢ (𝜑 → (bits‘(𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))) = (((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) |
118 | 117, 102 | syl6eqss 3948 |
. . . . . . 7
⊢ (𝜑 → (bits‘(𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))) ⊆ (0..^𝑁)) |
119 | 108 | nn0zd 11939 |
. . . . . . . 8
⊢ (𝜑 → (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) ∈ ℤ) |
120 | | bitsfzo 15621 |
. . . . . . . 8
⊢ (((𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) ∈ ℤ ∧ 𝑁 ∈ ℕ0) → ((𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) ↔ (bits‘(𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))) ⊆ (0..^𝑁))) |
121 | 119, 6, 120 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → ((𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) ↔ (bits‘(𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))) ⊆ (0..^𝑁))) |
122 | 118, 121 | mpbird 258 |
. . . . . 6
⊢ (𝜑 → (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁))) |
123 | | elfzolt2 12901 |
. . . . . 6
⊢ ((𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) → (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) < (2↑𝑁)) |
124 | 122, 123 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) < (2↑𝑁)) |
125 | | modid 13118 |
. . . . 5
⊢ ((((𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) ∈ ℝ ∧ (2↑𝑁) ∈ ℝ+)
∧ (0 ≤ (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) ∧ (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) < (2↑𝑁))) → ((𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) mod (2↑𝑁)) = (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))) |
126 | 109, 21, 110, 124, 125 | syl22anc 835 |
. . . 4
⊢ (𝜑 → ((𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) mod (2↑𝑁)) = (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))) |
127 | 93, 97, 126 | 3eqtr2d 2839 |
. . 3
⊢ (𝜑 → ((𝐴 + 𝐵) mod (2↑𝑁)) = (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))) |
128 | 127 | fveq2d 6549 |
. 2
⊢ (𝜑 → (bits‘((𝐴 + 𝐵) mod (2↑𝑁))) = (bits‘(𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))))) |
129 | 128, 117 | eqtr2d 2834 |
1
⊢ (𝜑 → (((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)) = (bits‘((𝐴 + 𝐵) mod (2↑𝑁)))) |