Theorem ine0

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

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

Proof

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