Theorem 2muline0

Description: ( 2 x. _i ) =/= 0 . (Contributed by David A. Wheeler, 8-Dec-2018)

	Ref	Expression
Assertion	2muline0	$$⊢2\mathrm{i}\ne 0$$

Proof

Step	Hyp	Ref	Expression
1		2cn	$$⊢2\in ℂ$$
2		ax-icn	$$⊢\mathrm{i}\in ℂ$$
3		2ne0	$$⊢2\ne 0$$
4		ine0	$$⊢\mathrm{i}\ne 0$$
5	1 2 3 4	mulne0i	$$⊢2\mathrm{i}\ne 0$$