Proof of Theorem sadaddlem
Step | Hyp | Ref
| Expression |
1 | | sadaddlem.k |
. . . . . . . . . . . . 13
⊢ 𝐾 = ◡(bits ↾
ℕ0) |
2 | 1 | fveq1i 6192 |
. . . . . . . . . . . 12
⊢ (𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) = (◡(bits ↾
ℕ0)‘((bits‘𝐴) ∩ (0..^𝑁))) |
3 | | sadaddlem.1 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 ∈ ℤ) |
4 | | 2nn 11185 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℕ |
5 | 4 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 2 ∈
ℕ) |
6 | | sadaddlem.3 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
7 | 5, 6 | nnexpcld 13030 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (2↑𝑁) ∈ ℕ) |
8 | 3, 7 | zmodcld 12691 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴 mod (2↑𝑁)) ∈
ℕ0) |
9 | | fvres 6207 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 mod (2↑𝑁)) ∈ ℕ0 → ((bits
↾ ℕ0)‘(𝐴 mod (2↑𝑁))) = (bits‘(𝐴 mod (2↑𝑁)))) |
10 | 8, 9 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((bits ↾
ℕ0)‘(𝐴 mod (2↑𝑁))) = (bits‘(𝐴 mod (2↑𝑁)))) |
11 | | bitsmod 15158 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (bits‘(𝐴 mod
(2↑𝑁))) =
((bits‘𝐴) ∩
(0..^𝑁))) |
12 | 3, 6, 11 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (bits‘(𝐴 mod (2↑𝑁))) = ((bits‘𝐴) ∩ (0..^𝑁))) |
13 | 10, 12 | eqtrd 2656 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((bits ↾
ℕ0)‘(𝐴 mod (2↑𝑁))) = ((bits‘𝐴) ∩ (0..^𝑁))) |
14 | | bitsf1o 15167 |
. . . . . . . . . . . . . 14
⊢ (bits
↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩
Fin) |
15 | | f1ocnvfv 6534 |
. . . . . . . . . . . . . 14
⊢ (((bits
↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩ Fin)
∧ (𝐴 mod (2↑𝑁)) ∈ ℕ0)
→ (((bits ↾ ℕ0)‘(𝐴 mod (2↑𝑁))) = ((bits‘𝐴) ∩ (0..^𝑁)) → (◡(bits ↾
ℕ0)‘((bits‘𝐴) ∩ (0..^𝑁))) = (𝐴 mod (2↑𝑁)))) |
16 | 14, 8, 15 | sylancr 695 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((bits ↾
ℕ0)‘(𝐴 mod (2↑𝑁))) = ((bits‘𝐴) ∩ (0..^𝑁)) → (◡(bits ↾
ℕ0)‘((bits‘𝐴) ∩ (0..^𝑁))) = (𝐴 mod (2↑𝑁)))) |
17 | 13, 16 | mpd 15 |
. . . . . . . . . . . 12
⊢ (𝜑 → (◡(bits ↾
ℕ0)‘((bits‘𝐴) ∩ (0..^𝑁))) = (𝐴 mod (2↑𝑁))) |
18 | 2, 17 | syl5eq 2668 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) = (𝐴 mod (2↑𝑁))) |
19 | 18 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) = (𝐴 − (𝐴 mod (2↑𝑁)))) |
20 | 19 | oveq1d 6665 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) / (2↑𝑁)) = ((𝐴 − (𝐴 mod (2↑𝑁))) / (2↑𝑁))) |
21 | 3 | zred 11482 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ ℝ) |
22 | 7 | nnrpd 11870 |
. . . . . . . . . 10
⊢ (𝜑 → (2↑𝑁) ∈
ℝ+) |
23 | | moddifz 12682 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧
(2↑𝑁) ∈
ℝ+) → ((𝐴 − (𝐴 mod (2↑𝑁))) / (2↑𝑁)) ∈ ℤ) |
24 | 21, 22, 23 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴 − (𝐴 mod (2↑𝑁))) / (2↑𝑁)) ∈ ℤ) |
25 | 20, 24 | eqeltrd 2701 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) / (2↑𝑁)) ∈ ℤ) |
26 | 7 | nnzd 11481 |
. . . . . . . . 9
⊢ (𝜑 → (2↑𝑁) ∈ ℤ) |
27 | 7 | nnne0d 11065 |
. . . . . . . . 9
⊢ (𝜑 → (2↑𝑁) ≠ 0) |
28 | | inss1 3833 |
. . . . . . . . . . . . . 14
⊢
((bits‘𝐴)
∩ (0..^𝑁)) ⊆
(bits‘𝐴) |
29 | | bitsss 15148 |
. . . . . . . . . . . . . 14
⊢
(bits‘𝐴)
⊆ ℕ0 |
30 | 28, 29 | sstri 3612 |
. . . . . . . . . . . . 13
⊢
((bits‘𝐴)
∩ (0..^𝑁)) ⊆
ℕ0 |
31 | | fzofi 12773 |
. . . . . . . . . . . . . 14
⊢
(0..^𝑁) ∈
Fin |
32 | | inss2 3834 |
. . . . . . . . . . . . . 14
⊢
((bits‘𝐴)
∩ (0..^𝑁)) ⊆
(0..^𝑁) |
33 | | ssfi 8180 |
. . . . . . . . . . . . . 14
⊢
(((0..^𝑁) ∈ Fin
∧ ((bits‘𝐴) ∩
(0..^𝑁)) ⊆ (0..^𝑁)) → ((bits‘𝐴) ∩ (0..^𝑁)) ∈ Fin) |
34 | 31, 32, 33 | mp2an 708 |
. . . . . . . . . . . . 13
⊢
((bits‘𝐴)
∩ (0..^𝑁)) ∈
Fin |
35 | | elfpw 8268 |
. . . . . . . . . . . . 13
⊢
(((bits‘𝐴)
∩ (0..^𝑁)) ∈
(𝒫 ℕ0 ∩ Fin) ↔ (((bits‘𝐴) ∩ (0..^𝑁)) ⊆ ℕ0 ∧
((bits‘𝐴) ∩
(0..^𝑁)) ∈
Fin)) |
36 | 30, 34, 35 | mpbir2an 955 |
. . . . . . . . . . . 12
⊢
((bits‘𝐴)
∩ (0..^𝑁)) ∈
(𝒫 ℕ0 ∩ Fin) |
37 | | f1ocnv 6149 |
. . . . . . . . . . . . . . 15
⊢ ((bits
↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩ Fin)
→ ◡(bits ↾
ℕ0):(𝒫 ℕ0 ∩ Fin)–1-1-onto→ℕ0) |
38 | | f1of 6137 |
. . . . . . . . . . . . . . 15
⊢ (◡(bits ↾
ℕ0):(𝒫 ℕ0 ∩ Fin)–1-1-onto→ℕ0 → ◡(bits ↾
ℕ0):(𝒫 ℕ0 ∩
Fin)⟶ℕ0) |
39 | 14, 37, 38 | mp2b 10 |
. . . . . . . . . . . . . 14
⊢ ◡(bits ↾
ℕ0):(𝒫 ℕ0 ∩
Fin)⟶ℕ0 |
40 | 1 | feq1i 6036 |
. . . . . . . . . . . . . 14
⊢ (𝐾:(𝒫 ℕ0
∩ Fin)⟶ℕ0 ↔ ◡(bits ↾
ℕ0):(𝒫 ℕ0 ∩
Fin)⟶ℕ0) |
41 | 39, 40 | mpbir 221 |
. . . . . . . . . . . . 13
⊢ 𝐾:(𝒫 ℕ0
∩ Fin)⟶ℕ0 |
42 | 41 | ffvelrni 6358 |
. . . . . . . . . . . 12
⊢
(((bits‘𝐴)
∩ (0..^𝑁)) ∈
(𝒫 ℕ0 ∩ Fin) → (𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) ∈
ℕ0) |
43 | 36, 42 | mp1i 13 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) ∈
ℕ0) |
44 | 43 | nn0zd 11480 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) ∈ ℤ) |
45 | 3, 44 | zsubcld 11487 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) ∈ ℤ) |
46 | | dvdsval2 14986 |
. . . . . . . . 9
⊢
(((2↑𝑁) ∈
ℤ ∧ (2↑𝑁)
≠ 0 ∧ (𝐴 −
(𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) ∈ ℤ) → ((2↑𝑁) ∥ (𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) ↔ ((𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) / (2↑𝑁)) ∈ ℤ)) |
47 | 26, 27, 45, 46 | syl3anc 1326 |
. . . . . . . 8
⊢ (𝜑 → ((2↑𝑁) ∥ (𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) ↔ ((𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) / (2↑𝑁)) ∈ ℤ)) |
48 | 25, 47 | mpbird 247 |
. . . . . . 7
⊢ (𝜑 → (2↑𝑁) ∥ (𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁))))) |
49 | 1 | fveq1i 6192 |
. . . . . . . . . . . 12
⊢ (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))) = (◡(bits ↾
ℕ0)‘((bits‘𝐵) ∩ (0..^𝑁))) |
50 | | sadaddlem.2 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐵 ∈ ℤ) |
51 | 50, 7 | zmodcld 12691 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐵 mod (2↑𝑁)) ∈
ℕ0) |
52 | | fvres 6207 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 mod (2↑𝑁)) ∈ ℕ0 → ((bits
↾ ℕ0)‘(𝐵 mod (2↑𝑁))) = (bits‘(𝐵 mod (2↑𝑁)))) |
53 | 51, 52 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((bits ↾
ℕ0)‘(𝐵 mod (2↑𝑁))) = (bits‘(𝐵 mod (2↑𝑁)))) |
54 | | bitsmod 15158 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (bits‘(𝐵 mod
(2↑𝑁))) =
((bits‘𝐵) ∩
(0..^𝑁))) |
55 | 50, 6, 54 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (bits‘(𝐵 mod (2↑𝑁))) = ((bits‘𝐵) ∩ (0..^𝑁))) |
56 | 53, 55 | eqtrd 2656 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((bits ↾
ℕ0)‘(𝐵 mod (2↑𝑁))) = ((bits‘𝐵) ∩ (0..^𝑁))) |
57 | | f1ocnvfv 6534 |
. . . . . . . . . . . . . 14
⊢ (((bits
↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩ Fin)
∧ (𝐵 mod (2↑𝑁)) ∈ ℕ0)
→ (((bits ↾ ℕ0)‘(𝐵 mod (2↑𝑁))) = ((bits‘𝐵) ∩ (0..^𝑁)) → (◡(bits ↾
ℕ0)‘((bits‘𝐵) ∩ (0..^𝑁))) = (𝐵 mod (2↑𝑁)))) |
58 | 14, 51, 57 | sylancr 695 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((bits ↾
ℕ0)‘(𝐵 mod (2↑𝑁))) = ((bits‘𝐵) ∩ (0..^𝑁)) → (◡(bits ↾
ℕ0)‘((bits‘𝐵) ∩ (0..^𝑁))) = (𝐵 mod (2↑𝑁)))) |
59 | 56, 58 | mpd 15 |
. . . . . . . . . . . 12
⊢ (𝜑 → (◡(bits ↾
ℕ0)‘((bits‘𝐵) ∩ (0..^𝑁))) = (𝐵 mod (2↑𝑁))) |
60 | 49, 59 | syl5eq 2668 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))) = (𝐵 mod (2↑𝑁))) |
61 | 60 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) = (𝐵 − (𝐵 mod (2↑𝑁)))) |
62 | 61 | oveq1d 6665 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) / (2↑𝑁)) = ((𝐵 − (𝐵 mod (2↑𝑁))) / (2↑𝑁))) |
63 | 50 | zred 11482 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ℝ) |
64 | | moddifz 12682 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ℝ ∧
(2↑𝑁) ∈
ℝ+) → ((𝐵 − (𝐵 mod (2↑𝑁))) / (2↑𝑁)) ∈ ℤ) |
65 | 63, 22, 64 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐵 − (𝐵 mod (2↑𝑁))) / (2↑𝑁)) ∈ ℤ) |
66 | 62, 65 | eqeltrd 2701 |
. . . . . . . 8
⊢ (𝜑 → ((𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) / (2↑𝑁)) ∈ ℤ) |
67 | | inss1 3833 |
. . . . . . . . . . . . . 14
⊢
((bits‘𝐵)
∩ (0..^𝑁)) ⊆
(bits‘𝐵) |
68 | | bitsss 15148 |
. . . . . . . . . . . . . 14
⊢
(bits‘𝐵)
⊆ ℕ0 |
69 | 67, 68 | sstri 3612 |
. . . . . . . . . . . . 13
⊢
((bits‘𝐵)
∩ (0..^𝑁)) ⊆
ℕ0 |
70 | | inss2 3834 |
. . . . . . . . . . . . . 14
⊢
((bits‘𝐵)
∩ (0..^𝑁)) ⊆
(0..^𝑁) |
71 | | ssfi 8180 |
. . . . . . . . . . . . . 14
⊢
(((0..^𝑁) ∈ Fin
∧ ((bits‘𝐵) ∩
(0..^𝑁)) ⊆ (0..^𝑁)) → ((bits‘𝐵) ∩ (0..^𝑁)) ∈ Fin) |
72 | 31, 70, 71 | mp2an 708 |
. . . . . . . . . . . . 13
⊢
((bits‘𝐵)
∩ (0..^𝑁)) ∈
Fin |
73 | | elfpw 8268 |
. . . . . . . . . . . . 13
⊢
(((bits‘𝐵)
∩ (0..^𝑁)) ∈
(𝒫 ℕ0 ∩ Fin) ↔ (((bits‘𝐵) ∩ (0..^𝑁)) ⊆ ℕ0 ∧
((bits‘𝐵) ∩
(0..^𝑁)) ∈
Fin)) |
74 | 69, 72, 73 | mpbir2an 955 |
. . . . . . . . . . . 12
⊢
((bits‘𝐵)
∩ (0..^𝑁)) ∈
(𝒫 ℕ0 ∩ Fin) |
75 | 41 | ffvelrni 6358 |
. . . . . . . . . . . 12
⊢
(((bits‘𝐵)
∩ (0..^𝑁)) ∈
(𝒫 ℕ0 ∩ Fin) → (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))) ∈
ℕ0) |
76 | 74, 75 | mp1i 13 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))) ∈
ℕ0) |
77 | 76 | nn0zd 11480 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))) ∈ ℤ) |
78 | 50, 77 | zsubcld 11487 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) ∈ ℤ) |
79 | | dvdsval2 14986 |
. . . . . . . . 9
⊢
(((2↑𝑁) ∈
ℤ ∧ (2↑𝑁)
≠ 0 ∧ (𝐵 −
(𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) ∈ ℤ) → ((2↑𝑁) ∥ (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) ↔ ((𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) / (2↑𝑁)) ∈ ℤ)) |
80 | 26, 27, 78, 79 | syl3anc 1326 |
. . . . . . . 8
⊢ (𝜑 → ((2↑𝑁) ∥ (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) ↔ ((𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) / (2↑𝑁)) ∈ ℤ)) |
81 | 66, 80 | mpbird 247 |
. . . . . . 7
⊢ (𝜑 → (2↑𝑁) ∥ (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))))) |
82 | | dvds2add 15015 |
. . . . . . . 8
⊢
(((2↑𝑁) ∈
ℤ ∧ (𝐴 −
(𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) ∈ ℤ ∧ (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) ∈ ℤ) → (((2↑𝑁) ∥ (𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) ∧ (2↑𝑁) ∥ (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))))) → (2↑𝑁) ∥ ((𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) + (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))))))) |
83 | 26, 45, 78, 82 | syl3anc 1326 |
. . . . . . 7
⊢ (𝜑 → (((2↑𝑁) ∥ (𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) ∧ (2↑𝑁) ∥ (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))))) → (2↑𝑁) ∥ ((𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) + (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))))))) |
84 | 48, 81, 83 | mp2and 715 |
. . . . . 6
⊢ (𝜑 → (2↑𝑁) ∥ ((𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) + (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))))) |
85 | 3 | zcnd 11483 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℂ) |
86 | 50 | zcnd 11483 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℂ) |
87 | 43 | nn0cnd 11353 |
. . . . . . 7
⊢ (𝜑 → (𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) ∈ ℂ) |
88 | 76 | nn0cnd 11353 |
. . . . . . 7
⊢ (𝜑 → (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))) ∈ ℂ) |
89 | 85, 86, 87, 88 | addsub4d 10439 |
. . . . . 6
⊢ (𝜑 → ((𝐴 + 𝐵) − ((𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) + (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))))) = ((𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) + (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))))) |
90 | 84, 89 | breqtrrd 4681 |
. . . . 5
⊢ (𝜑 → (2↑𝑁) ∥ ((𝐴 + 𝐵) − ((𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) + (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))))) |
91 | 3, 50 | zaddcld 11486 |
. . . . . 6
⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℤ) |
92 | 44, 77 | zaddcld 11486 |
. . . . . 6
⊢ (𝜑 → ((𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) + (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) ∈ ℤ) |
93 | | moddvds 14991 |
. . . . . 6
⊢
(((2↑𝑁) ∈
ℕ ∧ (𝐴 + 𝐵) ∈ ℤ ∧ ((𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) + (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) ∈ ℤ) → (((𝐴 + 𝐵) mod (2↑𝑁)) = (((𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) + (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) mod (2↑𝑁)) ↔ (2↑𝑁) ∥ ((𝐴 + 𝐵) − ((𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) + (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))))))) |
94 | 7, 91, 92, 93 | syl3anc 1326 |
. . . . 5
⊢ (𝜑 → (((𝐴 + 𝐵) mod (2↑𝑁)) = (((𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) + (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) mod (2↑𝑁)) ↔ (2↑𝑁) ∥ ((𝐴 + 𝐵) − ((𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) + (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))))))) |
95 | 90, 94 | mpbird 247 |
. . . 4
⊢ (𝜑 → ((𝐴 + 𝐵) mod (2↑𝑁)) = (((𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) + (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) mod (2↑𝑁))) |
96 | 29 | a1i 11 |
. . . . 5
⊢ (𝜑 → (bits‘𝐴) ⊆
ℕ0) |
97 | 68 | a1i 11 |
. . . . 5
⊢ (𝜑 → (bits‘𝐵) ⊆
ℕ0) |
98 | | sadaddlem.c |
. . . . 5
⊢ 𝐶 = seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0
↦ if(cadd(𝑚 ∈
(bits‘𝐴), 𝑚 ∈ (bits‘𝐵), ∅ ∈ 𝑐), 1𝑜,
∅)), (𝑛 ∈
ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) |
99 | 96, 97, 98, 6, 1 | sadadd3 15183 |
. . . 4
⊢ (𝜑 → ((𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) mod (2↑𝑁)) = (((𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) + (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) mod (2↑𝑁))) |
100 | | inss1 3833 |
. . . . . . . . 9
⊢
(((bits‘𝐴)
sadd (bits‘𝐵)) ∩
(0..^𝑁)) ⊆
((bits‘𝐴) sadd
(bits‘𝐵)) |
101 | | sadcl 15184 |
. . . . . . . . . 10
⊢
(((bits‘𝐴)
⊆ ℕ0 ∧ (bits‘𝐵) ⊆ ℕ0) →
((bits‘𝐴) sadd
(bits‘𝐵)) ⊆
ℕ0) |
102 | 29, 68, 101 | mp2an 708 |
. . . . . . . . 9
⊢
((bits‘𝐴) sadd
(bits‘𝐵)) ⊆
ℕ0 |
103 | 100, 102 | sstri 3612 |
. . . . . . . 8
⊢
(((bits‘𝐴)
sadd (bits‘𝐵)) ∩
(0..^𝑁)) ⊆
ℕ0 |
104 | | inss2 3834 |
. . . . . . . . 9
⊢
(((bits‘𝐴)
sadd (bits‘𝐵)) ∩
(0..^𝑁)) ⊆ (0..^𝑁) |
105 | | ssfi 8180 |
. . . . . . . . 9
⊢
(((0..^𝑁) ∈ Fin
∧ (((bits‘𝐴) sadd
(bits‘𝐵)) ∩
(0..^𝑁)) ⊆ (0..^𝑁)) → (((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)) ∈ Fin) |
106 | 31, 104, 105 | mp2an 708 |
. . . . . . . 8
⊢
(((bits‘𝐴)
sadd (bits‘𝐵)) ∩
(0..^𝑁)) ∈
Fin |
107 | | elfpw 8268 |
. . . . . . . 8
⊢
((((bits‘𝐴)
sadd (bits‘𝐵)) ∩
(0..^𝑁)) ∈ (𝒫
ℕ0 ∩ Fin) ↔ ((((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)) ⊆ ℕ0 ∧
(((bits‘𝐴) sadd
(bits‘𝐵)) ∩
(0..^𝑁)) ∈
Fin)) |
108 | 103, 106,
107 | mpbir2an 955 |
. . . . . . 7
⊢
(((bits‘𝐴)
sadd (bits‘𝐵)) ∩
(0..^𝑁)) ∈ (𝒫
ℕ0 ∩ Fin) |
109 | 41 | ffvelrni 6358 |
. . . . . . 7
⊢
((((bits‘𝐴)
sadd (bits‘𝐵)) ∩
(0..^𝑁)) ∈ (𝒫
ℕ0 ∩ Fin) → (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) ∈
ℕ0) |
110 | 108, 109 | mp1i 13 |
. . . . . 6
⊢ (𝜑 → (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) ∈
ℕ0) |
111 | 110 | nn0red 11352 |
. . . . 5
⊢ (𝜑 → (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) ∈ ℝ) |
112 | 110 | nn0ge0d 11354 |
. . . . 5
⊢ (𝜑 → 0 ≤ (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))) |
113 | 1 | fveq1i 6192 |
. . . . . . . . . 10
⊢ (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) = (◡(bits ↾
ℕ0)‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) |
114 | 113 | fveq2i 6194 |
. . . . . . . . 9
⊢ ((bits
↾ ℕ0)‘(𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))) = ((bits ↾
ℕ0)‘(◡(bits
↾ ℕ0)‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))) |
115 | | fvres 6207 |
. . . . . . . . . 10
⊢ ((𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) ∈ ℕ0 → ((bits
↾ ℕ0)‘(𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))) = (bits‘(𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))))) |
116 | 110, 115 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((bits ↾
ℕ0)‘(𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))) = (bits‘(𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))))) |
117 | 108 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin)) |
118 | | f1ocnvfv2 6533 |
. . . . . . . . . 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..^𝑁))) |
119 | 14, 117, 118 | sylancr 695 |
. . . . . . . . 9
⊢ (𝜑 → ((bits ↾
ℕ0)‘(◡(bits
↾ ℕ0)‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))) = (((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) |
120 | 114, 116,
119 | 3eqtr3a 2680 |
. . . . . . . 8
⊢ (𝜑 → (bits‘(𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))) = (((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) |
121 | 120, 104 | syl6eqss 3655 |
. . . . . . 7
⊢ (𝜑 → (bits‘(𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))) ⊆ (0..^𝑁)) |
122 | 110 | nn0zd 11480 |
. . . . . . . 8
⊢ (𝜑 → (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) ∈ ℤ) |
123 | | bitsfzo 15157 |
. . . . . . . 8
⊢ (((𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) ∈ ℤ ∧ 𝑁 ∈ ℕ0) → ((𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) ↔ (bits‘(𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))) ⊆ (0..^𝑁))) |
124 | 122, 6, 123 | syl2anc 693 |
. . . . . . 7
⊢ (𝜑 → ((𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) ↔ (bits‘(𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))) ⊆ (0..^𝑁))) |
125 | 121, 124 | mpbird 247 |
. . . . . 6
⊢ (𝜑 → (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁))) |
126 | | elfzolt2 12479 |
. . . . . 6
⊢ ((𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) → (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) < (2↑𝑁)) |
127 | 125, 126 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) < (2↑𝑁)) |
128 | | modid 12695 |
. . . . 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..^𝑁)))) |
129 | 111, 22, 112, 127, 128 | syl22anc 1327 |
. . . 4
⊢ (𝜑 → ((𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) mod (2↑𝑁)) = (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))) |
130 | 95, 99, 129 | 3eqtr2d 2662 |
. . 3
⊢ (𝜑 → ((𝐴 + 𝐵) mod (2↑𝑁)) = (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))) |
131 | 130 | fveq2d 6195 |
. 2
⊢ (𝜑 → (bits‘((𝐴 + 𝐵) mod (2↑𝑁))) = (bits‘(𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))))) |
132 | 131, 120 | eqtr2d 2657 |
1
⊢ (𝜑 → (((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)) = (bits‘((𝐴 + 𝐵) mod (2↑𝑁)))) |