Step | Hyp | Ref
| Expression |
1 | | inass 3785 |
. . . . . . . 8
⊢ ((𝐴 ∩ (0..^𝑁)) ∩ (0..^𝑁)) = (𝐴 ∩ ((0..^𝑁) ∩ (0..^𝑁))) |
2 | | inidm 3784 |
. . . . . . . . 9
⊢
((0..^𝑁) ∩
(0..^𝑁)) = (0..^𝑁) |
3 | 2 | ineq2i 3773 |
. . . . . . . 8
⊢ (𝐴 ∩ ((0..^𝑁) ∩ (0..^𝑁))) = (𝐴 ∩ (0..^𝑁)) |
4 | 1, 3 | eqtri 2632 |
. . . . . . 7
⊢ ((𝐴 ∩ (0..^𝑁)) ∩ (0..^𝑁)) = (𝐴 ∩ (0..^𝑁)) |
5 | 4 | fveq2i 6106 |
. . . . . 6
⊢ (◡(bits ↾
ℕ0)‘((𝐴 ∩ (0..^𝑁)) ∩ (0..^𝑁))) = (◡(bits ↾
ℕ0)‘(𝐴 ∩ (0..^𝑁))) |
6 | | inass 3785 |
. . . . . . . 8
⊢ ((𝐵 ∩ (0..^𝑁)) ∩ (0..^𝑁)) = (𝐵 ∩ ((0..^𝑁) ∩ (0..^𝑁))) |
7 | 2 | ineq2i 3773 |
. . . . . . . 8
⊢ (𝐵 ∩ ((0..^𝑁) ∩ (0..^𝑁))) = (𝐵 ∩ (0..^𝑁)) |
8 | 6, 7 | eqtri 2632 |
. . . . . . 7
⊢ ((𝐵 ∩ (0..^𝑁)) ∩ (0..^𝑁)) = (𝐵 ∩ (0..^𝑁)) |
9 | 8 | fveq2i 6106 |
. . . . . 6
⊢ (◡(bits ↾
ℕ0)‘((𝐵 ∩ (0..^𝑁)) ∩ (0..^𝑁))) = (◡(bits ↾
ℕ0)‘(𝐵 ∩ (0..^𝑁))) |
10 | 5, 9 | oveq12i 6561 |
. . . . 5
⊢ ((◡(bits ↾
ℕ0)‘((𝐴 ∩ (0..^𝑁)) ∩ (0..^𝑁))) + (◡(bits ↾
ℕ0)‘((𝐵 ∩ (0..^𝑁)) ∩ (0..^𝑁)))) = ((◡(bits ↾
ℕ0)‘(𝐴 ∩ (0..^𝑁))) + (◡(bits ↾
ℕ0)‘(𝐵 ∩ (0..^𝑁)))) |
11 | 10 | oveq1i 6559 |
. . . 4
⊢ (((◡(bits ↾
ℕ0)‘((𝐴 ∩ (0..^𝑁)) ∩ (0..^𝑁))) + (◡(bits ↾
ℕ0)‘((𝐵 ∩ (0..^𝑁)) ∩ (0..^𝑁)))) mod (2↑𝑁)) = (((◡(bits ↾
ℕ0)‘(𝐴 ∩ (0..^𝑁))) + (◡(bits ↾
ℕ0)‘(𝐵 ∩ (0..^𝑁)))) mod (2↑𝑁)) |
12 | | inss1 3795 |
. . . . . 6
⊢ (𝐴 ∩ (0..^𝑁)) ⊆ 𝐴 |
13 | | sadeq.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ⊆
ℕ0) |
14 | 12, 13 | syl5ss 3579 |
. . . . 5
⊢ (𝜑 → (𝐴 ∩ (0..^𝑁)) ⊆
ℕ0) |
15 | | inss1 3795 |
. . . . . 6
⊢ (𝐵 ∩ (0..^𝑁)) ⊆ 𝐵 |
16 | | sadeq.b |
. . . . . 6
⊢ (𝜑 → 𝐵 ⊆
ℕ0) |
17 | 15, 16 | syl5ss 3579 |
. . . . 5
⊢ (𝜑 → (𝐵 ∩ (0..^𝑁)) ⊆
ℕ0) |
18 | | eqid 2610 |
. . . . 5
⊢
seq0((𝑐 ∈
2𝑜, 𝑚
∈ ℕ0 ↦ if(cadd(𝑚 ∈ (𝐴 ∩ (0..^𝑁)), 𝑚 ∈ (𝐵 ∩ (0..^𝑁)), ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0
↦ if(𝑛 = 0, ∅,
(𝑛 − 1)))) =
seq0((𝑐 ∈
2𝑜, 𝑚
∈ ℕ0 ↦ if(cadd(𝑚 ∈ (𝐴 ∩ (0..^𝑁)), 𝑚 ∈ (𝐵 ∩ (0..^𝑁)), ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0
↦ if(𝑛 = 0, ∅,
(𝑛 −
1)))) |
19 | | sadeq.n |
. . . . 5
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
20 | | eqid 2610 |
. . . . 5
⊢ ◡(bits ↾ ℕ0) = ◡(bits ↾
ℕ0) |
21 | 14, 17, 18, 19, 20 | sadadd3 15021 |
. . . 4
⊢ (𝜑 → ((◡(bits ↾
ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) mod (2↑𝑁)) = (((◡(bits ↾
ℕ0)‘((𝐴 ∩ (0..^𝑁)) ∩ (0..^𝑁))) + (◡(bits ↾
ℕ0)‘((𝐵 ∩ (0..^𝑁)) ∩ (0..^𝑁)))) mod (2↑𝑁))) |
22 | | eqid 2610 |
. . . . 5
⊢
seq0((𝑐 ∈
2𝑜, 𝑚
∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0
↦ if(𝑛 = 0, ∅,
(𝑛 − 1)))) =
seq0((𝑐 ∈
2𝑜, 𝑚
∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0
↦ if(𝑛 = 0, ∅,
(𝑛 −
1)))) |
23 | 13, 16, 22, 19, 20 | sadadd3 15021 |
. . . 4
⊢ (𝜑 → ((◡(bits ↾
ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) mod (2↑𝑁)) = (((◡(bits ↾
ℕ0)‘(𝐴 ∩ (0..^𝑁))) + (◡(bits ↾
ℕ0)‘(𝐵 ∩ (0..^𝑁)))) mod (2↑𝑁))) |
24 | 11, 21, 23 | 3eqtr4a 2670 |
. . 3
⊢ (𝜑 → ((◡(bits ↾
ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) mod (2↑𝑁)) = ((◡(bits ↾
ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) mod (2↑𝑁))) |
25 | | inss1 3795 |
. . . . . . . 8
⊢ (((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)) ⊆ ((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) |
26 | | sadcl 15022 |
. . . . . . . . 9
⊢ (((𝐴 ∩ (0..^𝑁)) ⊆ ℕ0 ∧ (𝐵 ∩ (0..^𝑁)) ⊆ ℕ0) →
((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ⊆
ℕ0) |
27 | 14, 17, 26 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ⊆
ℕ0) |
28 | 25, 27 | syl5ss 3579 |
. . . . . . 7
⊢ (𝜑 → (((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)) ⊆
ℕ0) |
29 | | fzofi 12635 |
. . . . . . . . 9
⊢
(0..^𝑁) ∈
Fin |
30 | 29 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (0..^𝑁) ∈ Fin) |
31 | | inss2 3796 |
. . . . . . . 8
⊢ (((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)) ⊆ (0..^𝑁) |
32 | | ssfi 8065 |
. . . . . . . 8
⊢
(((0..^𝑁) ∈ Fin
∧ (((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)) ⊆ (0..^𝑁)) → (((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)) ∈ Fin) |
33 | 30, 31, 32 | sylancl 693 |
. . . . . . 7
⊢ (𝜑 → (((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)) ∈ Fin) |
34 | | elfpw 8151 |
. . . . . . 7
⊢ ((((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin) ↔ ((((𝐴
∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)) ⊆ ℕ0 ∧
(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)) ∈ Fin)) |
35 | 28, 33, 34 | sylanbrc 695 |
. . . . . 6
⊢ (𝜑 → (((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin)) |
36 | | bitsf1o 15005 |
. . . . . . . 8
⊢ (bits
↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩
Fin) |
37 | | f1ocnv 6062 |
. . . . . . . 8
⊢ ((bits
↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩ Fin)
→ ◡(bits ↾
ℕ0):(𝒫 ℕ0 ∩ Fin)–1-1-onto→ℕ0) |
38 | | f1of 6050 |
. . . . . . . 8
⊢ (◡(bits ↾
ℕ0):(𝒫 ℕ0 ∩ Fin)–1-1-onto→ℕ0 → ◡(bits ↾
ℕ0):(𝒫 ℕ0 ∩
Fin)⟶ℕ0) |
39 | 36, 37, 38 | mp2b 10 |
. . . . . . 7
⊢ ◡(bits ↾
ℕ0):(𝒫 ℕ0 ∩
Fin)⟶ℕ0 |
40 | 39 | ffvelrni 6266 |
. . . . . 6
⊢ ((((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin) → (◡(bits ↾
ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) ∈
ℕ0) |
41 | 35, 40 | syl 17 |
. . . . 5
⊢ (𝜑 → (◡(bits ↾
ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) ∈
ℕ0) |
42 | 41 | nn0red 11229 |
. . . 4
⊢ (𝜑 → (◡(bits ↾
ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) ∈ ℝ) |
43 | | 2rp 11713 |
. . . . . 6
⊢ 2 ∈
ℝ+ |
44 | 43 | a1i 11 |
. . . . 5
⊢ (𝜑 → 2 ∈
ℝ+) |
45 | 19 | nn0zd 11356 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℤ) |
46 | 44, 45 | rpexpcld 12894 |
. . . 4
⊢ (𝜑 → (2↑𝑁) ∈
ℝ+) |
47 | 41 | nn0ge0d 11231 |
. . . 4
⊢ (𝜑 → 0 ≤ (◡(bits ↾
ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)))) |
48 | | fvres 6117 |
. . . . . . . . 9
⊢ ((◡(bits ↾
ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) ∈ ℕ0 → ((bits
↾ ℕ0)‘(◡(bits ↾
ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)))) = (bits‘(◡(bits ↾
ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))))) |
49 | 41, 48 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((bits ↾
ℕ0)‘(◡(bits
↾ ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)))) = (bits‘(◡(bits ↾
ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))))) |
50 | | f1ocnvfv2 6433 |
. . . . . . . . 9
⊢ (((bits
↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩ Fin)
∧ (((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin)) → ((bits ↾ ℕ0)‘(◡(bits ↾
ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)))) = (((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) |
51 | 36, 35, 50 | sylancr 694 |
. . . . . . . 8
⊢ (𝜑 → ((bits ↾
ℕ0)‘(◡(bits
↾ ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)))) = (((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) |
52 | 49, 51 | eqtr3d 2646 |
. . . . . . 7
⊢ (𝜑 → (bits‘(◡(bits ↾
ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)))) = (((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) |
53 | 52, 31 | syl6eqss 3618 |
. . . . . 6
⊢ (𝜑 → (bits‘(◡(bits ↾
ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)))) ⊆ (0..^𝑁)) |
54 | 41 | nn0zd 11356 |
. . . . . . 7
⊢ (𝜑 → (◡(bits ↾
ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) ∈ ℤ) |
55 | | bitsfzo 14995 |
. . . . . . 7
⊢ (((◡(bits ↾
ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) ∈ ℤ ∧ 𝑁 ∈ ℕ0) → ((◡(bits ↾
ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) ↔ (bits‘(◡(bits ↾
ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)))) ⊆ (0..^𝑁))) |
56 | 54, 19, 55 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → ((◡(bits ↾
ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) ↔ (bits‘(◡(bits ↾
ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)))) ⊆ (0..^𝑁))) |
57 | 53, 56 | mpbird 246 |
. . . . 5
⊢ (𝜑 → (◡(bits ↾
ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁))) |
58 | | elfzolt2 12348 |
. . . . 5
⊢ ((◡(bits ↾
ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) → (◡(bits ↾
ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) < (2↑𝑁)) |
59 | 57, 58 | syl 17 |
. . . 4
⊢ (𝜑 → (◡(bits ↾
ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) < (2↑𝑁)) |
60 | | modid 12557 |
. . . 4
⊢ ((((◡(bits ↾
ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) ∈ ℝ ∧ (2↑𝑁) ∈ ℝ+)
∧ (0 ≤ (◡(bits ↾
ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) ∧ (◡(bits ↾
ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) < (2↑𝑁))) → ((◡(bits ↾
ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) mod (2↑𝑁)) = (◡(bits ↾
ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)))) |
61 | 42, 46, 47, 59, 60 | syl22anc 1319 |
. . 3
⊢ (𝜑 → ((◡(bits ↾
ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) mod (2↑𝑁)) = (◡(bits ↾
ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)))) |
62 | | inss1 3795 |
. . . . . . . 8
⊢ ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ⊆ (𝐴 sadd 𝐵) |
63 | | sadcl 15022 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ ℕ0
∧ 𝐵 ⊆
ℕ0) → (𝐴 sadd 𝐵) ⊆
ℕ0) |
64 | 13, 16, 63 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 sadd 𝐵) ⊆
ℕ0) |
65 | 62, 64 | syl5ss 3579 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ⊆
ℕ0) |
66 | | inss2 3796 |
. . . . . . . 8
⊢ ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ⊆ (0..^𝑁) |
67 | | ssfi 8065 |
. . . . . . . 8
⊢
(((0..^𝑁) ∈ Fin
∧ ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ⊆ (0..^𝑁)) → ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ Fin) |
68 | 30, 66, 67 | sylancl 693 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ Fin) |
69 | | elfpw 8151 |
. . . . . . 7
⊢ (((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin) ↔ (((𝐴 sadd
𝐵) ∩ (0..^𝑁)) ⊆ ℕ0
∧ ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ Fin)) |
70 | 65, 68, 69 | sylanbrc 695 |
. . . . . 6
⊢ (𝜑 → ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin)) |
71 | 39 | ffvelrni 6266 |
. . . . . 6
⊢ (((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin) → (◡(bits ↾
ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) ∈
ℕ0) |
72 | 70, 71 | syl 17 |
. . . . 5
⊢ (𝜑 → (◡(bits ↾
ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) ∈
ℕ0) |
73 | 72 | nn0red 11229 |
. . . 4
⊢ (𝜑 → (◡(bits ↾
ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) ∈ ℝ) |
74 | 72 | nn0ge0d 11231 |
. . . 4
⊢ (𝜑 → 0 ≤ (◡(bits ↾
ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁)))) |
75 | | fvres 6117 |
. . . . . . . . 9
⊢ ((◡(bits ↾
ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) ∈ ℕ0 → ((bits
↾ ℕ0)‘(◡(bits ↾
ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁)))) = (bits‘(◡(bits ↾
ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))))) |
76 | 72, 75 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((bits ↾
ℕ0)‘(◡(bits
↾ ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁)))) = (bits‘(◡(bits ↾
ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))))) |
77 | | f1ocnvfv2 6433 |
. . . . . . . . 9
⊢ (((bits
↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩ Fin)
∧ ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin)) → ((bits ↾ ℕ0)‘(◡(bits ↾
ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁)))) = ((𝐴 sadd 𝐵) ∩ (0..^𝑁))) |
78 | 36, 70, 77 | sylancr 694 |
. . . . . . . 8
⊢ (𝜑 → ((bits ↾
ℕ0)‘(◡(bits
↾ ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁)))) = ((𝐴 sadd 𝐵) ∩ (0..^𝑁))) |
79 | 76, 78 | eqtr3d 2646 |
. . . . . . 7
⊢ (𝜑 → (bits‘(◡(bits ↾
ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁)))) = ((𝐴 sadd 𝐵) ∩ (0..^𝑁))) |
80 | 79, 66 | syl6eqss 3618 |
. . . . . 6
⊢ (𝜑 → (bits‘(◡(bits ↾
ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁)))) ⊆ (0..^𝑁)) |
81 | 72 | nn0zd 11356 |
. . . . . . 7
⊢ (𝜑 → (◡(bits ↾
ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) ∈ ℤ) |
82 | | bitsfzo 14995 |
. . . . . . 7
⊢ (((◡(bits ↾
ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) ∈ ℤ ∧ 𝑁 ∈ ℕ0) → ((◡(bits ↾
ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) ↔ (bits‘(◡(bits ↾
ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁)))) ⊆ (0..^𝑁))) |
83 | 81, 19, 82 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → ((◡(bits ↾
ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) ↔ (bits‘(◡(bits ↾
ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁)))) ⊆ (0..^𝑁))) |
84 | 80, 83 | mpbird 246 |
. . . . 5
⊢ (𝜑 → (◡(bits ↾
ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁))) |
85 | | elfzolt2 12348 |
. . . . 5
⊢ ((◡(bits ↾
ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) → (◡(bits ↾
ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) < (2↑𝑁)) |
86 | 84, 85 | syl 17 |
. . . 4
⊢ (𝜑 → (◡(bits ↾
ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) < (2↑𝑁)) |
87 | | modid 12557 |
. . . 4
⊢ ((((◡(bits ↾
ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) ∈ ℝ ∧ (2↑𝑁) ∈ ℝ+)
∧ (0 ≤ (◡(bits ↾
ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) ∧ (◡(bits ↾
ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) < (2↑𝑁))) → ((◡(bits ↾
ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) mod (2↑𝑁)) = (◡(bits ↾
ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁)))) |
88 | 73, 46, 74, 86, 87 | syl22anc 1319 |
. . 3
⊢ (𝜑 → ((◡(bits ↾
ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) mod (2↑𝑁)) = (◡(bits ↾
ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁)))) |
89 | 24, 61, 88 | 3eqtr3rd 2653 |
. 2
⊢ (𝜑 → (◡(bits ↾
ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) = (◡(bits ↾
ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)))) |
90 | | f1of1 6049 |
. . . . 5
⊢ (◡(bits ↾
ℕ0):(𝒫 ℕ0 ∩ Fin)–1-1-onto→ℕ0 → ◡(bits ↾
ℕ0):(𝒫 ℕ0 ∩ Fin)–1-1→ℕ0) |
91 | 36, 37, 90 | mp2b 10 |
. . . 4
⊢ ◡(bits ↾
ℕ0):(𝒫 ℕ0 ∩ Fin)–1-1→ℕ0 |
92 | | f1fveq 6420 |
. . . 4
⊢ ((◡(bits ↾
ℕ0):(𝒫 ℕ0 ∩ Fin)–1-1→ℕ0 ∧ (((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin) ∧ (((𝐴 ∩
(0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin))) → ((◡(bits ↾
ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) = (◡(bits ↾
ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) ↔ ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) = (((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)))) |
93 | 91, 92 | mpan 702 |
. . 3
⊢ ((((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin) ∧ (((𝐴 ∩
(0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin)) → ((◡(bits ↾
ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) = (◡(bits ↾
ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) ↔ ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) = (((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)))) |
94 | 70, 35, 93 | syl2anc 691 |
. 2
⊢ (𝜑 → ((◡(bits ↾
ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) = (◡(bits ↾
ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) ↔ ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) = (((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)))) |
95 | 89, 94 | mpbid 221 |
1
⊢ (𝜑 → ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) = (((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) |