Theorem 1nei

Description: The imaginary unit _i is not one. (Contributed by Thierry Arnoux, 20-Aug-2023)

	Ref	Expression
Assertion	1nei	$$⊢1\ne \mathrm{i}$$

Proof

Step	Hyp	Ref	Expression
1		0ne2	$$⊢0\ne 2$$
2	1	nesymi	$$⊢\neg 2=0$$
3		oveq2	$$⊢1=-1\to 1+1=1+-1$$
4		1p1e2	$$⊢1+1=2$$
5		1pneg1e0	$$⊢1+-1=0$$
6	3 4 5	3eqtr3g	$$⊢1=-1\to 2=0$$
7	2 6	mto	$$⊢\neg 1=-1$$
8		id	$$⊢1=\mathrm{i}\to 1=\mathrm{i}$$
9	8 8	oveq12d	$$⊢1=\mathrm{i}\to 1\cdot 1=\mathrm{i}\mathrm{i}$$
10		1t1e1	$$⊢1\cdot 1=1$$
11		ixi	$$⊢\mathrm{i}\mathrm{i}=-1$$
12	9 10 11	3eqtr3g	$$⊢1=\mathrm{i}\to 1=-1$$
13	7 12	mto	$$⊢\neg 1=\mathrm{i}$$
14	13	neir	$$⊢1\ne \mathrm{i}$$