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	$$⊢\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	$$class1$$
5	2 4 3	co	$$class\left(\mathrm{i}\mathrm{i}+1\right)$$
6		cc0	$$class0$$
7	5 6	wceq	$$wff\mathrm{i}\mathrm{i}+1=0$$