This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database REAL AND COMPLEX NUMBERS Construction and axiomatization of real and complex numbers Real and complex number postulates restated as axioms 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