Metamath Proof Explorer


Axiom ax-i2m1

Description: i-squared equals -1 (expressed as i-squared plus 1 is 0). Axiom 12 of 22 for real and complex numbers, justified by Theorem axi2m1 . (Contributed by NM, 29-Jan-1995)

Ref Expression
Assertion ax-i2m1
|- ( ( _i x. _i ) + 1 ) = 0

Detailed syntax breakdown

Step Hyp Ref Expression
0 ci
 |-  _i
1 cmul
 |-  x.
2 0 0 1 co
 |-  ( _i x. _i )
3 caddc
 |-  +
4 c1
 |-  1
5 2 4 3 co
 |-  ( ( _i x. _i ) + 1 )
6 cc0
 |-  0
7 5 6 wceq
 |-  ( ( _i x. _i ) + 1 ) = 0