Metamath Proof Explorer

Theorem sadval

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)

Ref Expression
Hypotheses sadval.a ⊢ φ → A ⊆ ℕ 0
sadval.b ⊢ φ → B ⊆ ℕ 0
sadval.c ⊢ C = seq 0 c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1
sadcp1.n ⊢ φ → N ∈ ℕ 0
Assertion sadval ⊢ φ → N ∈ A sadd B ↔ hadd N ∈ A N ∈ B ∅ ∈ C ⁡ N

Proof

Step Hyp Ref Expression
1 sadval.a ⊢ φ → A ⊆ ℕ 0
2 sadval.b ⊢ φ → B ⊆ ℕ 0
3 sadval.c ⊢ C = seq 0 c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1
4 sadcp1.n ⊢ φ → N ∈ ℕ 0
5 1 2 3 sadfval ⊢ φ → A sadd B = k ∈ ℕ 0 | hadd k ∈ A k ∈ B ∅ ∈ C ⁡ k
6 5 eleq2d ⊢ φ → N ∈ A sadd B ↔ N ∈ k ∈ ℕ 0 | hadd k ∈ A k ∈ B ∅ ∈ C ⁡ k
7 eleq1 ⊢ k = N → k ∈ A ↔ N ∈ A
8 eleq1 ⊢ k = N → k ∈ B ↔ N ∈ B
9 fveq2 ⊢ k = N → C ⁡ k = C ⁡ N
10 9 eleq2d ⊢ k = N → ∅ ∈ C ⁡ k ↔ ∅ ∈ C ⁡ N
11 7 8 10 hadbi123d ⊢ k = N → hadd k ∈ A k ∈ B ∅ ∈ C ⁡ k ↔ hadd N ∈ A N ∈ B ∅ ∈ C ⁡ N
12 11 elrab3 ⊢ N ∈ ℕ 0 → N ∈ k ∈ ℕ 0 | hadd k ∈ A k ∈ B ∅ ∈ C ⁡ k ↔ hadd N ∈ A N ∈ B ∅ ∈ C ⁡ N
13 4 12 syl ⊢ φ → N ∈ k ∈ ℕ 0 | hadd k ∈ A k ∈ B ∅ ∈ C ⁡ k ↔ hadd N ∈ A N ∈ B ∅ ∈ C ⁡ N
14 6 13 bitrd ⊢ φ → N ∈ A sadd B ↔ hadd N ∈ A N ∈ B ∅ ∈ C ⁡ N