Theorem sn-mul01

Description: mul01 without ax-mulcom . (Contributed by SN, 5-May-2024)

	Ref	Expression
Assertion	sn-mul01	$$⊢A\in ℂ\to A\cdot 0=0$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢A\in ℂ\to A\in ℂ$$
2		0cnd	$$⊢A\in ℂ\to 0\in ℂ$$
3	1 2	mulcld	$$⊢A\in ℂ\to A\cdot 0\in ℂ$$
4		sn-00id	$$⊢0+0=0$$
5	4	oveq2i	$$⊢A\left(0+0\right)=A\cdot 0$$
6	1 2 2	adddid	$$⊢A\in ℂ\to A\left(0+0\right)=A\cdot 0+A\cdot 0$$
7	5 6	syl5reqr	$$⊢A\in ℂ\to A\cdot 0+A\cdot 0=A\cdot 0$$
8	3 7	sn-addid0	$$⊢A\in ℂ\to A\cdot 0=0$$