Definition df-sad 16010

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

Assertion

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

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

Detailed syntax breakdown of Definition df-sad

Step	Hyp	Ref	Expression
1		csad 15979	. 2 class sadd
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cn0 12090	. . . 4 class ℕ0
5	4	cpw 4513	. . 3 class 𝒫 ℕ0
6		vk	. . . . . 6 setvar 𝑘
7	6, 2	wel 2111	. . . . 5 wff 𝑘 ∈ 𝑥
8	6, 3	wel 2111	. . . . 5 wff 𝑘 ∈ 𝑦
9		c0 4237	. . . . . 6 class ∅
10	6	cv 1542	. . . . . . 7 class 𝑘
11		vc	. . . . . . . . 9 setvar 𝑐
12		vm	. . . . . . . . 9 setvar 𝑚
13		c2o 8196	. . . . . . . . 9 class 2o
14	12, 2	wel 2111	. . . . . . . . . . 11 wff 𝑚 ∈ 𝑥
15	12, 3	wel 2111	. . . . . . . . . . 11 wff 𝑚 ∈ 𝑦
16	11	cv 1542	. . . . . . . . . . . 12 class 𝑐
17	9, 16	wcel 2110	. . . . . . . . . . 11 wff ∅ ∈ 𝑐
18	14, 15, 17	wcad 1613	. . . . . . . . . 10 wff cadd(𝑚 ∈ 𝑥, 𝑚 ∈ 𝑦, ∅ ∈ 𝑐)
19		c1o 8195	. . . . . . . . . 10 class 1o
20	18, 19, 9	cif 4439	. . . . . . . . 9 class if(cadd(𝑚 ∈ 𝑥, 𝑚 ∈ 𝑦, ∅ ∈ 𝑐), 1o, ∅)
21	11, 12, 13, 4, 20	cmpo 7215	. . . . . . . 8 class (𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝑥, 𝑚 ∈ 𝑦, ∅ ∈ 𝑐), 1o, ∅))
22		vn	. . . . . . . . 9 setvar 𝑛
23	22	cv 1542	. . . . . . . . . . 11 class 𝑛
24		cc0 10729	. . . . . . . . . . 11 class 0
25	23, 24	wceq 1543	. . . . . . . . . 10 wff 𝑛 = 0
26		c1 10730	. . . . . . . . . . 11 class 1
27		cmin 11062	. . . . . . . . . . 11 class −
28	23, 26, 27	co 7213	. . . . . . . . . 10 class (𝑛 − 1)
29	25, 9, 28	cif 4439	. . . . . . . . 9 class if(𝑛 = 0, ∅, (𝑛 − 1))
30	22, 4, 29	cmpt 5135	. . . . . . . 8 class (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))
31	21, 30, 24	cseq 13574	. . . . . . 7 class seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝑥, 𝑚 ∈ 𝑦, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))
32	10, 31	cfv 6380	. . . . . 6 class (seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝑥, 𝑚 ∈ 𝑦, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘)
33	9, 32	wcel 2110	. . . . 5 wff ∅ ∈ (seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝑥, 𝑚 ∈ 𝑦, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘)
34	7, 8, 33	whad 1599	. . . 4 wff hadd(𝑘 ∈ 𝑥, 𝑘 ∈ 𝑦, ∅ ∈ (seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝑥, 𝑚 ∈ 𝑦, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘))
35	34, 6, 4	crab 3065	. . 3 class {𝑘 ∈ ℕ0 ∣ hadd(𝑘 ∈ 𝑥, 𝑘 ∈ 𝑦, ∅ ∈ (seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝑥, 𝑚 ∈ 𝑦, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘))}
36	2, 3, 5, 5, 35	cmpo 7215	. 2 class (𝑥 ∈ 𝒫 ℕ0, 𝑦 ∈ 𝒫 ℕ0 ↦ {𝑘 ∈ ℕ0 ∣ hadd(𝑘 ∈ 𝑥, 𝑘 ∈ 𝑦, ∅ ∈ (seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝑥, 𝑚 ∈ 𝑦, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘))})
37	1, 36	wceq 1543	1 wff sadd = (𝑥 ∈ 𝒫 ℕ0, 𝑦 ∈ 𝒫 ℕ0 ↦ {𝑘 ∈ ℕ0 ∣ hadd(𝑘 ∈ 𝑥, 𝑘 ∈ 𝑦, ∅ ∈ (seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝑥, 𝑚 ∈ 𝑦, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘))})

This definition is referenced by:  sadfval  16011