Metamath Proof Explorer

Theorem ixi

Description: _i times itself is minus 1. (Contributed by NM, 6-May-1999) (Proof shortened by Andrew Salmon, 19-Nov-2011)

Ref Expression
Assertion ixi 
|- ( _i x. _i ) = -u 1

Proof

Step Hyp Ref Expression
1 df-neg 
 |-  -u 1 = ( 0 - 1 )
2 ax-i2m1 
 |-  ( ( _i x. _i ) + 1 ) = 0
3 0cn 
 |-  0 e. CC
4 ax-1cn 
 |-  1 e. CC
5 ax-icn 
 |-  _i e. CC
6 5 5 mulcli 
 |-  ( _i x. _i ) e. CC
7 3 4 6 subadd2i 
 |-  ( ( 0 - 1 ) = ( _i x. _i ) <-> ( ( _i x. _i ) + 1 ) = 0 )
8 2 7 mpbir 
 |-  ( 0 - 1 ) = ( _i x. _i )
9 1 8 eqtr2i 
 |-  ( _i x. _i ) = -u 1