Theorem smucl

Description: The product of two sequences is a sequence. (Contributed by Mario Carneiro, 19-Sep-2016)

	Ref	Expression
Assertion	smucl	|- ( ( A C_ NN0 /\ B C_ NN0 ) -> ( A smul B ) C_ NN0 )

Proof

Step	Hyp	Ref	Expression
1		simpl	|- ( ( A C_ NN0 /\ B C_ NN0 ) -> A C_ NN0 )
2		simpr	|- ( ( A C_ NN0 /\ B C_ NN0 ) -> B C_ NN0 )
3		eqid	|- 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 ) ) ) ) = 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	1 2 3	smufval	|- ( ( A C_ NN0 /\ B C_ NN0 ) -> ( A smul B ) = { k e. NN0 | k e. ( 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 ) ) ) ) ` ( k + 1 ) ) } )
5		ssrab2	|- { k e. NN0 | k e. ( 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 ) ) ) ) ` ( k + 1 ) ) } C_ NN0
6	4 5	eqsstrdi	|- ( ( A C_ NN0 /\ B C_ NN0 ) -> ( A smul B ) C_ NN0 )