Step | Hyp | Ref
| Expression |
1 | | 2nn 11976 |
. . . . . . . . 9
⊢ 2 ∈
ℕ |
2 | 1 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 2 ∈
ℕ) |
3 | | sadcp1.n |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
4 | 2, 3 | nnexpcld 13888 |
. . . . . . 7
⊢ (𝜑 → (2↑𝑁) ∈ ℕ) |
5 | 4 | nnzd 12354 |
. . . . . 6
⊢ (𝜑 → (2↑𝑁) ∈ ℤ) |
6 | | iddvds 15907 |
. . . . . 6
⊢
((2↑𝑁) ∈
ℤ → (2↑𝑁)
∥ (2↑𝑁)) |
7 | 5, 6 | syl 17 |
. . . . 5
⊢ (𝜑 → (2↑𝑁) ∥ (2↑𝑁)) |
8 | | dvds0 15909 |
. . . . . 6
⊢
((2↑𝑁) ∈
ℤ → (2↑𝑁)
∥ 0) |
9 | 5, 8 | syl 17 |
. . . . 5
⊢ (𝜑 → (2↑𝑁) ∥ 0) |
10 | | breq2 5074 |
. . . . . 6
⊢
((2↑𝑁) =
if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0) → ((2↑𝑁) ∥ (2↑𝑁) ↔ (2↑𝑁) ∥ if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0))) |
11 | | breq2 5074 |
. . . . . 6
⊢ (0 =
if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0) → ((2↑𝑁) ∥ 0 ↔ (2↑𝑁) ∥ if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0))) |
12 | 10, 11 | ifboth 4495 |
. . . . 5
⊢
(((2↑𝑁) ∥
(2↑𝑁) ∧
(2↑𝑁) ∥ 0)
→ (2↑𝑁) ∥
if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0)) |
13 | 7, 9, 12 | syl2anc 583 |
. . . 4
⊢ (𝜑 → (2↑𝑁) ∥ if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0)) |
14 | | inss1 4159 |
. . . . . . . . 9
⊢ ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ⊆ (𝐴 sadd 𝐵) |
15 | | sadval.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ⊆
ℕ0) |
16 | | sadval.b |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ⊆
ℕ0) |
17 | | sadval.c |
. . . . . . . . . . 11
⊢ 𝐶 = seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦
if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0
↦ if(𝑛 = 0, ∅,
(𝑛 −
1)))) |
18 | 15, 16, 17 | sadfval 16087 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 sadd 𝐵) = {𝑘 ∈ ℕ0 ∣
hadd(𝑘 ∈ 𝐴, 𝑘 ∈ 𝐵, ∅ ∈ (𝐶‘𝑘))}) |
19 | | ssrab2 4009 |
. . . . . . . . . 10
⊢ {𝑘 ∈ ℕ0
∣ hadd(𝑘 ∈ 𝐴, 𝑘 ∈ 𝐵, ∅ ∈ (𝐶‘𝑘))} ⊆
ℕ0 |
20 | 18, 19 | eqsstrdi 3971 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 sadd 𝐵) ⊆
ℕ0) |
21 | 14, 20 | sstrid 3928 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ⊆
ℕ0) |
22 | | fzofi 13622 |
. . . . . . . . . 10
⊢
(0..^𝑁) ∈
Fin |
23 | 22 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (0..^𝑁) ∈ Fin) |
24 | | inss2 4160 |
. . . . . . . . 9
⊢ ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ⊆ (0..^𝑁) |
25 | | ssfi 8918 |
. . . . . . . . 9
⊢
(((0..^𝑁) ∈ Fin
∧ ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ⊆ (0..^𝑁)) → ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ Fin) |
26 | 23, 24, 25 | sylancl 585 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ Fin) |
27 | | elfpw 9051 |
. . . . . . . 8
⊢ (((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin) ↔ (((𝐴 sadd
𝐵) ∩ (0..^𝑁)) ⊆ ℕ0
∧ ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ Fin)) |
28 | 21, 26, 27 | sylanbrc 582 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin)) |
29 | | bitsf1o 16080 |
. . . . . . . . . 10
⊢ (bits
↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩
Fin) |
30 | | f1ocnv 6712 |
. . . . . . . . . 10
⊢ ((bits
↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩ Fin)
→ ◡(bits ↾
ℕ0):(𝒫 ℕ0 ∩ Fin)–1-1-onto→ℕ0) |
31 | | f1of 6700 |
. . . . . . . . . 10
⊢ (◡(bits ↾
ℕ0):(𝒫 ℕ0 ∩ Fin)–1-1-onto→ℕ0 → ◡(bits ↾
ℕ0):(𝒫 ℕ0 ∩
Fin)⟶ℕ0) |
32 | 29, 30, 31 | mp2b 10 |
. . . . . . . . 9
⊢ ◡(bits ↾
ℕ0):(𝒫 ℕ0 ∩
Fin)⟶ℕ0 |
33 | | sadcadd.k |
. . . . . . . . . 10
⊢ 𝐾 = ◡(bits ↾
ℕ0) |
34 | 33 | feq1i 6575 |
. . . . . . . . 9
⊢ (𝐾:(𝒫 ℕ0
∩ Fin)⟶ℕ0 ↔ ◡(bits ↾
ℕ0):(𝒫 ℕ0 ∩
Fin)⟶ℕ0) |
35 | 32, 34 | mpbir 230 |
. . . . . . . 8
⊢ 𝐾:(𝒫 ℕ0
∩ Fin)⟶ℕ0 |
36 | 35 | ffvelrni 6942 |
. . . . . . 7
⊢ (((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin) → (𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) ∈
ℕ0) |
37 | 28, 36 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) ∈
ℕ0) |
38 | 37 | nn0cnd 12225 |
. . . . 5
⊢ (𝜑 → (𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) ∈ ℂ) |
39 | 4 | nncnd 11919 |
. . . . . 6
⊢ (𝜑 → (2↑𝑁) ∈ ℂ) |
40 | | 0cn 10898 |
. . . . . 6
⊢ 0 ∈
ℂ |
41 | | ifcl 4501 |
. . . . . 6
⊢
(((2↑𝑁) ∈
ℂ ∧ 0 ∈ ℂ) → if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0) ∈ ℂ) |
42 | 39, 40, 41 | sylancl 585 |
. . . . 5
⊢ (𝜑 → if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0) ∈ ℂ) |
43 | 38, 42 | pncan2d 11264 |
. . . 4
⊢ (𝜑 → (((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0)) − (𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁)))) = if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0)) |
44 | 13, 43 | breqtrrd 5098 |
. . 3
⊢ (𝜑 → (2↑𝑁) ∥ (((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0)) − (𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))))) |
45 | 37 | nn0zd 12353 |
. . . . 5
⊢ (𝜑 → (𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) ∈ ℤ) |
46 | 5 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) → (2↑𝑁) ∈ ℤ) |
47 | | 0zd 12261 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) → 0 ∈ ℤ) |
48 | 46, 47 | ifclda 4491 |
. . . . 5
⊢ (𝜑 → if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0) ∈ ℤ) |
49 | 45, 48 | zaddcld 12359 |
. . . 4
⊢ (𝜑 → ((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0)) ∈ ℤ) |
50 | | moddvds 15902 |
. . . 4
⊢
(((2↑𝑁) ∈
ℕ ∧ ((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0)) ∈ ℤ ∧ (𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) ∈ ℤ) → ((((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0)) mod (2↑𝑁)) = ((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) mod (2↑𝑁)) ↔ (2↑𝑁) ∥ (((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0)) − (𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁)))))) |
51 | 4, 49, 45, 50 | syl3anc 1369 |
. . 3
⊢ (𝜑 → ((((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0)) mod (2↑𝑁)) = ((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) mod (2↑𝑁)) ↔ (2↑𝑁) ∥ (((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0)) − (𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁)))))) |
52 | 44, 51 | mpbird 256 |
. 2
⊢ (𝜑 → (((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0)) mod (2↑𝑁)) = ((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) mod (2↑𝑁))) |
53 | 15, 16, 17, 3, 33 | sadadd2 16095 |
. . 3
⊢ (𝜑 → ((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0)) = ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁))))) |
54 | 53 | oveq1d 7270 |
. 2
⊢ (𝜑 → (((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0)) mod (2↑𝑁)) = (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) mod (2↑𝑁))) |
55 | 52, 54 | eqtr3d 2780 |
1
⊢ (𝜑 → ((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) mod (2↑𝑁)) = (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) mod (2↑𝑁))) |