Theorem smu01

Description: Multiplication of a sequence by 0 on the right. (Contributed by Mario Carneiro, 19-Sep-2016)

	Ref	Expression
Assertion	smu01	$$⊢A\subseteq {\mathbb{N}}_0\to A\mathrm{smul}\varnothing =\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢A\subseteq {\mathbb{N}}_0\to A\subseteq {\mathbb{N}}_0$$
2		0ss	$$⊢\varnothing \subseteq {\mathbb{N}}_0$$
3	2	a1i	$$⊢A\subseteq {\mathbb{N}}_0\to \varnothing \subseteq {\mathbb{N}}_0$$
4		noel	$$⊢\neg n-k\in \varnothing$$
5	4	intnan	$$⊢\neg \left(k\in A\wedge n-k\in \varnothing \right)$$
6	5	a1i	$$⊢\left(A\subseteq {\mathbb{N}}_0\wedge \left(k\in {\mathbb{N}}_0\wedge n\in {\mathbb{N}}_0\right)\right)\to \neg \left(k\in A\wedge n-k\in \varnothing \right)$$
7	1 3 6	smu01lem	$$⊢A\subseteq {\mathbb{N}}_0\to A\mathrm{smul}\varnothing =\varnothing$$