Theorem smu02

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

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

Proof

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