Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-sad Structured version   Visualization version   GIF version

 Description: Define the addition of two bit sequences, using df-had 1530 and df-cad 1543 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
StepHypRef Expression
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cn0 11236 . . . 4 class 0
54cpw 4130 . . 3 class 𝒫 ℕ0
6 vk . . . . . 6 setvar 𝑘
76, 2wel 1988 . . . . 5 wff 𝑘𝑥
86, 3wel 1988 . . . . 5 wff 𝑘𝑦
9 c0 3891 . . . . . 6 class
106cv 1479 . . . . . . 7 class 𝑘
11 vc . . . . . . . . 9 setvar 𝑐
12 vm . . . . . . . . 9 setvar 𝑚
13 c2o 7499 . . . . . . . . 9 class 2𝑜
1412, 2wel 1988 . . . . . . . . . . 11 wff 𝑚𝑥
1512, 3wel 1988 . . . . . . . . . . 11 wff 𝑚𝑦
1611cv 1479 . . . . . . . . . . . 12 class 𝑐
179, 16wcel 1987 . . . . . . . . . . 11 wff ∅ ∈ 𝑐
1814, 15, 17wcad 1542 . . . . . . . . . 10 wff cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐)
19 c1o 7498 . . . . . . . . . 10 class 1𝑜
2018, 19, 9cif 4058 . . . . . . . . 9 class if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1𝑜, ∅)
2111, 12, 13, 4, 20cmpt2 6606 . . . . . . . 8 class (𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1𝑜, ∅))
22 vn . . . . . . . . 9 setvar 𝑛
2322cv 1479 . . . . . . . . . . 11 class 𝑛
24 cc0 9880 . . . . . . . . . . 11 class 0
2523, 24wceq 1480 . . . . . . . . . 10 wff 𝑛 = 0
26 c1 9881 . . . . . . . . . . 11 class 1
27 cmin 10210 . . . . . . . . . . 11 class
2823, 26, 27co 6604 . . . . . . . . . 10 class (𝑛 − 1)
2925, 9, 28cif 4058 . . . . . . . . 9 class if(𝑛 = 0, ∅, (𝑛 − 1))
3022, 4, 29cmpt 4673 . . . . . . . 8 class (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))
3121, 30, 24cseq 12741 . . . . . . 7 class seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))
3210, 31cfv 5847 . . . . . 6 class (seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘)
339, 32wcel 1987 . . . . 5 wff ∅ ∈ (seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘)
347, 8, 33whad 1529 . . . 4 wff hadd(𝑘𝑥, 𝑘𝑦, ∅ ∈ (seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘))
3534, 6, 4crab 2911 . . 3 class {𝑘 ∈ ℕ0 ∣ hadd(𝑘𝑥, 𝑘𝑦, ∅ ∈ (seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘))}
362, 3, 5, 5, 35cmpt2 6606 . 2 class (𝑥 ∈ 𝒫 ℕ0, 𝑦 ∈ 𝒫 ℕ0 ↦ {𝑘 ∈ ℕ0 ∣ hadd(𝑘𝑥, 𝑘𝑦, ∅ ∈ (seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘))})
371, 36wceq 1480 1 wff sadd = (𝑥 ∈ 𝒫 ℕ0, 𝑦 ∈ 𝒫 ℕ0 ↦ {𝑘 ∈ ℕ0 ∣ hadd(𝑘𝑥, 𝑘𝑦, ∅ ∈ (seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘))})
 Colors of variables: wff setvar class This definition is referenced by:  sadfval  15098
 Copyright terms: Public domain W3C validator