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 = - 1 → ( 1 + 1 ) = ( 1 + - 1 ) )
4		1p1e2	⊢ ( 1 + 1 ) = 2
5		1pneg1e0	⊢ ( 1 + - 1 ) = 0
6	3 4 5	3eqtr3g	⊢ ( 1 = - 1 → 2 = 0 )
7	2 6	mto	⊢ ¬ 1 = - 1
8		id	⊢ ( 1 = i → 1 = i )
9	8 8	oveq12d	⊢ ( 1 = i → ( 1 · 1 ) = ( i · i ) )
10		1t1e1	⊢ ( 1 · 1 ) = 1
11		ixi	⊢ ( i · i ) = - 1
12	9 10 11	3eqtr3g	⊢ ( 1 = i → 1 = - 1 )
13	7 12	mto	⊢ ¬ 1 = i
14	13	neir	⊢ 1 ≠ i