| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 2nn 12339 | . . . . . . . . 9
⊢ 2 ∈
ℕ | 
| 2 | 1 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → 2 ∈
ℕ) | 
| 3 |  | sadcp1.n | . . . . . . . 8
⊢ (𝜑 → 𝑁 ∈
ℕ0) | 
| 4 | 2, 3 | nnexpcld 14284 | . . . . . . 7
⊢ (𝜑 → (2↑𝑁) ∈ ℕ) | 
| 5 | 4 | nnzd 12640 | . . . . . 6
⊢ (𝜑 → (2↑𝑁) ∈ ℤ) | 
| 6 |  | iddvds 16307 | . . . . . 6
⊢
((2↑𝑁) ∈
ℤ → (2↑𝑁)
∥ (2↑𝑁)) | 
| 7 | 5, 6 | syl 17 | . . . . 5
⊢ (𝜑 → (2↑𝑁) ∥ (2↑𝑁)) | 
| 8 |  | dvds0 16309 | . . . . . 6
⊢
((2↑𝑁) ∈
ℤ → (2↑𝑁)
∥ 0) | 
| 9 | 5, 8 | syl 17 | . . . . 5
⊢ (𝜑 → (2↑𝑁) ∥ 0) | 
| 10 |  | breq2 5147 | . . . . . 6
⊢
((2↑𝑁) =
if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0) → ((2↑𝑁) ∥ (2↑𝑁) ↔ (2↑𝑁) ∥ if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0))) | 
| 11 |  | breq2 5147 | . . . . . 6
⊢ (0 =
if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0) → ((2↑𝑁) ∥ 0 ↔ (2↑𝑁) ∥ if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0))) | 
| 12 | 10, 11 | ifboth 4565 | . . . . 5
⊢
(((2↑𝑁) ∥
(2↑𝑁) ∧
(2↑𝑁) ∥ 0)
→ (2↑𝑁) ∥
if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0)) | 
| 13 | 7, 9, 12 | syl2anc 584 | . . . 4
⊢ (𝜑 → (2↑𝑁) ∥ if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0)) | 
| 14 |  | inss1 4237 | . . . . . . . . 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 16489 | . . . . . . . . . 10
⊢ (𝜑 → (𝐴 sadd 𝐵) = {𝑘 ∈ ℕ0 ∣
hadd(𝑘 ∈ 𝐴, 𝑘 ∈ 𝐵, ∅ ∈ (𝐶‘𝑘))}) | 
| 19 |  | ssrab2 4080 | . . . . . . . . . 10
⊢ {𝑘 ∈ ℕ0
∣ hadd(𝑘 ∈ 𝐴, 𝑘 ∈ 𝐵, ∅ ∈ (𝐶‘𝑘))} ⊆
ℕ0 | 
| 20 | 18, 19 | eqsstrdi 4028 | . . . . . . . . 9
⊢ (𝜑 → (𝐴 sadd 𝐵) ⊆
ℕ0) | 
| 21 | 14, 20 | sstrid 3995 | . . . . . . . 8
⊢ (𝜑 → ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ⊆
ℕ0) | 
| 22 |  | fzofi 14015 | . . . . . . . . . 10
⊢
(0..^𝑁) ∈
Fin | 
| 23 | 22 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → (0..^𝑁) ∈ Fin) | 
| 24 |  | inss2 4238 | . . . . . . . . 9
⊢ ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ⊆ (0..^𝑁) | 
| 25 |  | ssfi 9213 | . . . . . . . . 9
⊢
(((0..^𝑁) ∈ Fin
∧ ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ⊆ (0..^𝑁)) → ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ Fin) | 
| 26 | 23, 24, 25 | sylancl 586 | . . . . . . . 8
⊢ (𝜑 → ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ Fin) | 
| 27 |  | elfpw 9394 | . . . . . . . 8
⊢ (((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin) ↔ (((𝐴 sadd
𝐵) ∩ (0..^𝑁)) ⊆ ℕ0
∧ ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ Fin)) | 
| 28 | 21, 26, 27 | sylanbrc 583 | . . . . . . 7
⊢ (𝜑 → ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin)) | 
| 29 |  | bitsf1o 16482 | . . . . . . . . . 10
⊢ (bits
↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩
Fin) | 
| 30 |  | f1ocnv 6860 | . . . . . . . . . 10
⊢ ((bits
↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩ Fin)
→ ◡(bits ↾
ℕ0):(𝒫 ℕ0 ∩ Fin)–1-1-onto→ℕ0) | 
| 31 |  | f1of 6848 | . . . . . . . . . 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 6727 | . . . . . . . . 9
⊢ (𝐾:(𝒫 ℕ0
∩ Fin)⟶ℕ0 ↔ ◡(bits ↾
ℕ0):(𝒫 ℕ0 ∩
Fin)⟶ℕ0) | 
| 35 | 32, 34 | mpbir 231 | . . . . . . . 8
⊢ 𝐾:(𝒫 ℕ0
∩ Fin)⟶ℕ0 | 
| 36 | 35 | ffvelcdmi 7103 | . . . . . . 7
⊢ (((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin) → (𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) ∈
ℕ0) | 
| 37 | 28, 36 | syl 17 | . . . . . 6
⊢ (𝜑 → (𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) ∈
ℕ0) | 
| 38 | 37 | nn0cnd 12589 | . . . . 5
⊢ (𝜑 → (𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) ∈ ℂ) | 
| 39 | 4 | nncnd 12282 | . . . . . 6
⊢ (𝜑 → (2↑𝑁) ∈ ℂ) | 
| 40 |  | 0cn 11253 | . . . . . 6
⊢ 0 ∈
ℂ | 
| 41 |  | ifcl 4571 | . . . . . 6
⊢
(((2↑𝑁) ∈
ℂ ∧ 0 ∈ ℂ) → if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0) ∈ ℂ) | 
| 42 | 39, 40, 41 | sylancl 586 | . . . . 5
⊢ (𝜑 → if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0) ∈ ℂ) | 
| 43 | 38, 42 | pncan2d 11622 | . . . 4
⊢ (𝜑 → (((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0)) − (𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁)))) = if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0)) | 
| 44 | 13, 43 | breqtrrd 5171 | . . 3
⊢ (𝜑 → (2↑𝑁) ∥ (((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0)) − (𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))))) | 
| 45 | 37 | nn0zd 12639 | . . . . 5
⊢ (𝜑 → (𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) ∈ ℤ) | 
| 46 | 5 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) → (2↑𝑁) ∈ ℤ) | 
| 47 |  | 0zd 12625 | . . . . . 6
⊢ ((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) → 0 ∈ ℤ) | 
| 48 | 46, 47 | ifclda 4561 | . . . . 5
⊢ (𝜑 → if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0) ∈ ℤ) | 
| 49 | 45, 48 | zaddcld 12726 | . . . 4
⊢ (𝜑 → ((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0)) ∈ ℤ) | 
| 50 |  | moddvds 16301 | . . . 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 1373 | . . 3
⊢ (𝜑 → ((((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0)) mod (2↑𝑁)) = ((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) mod (2↑𝑁)) ↔ (2↑𝑁) ∥ (((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0)) − (𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁)))))) | 
| 52 | 44, 51 | mpbird 257 | . 2
⊢ (𝜑 → (((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0)) mod (2↑𝑁)) = ((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) mod (2↑𝑁))) | 
| 53 | 15, 16, 17, 3, 33 | sadadd2 16497 | . . 3
⊢ (𝜑 → ((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0)) = ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁))))) | 
| 54 | 53 | oveq1d 7446 | . 2
⊢ (𝜑 → (((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0)) mod (2↑𝑁)) = (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) mod (2↑𝑁))) | 
| 55 | 52, 54 | eqtr3d 2779 | 1
⊢ (𝜑 → ((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) mod (2↑𝑁)) = (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) mod (2↑𝑁))) |