This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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$

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 (0 + 0) = A \cdot 0 + A \cdot 0$
5		sn-00id	$⊢ 0 + 0 = 0$
6	5	oveq2i	$⊢ A (0 + 0) = 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$