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