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

 Description: The full adder sequence is the half adder function applied to the inputs and the carry sequence. (Contributed by Mario Carneiro, 5-Sep-2016.)
Hypotheses
Ref Expression
sadval.c 𝐶 = seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝐴, 𝑚𝐵, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))
Assertion
Ref Expression
Distinct variable groups:   𝑚,𝑐,𝑛   𝐴,𝑐,𝑚   𝐵,𝑐,𝑚   𝑛,𝑁
Allowed substitution hints:   𝜑(𝑚,𝑛,𝑐)   𝐴(𝑛)   𝐵(𝑛)   𝐶(𝑚,𝑛,𝑐)   𝑁(𝑚,𝑐)

Dummy variable 𝑘 is distinct from all other variables.
StepHypRef Expression
1 sadval.a . . . 4 (𝜑𝐴 ⊆ ℕ0)
2 sadval.b . . . 4 (𝜑𝐵 ⊆ ℕ0)
3 sadval.c . . . 4 𝐶 = seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝐴, 𝑚𝐵, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))
41, 2, 3sadfval 15794 . . 3 (𝜑 → (𝐴 sadd 𝐵) = {𝑘 ∈ ℕ0 ∣ hadd(𝑘𝐴, 𝑘𝐵, ∅ ∈ (𝐶𝑘))})
54eleq2d 2878 . 2 (𝜑 → (𝑁 ∈ (𝐴 sadd 𝐵) ↔ 𝑁 ∈ {𝑘 ∈ ℕ0 ∣ hadd(𝑘𝐴, 𝑘𝐵, ∅ ∈ (𝐶𝑘))}))
6 sadcp1.n . . 3 (𝜑𝑁 ∈ ℕ0)
7 eleq1 2880 . . . . 5 (𝑘 = 𝑁 → (𝑘𝐴𝑁𝐴))
8 eleq1 2880 . . . . 5 (𝑘 = 𝑁 → (𝑘𝐵𝑁𝐵))
9 fveq2 6649 . . . . . 6 (𝑘 = 𝑁 → (𝐶𝑘) = (𝐶𝑁))
109eleq2d 2878 . . . . 5 (𝑘 = 𝑁 → (∅ ∈ (𝐶𝑘) ↔ ∅ ∈ (𝐶𝑁)))
117, 8, 10hadbi123d 1596 . . . 4 (𝑘 = 𝑁 → (hadd(𝑘𝐴, 𝑘𝐵, ∅ ∈ (𝐶𝑘)) ↔ hadd(𝑁𝐴, 𝑁𝐵, ∅ ∈ (𝐶𝑁))))
1211elrab3 3632 . . 3 (𝑁 ∈ ℕ0 → (𝑁 ∈ {𝑘 ∈ ℕ0 ∣ hadd(𝑘𝐴, 𝑘𝐵, ∅ ∈ (𝐶𝑘))} ↔ hadd(𝑁𝐴, 𝑁𝐵, ∅ ∈ (𝐶𝑁))))
136, 12syl 17 . 2 (𝜑 → (𝑁 ∈ {𝑘 ∈ ℕ0 ∣ hadd(𝑘𝐴, 𝑘𝐵, ∅ ∈ (𝐶𝑘))} ↔ hadd(𝑁𝐴, 𝑁𝐵, ∅ ∈ (𝐶𝑁))))
145, 13bitrd 282 1 (𝜑 → (𝑁 ∈ (𝐴 sadd 𝐵) ↔ hadd(𝑁𝐴, 𝑁𝐵, ∅ ∈ (𝐶𝑁))))