Theorem smucl

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

	Ref	Expression
Assertion	smucl	$$⊢\left(A\subseteq {\mathbb{N}}_0\wedge B\subseteq {\mathbb{N}}_0\right)\to A\mathrm{smul}B\subseteq {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		simpl	$$⊢\left(A\subseteq {\mathbb{N}}_0\wedge B\subseteq {\mathbb{N}}_0\right)\to A\subseteq {\mathbb{N}}_0$$
2		simpr	$$⊢\left(A\subseteq {\mathbb{N}}_0\wedge B\subseteq {\mathbb{N}}_0\right)\to B\subseteq {\mathbb{N}}_0$$
3		eqid	$$⊢seq0\left(\left(p\in 𝒫{\mathbb{N}}_0,m\in {\mathbb{N}}_0⟼p\mathrm{sadd}\left\{n\in {\mathbb{N}}_0|\left(m\in A\wedge n-m\in B\right)\right\}\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)=seq0\left(\left(p\in 𝒫{\mathbb{N}}_0,m\in {\mathbb{N}}_0⟼p\mathrm{sadd}\left\{n\in {\mathbb{N}}_0|\left(m\in A\wedge n-m\in B\right)\right\}\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)$$
4	1 2 3	smufval	$$⊢\left(A\subseteq {\mathbb{N}}_0\wedge B\subseteq {\mathbb{N}}_0\right)\to A\mathrm{smul}B=\left\{k\in {\mathbb{N}}_0|k\in seq0\left(\left(p\in 𝒫{\mathbb{N}}_0,m\in {\mathbb{N}}_0⟼p\mathrm{sadd}\left\{n\in {\mathbb{N}}_0|\left(m\in A\wedge n-m\in B\right)\right\}\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)\left(k+1\right)\right\}$$
5		ssrab2	$$⊢\left\{k\in {\mathbb{N}}_0|k\in seq0\left(\left(p\in 𝒫{\mathbb{N}}_0,m\in {\mathbb{N}}_0⟼p\mathrm{sadd}\left\{n\in {\mathbb{N}}_0|\left(m\in A\wedge n-m\in B\right)\right\}\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)\left(k+1\right)\right\}\subseteq {\mathbb{N}}_0$$
6	4 5	eqsstrdi	$$⊢\left(A\subseteq {\mathbb{N}}_0\wedge B\subseteq {\mathbb{N}}_0\right)\to A\mathrm{smul}B\subseteq {\mathbb{N}}_0$$