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	|- ( ph -> A C_ NN0 )
	sadval.b	|- ( ph -> B C_ NN0 )
	sadval.c	|- C = seq 0 ( ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) )
	sadcp1.n	|- ( ph -> N e. NN0 )
Assertion	sadval	|- ( ph -> ( N e. ( A sadd B ) <-> hadd ( N e. A , N e. B , (/) e. ( C ` N ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		sadval.a	|- ( ph -> A C_ NN0 )
2		sadval.b	|- ( ph -> B C_ NN0 )
3		sadval.c	|- C = seq 0 ( ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. A , m e. B , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) )
4		sadcp1.n	|- ( ph -> N e. NN0 )
5	1 2 3	sadfval	|- ( ph -> ( A sadd B ) = { k e. NN0 | hadd ( k e. A , k e. B , (/) e. ( C ` k ) ) } )
6	5	eleq2d	|- ( ph -> ( N e. ( A sadd B ) <-> N e. { k e. NN0 | hadd ( k e. A , k e. B , (/) e. ( C ` k ) ) } ) )
7		eleq1	|- ( k = N -> ( k e. A <-> N e. A ) )
8		eleq1	|- ( k = N -> ( k e. B <-> N e. B ) )
9		fveq2	|- ( k = N -> ( C ` k ) = ( C ` N ) )
10	9	eleq2d	|- ( k = N -> ( (/) e. ( C ` k ) <-> (/) e. ( C ` N ) ) )
11	7 8 10	hadbi123d	|- ( k = N -> ( hadd ( k e. A , k e. B , (/) e. ( C ` k ) ) <-> hadd ( N e. A , N e. B , (/) e. ( C ` N ) ) ) )
12	11	elrab3	|- ( N e. NN0 -> ( N e. { k e. NN0 | hadd ( k e. A , k e. B , (/) e. ( C ` k ) ) } <-> hadd ( N e. A , N e. B , (/) e. ( C ` N ) ) ) )
13	4 12	syl	|- ( ph -> ( N e. { k e. NN0 | hadd ( k e. A , k e. B , (/) e. ( C ` k ) ) } <-> hadd ( N e. A , N e. B , (/) e. ( C ` N ) ) ) )
14	6 13	bitrd	|- ( ph -> ( N e. ( A sadd B ) <-> hadd ( N e. A , N e. B , (/) e. ( C ` N ) ) ) )