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 = ( 𝑥 ∈ 𝒫 ℕ0 , 𝑦 ∈ 𝒫 ℕ0 ↦ { 𝑘 ∈ ℕ0 ∣ hadd ( 𝑘 ∈ 𝑥 , 𝑘 ∈ 𝑦 , ∅ ∈ ( seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝑥 , 𝑚 ∈ 𝑦 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csad	⊢ sadd
1		vx	⊢ 𝑥
2		cn0	⊢ ℕ0
3	2	cpw	⊢ 𝒫 ℕ0
4		vy	⊢ 𝑦
5		vk	⊢ 𝑘
6	5	cv	⊢ 𝑘
7	1	cv	⊢ 𝑥
8	6 7	wcel	⊢ 𝑘 ∈ 𝑥
9	4	cv	⊢ 𝑦
10	6 9	wcel	⊢ 𝑘 ∈ 𝑦
11		c0	⊢ ∅
12		cc0	⊢ 0
13		vc	⊢ 𝑐
14		c2o	⊢ 2o
15		vm	⊢ 𝑚
16	15	cv	⊢ 𝑚
17	16 7	wcel	⊢ 𝑚 ∈ 𝑥
18	16 9	wcel	⊢ 𝑚 ∈ 𝑦
19	13	cv	⊢ 𝑐
20	11 19	wcel	⊢ ∅ ∈ 𝑐
21	17 18 20	wcad	⊢ cadd ( 𝑚 ∈ 𝑥 , 𝑚 ∈ 𝑦 , ∅ ∈ 𝑐 )
22		c1o	⊢ 1o
23	21 22 11	cif	⊢ if ( cadd ( 𝑚 ∈ 𝑥 , 𝑚 ∈ 𝑦 , ∅ ∈ 𝑐 ) , 1o , ∅ )
24	13 15 14 2 23	cmpo	⊢ ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝑥 , 𝑚 ∈ 𝑦 , ∅ ∈ 𝑐 ) , 1o , ∅ ) )
25		vn	⊢ 𝑛
26	25	cv	⊢ 𝑛
27	26 12	wceq	⊢ 𝑛 = 0
28		cmin	⊢ −
29		c1	⊢ 1
30	26 29 28	co	⊢ ( 𝑛 − 1 )
31	27 11 30	cif	⊢ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) )
32	25 2 31	cmpt	⊢ ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) )
33	24 32 12	cseq	⊢ seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝑥 , 𝑚 ∈ 𝑦 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) )
34	6 33	cfv	⊢ ( seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝑥 , 𝑚 ∈ 𝑦 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 )
35	11 34	wcel	⊢ ∅ ∈ ( seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝑥 , 𝑚 ∈ 𝑦 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 )
36	8 10 35	whad	⊢ hadd ( 𝑘 ∈ 𝑥 , 𝑘 ∈ 𝑦 , ∅ ∈ ( seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝑥 , 𝑚 ∈ 𝑦 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) )
37	36 5 2	crab	⊢ { 𝑘 ∈ ℕ0 ∣ hadd ( 𝑘 ∈ 𝑥 , 𝑘 ∈ 𝑦 , ∅ ∈ ( seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝑥 , 𝑚 ∈ 𝑦 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) ) }
38	1 4 3 3 37	cmpo	⊢ ( 𝑥 ∈ 𝒫 ℕ0 , 𝑦 ∈ 𝒫 ℕ0 ↦ { 𝑘 ∈ ℕ0 ∣ hadd ( 𝑘 ∈ 𝑥 , 𝑘 ∈ 𝑦 , ∅ ∈ ( seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝑥 , 𝑚 ∈ 𝑦 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) ) } )
39	0 38	wceq	⊢ sadd = ( 𝑥 ∈ 𝒫 ℕ0 , 𝑦 ∈ 𝒫 ℕ0 ↦ { 𝑘 ∈ ℕ0 ∣ hadd ( 𝑘 ∈ 𝑥 , 𝑘 ∈ 𝑦 , ∅ ∈ ( seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝑥 , 𝑚 ∈ 𝑦 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) ) } )