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

Metamath Proof Explorer

Theorem 0tie0

Description: 0 times _i equals 0. (Contributed by SN, 25-Apr-2025)

		Ref	Expression
	Assertion	0tie0	$⊢ 0 \cdot i = 0$

Step	Hyp	Ref	Expression
1		ax-icn	$⊢ i \in ℂ$
2		0cn	$⊢ 0 \in ℂ$
3		it0e0	$⊢ i \cdot 0 = 0$
4	1 2 3	mulcomli	$⊢ 0 \cdot i = 0$