This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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