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	1 2 2	adddid	$$⊢A\in ℂ\to A\left(0+0\right)=A\cdot 0+A\cdot 0$$
5		sn-00id	$$⊢0+0=0$$
6	5	oveq2i	$$⊢A\left(0+0\right)=A\cdot 0$$
7	4 6	eqtr3di	$$⊢A\in ℂ\to A\cdot 0+A\cdot 0=A\cdot 0$$
8	3 7	sn-addid0	$$⊢A\in ℂ\to A\cdot 0=0$$