Definition df-sad 15173

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

Assertion

Ref	Expression
df-sad	⊢ sadd = (𝑥 ∈ 𝒫 ℕ0, 𝑦 ∈ 𝒫 ℕ0 ↦ {𝑘 ∈ ℕ0 ∣ hadd(𝑘 ∈ 𝑥, 𝑘 ∈ 𝑦, ∅ ∈ (seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝑥, 𝑚 ∈ 𝑦, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘))})

Distinct variable group:   𝑘,𝑐,𝑚,𝑛,𝑥,𝑦

Detailed syntax breakdown of Definition df-sad

Step	Hyp	Ref	Expression
1		csad 15142	. 2 class sadd
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cn0 11292	. . . 4 class ℕ0
5	4	cpw 4158	. . 3 class 𝒫 ℕ0
6		vk	. . . . . 6 setvar 𝑘
7	6, 2	wel 1991	. . . . 5 wff 𝑘 ∈ 𝑥
8	6, 3	wel 1991	. . . . 5 wff 𝑘 ∈ 𝑦
9		c0 3915	. . . . . 6 class ∅
10	6	cv 1482	. . . . . . 7 class 𝑘
11		vc	. . . . . . . . 9 setvar 𝑐
12		vm	. . . . . . . . 9 setvar 𝑚
13		c2o 7554	. . . . . . . . 9 class 2𝑜
14	12, 2	wel 1991	. . . . . . . . . . 11 wff 𝑚 ∈ 𝑥
15	12, 3	wel 1991	. . . . . . . . . . 11 wff 𝑚 ∈ 𝑦
16	11	cv 1482	. . . . . . . . . . . 12 class 𝑐
17	9, 16	wcel 1990	. . . . . . . . . . 11 wff ∅ ∈ 𝑐
18	14, 15, 17	wcad 1545	. . . . . . . . . 10 wff cadd(𝑚 ∈ 𝑥, 𝑚 ∈ 𝑦, ∅ ∈ 𝑐)
19		c1o 7553	. . . . . . . . . 10 class 1𝑜
20	18, 19, 9	cif 4086	. . . . . . . . 9 class if(cadd(𝑚 ∈ 𝑥, 𝑚 ∈ 𝑦, ∅ ∈ 𝑐), 1𝑜, ∅)
21	11, 12, 13, 4, 20	cmpt2 6652	. . . . . . . 8 class (𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝑥, 𝑚 ∈ 𝑦, ∅ ∈ 𝑐), 1𝑜, ∅))
22		vn	. . . . . . . . 9 setvar 𝑛
23	22	cv 1482	. . . . . . . . . . 11 class 𝑛
24		cc0 9936	. . . . . . . . . . 11 class 0
25	23, 24	wceq 1483	. . . . . . . . . 10 wff 𝑛 = 0
26		c1 9937	. . . . . . . . . . 11 class 1
27		cmin 10266	. . . . . . . . . . 11 class −
28	23, 26, 27	co 6650	. . . . . . . . . 10 class (𝑛 − 1)
29	25, 9, 28	cif 4086	. . . . . . . . 9 class if(𝑛 = 0, ∅, (𝑛 − 1))
30	22, 4, 29	cmpt 4729	. . . . . . . 8 class (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))
31	21, 30, 24	cseq 12801	. . . . . . 7 class seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝑥, 𝑚 ∈ 𝑦, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))
32	10, 31	cfv 5888	. . . . . 6 class (seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝑥, 𝑚 ∈ 𝑦, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘)
33	9, 32	wcel 1990	. . . . 5 wff ∅ ∈ (seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝑥, 𝑚 ∈ 𝑦, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘)
34	7, 8, 33	whad 1532	. . . 4 wff hadd(𝑘 ∈ 𝑥, 𝑘 ∈ 𝑦, ∅ ∈ (seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝑥, 𝑚 ∈ 𝑦, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘))
35	34, 6, 4	crab 2916	. . 3 class {𝑘 ∈ ℕ0 ∣ hadd(𝑘 ∈ 𝑥, 𝑘 ∈ 𝑦, ∅ ∈ (seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝑥, 𝑚 ∈ 𝑦, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘))}
36	2, 3, 5, 5, 35	cmpt2 6652	. 2 class (𝑥 ∈ 𝒫 ℕ0, 𝑦 ∈ 𝒫 ℕ0 ↦ {𝑘 ∈ ℕ0 ∣ hadd(𝑘 ∈ 𝑥, 𝑘 ∈ 𝑦, ∅ ∈ (seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝑥, 𝑚 ∈ 𝑦, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘))})
37	1, 36	wceq 1483	1 wff sadd = (𝑥 ∈ 𝒫 ℕ0, 𝑦 ∈ 𝒫 ℕ0 ↦ {𝑘 ∈ ℕ0 ∣ hadd(𝑘 ∈ 𝑥, 𝑘 ∈ 𝑦, ∅ ∈ (seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝑥, 𝑚 ∈ 𝑦, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘))})

This definition is referenced by:  sadfval  15174