ine0

Description: The imaginary unit _i is not zero. (Contributed by NM, 6-May-1999)

		Ref	Expression
	Assertion	ine0	$⊢ i \neq 0$

Step	Hyp	Ref	Expression
1		ax-1ne0	$⊢ 1 \neq 0$
2	1	neii	$⊢ \neg 1 = 0$
3		oveq2	$⊢ i = 0 \to i i = i \cdot 0$
4		ax-icn	$⊢ i \in ℂ$
5	4	mul01i	$⊢ i \cdot 0 = 0$
6	3 5	eqtr2di	$⊢ i = 0 \to 0 = i i$
7	6	oveq1d	$⊢ i = 0 \to 0 + 1 = i i + 1$
8		ax-1cn	$⊢ 1 \in ℂ$
9	8	addlidi	$⊢ 0 + 1 = 1$
10		ax-i2m1	$⊢ i i + 1 = 0$
11	7 9 10	3eqtr3g	$⊢ i = 0 \to 1 = 0$
12	2 11	mto	$⊢ \neg i = 0$
13	12	neir	$⊢ i \neq 0$

Metamath Proof Explorer