Theorem 1nei

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

	Ref	Expression
Assertion	1nei	|- 1 =/= _i

Proof

Step	Hyp	Ref	Expression
1		0ne2	|- 0 =/= 2
2	1	nesymi	|- -. 2 = 0
3		oveq2	|- ( 1 = -u 1 -> ( 1 + 1 ) = ( 1 + -u 1 ) )
4		1p1e2	|- ( 1 + 1 ) = 2
5		1pneg1e0	|- ( 1 + -u 1 ) = 0
6	3 4 5	3eqtr3g	|- ( 1 = -u 1 -> 2 = 0 )
7	2 6	mto	|- -. 1 = -u 1
8		id	|- ( 1 = _i -> 1 = _i )
9	8 8	oveq12d	|- ( 1 = _i -> ( 1 x. 1 ) = ( _i x. _i ) )
10		1t1e1	|- ( 1 x. 1 ) = 1
11		ixi	|- ( _i x. _i ) = -u 1
12	9 10 11	3eqtr3g	|- ( 1 = _i -> 1 = -u 1 )
13	7 12	mto	|- -. 1 = _i
14	13	neir	|- 1 =/= _i