# Metamath Proof Explorer

Ref Expression
Hypotheses sadval.a ${⊢}{\phi }\to {A}\subseteq {ℕ}_{0}$
sadval.b ${⊢}{\phi }\to {B}\subseteq {ℕ}_{0}$
sadval.c ${⊢}{C}=seq0\left(\left({c}\in {2}_{𝑜},{m}\in {ℕ}_{0}⟼if\left(cadd\left({m}\in {A},{m}\in {B},\varnothing \in {c}\right),{1}_{𝑜},\varnothing \right)\right),\left({n}\in {ℕ}_{0}⟼if\left({n}=0,\varnothing ,{n}-1\right)\right)\right)$
sadcp1.n ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
sadcadd.k ${⊢}{K}={\left({\mathrm{bits}↾}_{{ℕ}_{0}}\right)}^{-1}$
sadadd2lem.1 ${⊢}{\phi }\to {K}\left(\left({A}\mathrm{sadd}{B}\right)\cap \left(0..^{N}\right)\right)+if\left(\varnothing \in {C}\left({N}\right),{2}^{{N}},0\right)={K}\left({A}\cap \left(0..^{N}\right)\right)+{K}\left({B}\cap \left(0..^{N}\right)\right)$
Assertion sadadd2lem ${⊢}{\phi }\to {K}\left(\left({A}\mathrm{sadd}{B}\right)\cap \left(0..^{N}+1\right)\right)+if\left(\varnothing \in {C}\left({N}+1\right),{2}^{{N}+1},0\right)={K}\left({A}\cap \left(0..^{N}+1\right)\right)+{K}\left({B}\cap \left(0..^{N}+1\right)\right)$

### Proof

Step Hyp Ref Expression
1 sadval.a ${⊢}{\phi }\to {A}\subseteq {ℕ}_{0}$
2 sadval.b ${⊢}{\phi }\to {B}\subseteq {ℕ}_{0}$
3 sadval.c ${⊢}{C}=seq0\left(\left({c}\in {2}_{𝑜},{m}\in {ℕ}_{0}⟼if\left(cadd\left({m}\in {A},{m}\in {B},\varnothing \in {c}\right),{1}_{𝑜},\varnothing \right)\right),\left({n}\in {ℕ}_{0}⟼if\left({n}=0,\varnothing ,{n}-1\right)\right)\right)$
4 sadcp1.n ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
5 sadcadd.k ${⊢}{K}={\left({\mathrm{bits}↾}_{{ℕ}_{0}}\right)}^{-1}$
6 sadadd2lem.1 ${⊢}{\phi }\to {K}\left(\left({A}\mathrm{sadd}{B}\right)\cap \left(0..^{N}\right)\right)+if\left(\varnothing \in {C}\left({N}\right),{2}^{{N}},0\right)={K}\left({A}\cap \left(0..^{N}\right)\right)+{K}\left({B}\cap \left(0..^{N}\right)\right)$
7 inss1 ${⊢}\left({A}\mathrm{sadd}{B}\right)\cap \left(0..^{N}\right)\subseteq {A}\mathrm{sadd}{B}$
8 1 2 3 sadfval ${⊢}{\phi }\to {A}\mathrm{sadd}{B}=\left\{{k}\in {ℕ}_{0}|hadd\left({k}\in {A},{k}\in {B},\varnothing \in {C}\left({k}\right)\right)\right\}$
9 ssrab2 ${⊢}\left\{{k}\in {ℕ}_{0}|hadd\left({k}\in {A},{k}\in {B},\varnothing \in {C}\left({k}\right)\right)\right\}\subseteq {ℕ}_{0}$
10 8 9 eqsstrdi ${⊢}{\phi }\to {A}\mathrm{sadd}{B}\subseteq {ℕ}_{0}$
11 7 10 sstrid ${⊢}{\phi }\to \left({A}\mathrm{sadd}{B}\right)\cap \left(0..^{N}\right)\subseteq {ℕ}_{0}$
12 fzofi ${⊢}\left(0..^{N}\right)\in \mathrm{Fin}$
13 12 a1i ${⊢}{\phi }\to \left(0..^{N}\right)\in \mathrm{Fin}$
14 inss2 ${⊢}\left({A}\mathrm{sadd}{B}\right)\cap \left(0..^{N}\right)\subseteq \left(0..^{N}\right)$
15 ssfi ${⊢}\left(\left(0..^{N}\right)\in \mathrm{Fin}\wedge \left({A}\mathrm{sadd}{B}\right)\cap \left(0..^{N}\right)\subseteq \left(0..^{N}\right)\right)\to \left({A}\mathrm{sadd}{B}\right)\cap \left(0..^{N}\right)\in \mathrm{Fin}$
16 13 14 15 sylancl ${⊢}{\phi }\to \left({A}\mathrm{sadd}{B}\right)\cap \left(0..^{N}\right)\in \mathrm{Fin}$
17 elfpw ${⊢}\left({A}\mathrm{sadd}{B}\right)\cap \left(0..^{N}\right)\in \left(𝒫{ℕ}_{0}\cap \mathrm{Fin}\right)↔\left(\left({A}\mathrm{sadd}{B}\right)\cap \left(0..^{N}\right)\subseteq {ℕ}_{0}\wedge \left({A}\mathrm{sadd}{B}\right)\cap \left(0..^{N}\right)\in \mathrm{Fin}\right)$
18 11 16 17 sylanbrc ${⊢}{\phi }\to \left({A}\mathrm{sadd}{B}\right)\cap \left(0..^{N}\right)\in \left(𝒫{ℕ}_{0}\cap \mathrm{Fin}\right)$
19 bitsf1o ${⊢}\left({\mathrm{bits}↾}_{{ℕ}_{0}}\right):{ℕ}_{0}\underset{1-1 onto}{⟶}𝒫{ℕ}_{0}\cap \mathrm{Fin}$
20 f1ocnv ${⊢}\left({\mathrm{bits}↾}_{{ℕ}_{0}}\right):{ℕ}_{0}\underset{1-1 onto}{⟶}𝒫{ℕ}_{0}\cap \mathrm{Fin}\to {\left({\mathrm{bits}↾}_{{ℕ}_{0}}\right)}^{-1}:𝒫{ℕ}_{0}\cap \mathrm{Fin}\underset{1-1 onto}{⟶}{ℕ}_{0}$
21 f1of ${⊢}{\left({\mathrm{bits}↾}_{{ℕ}_{0}}\right)}^{-1}:𝒫{ℕ}_{0}\cap \mathrm{Fin}\underset{1-1 onto}{⟶}{ℕ}_{0}\to {\left({\mathrm{bits}↾}_{{ℕ}_{0}}\right)}^{-1}:𝒫{ℕ}_{0}\cap \mathrm{Fin}⟶{ℕ}_{0}$
22 19 20 21 mp2b ${⊢}{\left({\mathrm{bits}↾}_{{ℕ}_{0}}\right)}^{-1}:𝒫{ℕ}_{0}\cap \mathrm{Fin}⟶{ℕ}_{0}$
23 5 feq1i ${⊢}{K}:𝒫{ℕ}_{0}\cap \mathrm{Fin}⟶{ℕ}_{0}↔{\left({\mathrm{bits}↾}_{{ℕ}_{0}}\right)}^{-1}:𝒫{ℕ}_{0}\cap \mathrm{Fin}⟶{ℕ}_{0}$
24 22 23 mpbir ${⊢}{K}:𝒫{ℕ}_{0}\cap \mathrm{Fin}⟶{ℕ}_{0}$
25 24 ffvelrni ${⊢}\left({A}\mathrm{sadd}{B}\right)\cap \left(0..^{N}\right)\in \left(𝒫{ℕ}_{0}\cap \mathrm{Fin}\right)\to {K}\left(\left({A}\mathrm{sadd}{B}\right)\cap \left(0..^{N}\right)\right)\in {ℕ}_{0}$
26 18 25 syl ${⊢}{\phi }\to {K}\left(\left({A}\mathrm{sadd}{B}\right)\cap \left(0..^{N}\right)\right)\in {ℕ}_{0}$
27 26 nn0cnd ${⊢}{\phi }\to {K}\left(\left({A}\mathrm{sadd}{B}\right)\cap \left(0..^{N}\right)\right)\in ℂ$
28 2nn0 ${⊢}2\in {ℕ}_{0}$
29 28 a1i ${⊢}{\phi }\to 2\in {ℕ}_{0}$
30 29 4 nn0expcld ${⊢}{\phi }\to {2}^{{N}}\in {ℕ}_{0}$
31 0nn0 ${⊢}0\in {ℕ}_{0}$
32 ifcl ${⊢}\left({2}^{{N}}\in {ℕ}_{0}\wedge 0\in {ℕ}_{0}\right)\to if\left({N}\in \left({A}\mathrm{sadd}{B}\right),{2}^{{N}},0\right)\in {ℕ}_{0}$
33 30 31 32 sylancl ${⊢}{\phi }\to if\left({N}\in \left({A}\mathrm{sadd}{B}\right),{2}^{{N}},0\right)\in {ℕ}_{0}$
34 33 nn0cnd ${⊢}{\phi }\to if\left({N}\in \left({A}\mathrm{sadd}{B}\right),{2}^{{N}},0\right)\in ℂ$
35 1nn0 ${⊢}1\in {ℕ}_{0}$
36 35 a1i ${⊢}{\phi }\to 1\in {ℕ}_{0}$
37 4 36 nn0addcld ${⊢}{\phi }\to {N}+1\in {ℕ}_{0}$
38 29 37 nn0expcld ${⊢}{\phi }\to {2}^{{N}+1}\in {ℕ}_{0}$
39 ifcl ${⊢}\left({2}^{{N}+1}\in {ℕ}_{0}\wedge 0\in {ℕ}_{0}\right)\to if\left(\varnothing \in {C}\left({N}+1\right),{2}^{{N}+1},0\right)\in {ℕ}_{0}$
40 38 31 39 sylancl ${⊢}{\phi }\to if\left(\varnothing \in {C}\left({N}+1\right),{2}^{{N}+1},0\right)\in {ℕ}_{0}$
41 40 nn0cnd ${⊢}{\phi }\to if\left(\varnothing \in {C}\left({N}+1\right),{2}^{{N}+1},0\right)\in ℂ$
42 34 41 addcld ${⊢}{\phi }\to if\left({N}\in \left({A}\mathrm{sadd}{B}\right),{2}^{{N}},0\right)+if\left(\varnothing \in {C}\left({N}+1\right),{2}^{{N}+1},0\right)\in ℂ$
43 27 42 addcld ${⊢}{\phi }\to {K}\left(\left({A}\mathrm{sadd}{B}\right)\cap \left(0..^{N}\right)\right)+if\left({N}\in \left({A}\mathrm{sadd}{B}\right),{2}^{{N}},0\right)+if\left(\varnothing \in {C}\left({N}+1\right),{2}^{{N}+1},0\right)\in ℂ$
44 inss1 ${⊢}{A}\cap \left(0..^{N}\right)\subseteq {A}$
45 44 1 sstrid ${⊢}{\phi }\to {A}\cap \left(0..^{N}\right)\subseteq {ℕ}_{0}$
46 inss2 ${⊢}{A}\cap \left(0..^{N}\right)\subseteq \left(0..^{N}\right)$
47 ssfi ${⊢}\left(\left(0..^{N}\right)\in \mathrm{Fin}\wedge {A}\cap \left(0..^{N}\right)\subseteq \left(0..^{N}\right)\right)\to {A}\cap \left(0..^{N}\right)\in \mathrm{Fin}$
48 13 46 47 sylancl ${⊢}{\phi }\to {A}\cap \left(0..^{N}\right)\in \mathrm{Fin}$
49 elfpw ${⊢}{A}\cap \left(0..^{N}\right)\in \left(𝒫{ℕ}_{0}\cap \mathrm{Fin}\right)↔\left({A}\cap \left(0..^{N}\right)\subseteq {ℕ}_{0}\wedge {A}\cap \left(0..^{N}\right)\in \mathrm{Fin}\right)$
50 45 48 49 sylanbrc ${⊢}{\phi }\to {A}\cap \left(0..^{N}\right)\in \left(𝒫{ℕ}_{0}\cap \mathrm{Fin}\right)$
51 24 ffvelrni ${⊢}{A}\cap \left(0..^{N}\right)\in \left(𝒫{ℕ}_{0}\cap \mathrm{Fin}\right)\to {K}\left({A}\cap \left(0..^{N}\right)\right)\in {ℕ}_{0}$
52 50 51 syl ${⊢}{\phi }\to {K}\left({A}\cap \left(0..^{N}\right)\right)\in {ℕ}_{0}$
53 52 nn0cnd ${⊢}{\phi }\to {K}\left({A}\cap \left(0..^{N}\right)\right)\in ℂ$
54 inss1 ${⊢}{B}\cap \left(0..^{N}\right)\subseteq {B}$
55 54 2 sstrid ${⊢}{\phi }\to {B}\cap \left(0..^{N}\right)\subseteq {ℕ}_{0}$
56 inss2 ${⊢}{B}\cap \left(0..^{N}\right)\subseteq \left(0..^{N}\right)$
57 ssfi ${⊢}\left(\left(0..^{N}\right)\in \mathrm{Fin}\wedge {B}\cap \left(0..^{N}\right)\subseteq \left(0..^{N}\right)\right)\to {B}\cap \left(0..^{N}\right)\in \mathrm{Fin}$
58 13 56 57 sylancl ${⊢}{\phi }\to {B}\cap \left(0..^{N}\right)\in \mathrm{Fin}$
59 elfpw ${⊢}{B}\cap \left(0..^{N}\right)\in \left(𝒫{ℕ}_{0}\cap \mathrm{Fin}\right)↔\left({B}\cap \left(0..^{N}\right)\subseteq {ℕ}_{0}\wedge {B}\cap \left(0..^{N}\right)\in \mathrm{Fin}\right)$
60 55 58 59 sylanbrc ${⊢}{\phi }\to {B}\cap \left(0..^{N}\right)\in \left(𝒫{ℕ}_{0}\cap \mathrm{Fin}\right)$
61 24 ffvelrni ${⊢}{B}\cap \left(0..^{N}\right)\in \left(𝒫{ℕ}_{0}\cap \mathrm{Fin}\right)\to {K}\left({B}\cap \left(0..^{N}\right)\right)\in {ℕ}_{0}$
62 60 61 syl ${⊢}{\phi }\to {K}\left({B}\cap \left(0..^{N}\right)\right)\in {ℕ}_{0}$
63 62 nn0cnd ${⊢}{\phi }\to {K}\left({B}\cap \left(0..^{N}\right)\right)\in ℂ$
64 53 63 addcld ${⊢}{\phi }\to {K}\left({A}\cap \left(0..^{N}\right)\right)+{K}\left({B}\cap \left(0..^{N}\right)\right)\in ℂ$
65 ifcl ${⊢}\left({2}^{{N}}\in {ℕ}_{0}\wedge 0\in {ℕ}_{0}\right)\to if\left({N}\in {A},{2}^{{N}},0\right)\in {ℕ}_{0}$
66 30 31 65 sylancl ${⊢}{\phi }\to if\left({N}\in {A},{2}^{{N}},0\right)\in {ℕ}_{0}$
67 66 nn0cnd ${⊢}{\phi }\to if\left({N}\in {A},{2}^{{N}},0\right)\in ℂ$
68 ifcl ${⊢}\left({2}^{{N}}\in {ℕ}_{0}\wedge 0\in {ℕ}_{0}\right)\to if\left({N}\in {B},{2}^{{N}},0\right)\in {ℕ}_{0}$
69 30 31 68 sylancl ${⊢}{\phi }\to if\left({N}\in {B},{2}^{{N}},0\right)\in {ℕ}_{0}$
70 69 nn0cnd ${⊢}{\phi }\to if\left({N}\in {B},{2}^{{N}},0\right)\in ℂ$
71 67 70 addcld ${⊢}{\phi }\to if\left({N}\in {A},{2}^{{N}},0\right)+if\left({N}\in {B},{2}^{{N}},0\right)\in ℂ$
72 64 71 addcld ${⊢}{\phi }\to {K}\left({A}\cap \left(0..^{N}\right)\right)+{K}\left({B}\cap \left(0..^{N}\right)\right)+if\left({N}\in {A},{2}^{{N}},0\right)+if\left({N}\in {B},{2}^{{N}},0\right)\in ℂ$
73 30 nn0cnd ${⊢}{\phi }\to {2}^{{N}}\in ℂ$
74 73 adantr ${⊢}\left({\phi }\wedge \varnothing \in {C}\left({N}\right)\right)\to {2}^{{N}}\in ℂ$
75 0cnd ${⊢}\left({\phi }\wedge ¬\varnothing \in {C}\left({N}\right)\right)\to 0\in ℂ$
76 74 75 ifclda ${⊢}{\phi }\to if\left(\varnothing \in {C}\left({N}\right),{2}^{{N}},0\right)\in ℂ$
77 1 2 3 4 sadval ${⊢}{\phi }\to \left({N}\in \left({A}\mathrm{sadd}{B}\right)↔hadd\left({N}\in {A},{N}\in {B},\varnothing \in {C}\left({N}\right)\right)\right)$
78 77 ifbid ${⊢}{\phi }\to if\left({N}\in \left({A}\mathrm{sadd}{B}\right),{2}^{{N}},0\right)=if\left(hadd\left({N}\in {A},{N}\in {B},\varnothing \in {C}\left({N}\right)\right),{2}^{{N}},0\right)$
79 1 2 3 4 sadcp1 ${⊢}{\phi }\to \left(\varnothing \in {C}\left({N}+1\right)↔cadd\left({N}\in {A},{N}\in {B},\varnothing \in {C}\left({N}\right)\right)\right)$
80 29 nn0cnd ${⊢}{\phi }\to 2\in ℂ$
81 80 4 expp1d ${⊢}{\phi }\to {2}^{{N}+1}={2}^{{N}}\cdot 2$
82 73 80 mulcomd ${⊢}{\phi }\to {2}^{{N}}\cdot 2=2{2}^{{N}}$
83 81 82 eqtrd ${⊢}{\phi }\to {2}^{{N}+1}=2{2}^{{N}}$
84 79 83 ifbieq1d ${⊢}{\phi }\to if\left(\varnothing \in {C}\left({N}+1\right),{2}^{{N}+1},0\right)=if\left(cadd\left({N}\in {A},{N}\in {B},\varnothing \in {C}\left({N}\right)\right),2{2}^{{N}},0\right)$
85 78 84 oveq12d ${⊢}{\phi }\to if\left({N}\in \left({A}\mathrm{sadd}{B}\right),{2}^{{N}},0\right)+if\left(\varnothing \in {C}\left({N}+1\right),{2}^{{N}+1},0\right)=if\left(hadd\left({N}\in {A},{N}\in {B},\varnothing \in {C}\left({N}\right)\right),{2}^{{N}},0\right)+if\left(cadd\left({N}\in {A},{N}\in {B},\varnothing \in {C}\left({N}\right)\right),2{2}^{{N}},0\right)$
86 sadadd2lem2 ${⊢}{2}^{{N}}\in ℂ\to if\left(hadd\left({N}\in {A},{N}\in {B},\varnothing \in {C}\left({N}\right)\right),{2}^{{N}},0\right)+if\left(cadd\left({N}\in {A},{N}\in {B},\varnothing \in {C}\left({N}\right)\right),2{2}^{{N}},0\right)=if\left({N}\in {A},{2}^{{N}},0\right)+if\left({N}\in {B},{2}^{{N}},0\right)+if\left(\varnothing \in {C}\left({N}\right),{2}^{{N}},0\right)$
87 73 86 syl ${⊢}{\phi }\to if\left(hadd\left({N}\in {A},{N}\in {B},\varnothing \in {C}\left({N}\right)\right),{2}^{{N}},0\right)+if\left(cadd\left({N}\in {A},{N}\in {B},\varnothing \in {C}\left({N}\right)\right),2{2}^{{N}},0\right)=if\left({N}\in {A},{2}^{{N}},0\right)+if\left({N}\in {B},{2}^{{N}},0\right)+if\left(\varnothing \in {C}\left({N}\right),{2}^{{N}},0\right)$
88 85 87 eqtrd ${⊢}{\phi }\to if\left({N}\in \left({A}\mathrm{sadd}{B}\right),{2}^{{N}},0\right)+if\left(\varnothing \in {C}\left({N}+1\right),{2}^{{N}+1},0\right)=if\left({N}\in {A},{2}^{{N}},0\right)+if\left({N}\in {B},{2}^{{N}},0\right)+if\left(\varnothing \in {C}\left({N}\right),{2}^{{N}},0\right)$
89 6 88 oveq12d ${⊢}{\phi }\to {K}\left(\left({A}\mathrm{sadd}{B}\right)\cap \left(0..^{N}\right)\right)+if\left(\varnothing \in {C}\left({N}\right),{2}^{{N}},0\right)+if\left({N}\in \left({A}\mathrm{sadd}{B}\right),{2}^{{N}},0\right)+if\left(\varnothing \in {C}\left({N}+1\right),{2}^{{N}+1},0\right)={K}\left({A}\cap \left(0..^{N}\right)\right)+{K}\left({B}\cap \left(0..^{N}\right)\right)+\left(if\left({N}\in {A},{2}^{{N}},0\right)+if\left({N}\in {B},{2}^{{N}},0\right)\right)+if\left(\varnothing \in {C}\left({N}\right),{2}^{{N}},0\right)$
90 27 42 76 add32d ${⊢}{\phi }\to {K}\left(\left({A}\mathrm{sadd}{B}\right)\cap \left(0..^{N}\right)\right)+\left(if\left({N}\in \left({A}\mathrm{sadd}{B}\right),{2}^{{N}},0\right)+if\left(\varnothing \in {C}\left({N}+1\right),{2}^{{N}+1},0\right)\right)+if\left(\varnothing \in {C}\left({N}\right),{2}^{{N}},0\right)={K}\left(\left({A}\mathrm{sadd}{B}\right)\cap \left(0..^{N}\right)\right)+if\left(\varnothing \in {C}\left({N}\right),{2}^{{N}},0\right)+if\left({N}\in \left({A}\mathrm{sadd}{B}\right),{2}^{{N}},0\right)+if\left(\varnothing \in {C}\left({N}+1\right),{2}^{{N}+1},0\right)$
91 64 71 76 addassd ${⊢}{\phi }\to \left({K}\left({A}\cap \left(0..^{N}\right)\right)+{K}\left({B}\cap \left(0..^{N}\right)\right)\right)+\left(if\left({N}\in {A},{2}^{{N}},0\right)+if\left({N}\in {B},{2}^{{N}},0\right)\right)+if\left(\varnothing \in {C}\left({N}\right),{2}^{{N}},0\right)={K}\left({A}\cap \left(0..^{N}\right)\right)+{K}\left({B}\cap \left(0..^{N}\right)\right)+\left(if\left({N}\in {A},{2}^{{N}},0\right)+if\left({N}\in {B},{2}^{{N}},0\right)\right)+if\left(\varnothing \in {C}\left({N}\right),{2}^{{N}},0\right)$
92 89 90 91 3eqtr4d ${⊢}{\phi }\to {K}\left(\left({A}\mathrm{sadd}{B}\right)\cap \left(0..^{N}\right)\right)+\left(if\left({N}\in \left({A}\mathrm{sadd}{B}\right),{2}^{{N}},0\right)+if\left(\varnothing \in {C}\left({N}+1\right),{2}^{{N}+1},0\right)\right)+if\left(\varnothing \in {C}\left({N}\right),{2}^{{N}},0\right)=\left({K}\left({A}\cap \left(0..^{N}\right)\right)+{K}\left({B}\cap \left(0..^{N}\right)\right)\right)+\left(if\left({N}\in {A},{2}^{{N}},0\right)+if\left({N}\in {B},{2}^{{N}},0\right)\right)+if\left(\varnothing \in {C}\left({N}\right),{2}^{{N}},0\right)$
93 43 72 76 92 addcan2ad ${⊢}{\phi }\to {K}\left(\left({A}\mathrm{sadd}{B}\right)\cap \left(0..^{N}\right)\right)+if\left({N}\in \left({A}\mathrm{sadd}{B}\right),{2}^{{N}},0\right)+if\left(\varnothing \in {C}\left({N}+1\right),{2}^{{N}+1},0\right)={K}\left({A}\cap \left(0..^{N}\right)\right)+{K}\left({B}\cap \left(0..^{N}\right)\right)+if\left({N}\in {A},{2}^{{N}},0\right)+if\left({N}\in {B},{2}^{{N}},0\right)$
94 27 34 41 addassd ${⊢}{\phi }\to {K}\left(\left({A}\mathrm{sadd}{B}\right)\cap \left(0..^{N}\right)\right)+if\left({N}\in \left({A}\mathrm{sadd}{B}\right),{2}^{{N}},0\right)+if\left(\varnothing \in {C}\left({N}+1\right),{2}^{{N}+1},0\right)={K}\left(\left({A}\mathrm{sadd}{B}\right)\cap \left(0..^{N}\right)\right)+if\left({N}\in \left({A}\mathrm{sadd}{B}\right),{2}^{{N}},0\right)+if\left(\varnothing \in {C}\left({N}+1\right),{2}^{{N}+1},0\right)$
95 53 67 63 70 add4d ${⊢}{\phi }\to {K}\left({A}\cap \left(0..^{N}\right)\right)+if\left({N}\in {A},{2}^{{N}},0\right)+{K}\left({B}\cap \left(0..^{N}\right)\right)+if\left({N}\in {B},{2}^{{N}},0\right)={K}\left({A}\cap \left(0..^{N}\right)\right)+{K}\left({B}\cap \left(0..^{N}\right)\right)+if\left({N}\in {A},{2}^{{N}},0\right)+if\left({N}\in {B},{2}^{{N}},0\right)$
96 93 94 95 3eqtr4d ${⊢}{\phi }\to {K}\left(\left({A}\mathrm{sadd}{B}\right)\cap \left(0..^{N}\right)\right)+if\left({N}\in \left({A}\mathrm{sadd}{B}\right),{2}^{{N}},0\right)+if\left(\varnothing \in {C}\left({N}+1\right),{2}^{{N}+1},0\right)={K}\left({A}\cap \left(0..^{N}\right)\right)+if\left({N}\in {A},{2}^{{N}},0\right)+{K}\left({B}\cap \left(0..^{N}\right)\right)+if\left({N}\in {B},{2}^{{N}},0\right)$
97 5 bitsinvp1 ${⊢}\left({A}\mathrm{sadd}{B}\subseteq {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to {K}\left(\left({A}\mathrm{sadd}{B}\right)\cap \left(0..^{N}+1\right)\right)={K}\left(\left({A}\mathrm{sadd}{B}\right)\cap \left(0..^{N}\right)\right)+if\left({N}\in \left({A}\mathrm{sadd}{B}\right),{2}^{{N}},0\right)$
98 10 4 97 syl2anc ${⊢}{\phi }\to {K}\left(\left({A}\mathrm{sadd}{B}\right)\cap \left(0..^{N}+1\right)\right)={K}\left(\left({A}\mathrm{sadd}{B}\right)\cap \left(0..^{N}\right)\right)+if\left({N}\in \left({A}\mathrm{sadd}{B}\right),{2}^{{N}},0\right)$
99 98 oveq1d ${⊢}{\phi }\to {K}\left(\left({A}\mathrm{sadd}{B}\right)\cap \left(0..^{N}+1\right)\right)+if\left(\varnothing \in {C}\left({N}+1\right),{2}^{{N}+1},0\right)={K}\left(\left({A}\mathrm{sadd}{B}\right)\cap \left(0..^{N}\right)\right)+if\left({N}\in \left({A}\mathrm{sadd}{B}\right),{2}^{{N}},0\right)+if\left(\varnothing \in {C}\left({N}+1\right),{2}^{{N}+1},0\right)$
100 5 bitsinvp1 ${⊢}\left({A}\subseteq {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to {K}\left({A}\cap \left(0..^{N}+1\right)\right)={K}\left({A}\cap \left(0..^{N}\right)\right)+if\left({N}\in {A},{2}^{{N}},0\right)$
101 1 4 100 syl2anc ${⊢}{\phi }\to {K}\left({A}\cap \left(0..^{N}+1\right)\right)={K}\left({A}\cap \left(0..^{N}\right)\right)+if\left({N}\in {A},{2}^{{N}},0\right)$
102 5 bitsinvp1 ${⊢}\left({B}\subseteq {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to {K}\left({B}\cap \left(0..^{N}+1\right)\right)={K}\left({B}\cap \left(0..^{N}\right)\right)+if\left({N}\in {B},{2}^{{N}},0\right)$
103 2 4 102 syl2anc ${⊢}{\phi }\to {K}\left({B}\cap \left(0..^{N}+1\right)\right)={K}\left({B}\cap \left(0..^{N}\right)\right)+if\left({N}\in {B},{2}^{{N}},0\right)$
104 101 103 oveq12d ${⊢}{\phi }\to {K}\left({A}\cap \left(0..^{N}+1\right)\right)+{K}\left({B}\cap \left(0..^{N}+1\right)\right)={K}\left({A}\cap \left(0..^{N}\right)\right)+if\left({N}\in {A},{2}^{{N}},0\right)+{K}\left({B}\cap \left(0..^{N}\right)\right)+if\left({N}\in {B},{2}^{{N}},0\right)$
105 96 99 104 3eqtr4d ${⊢}{\phi }\to {K}\left(\left({A}\mathrm{sadd}{B}\right)\cap \left(0..^{N}+1\right)\right)+if\left(\varnothing \in {C}\left({N}+1\right),{2}^{{N}+1},0\right)={K}\left({A}\cap \left(0..^{N}+1\right)\right)+{K}\left({B}\cap \left(0..^{N}+1\right)\right)$