ax-i2m1 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ax-i2m1		Structured version Visualization version GIF version

Axiom ax-i2m1 11198

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 11174. (Contributed by NM, 29-Jan-1995.)

**Assertion**
Ref	Expression
ax-i2m1	⊢ ((i · i) + 1) = 0

**Detailed syntax breakdown of Axiom ax-i2m1**
Step	Hyp	Ref	Expression
1		ci 11132	. . . 4 class i
2		cmul 11135	. . . 4 class ·
3	1, 1, 2	co 7414	. . 3 class (i · i)
4		c1 11131	. . 3 class 1
5		caddc 11133	. . 3 class +
6	3, 4, 5	co 7414	. 2 class ((i · i) + 1)
7		cc0 11130	. 2 class 0
8	6, 7	wceq 1534	1 wff ((i · i) + 1) = 0

Colors of variables: wff setvar class

This axiom is referenced by: 0cn 11228 mul02lem2 11413 addrid 11416 cnegex2 11418 ine0 11671 ixi 11865 inelr 12224 c0exALT 41756 sn-1ne2 41762 re1m1e0m0 41874 reixi 41899 sn-inelr 41942

W3C validator

	
		OSZAR »