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 |
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 |