Metamath Proof Explorer

Definition df-sad

Description: Define the addition of two bit sequences, using df-had and df-cad bit operations. (Contributed by Mario Carneiro, 5-Sep-2016)

Ref Expression
Assertion df-sad ⊢sadd=x∈𝒫ℕ0,y∈𝒫ℕ0⟼k∈ℕ0|haddk∈xk∈y∅∈seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈xm∈y∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1⁡k

Detailed syntax breakdown

Step Hyp Ref Expression
0 csad classsadd
1 vx setvarx
2 cn0 classℕ0
3 2 cpw class𝒫ℕ0
4 vy setvary
5 vk setvark
6 5 cv setvark
7 1 cv setvarx
8 6 7 wcel wffk∈x
9 4 cv setvary
10 6 9 wcel wffk∈y
11 c0 class∅
12 cc0 class0
13 vc setvarc
14 c2o class2𝑜
15 vm setvarm
16 15 cv setvarm
17 16 7 wcel wffm∈x
18 16 9 wcel wffm∈y
19 13 cv setvarc
20 11 19 wcel wff∅∈c
21 17 18 20 wcad wffcaddm∈xm∈y∅∈c
22 c1o class1𝑜
23 21 22 11 cif classifcaddm∈xm∈y∅∈c1𝑜∅
24 13 15 14 2 23 cmpo classc∈2𝑜,m∈ℕ0⟼ifcaddm∈xm∈y∅∈c1𝑜∅
25 vn setvarn
26 25 cv setvarn
27 26 12 wceq wffn=0
28 cmin class−
29 c1 class1
30 26 29 28 co classn−1
31 27 11 30 cif classifn=0∅n−1
32 25 2 31 cmpt classn∈ℕ0⟼ifn=0∅n−1
33 24 32 12 cseq classseq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈xm∈y∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1
34 6 33 cfv classseq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈xm∈y∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1⁡k
35 11 34 wcel wff∅∈seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈xm∈y∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1⁡k
36 8 10 35 whad wffhaddk∈xk∈y∅∈seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈xm∈y∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1⁡k
37 36 5 2 crab classk∈ℕ0|haddk∈xk∈y∅∈seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈xm∈y∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1⁡k
38 1 4 3 3 37 cmpo classx∈𝒫ℕ0,y∈𝒫ℕ0⟼k∈ℕ0|haddk∈xk∈y∅∈seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈xm∈y∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1⁡k
39 0 38 wceq wffsadd=x∈𝒫ℕ0,y∈𝒫ℕ0⟼k∈ℕ0|haddk∈xk∈y∅∈seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈xm∈y∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1⁡k