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 1595 and df-cad 1609 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
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cn0 11888 . . . 4 class 0
54cpw 4497 . . 3 class 𝒫 ℕ0
6 vk . . . . . 6 setvar 𝑘
76, 2wel 2112 . . . . 5 wff 𝑘𝑥
86, 3wel 2112 . . . . 5 wff 𝑘𝑦
9 c0 4243 . . . . . 6 class
106cv 1537 . . . . . . 7 class 𝑘
11 vc . . . . . . . . 9 setvar 𝑐
12 vm . . . . . . . . 9 setvar 𝑚
13 c2o 8082 . . . . . . . . 9 class 2o
1412, 2wel 2112 . . . . . . . . . . 11 wff 𝑚𝑥
1512, 3wel 2112 . . . . . . . . . . 11 wff 𝑚𝑦
1611cv 1537 . . . . . . . . . . . 12 class 𝑐
179, 16wcel 2111 . . . . . . . . . . 11 wff ∅ ∈ 𝑐
1814, 15, 17wcad 1608 . . . . . . . . . 10 wff cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐)
19 c1o 8081 . . . . . . . . . 10 class 1o
2018, 19, 9cif 4425 . . . . . . . . 9 class if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1o, ∅)
2111, 12, 13, 4, 20cmpo 7138 . . . . . . . 8 class (𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1o, ∅))
22 vn . . . . . . . . 9 setvar 𝑛
2322cv 1537 . . . . . . . . . . 11 class 𝑛
24 cc0 10529 . . . . . . . . . . 11 class 0
2523, 24wceq 1538 . . . . . . . . . 10 wff 𝑛 = 0
26 c1 10530 . . . . . . . . . . 11 class 1
27 cmin 10862 . . . . . . . . . . 11 class
2823, 26, 27co 7136 . . . . . . . . . 10 class (𝑛 − 1)
2925, 9, 28cif 4425 . . . . . . . . 9 class if(𝑛 = 0, ∅, (𝑛 − 1))
3022, 4, 29cmpt 5111 . . . . . . . 8 class (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))
3121, 30, 24cseq 13367 . . . . . . 7 class seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))
3210, 31cfv 6325 . . . . . 6 class (seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘)
339, 32wcel 2111 . . . . 5 wff ∅ ∈ (seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘)
347, 8, 33whad 1594 . . . 4 wff hadd(𝑘𝑥, 𝑘𝑦, ∅ ∈ (seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘))
3534, 6, 4crab 3110 . . 3 class {𝑘 ∈ ℕ0 ∣ hadd(𝑘𝑥, 𝑘𝑦, ∅ ∈ (seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘))}
362, 3, 5, 5, 35cmpo 7138 . 2 class (𝑥 ∈ 𝒫 ℕ0, 𝑦 ∈ 𝒫 ℕ0 ↦ {𝑘 ∈ ℕ0 ∣ hadd(𝑘𝑥, 𝑘𝑦, ∅ ∈ (seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘))})
371, 36wceq 1538 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  15794
 Copyright terms: Public domain W3C validator