Theorem sqrtm1

Description: The imaginary unit is the square root of negative 1. A lot of people like to call this the "definition" of _i , but the definition of sqrt df-sqrt has already been crafted with _i being mentioned explicitly, and in any case it doesn't make too much sense to define a value based on a function evaluated outside its domain. A more appropriate view is to take ax-i2m1 or i2 as the "definition", and simply postulate the existence of a number satisfying this property. This is the approach we take here. (Contributed by Mario Carneiro, 10-Jul-2013)

	Ref	Expression
Assertion	sqrtm1	⊢ i = ( √ ‘ - 1 )

Proof

Step	Hyp	Ref	Expression
1		1re	⊢ 1 ∈ ℝ
2		0le1	⊢ 0 ≤ 1
3		sqrtneg	⊢ ( ( 1 ∈ ℝ ∧ 0 ≤ 1 ) → ( √ ‘ - 1 ) = ( i · ( √ ‘ 1 ) ) )
4	1 2 3	mp2an	⊢ ( √ ‘ - 1 ) = ( i · ( √ ‘ 1 ) )
5		sqrt1	⊢ ( √ ‘ 1 ) = 1
6	5	oveq2i	⊢ ( i · ( √ ‘ 1 ) ) = ( i · 1 )
7		ax-icn	⊢ i ∈ ℂ
8	7	mulid1i	⊢ ( i · 1 ) = i
9	4 6 8	3eqtrri	⊢ i = ( √ ‘ - 1 )