Theorem 2muline0

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

	Ref	Expression
Assertion	2muline0	⊢ ( 2 · i ) ≠ 0

Proof

Step	Hyp	Ref	Expression
1		2cn	⊢ 2 ∈ ℂ
2		ax-icn	⊢ i ∈ ℂ
3		2ne0	⊢ 2 ≠ 0
4		ine0	⊢ i ≠ 0
5	1 2 3 4	mulne0i	⊢ ( 2 · i ) ≠ 0