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	⊢ ( 𝜑 → 𝐴 ⊆ ℕ0 )
	sadval.b	⊢ ( 𝜑 → 𝐵 ⊆ ℕ0 )
	sadval.c	⊢ 𝐶 = seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) )
	sadcp1.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion	sadval	⊢ ( 𝜑 → ( 𝑁 ∈ ( 𝐴 sadd 𝐵 ) ↔ hadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		sadval.a	⊢ ( 𝜑 → 𝐴 ⊆ ℕ0 )
2		sadval.b	⊢ ( 𝜑 → 𝐵 ⊆ ℕ0 )
3		sadval.c	⊢ 𝐶 = seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) )
4		sadcp1.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
5	1 2 3	sadfval	⊢ ( 𝜑 → ( 𝐴 sadd 𝐵 ) = { 𝑘 ∈ ℕ0 ∣ hadd ( 𝑘 ∈ 𝐴 , 𝑘 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑘 ) ) } )
6	5	eleq2d	⊢ ( 𝜑 → ( 𝑁 ∈ ( 𝐴 sadd 𝐵 ) ↔ 𝑁 ∈ { 𝑘 ∈ ℕ0 ∣ hadd ( 𝑘 ∈ 𝐴 , 𝑘 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑘 ) ) } ) )
7		eleq1	⊢ ( 𝑘 = 𝑁 → ( 𝑘 ∈ 𝐴 ↔ 𝑁 ∈ 𝐴 ) )
8		eleq1	⊢ ( 𝑘 = 𝑁 → ( 𝑘 ∈ 𝐵 ↔ 𝑁 ∈ 𝐵 ) )
9		fveq2	⊢ ( 𝑘 = 𝑁 → ( 𝐶 ‘ 𝑘 ) = ( 𝐶 ‘ 𝑁 ) )
10	9	eleq2d	⊢ ( 𝑘 = 𝑁 → ( ∅ ∈ ( 𝐶 ‘ 𝑘 ) ↔ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) )
11	7 8 10	hadbi123d	⊢ ( 𝑘 = 𝑁 → ( hadd ( 𝑘 ∈ 𝐴 , 𝑘 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑘 ) ) ↔ hadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ) )
12	11	elrab3	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 ∈ { 𝑘 ∈ ℕ0 ∣ hadd ( 𝑘 ∈ 𝐴 , 𝑘 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑘 ) ) } ↔ hadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ) )
13	4 12	syl	⊢ ( 𝜑 → ( 𝑁 ∈ { 𝑘 ∈ ℕ0 ∣ hadd ( 𝑘 ∈ 𝐴 , 𝑘 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑘 ) ) } ↔ hadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ) )
14	6 13	bitrd	⊢ ( 𝜑 → ( 𝑁 ∈ ( 𝐴 sadd 𝐵 ) ↔ hadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ) )