Theorem smu01

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

	Ref	Expression
Assertion	smu01	⊢ ( 𝐴 ⊆ ℕ0 → ( 𝐴 smul ∅ ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝐴 ⊆ ℕ0 → 𝐴 ⊆ ℕ0 )
2		0ss	⊢ ∅ ⊆ ℕ0
3	2	a1i	⊢ ( 𝐴 ⊆ ℕ0 → ∅ ⊆ ℕ0 )
4		noel	⊢ ¬ ( 𝑛 − 𝑘 ) ∈ ∅
5	4	intnan	⊢ ¬ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ ∅ )
6	5	a1i	⊢ ( ( 𝐴 ⊆ ℕ0 ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → ¬ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ ∅ ) )
7	1 3 6	smu01lem	⊢ ( 𝐴 ⊆ ℕ0 → ( 𝐴 smul ∅ ) = ∅ )