Database
REAL AND COMPLEX NUMBERS
Construction and axiomatization of real and complex numbers
Real and complex number postulates restated as axioms
ax-i2m1
Metamath Proof Explorer
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
$${\u22a2}\mathrm{i}\mathrm{i}+1=0$$

Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
ci
$${class}\mathrm{i}$$
1
cmul
$${class}\times $$
2
0 0 1
co
$${class}\mathrm{i}\mathrm{i}$$
3
caddc
$${class}+$$
4
c1
$${class}1$$
5
2 4 3
co
$${class}\left(\mathrm{i}\mathrm{i}+1\right)$$
6
cc0
$${class}0$$
7
5 6
wceq
$${wff}\mathrm{i}\mathrm{i}+1=0$$