| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | inss1 4236 | . . . . . . . . 9
⊢ ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ⊆ (𝐴 sadd 𝐵) | 
| 2 |  | sadval.a | . . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ⊆
ℕ0) | 
| 3 |  | sadval.b | . . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ⊆
ℕ0) | 
| 4 |  | sadval.c | . . . . . . . . . . 11
⊢ 𝐶 = seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦
if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0
↦ if(𝑛 = 0, ∅,
(𝑛 −
1)))) | 
| 5 | 2, 3, 4 | sadfval 16490 | . . . . . . . . . 10
⊢ (𝜑 → (𝐴 sadd 𝐵) = {𝑘 ∈ ℕ0 ∣
hadd(𝑘 ∈ 𝐴, 𝑘 ∈ 𝐵, ∅ ∈ (𝐶‘𝑘))}) | 
| 6 |  | ssrab2 4079 | . . . . . . . . . 10
⊢ {𝑘 ∈ ℕ0
∣ hadd(𝑘 ∈ 𝐴, 𝑘 ∈ 𝐵, ∅ ∈ (𝐶‘𝑘))} ⊆
ℕ0 | 
| 7 | 5, 6 | eqsstrdi 4027 | . . . . . . . . 9
⊢ (𝜑 → (𝐴 sadd 𝐵) ⊆
ℕ0) | 
| 8 | 1, 7 | sstrid 3994 | . . . . . . . 8
⊢ (𝜑 → ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ⊆
ℕ0) | 
| 9 |  | fzofi 14016 | . . . . . . . . . 10
⊢
(0..^𝑁) ∈
Fin | 
| 10 | 9 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → (0..^𝑁) ∈ Fin) | 
| 11 |  | inss2 4237 | . . . . . . . . 9
⊢ ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ⊆ (0..^𝑁) | 
| 12 |  | ssfi 9214 | . . . . . . . . 9
⊢
(((0..^𝑁) ∈ Fin
∧ ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ⊆ (0..^𝑁)) → ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ Fin) | 
| 13 | 10, 11, 12 | sylancl 586 | . . . . . . . 8
⊢ (𝜑 → ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ Fin) | 
| 14 |  | elfpw 9395 | . . . . . . . 8
⊢ (((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin) ↔ (((𝐴 sadd
𝐵) ∩ (0..^𝑁)) ⊆ ℕ0
∧ ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ Fin)) | 
| 15 | 8, 13, 14 | sylanbrc 583 | . . . . . . 7
⊢ (𝜑 → ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin)) | 
| 16 |  | bitsf1o 16483 | . . . . . . . . . 10
⊢ (bits
↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩
Fin) | 
| 17 |  | f1ocnv 6859 | . . . . . . . . . 10
⊢ ((bits
↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩ Fin)
→ ◡(bits ↾
ℕ0):(𝒫 ℕ0 ∩ Fin)–1-1-onto→ℕ0) | 
| 18 |  | f1of 6847 | . . . . . . . . . 10
⊢ (◡(bits ↾
ℕ0):(𝒫 ℕ0 ∩ Fin)–1-1-onto→ℕ0 → ◡(bits ↾
ℕ0):(𝒫 ℕ0 ∩
Fin)⟶ℕ0) | 
| 19 | 16, 17, 18 | mp2b 10 | . . . . . . . . 9
⊢ ◡(bits ↾
ℕ0):(𝒫 ℕ0 ∩
Fin)⟶ℕ0 | 
| 20 |  | sadcadd.k | . . . . . . . . . 10
⊢ 𝐾 = ◡(bits ↾
ℕ0) | 
| 21 | 20 | feq1i 6726 | . . . . . . . . 9
⊢ (𝐾:(𝒫 ℕ0
∩ Fin)⟶ℕ0 ↔ ◡(bits ↾
ℕ0):(𝒫 ℕ0 ∩
Fin)⟶ℕ0) | 
| 22 | 19, 21 | mpbir 231 | . . . . . . . 8
⊢ 𝐾:(𝒫 ℕ0
∩ Fin)⟶ℕ0 | 
| 23 | 22 | ffvelcdmi 7102 | . . . . . . 7
⊢ (((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin) → (𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) ∈
ℕ0) | 
| 24 | 15, 23 | syl 17 | . . . . . 6
⊢ (𝜑 → (𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) ∈
ℕ0) | 
| 25 | 24 | nn0cnd 12591 | . . . . 5
⊢ (𝜑 → (𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) ∈ ℂ) | 
| 26 |  | 2nn0 12545 | . . . . . . . . . 10
⊢ 2 ∈
ℕ0 | 
| 27 | 26 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → 2 ∈
ℕ0) | 
| 28 |  | sadcp1.n | . . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈
ℕ0) | 
| 29 | 27, 28 | nn0expcld 14286 | . . . . . . . 8
⊢ (𝜑 → (2↑𝑁) ∈
ℕ0) | 
| 30 |  | 0nn0 12543 | . . . . . . . 8
⊢ 0 ∈
ℕ0 | 
| 31 |  | ifcl 4570 | . . . . . . . 8
⊢
(((2↑𝑁) ∈
ℕ0 ∧ 0 ∈ ℕ0) → if(𝑁 ∈ (𝐴 sadd 𝐵), (2↑𝑁), 0) ∈
ℕ0) | 
| 32 | 29, 30, 31 | sylancl 586 | . . . . . . 7
⊢ (𝜑 → if(𝑁 ∈ (𝐴 sadd 𝐵), (2↑𝑁), 0) ∈
ℕ0) | 
| 33 | 32 | nn0cnd 12591 | . . . . . 6
⊢ (𝜑 → if(𝑁 ∈ (𝐴 sadd 𝐵), (2↑𝑁), 0) ∈ ℂ) | 
| 34 |  | 1nn0 12544 | . . . . . . . . . . 11
⊢ 1 ∈
ℕ0 | 
| 35 | 34 | a1i 11 | . . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℕ0) | 
| 36 | 28, 35 | nn0addcld 12593 | . . . . . . . . 9
⊢ (𝜑 → (𝑁 + 1) ∈
ℕ0) | 
| 37 | 27, 36 | nn0expcld 14286 | . . . . . . . 8
⊢ (𝜑 → (2↑(𝑁 + 1)) ∈
ℕ0) | 
| 38 |  | ifcl 4570 | . . . . . . . 8
⊢
(((2↑(𝑁 + 1))
∈ ℕ0 ∧ 0 ∈ ℕ0) →
if(∅ ∈ (𝐶‘(𝑁 + 1)), (2↑(𝑁 + 1)), 0) ∈
ℕ0) | 
| 39 | 37, 30, 38 | sylancl 586 | . . . . . . 7
⊢ (𝜑 → if(∅ ∈ (𝐶‘(𝑁 + 1)), (2↑(𝑁 + 1)), 0) ∈
ℕ0) | 
| 40 | 39 | nn0cnd 12591 | . . . . . 6
⊢ (𝜑 → if(∅ ∈ (𝐶‘(𝑁 + 1)), (2↑(𝑁 + 1)), 0) ∈ ℂ) | 
| 41 | 33, 40 | addcld 11281 | . . . . 5
⊢ (𝜑 → (if(𝑁 ∈ (𝐴 sadd 𝐵), (2↑𝑁), 0) + if(∅ ∈ (𝐶‘(𝑁 + 1)), (2↑(𝑁 + 1)), 0)) ∈ ℂ) | 
| 42 | 25, 41 | addcld 11281 | . . . 4
⊢ (𝜑 → ((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + (if(𝑁 ∈ (𝐴 sadd 𝐵), (2↑𝑁), 0) + if(∅ ∈ (𝐶‘(𝑁 + 1)), (2↑(𝑁 + 1)), 0))) ∈
ℂ) | 
| 43 |  | inss1 4236 | . . . . . . . . . 10
⊢ (𝐴 ∩ (0..^𝑁)) ⊆ 𝐴 | 
| 44 | 43, 2 | sstrid 3994 | . . . . . . . . 9
⊢ (𝜑 → (𝐴 ∩ (0..^𝑁)) ⊆
ℕ0) | 
| 45 |  | inss2 4237 | . . . . . . . . . 10
⊢ (𝐴 ∩ (0..^𝑁)) ⊆ (0..^𝑁) | 
| 46 |  | ssfi 9214 | . . . . . . . . . 10
⊢
(((0..^𝑁) ∈ Fin
∧ (𝐴 ∩ (0..^𝑁)) ⊆ (0..^𝑁)) → (𝐴 ∩ (0..^𝑁)) ∈ Fin) | 
| 47 | 10, 45, 46 | sylancl 586 | . . . . . . . . 9
⊢ (𝜑 → (𝐴 ∩ (0..^𝑁)) ∈ Fin) | 
| 48 |  | elfpw 9395 | . . . . . . . . 9
⊢ ((𝐴 ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin) ↔ ((𝐴 ∩
(0..^𝑁)) ⊆
ℕ0 ∧ (𝐴 ∩ (0..^𝑁)) ∈ Fin)) | 
| 49 | 44, 47, 48 | sylanbrc 583 | . . . . . . . 8
⊢ (𝜑 → (𝐴 ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin)) | 
| 50 | 22 | ffvelcdmi 7102 | . . . . . . . 8
⊢ ((𝐴 ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin) → (𝐾‘(𝐴 ∩ (0..^𝑁))) ∈
ℕ0) | 
| 51 | 49, 50 | syl 17 | . . . . . . 7
⊢ (𝜑 → (𝐾‘(𝐴 ∩ (0..^𝑁))) ∈
ℕ0) | 
| 52 | 51 | nn0cnd 12591 | . . . . . 6
⊢ (𝜑 → (𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ ℂ) | 
| 53 |  | inss1 4236 | . . . . . . . . . 10
⊢ (𝐵 ∩ (0..^𝑁)) ⊆ 𝐵 | 
| 54 | 53, 3 | sstrid 3994 | . . . . . . . . 9
⊢ (𝜑 → (𝐵 ∩ (0..^𝑁)) ⊆
ℕ0) | 
| 55 |  | inss2 4237 | . . . . . . . . . 10
⊢ (𝐵 ∩ (0..^𝑁)) ⊆ (0..^𝑁) | 
| 56 |  | ssfi 9214 | . . . . . . . . . 10
⊢
(((0..^𝑁) ∈ Fin
∧ (𝐵 ∩ (0..^𝑁)) ⊆ (0..^𝑁)) → (𝐵 ∩ (0..^𝑁)) ∈ Fin) | 
| 57 | 10, 55, 56 | sylancl 586 | . . . . . . . . 9
⊢ (𝜑 → (𝐵 ∩ (0..^𝑁)) ∈ Fin) | 
| 58 |  | elfpw 9395 | . . . . . . . . 9
⊢ ((𝐵 ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin) ↔ ((𝐵 ∩
(0..^𝑁)) ⊆
ℕ0 ∧ (𝐵 ∩ (0..^𝑁)) ∈ Fin)) | 
| 59 | 54, 57, 58 | sylanbrc 583 | . . . . . . . 8
⊢ (𝜑 → (𝐵 ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin)) | 
| 60 | 22 | ffvelcdmi 7102 | . . . . . . . 8
⊢ ((𝐵 ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin) → (𝐾‘(𝐵 ∩ (0..^𝑁))) ∈
ℕ0) | 
| 61 | 59, 60 | syl 17 | . . . . . . 7
⊢ (𝜑 → (𝐾‘(𝐵 ∩ (0..^𝑁))) ∈
ℕ0) | 
| 62 | 61 | nn0cnd 12591 | . . . . . 6
⊢ (𝜑 → (𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ ℂ) | 
| 63 | 52, 62 | addcld 11281 | . . . . 5
⊢ (𝜑 → ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) ∈ ℂ) | 
| 64 |  | ifcl 4570 | . . . . . . . 8
⊢
(((2↑𝑁) ∈
ℕ0 ∧ 0 ∈ ℕ0) → if(𝑁 ∈ 𝐴, (2↑𝑁), 0) ∈
ℕ0) | 
| 65 | 29, 30, 64 | sylancl 586 | . . . . . . 7
⊢ (𝜑 → if(𝑁 ∈ 𝐴, (2↑𝑁), 0) ∈
ℕ0) | 
| 66 | 65 | nn0cnd 12591 | . . . . . 6
⊢ (𝜑 → if(𝑁 ∈ 𝐴, (2↑𝑁), 0) ∈ ℂ) | 
| 67 |  | ifcl 4570 | . . . . . . . 8
⊢
(((2↑𝑁) ∈
ℕ0 ∧ 0 ∈ ℕ0) → if(𝑁 ∈ 𝐵, (2↑𝑁), 0) ∈
ℕ0) | 
| 68 | 29, 30, 67 | sylancl 586 | . . . . . . 7
⊢ (𝜑 → if(𝑁 ∈ 𝐵, (2↑𝑁), 0) ∈
ℕ0) | 
| 69 | 68 | nn0cnd 12591 | . . . . . 6
⊢ (𝜑 → if(𝑁 ∈ 𝐵, (2↑𝑁), 0) ∈ ℂ) | 
| 70 | 66, 69 | addcld 11281 | . . . . 5
⊢ (𝜑 → (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) ∈ ℂ) | 
| 71 | 63, 70 | addcld 11281 | . . . 4
⊢ (𝜑 → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) ∈ ℂ) | 
| 72 | 29 | nn0cnd 12591 | . . . . . 6
⊢ (𝜑 → (2↑𝑁) ∈ ℂ) | 
| 73 | 72 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) → (2↑𝑁) ∈ ℂ) | 
| 74 |  | 0cnd 11255 | . . . . 5
⊢ ((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) → 0 ∈ ℂ) | 
| 75 | 73, 74 | ifclda 4560 | . . . 4
⊢ (𝜑 → if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0) ∈ ℂ) | 
| 76 |  | sadadd2lem.1 | . . . . . 6
⊢ (𝜑 → ((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0)) = ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁))))) | 
| 77 | 2, 3, 4, 28 | sadval 16494 | . . . . . . . . 9
⊢ (𝜑 → (𝑁 ∈ (𝐴 sadd 𝐵) ↔ hadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)))) | 
| 78 | 77 | ifbid 4548 | . . . . . . . 8
⊢ (𝜑 → if(𝑁 ∈ (𝐴 sadd 𝐵), (2↑𝑁), 0) = if(hadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)), (2↑𝑁), 0)) | 
| 79 | 2, 3, 4, 28 | sadcp1 16493 | . . . . . . . . 9
⊢ (𝜑 → (∅ ∈ (𝐶‘(𝑁 + 1)) ↔ cadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)))) | 
| 80 | 27 | nn0cnd 12591 | . . . . . . . . . . 11
⊢ (𝜑 → 2 ∈
ℂ) | 
| 81 | 80, 28 | expp1d 14188 | . . . . . . . . . 10
⊢ (𝜑 → (2↑(𝑁 + 1)) = ((2↑𝑁) · 2)) | 
| 82 | 72, 80 | mulcomd 11283 | . . . . . . . . . 10
⊢ (𝜑 → ((2↑𝑁) · 2) = (2 · (2↑𝑁))) | 
| 83 | 81, 82 | eqtrd 2776 | . . . . . . . . 9
⊢ (𝜑 → (2↑(𝑁 + 1)) = (2 · (2↑𝑁))) | 
| 84 | 79, 83 | ifbieq1d 4549 | . . . . . . . 8
⊢ (𝜑 → if(∅ ∈ (𝐶‘(𝑁 + 1)), (2↑(𝑁 + 1)), 0) = if(cadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)), (2 · (2↑𝑁)), 0)) | 
| 85 | 78, 84 | oveq12d 7450 | . . . . . . 7
⊢ (𝜑 → (if(𝑁 ∈ (𝐴 sadd 𝐵), (2↑𝑁), 0) + if(∅ ∈ (𝐶‘(𝑁 + 1)), (2↑(𝑁 + 1)), 0)) = (if(hadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)), (2↑𝑁), 0) + if(cadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)), (2 · (2↑𝑁)), 0))) | 
| 86 |  | sadadd2lem2 16488 | . . . . . . . 8
⊢
((2↑𝑁) ∈
ℂ → (if(hadd(𝑁
∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)), (2↑𝑁), 0) + if(cadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)), (2 · (2↑𝑁)), 0)) = ((if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) + if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0))) | 
| 87 | 72, 86 | syl 17 | . . . . . . 7
⊢ (𝜑 → (if(hadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)), (2↑𝑁), 0) + if(cadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)), (2 · (2↑𝑁)), 0)) = ((if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) + if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0))) | 
| 88 | 85, 87 | eqtrd 2776 | . . . . . 6
⊢ (𝜑 → (if(𝑁 ∈ (𝐴 sadd 𝐵), (2↑𝑁), 0) + if(∅ ∈ (𝐶‘(𝑁 + 1)), (2↑(𝑁 + 1)), 0)) = ((if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) + if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0))) | 
| 89 | 76, 88 | oveq12d 7450 | . . . . 5
⊢ (𝜑 → (((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0)) + (if(𝑁 ∈ (𝐴 sadd 𝐵), (2↑𝑁), 0) + if(∅ ∈ (𝐶‘(𝑁 + 1)), (2↑(𝑁 + 1)), 0))) = (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + ((if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) + if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0)))) | 
| 90 | 25, 41, 75 | add32d 11490 | . . . . 5
⊢ (𝜑 → (((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + (if(𝑁 ∈ (𝐴 sadd 𝐵), (2↑𝑁), 0) + if(∅ ∈ (𝐶‘(𝑁 + 1)), (2↑(𝑁 + 1)), 0))) + if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0)) = (((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0)) + (if(𝑁 ∈ (𝐴 sadd 𝐵), (2↑𝑁), 0) + if(∅ ∈ (𝐶‘(𝑁 + 1)), (2↑(𝑁 + 1)), 0)))) | 
| 91 | 63, 70, 75 | addassd 11284 | . . . . 5
⊢ (𝜑 → ((((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) + if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0)) = (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + ((if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) + if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0)))) | 
| 92 | 89, 90, 91 | 3eqtr4d 2786 | . . . 4
⊢ (𝜑 → (((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + (if(𝑁 ∈ (𝐴 sadd 𝐵), (2↑𝑁), 0) + if(∅ ∈ (𝐶‘(𝑁 + 1)), (2↑(𝑁 + 1)), 0))) + if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0)) = ((((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) + if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0))) | 
| 93 | 42, 71, 75, 92 | addcan2ad 11468 | . . 3
⊢ (𝜑 → ((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + (if(𝑁 ∈ (𝐴 sadd 𝐵), (2↑𝑁), 0) + if(∅ ∈ (𝐶‘(𝑁 + 1)), (2↑(𝑁 + 1)), 0))) = (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)))) | 
| 94 | 25, 33, 40 | addassd 11284 | . . 3
⊢ (𝜑 → (((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + if(𝑁 ∈ (𝐴 sadd 𝐵), (2↑𝑁), 0)) + if(∅ ∈ (𝐶‘(𝑁 + 1)), (2↑(𝑁 + 1)), 0)) = ((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + (if(𝑁 ∈ (𝐴 sadd 𝐵), (2↑𝑁), 0) + if(∅ ∈ (𝐶‘(𝑁 + 1)), (2↑(𝑁 + 1)), 0)))) | 
| 95 | 52, 66, 62, 69 | add4d 11491 | . . 3
⊢ (𝜑 → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + if(𝑁 ∈ 𝐴, (2↑𝑁), 0)) + ((𝐾‘(𝐵 ∩ (0..^𝑁))) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) = (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)))) | 
| 96 | 93, 94, 95 | 3eqtr4d 2786 | . 2
⊢ (𝜑 → (((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + if(𝑁 ∈ (𝐴 sadd 𝐵), (2↑𝑁), 0)) + if(∅ ∈ (𝐶‘(𝑁 + 1)), (2↑(𝑁 + 1)), 0)) = (((𝐾‘(𝐴 ∩ (0..^𝑁))) + if(𝑁 ∈ 𝐴, (2↑𝑁), 0)) + ((𝐾‘(𝐵 ∩ (0..^𝑁))) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)))) | 
| 97 | 20 | bitsinvp1 16487 | . . . 4
⊢ (((𝐴 sadd 𝐵) ⊆ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ (𝐾‘((𝐴 sadd 𝐵) ∩ (0..^(𝑁 + 1)))) = ((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + if(𝑁 ∈ (𝐴 sadd 𝐵), (2↑𝑁), 0))) | 
| 98 | 7, 28, 97 | syl2anc 584 | . . 3
⊢ (𝜑 → (𝐾‘((𝐴 sadd 𝐵) ∩ (0..^(𝑁 + 1)))) = ((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + if(𝑁 ∈ (𝐴 sadd 𝐵), (2↑𝑁), 0))) | 
| 99 | 98 | oveq1d 7447 | . 2
⊢ (𝜑 → ((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^(𝑁 + 1)))) + if(∅ ∈ (𝐶‘(𝑁 + 1)), (2↑(𝑁 + 1)), 0)) = (((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + if(𝑁 ∈ (𝐴 sadd 𝐵), (2↑𝑁), 0)) + if(∅ ∈ (𝐶‘(𝑁 + 1)), (2↑(𝑁 + 1)), 0))) | 
| 100 | 20 | bitsinvp1 16487 | . . . 4
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝐾‘(𝐴 ∩ (0..^(𝑁 + 1)))) = ((𝐾‘(𝐴 ∩ (0..^𝑁))) + if(𝑁 ∈ 𝐴, (2↑𝑁), 0))) | 
| 101 | 2, 28, 100 | syl2anc 584 | . . 3
⊢ (𝜑 → (𝐾‘(𝐴 ∩ (0..^(𝑁 + 1)))) = ((𝐾‘(𝐴 ∩ (0..^𝑁))) + if(𝑁 ∈ 𝐴, (2↑𝑁), 0))) | 
| 102 | 20 | bitsinvp1 16487 | . . . 4
⊢ ((𝐵 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝐾‘(𝐵 ∩ (0..^(𝑁 + 1)))) = ((𝐾‘(𝐵 ∩ (0..^𝑁))) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) | 
| 103 | 3, 28, 102 | syl2anc 584 | . . 3
⊢ (𝜑 → (𝐾‘(𝐵 ∩ (0..^(𝑁 + 1)))) = ((𝐾‘(𝐵 ∩ (0..^𝑁))) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) | 
| 104 | 101, 103 | oveq12d 7450 | . 2
⊢ (𝜑 → ((𝐾‘(𝐴 ∩ (0..^(𝑁 + 1)))) + (𝐾‘(𝐵 ∩ (0..^(𝑁 + 1))))) = (((𝐾‘(𝐴 ∩ (0..^𝑁))) + if(𝑁 ∈ 𝐴, (2↑𝑁), 0)) + ((𝐾‘(𝐵 ∩ (0..^𝑁))) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)))) | 
| 105 | 96, 99, 104 | 3eqtr4d 2786 | 1
⊢ (𝜑 → ((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^(𝑁 + 1)))) + if(∅ ∈ (𝐶‘(𝑁 + 1)), (2↑(𝑁 + 1)), 0)) = ((𝐾‘(𝐴 ∩ (0..^(𝑁 + 1)))) + (𝐾‘(𝐵 ∩ (0..^(𝑁 + 1)))))) |