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

Definition df-sad 15011
Description: Define the addition of two bit sequences, using df-had 1524 and df-cad 1537 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
1 csad 14980 . 2 class sadd
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cn0 11169 . . . 4 class 0
54cpw 4108 . . 3 class 𝒫 ℕ0
6 vk . . . . . 6 setvar 𝑘
76, 2wel 1978 . . . . 5 wff 𝑘𝑥
86, 3wel 1978 . . . . 5 wff 𝑘𝑦
9 c0 3874 . . . . . 6 class
106cv 1474 . . . . . . 7 class 𝑘
11 vc . . . . . . . . 9 setvar 𝑐
12 vm . . . . . . . . 9 setvar 𝑚
13 c2o 7441 . . . . . . . . 9 class 2𝑜
1412, 2wel 1978 . . . . . . . . . . 11 wff 𝑚𝑥
1512, 3wel 1978 . . . . . . . . . . 11 wff 𝑚𝑦
1611cv 1474 . . . . . . . . . . . 12 class 𝑐
179, 16wcel 1977 . . . . . . . . . . 11 wff ∅ ∈ 𝑐
1814, 15, 17wcad 1536 . . . . . . . . . 10 wff cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐)
19 c1o 7440 . . . . . . . . . 10 class 1𝑜
2018, 19, 9cif 4036 . . . . . . . . 9 class if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1𝑜, ∅)
2111, 12, 13, 4, 20cmpt2 6551 . . . . . . . 8 class (𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1𝑜, ∅))
22 vn . . . . . . . . 9 setvar 𝑛
2322cv 1474 . . . . . . . . . . 11 class 𝑛
24 cc0 9815 . . . . . . . . . . 11 class 0
2523, 24wceq 1475 . . . . . . . . . 10 wff 𝑛 = 0
26 c1 9816 . . . . . . . . . . 11 class 1
27 cmin 10145 . . . . . . . . . . 11 class
2823, 26, 27co 6549 . . . . . . . . . 10 class (𝑛 − 1)
2925, 9, 28cif 4036 . . . . . . . . 9 class if(𝑛 = 0, ∅, (𝑛 − 1))
3022, 4, 29cmpt 4643 . . . . . . . 8 class (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))
3121, 30, 24cseq 12663 . . . . . . 7 class seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))
3210, 31cfv 5804 . . . . . 6 class (seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘)
339, 32wcel 1977 . . . . 5 wff ∅ ∈ (seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘)
347, 8, 33whad 1523 . . . 4 wff hadd(𝑘𝑥, 𝑘𝑦, ∅ ∈ (seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘))
3534, 6, 4crab 2900 . . 3 class {𝑘 ∈ ℕ0 ∣ hadd(𝑘𝑥, 𝑘𝑦, ∅ ∈ (seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘))}
362, 3, 5, 5, 35cmpt2 6551 . 2 class (𝑥 ∈ 𝒫 ℕ0, 𝑦 ∈ 𝒫 ℕ0 ↦ {𝑘 ∈ ℕ0 ∣ hadd(𝑘𝑥, 𝑘𝑦, ∅ ∈ (seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘))})
371, 36wceq 1475 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  15012
  Copyright terms: Public domain W3C validator