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 = ( sqrt ` -u 1 )

Proof

Step	Hyp	Ref	Expression
1		1re	|- 1 e. RR
2		0le1	|- 0 <_ 1
3		sqrtneg	|- ( ( 1 e. RR /\ 0 <_ 1 ) -> ( sqrt ` -u 1 ) = ( _i x. ( sqrt ` 1 ) ) )
4	1 2 3	mp2an	|- ( sqrt ` -u 1 ) = ( _i x. ( sqrt ` 1 ) )
5		sqrt1	|- ( sqrt ` 1 ) = 1
6	5	oveq2i	|- ( _i x. ( sqrt ` 1 ) ) = ( _i x. 1 )
7		ax-icn	|- _i e. CC
8	7	mulid1i	|- ( _i x. 1 ) = _i
9	4 6 8	3eqtrri	|- _i = ( sqrt ` -u 1 )