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 = ( 𝑥 ∈ 𝒫 ℕ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 ) ) ) ) ‘ 𝑘 ) ) } )