Theorem smuval

Description: Define the addition of two bit sequences, using df-had and df-cad bit operations. (Contributed by Mario Carneiro, 9-Sep-2016)

	Ref	Expression
Hypotheses	smuval.a	|- ( ph -> A C_ NN0 )
	smuval.b	|- ( ph -> B C_ NN0 )
	smuval.p	|- P = seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) )
	smuval.n	|- ( ph -> N e. NN0 )
Assertion	smuval	|- ( ph -> ( N e. ( A smul B ) <-> N e. ( P ` ( N + 1 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		smuval.a	|- ( ph -> A C_ NN0 )
2		smuval.b	|- ( ph -> B C_ NN0 )
3		smuval.p	|- P = seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) )
4		smuval.n	|- ( ph -> N e. NN0 )
5	1 2 3	smufval	|- ( ph -> ( A smul B ) = { k e. NN0 | k e. ( P ` ( k + 1 ) ) } )
6	5	eleq2d	|- ( ph -> ( N e. ( A smul B ) <-> N e. { k e. NN0 | k e. ( P ` ( k + 1 ) ) } ) )
7		id	|- ( k = N -> k = N )
8		fvoveq1	|- ( k = N -> ( P ` ( k + 1 ) ) = ( P ` ( N + 1 ) ) )
9	7 8	eleq12d	|- ( k = N -> ( k e. ( P ` ( k + 1 ) ) <-> N e. ( P ` ( N + 1 ) ) ) )
10	9	elrab3	|- ( N e. NN0 -> ( N e. { k e. NN0 | k e. ( P ` ( k + 1 ) ) } <-> N e. ( P ` ( N + 1 ) ) ) )
11	4 10	syl	|- ( ph -> ( N e. { k e. NN0 | k e. ( P ` ( k + 1 ) ) } <-> N e. ( P ` ( N + 1 ) ) ) )
12	6 11	bitrd	|- ( ph -> ( N e. ( A smul B ) <-> N e. ( P ` ( N + 1 ) ) ) )