Definition df-sad 16614

Description: Define the addition of two bit sequences, using df-had 1624 and df-cad 1640 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 16583	. 2 class sadd
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cn0 12599	. . . 4 class ℕ0
5	4	cpw 4557	. . 3 class 𝒫 ℕ0
6		vk	. . . . . 6 setvar 𝑘
7	6, 2	wel 2146	. . . . 5 wff 𝑘 ∈ 𝑥
8	6, 3	wel 2146	. . . . 5 wff 𝑘 ∈ 𝑦
9		c0 4279	. . . . . 6 class ∅
10	6	cv 1569	. . . . . . 7 class 𝑘
11		vc	. . . . . . . . 9 setvar 𝑐
12		vm	. . . . . . . . 9 setvar 𝑚
13		c2o 8463	. . . . . . . . 9 class 2o
14	12, 2	wel 2146	. . . . . . . . . . 11 wff 𝑚 ∈ 𝑥
15	12, 3	wel 2146	. . . . . . . . . . 11 wff 𝑚 ∈ 𝑦
16	11	cv 1569	. . . . . . . . . . . 12 class 𝑐
17	9, 16	wcel 2145	. . . . . . . . . . 11 wff ∅ ∈ 𝑐
18	14, 15, 17	wcad 1639	. . . . . . . . . 10 wff cadd(𝑚 ∈ 𝑥, 𝑚 ∈ 𝑦, ∅ ∈ 𝑐)
19		c1o 8462	. . . . . . . . . 10 class 1o
20	18, 19, 9	cif 4482	. . . . . . . . 9 class if(cadd(𝑚 ∈ 𝑥, 𝑚 ∈ 𝑦, ∅ ∈ 𝑐), 1o, ∅)
21	11, 12, 13, 4, 20	cmpo 7420	. . . . . . . 8 class (𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝑥, 𝑚 ∈ 𝑦, ∅ ∈ 𝑐), 1o, ∅))
22		vn	. . . . . . . . 9 setvar 𝑛
23	22	cv 1569	. . . . . . . . . . 11 class 𝑛
24		cc0 11193	. . . . . . . . . . 11 class 0
25	23, 24	wceq 1570	. . . . . . . . . 10 wff 𝑛 = 0
26		c1 11194	. . . . . . . . . . 11 class 1
27		cmin 11534	. . . . . . . . . . 11 class −
28	23, 26, 27	co 7418	. . . . . . . . . 10 class (𝑛 − 1)
29	25, 9, 28	cif 4482	. . . . . . . . 9 class if(𝑛 = 0, ∅, (𝑛 − 1))
30	22, 4, 29	cmpt 5186	. . . . . . . 8 class (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))
31	21, 30, 24	cseq 14137	. . . . . . 7 class seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝑥, 𝑚 ∈ 𝑦, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))
32	10, 31	cfv 6537	. . . . . 6 class (seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝑥, 𝑚 ∈ 𝑦, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘)
33	9, 32	wcel 2145	. . . . 5 wff ∅ ∈ (seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝑥, 𝑚 ∈ 𝑦, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘)
34	7, 8, 33	whad 1623	. . . 4 wff hadd(𝑘 ∈ 𝑥, 𝑘 ∈ 𝑦, ∅ ∈ (seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝑥, 𝑚 ∈ 𝑦, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘))
35	34, 6, 4	crab 3413	. . 3 class {𝑘 ∈ ℕ0 ∣ hadd(𝑘 ∈ 𝑥, 𝑘 ∈ 𝑦, ∅ ∈ (seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝑥, 𝑚 ∈ 𝑦, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘))}
36	2, 3, 5, 5, 35	cmpo 7420	. 2 class (𝑥 ∈ 𝒫 ℕ0, 𝑦 ∈ 𝒫 ℕ0 ↦ {𝑘 ∈ ℕ0 ∣ hadd(𝑘 ∈ 𝑥, 𝑘 ∈ 𝑦, ∅ ∈ (seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝑥, 𝑚 ∈ 𝑦, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘))})
37	1, 36	wceq 1570	1 wff sadd = (𝑥 ∈ 𝒫 ℕ0, 𝑦 ∈ 𝒫 ℕ0 ↦ {𝑘 ∈ ℕ0 ∣ hadd(𝑘 ∈ 𝑥, 𝑘 ∈ 𝑦, ∅ ∈ (seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝑥, 𝑚 ∈ 𝑦, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘))})

This definition is used by:  sadfval  16615