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 · i ) + 1 ) = 0

Detailed syntax breakdown

Step Hyp Ref Expression
0 ci i
1 cmul ·
2 0 0 1 co ( i · i )
3 caddc +
4 c1 1
5 2 4 3 co ( ( i · i ) + 1 )
6 cc0 0
7 5 6 wceq ( ( i · i ) + 1 ) = 0