Theorem smu02

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

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

Proof

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