This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 mulridi 
 |-  ( _i x. 1 ) = _i
9 4 6 8 3eqtrri 
 |-  _i = ( sqrt ` -u 1 )