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

 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.)
Hypotheses
Ref Expression
sadval.c 𝐶 = seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝐴, 𝑚𝐵, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))
Assertion
Ref Expression
Distinct variable groups:   𝑘,𝑐,𝑚,𝑛   𝐴,𝑐,𝑘,𝑚   𝐵,𝑐,𝑘,𝑚   𝐶,𝑘   𝜑,𝑘
Allowed substitution hints:   𝜑(𝑚,𝑛,𝑐)   𝐴(𝑛)   𝐵(𝑛)   𝐶(𝑚,𝑛,𝑐)

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sadval.a . . 3 (𝜑𝐴 ⊆ ℕ0)
2 nn0ex 11175 . . . 4 0 ∈ V
32elpw2 4755 . . 3 (𝐴 ∈ 𝒫 ℕ0𝐴 ⊆ ℕ0)
41, 3sylibr 223 . 2 (𝜑𝐴 ∈ 𝒫 ℕ0)
5 sadval.b . . 3 (𝜑𝐵 ⊆ ℕ0)
62elpw2 4755 . . 3 (𝐵 ∈ 𝒫 ℕ0𝐵 ⊆ ℕ0)
75, 6sylibr 223 . 2 (𝜑𝐵 ∈ 𝒫 ℕ0)
8 simpl 472 . . . . . 6 ((𝑥 = 𝐴𝑦 = 𝐵) → 𝑥 = 𝐴)
98eleq2d 2673 . . . . 5 ((𝑥 = 𝐴𝑦 = 𝐵) → (𝑘𝑥𝑘𝐴))
10 simpr 476 . . . . . 6 ((𝑥 = 𝐴𝑦 = 𝐵) → 𝑦 = 𝐵)
1110eleq2d 2673 . . . . 5 ((𝑥 = 𝐴𝑦 = 𝐵) → (𝑘𝑦𝑘𝐵))
12 simp1l 1078 . . . . . . . . . . . . 13 (((𝑥 = 𝐴𝑦 = 𝐵) ∧ 𝑐 ∈ 2𝑜𝑚 ∈ ℕ0) → 𝑥 = 𝐴)
1312eleq2d 2673 . . . . . . . . . . . 12 (((𝑥 = 𝐴𝑦 = 𝐵) ∧ 𝑐 ∈ 2𝑜𝑚 ∈ ℕ0) → (𝑚𝑥𝑚𝐴))
14 simp1r 1079 . . . . . . . . . . . . 13 (((𝑥 = 𝐴𝑦 = 𝐵) ∧ 𝑐 ∈ 2𝑜𝑚 ∈ ℕ0) → 𝑦 = 𝐵)
1514eleq2d 2673 . . . . . . . . . . . 12 (((𝑥 = 𝐴𝑦 = 𝐵) ∧ 𝑐 ∈ 2𝑜𝑚 ∈ ℕ0) → (𝑚𝑦𝑚𝐵))
16 biidd 251 . . . . . . . . . . . 12 (((𝑥 = 𝐴𝑦 = 𝐵) ∧ 𝑐 ∈ 2𝑜𝑚 ∈ ℕ0) → (∅ ∈ 𝑐 ↔ ∅ ∈ 𝑐))
1713, 15, 16cadbi123d 1540 . . . . . . . . . . 11 (((𝑥 = 𝐴𝑦 = 𝐵) ∧ 𝑐 ∈ 2𝑜𝑚 ∈ ℕ0) → (cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐) ↔ cadd(𝑚𝐴, 𝑚𝐵, ∅ ∈ 𝑐)))
1817ifbid 4058 . . . . . . . . . 10 (((𝑥 = 𝐴𝑦 = 𝐵) ∧ 𝑐 ∈ 2𝑜𝑚 ∈ ℕ0) → if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1𝑜, ∅) = if(cadd(𝑚𝐴, 𝑚𝐵, ∅ ∈ 𝑐), 1𝑜, ∅))
1918mpt2eq3dva 6617 . . . . . . . . 9 ((𝑥 = 𝐴𝑦 = 𝐵) → (𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1𝑜, ∅)) = (𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝐴, 𝑚𝐵, ∅ ∈ 𝑐), 1𝑜, ∅)))
2019seqeq2d 12670 . . . . . . . 8 ((𝑥 = 𝐴𝑦 = 𝐵) → seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) = seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝐴, 𝑚𝐵, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))))
21 sadval.c . . . . . . . 8 𝐶 = seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝐴, 𝑚𝐵, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))
2220, 21syl6eqr 2662 . . . . . . 7 ((𝑥 = 𝐴𝑦 = 𝐵) → seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) = 𝐶)
2322fveq1d 6105 . . . . . 6 ((𝑥 = 𝐴𝑦 = 𝐵) → (seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘) = (𝐶𝑘))
2423eleq2d 2673 . . . . 5 ((𝑥 = 𝐴𝑦 = 𝐵) → (∅ ∈ (seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘) ↔ ∅ ∈ (𝐶𝑘)))
259, 11, 24hadbi123d 1525 . . . 4 ((𝑥 = 𝐴𝑦 = 𝐵) → (hadd(𝑘𝑥, 𝑘𝑦, ∅ ∈ (seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘)) ↔ hadd(𝑘𝐴, 𝑘𝐵, ∅ ∈ (𝐶𝑘))))
2625rabbidv 3164 . . 3 ((𝑥 = 𝐴𝑦 = 𝐵) → {𝑘 ∈ ℕ0 ∣ hadd(𝑘𝑥, 𝑘𝑦, ∅ ∈ (seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘))} = {𝑘 ∈ ℕ0 ∣ hadd(𝑘𝐴, 𝑘𝐵, ∅ ∈ (𝐶𝑘))})
27 df-sad 15011 . . 3 sadd = (𝑥 ∈ 𝒫 ℕ0, 𝑦 ∈ 𝒫 ℕ0 ↦ {𝑘 ∈ ℕ0 ∣ hadd(𝑘𝑥, 𝑘𝑦, ∅ ∈ (seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝑥, 𝑚𝑦, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘))})
282rabex 4740 . . 3 {𝑘 ∈ ℕ0 ∣ hadd(𝑘𝐴, 𝑘𝐵, ∅ ∈ (𝐶𝑘))} ∈ V
2926, 27, 28ovmpt2a 6689 . 2 ((𝐴 ∈ 𝒫 ℕ0𝐵 ∈ 𝒫 ℕ0) → (𝐴 sadd 𝐵) = {𝑘 ∈ ℕ0 ∣ hadd(𝑘𝐴, 𝑘𝐵, ∅ ∈ (𝐶𝑘))})
304, 7, 29syl2anc 691 1 (𝜑 → (𝐴 sadd 𝐵) = {𝑘 ∈ ℕ0 ∣ hadd(𝑘𝐴, 𝑘𝐵, ∅ ∈ (𝐶𝑘))})