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 |