Description: The imaginary unit _i is not one. (Contributed by Thierry Arnoux, 20Aug2023)
Ref  Expression  

Assertion  1nei   1 =/= _i 
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 