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 15788
Description: Define the addition of two bit sequences, using df-had 1585 and df-cad 1599 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
StepHypRef Expression
1 csad 15757 . 2 class sadd
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cn0 11885 . . . 4 class 0
54cpw 4535 . . 3 class 𝒫 ℕ0
6 vk . . . . . 6 setvar 𝑘
76, 2wel 2106 . . . . 5 wff 𝑘𝑥
86, 3wel 2106 . . . . 5 wff 𝑘𝑦
9 c0 4288 . . . . . 6 class
106cv 1527 . . . . . . 7 class 𝑘
11 vc . . . . . . . . 9 setvar 𝑐
12 vm . . . . . . . . 9 setvar 𝑚
13 c2o 8085 . . . . . . . . 9 class 2o
1412, 2wel 2106 . . . . . . . . . . 11 wff 𝑚𝑥
1512, 3wel 2106 . . . . . . . . . . 11 wff 𝑚𝑦
1611cv 1527 . . . . . . . . . . . 12 class 𝑐
179, 16wcel 2105 . . . . . . . . . . 11 wff ∅ ∈ 𝑐
1814, 15, 17wcad 1598 . . . . . . . . . 10 wff cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐)
19 c1o 8084 . . . . . . . . . 10 class 1o
2018, 19, 9cif 4463 . . . . . . . . 9 class if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1o, ∅)
2111, 12, 13, 4, 20cmpo 7147 . . . . . . . 8 class (𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1o, ∅))
22 vn . . . . . . . . 9 setvar 𝑛
2322cv 1527 . . . . . . . . . . 11 class 𝑛
24 cc0 10525 . . . . . . . . . . 11 class 0
2523, 24wceq 1528 . . . . . . . . . 10 wff 𝑛 = 0
26 c1 10526 . . . . . . . . . . 11 class 1
27 cmin 10858 . . . . . . . . . . 11 class
2823, 26, 27co 7145 . . . . . . . . . 10 class (𝑛 − 1)
2925, 9, 28cif 4463 . . . . . . . . 9 class if(𝑛 = 0, ∅, (𝑛 − 1))
3022, 4, 29cmpt 5137 . . . . . . . 8 class (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))
3121, 30, 24cseq 13357 . . . . . . 7 class seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))
3210, 31cfv 6348 . . . . . 6 class (seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘)
339, 32wcel 2105 . . . . 5 wff ∅ ∈ (seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘)
347, 8, 33whad 1584 . . . 4 wff hadd(𝑘𝑥, 𝑘𝑦, ∅ ∈ (seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘))
3534, 6, 4crab 3139 . . 3 class {𝑘 ∈ ℕ0 ∣ hadd(𝑘𝑥, 𝑘𝑦, ∅ ∈ (seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘))}
362, 3, 5, 5, 35cmpo 7147 . 2 class (𝑥 ∈ 𝒫 ℕ0, 𝑦 ∈ 𝒫 ℕ0 ↦ {𝑘 ∈ ℕ0 ∣ hadd(𝑘𝑥, 𝑘𝑦, ∅ ∈ (seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘))})
371, 36wceq 1528 1 wff sadd = (𝑥 ∈ 𝒫 ℕ0, 𝑦 ∈ 𝒫 ℕ0 ↦ {𝑘 ∈ ℕ0 ∣ hadd(𝑘𝑥, 𝑘𝑦, ∅ ∈ (seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘))})
Colors of variables: wff setvar class
This definition is referenced by:  sadfval  15789
  Copyright terms: Public domain W3C validator